Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 7743751

Browse files
authoredSep 4, 2022
Merge pull request #7097 from diffblue/typet_subtype_const4
protect typet::subtype() const
2 parents 77aa274 + 4067de6 commit 7743751

File tree

7 files changed

+95
-53
lines changed

7 files changed

+95
-53
lines changed
 

‎jbmc/unit/java-testing-utils/require_goto_statements.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -424,7 +424,7 @@ const irep_idt &require_goto_statements::require_struct_component_assignment(
424424
require_goto_statements::require_declaration_of_name(
425425
symbol_identifier, entry_point_instructions);
426426
const typet &component_type =
427-
to_pointer_type(component_declaration.symbol().type()).subtype();
427+
to_pointer_type(component_declaration.symbol().type()).base_type();
428428
REQUIRE(component_type.id() == ID_struct_tag);
429429
const auto &component_struct =
430430
ns.follow_tag(to_struct_tag_type(component_type));
@@ -480,7 +480,7 @@ require_goto_statements::require_struct_array_component_assignment(
480480
REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
481481
REQUIRE(
482482
to_struct_tag_type(
483-
to_pointer_type(component_assignment_rhs.type()).subtype())
483+
to_pointer_type(component_assignment_rhs.type()).base_type())
484484
.get(ID_identifier) == array_type_name);
485485

486486
// Get the tmp_object name and find assignments to it, there should be only
@@ -501,7 +501,8 @@ require_goto_statements::require_struct_array_component_assignment(
501501
PRECONDITION(
502502
array_component_reference_assignment_rhs.type().id() == ID_pointer);
503503
const typet &array =
504-
to_pointer_type(array_component_reference_assignment_rhs.type()).subtype();
504+
to_pointer_type(array_component_reference_assignment_rhs.type())
505+
.base_type();
505506
PRECONDITION(is_java_array_tag(array.get(ID_identifier)));
506507
REQUIRE(array.get(ID_identifier) == array_type_name);
507508

‎jbmc/unit/java-testing-utils/require_type.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ pointer_typet require_type::require_pointer(
2323
const pointer_typet &pointer = to_pointer_type(type);
2424

2525
if(subtype)
26-
REQUIRE(pointer.subtype() == subtype.value());
26+
REQUIRE(pointer.base_type() == subtype.value());
2727

2828
return pointer;
2929
}
@@ -155,8 +155,8 @@ bool require_java_generic_type_argument_expectation(
155155
{
156156
REQUIRE(!is_java_generic_parameter(type_argument));
157157
REQUIRE(
158-
to_struct_tag_type(type_argument.subtype()).get_identifier() ==
159-
expected.description);
158+
to_struct_tag_type(to_pointer_type(type_argument).base_type())
159+
.get_identifier() == expected.description);
160160
return true;
161161
}
162162
}
@@ -248,7 +248,7 @@ const typet &require_type::require_java_non_generic_type(
248248
REQUIRE(!is_java_generic_parameter(type));
249249
REQUIRE(!is_java_generic_type(type));
250250
if(expect_subtype)
251-
REQUIRE(type.subtype() == expect_subtype.value());
251+
REQUIRE(to_pointer_type(type).base_type() == expect_subtype.value());
252252
return type;
253253
}
254254

@@ -474,7 +474,7 @@ pointer_typet
474474
require_type::require_pointer_to_tag(const typet &type, const irep_idt &tag)
475475
{
476476
const auto pointer_type = require_type::require_pointer(type, {});
477-
require_type::require_struct_tag(pointer_type.subtype(), tag);
477+
require_type::require_struct_tag(pointer_type.base_type(), tag);
478478
return pointer_type;
479479
}
480480

‎src/cpp/cpp_typecheck_conversions.cpp

Lines changed: 25 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -687,7 +687,8 @@ bool cpp_typecheckt::standard_conversion_sequence(
687687

688688
// bit fields are converted like their underlying type
689689
if(type.id()==ID_c_bit_field)
690-
return standard_conversion_sequence(expr, type.subtype(), new_expr, rank);
690+
return standard_conversion_sequence(
691+
expr, to_c_bit_field_type(type).underlying_type(), new_expr, rank);
691692

692693
// we turn bit fields into their underlying type
693694
if(curr_expr.type().id()==ID_c_bit_field)
@@ -774,7 +775,9 @@ bool cpp_typecheckt::standard_conversion_sequence(
774775
}
775776
else if(type.id()==ID_pointer)
776777
{
777-
if(expr.type().subtype().id()==ID_nullptr)
778+
if(
779+
expr.type().id() == ID_pointer &&
780+
to_pointer_type(expr.type()).base_type().id() == ID_nullptr)
778781
{
779782
// std::nullptr_t to _any_ pointer type is ok
780783
new_expr = typecast_exprt::conditional_cast(new_expr, type);
@@ -1132,9 +1135,9 @@ bool cpp_typecheckt::reference_related(
11321135
return subtype_typecast(to_struct_type(from),
11331136
to_struct_type(to));
11341137

1135-
if(from.id()==ID_struct &&
1136-
type.get_bool(ID_C_this) &&
1137-
type.subtype().id()==ID_empty)
1138+
if(
1139+
from.id() == ID_struct && type.get_bool(ID_C_this) &&
1140+
to_pointer_type(type).base_type().id() == ID_empty)
11381141
{
11391142
// virtual-call case
11401143
return true;
@@ -1158,14 +1161,14 @@ bool cpp_typecheckt::reference_compatible(
11581161
if(!reference_related(expr, type))
11591162
return false;
11601163

1161-
if(expr.type()!=type.subtype())
1164+
if(expr.type() != to_reference_type(type).base_type())
11621165
rank+=3;
11631166

11641167
c_qualifierst qual_from;
11651168
qual_from.read(expr.type());
11661169

11671170
c_qualifierst qual_to;
1168-
qual_to.read(type.subtype());
1171+
qual_to.read(to_reference_type(type).base_type());
11691172

11701173
if(qual_from!=qual_to)
11711174
rank+=1;
@@ -1264,7 +1267,7 @@ bool cpp_typecheckt::reference_binding(
12641267
new_expr.swap(tmp);
12651268
}
12661269

1267-
if(expr.type()!=type.subtype())
1270+
if(expr.type() != to_reference_type(type).base_type())
12681271
{
12691272
c_qualifierst qual_from;
12701273
qual_from.read(expr.type());
@@ -1341,7 +1344,7 @@ bool cpp_typecheckt::reference_binding(
13411344

13421345
new_expr = to_multi_ary_expr(returned_value).op0();
13431346

1344-
if(returned_value.type() != type.subtype())
1347+
if(returned_value.type() != to_reference_type(type).base_type())
13451348
{
13461349
c_qualifierst qual_from;
13471350
qual_from.read(returned_value.type());
@@ -1359,13 +1362,15 @@ bool cpp_typecheckt::reference_binding(
13591362
if(type.get_bool(ID_C_this))
13601363
return false;
13611364

1362-
if(!type.subtype().get_bool(ID_C_constant) ||
1363-
type.subtype().get_bool(ID_C_volatile))
1365+
if(
1366+
!to_reference_type(type).base_type().get_bool(ID_C_constant) ||
1367+
to_reference_type(type).base_type().get_bool(ID_C_volatile))
13641368
return false;
13651369

13661370
// TODO: handle the case for implicit parameters
1367-
if(!type.subtype().get_bool(ID_C_constant) &&
1368-
!expr.get_bool(ID_C_lvalue))
1371+
if(
1372+
!to_reference_type(type).base_type().get_bool(ID_C_constant) &&
1373+
!expr.get_bool(ID_C_lvalue))
13691374
return false;
13701375

13711376
exprt arg_expr=expr;
@@ -1376,7 +1381,8 @@ bool cpp_typecheckt::reference_binding(
13761381
arg_expr.set(ID_C_lvalue, true);
13771382
}
13781383

1379-
if(user_defined_conversion_sequence(arg_expr, type.subtype(), new_expr, rank))
1384+
if(user_defined_conversion_sequence(
1385+
arg_expr, to_reference_type(type).base_type(), new_expr, rank))
13801386
{
13811387
address_of_exprt tmp(new_expr, reference_type(new_expr.type()));
13821388
tmp.add_source_location()=new_expr.source_location();
@@ -1385,12 +1391,15 @@ bool cpp_typecheckt::reference_binding(
13851391
}
13861392

13871393
rank=backup_rank;
1388-
if(standard_conversion_sequence(expr, type.subtype(), new_expr, rank))
1394+
if(standard_conversion_sequence(
1395+
expr, to_reference_type(type).base_type(), new_expr, rank))
13891396
{
13901397
{
13911398
// create temporary object
13921399
side_effect_exprt tmp(
1393-
ID_temporary_object, type.subtype(), expr.source_location());
1400+
ID_temporary_object,
1401+
to_reference_type(type).base_type(),
1402+
expr.source_location());
13941403
tmp.set(ID_mode, ID_cpp);
13951404
// tmp.set(ID_C_lvalue, true);
13961405
tmp.add_to_operands(std::move(new_expr));

‎src/cpp/cpp_typecheck_expr.cpp

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -324,12 +324,13 @@ void cpp_typecheckt::typecheck_expr_sizeof(exprt &expr)
324324
{
325325
// sizeof(expr[index]) can be parsed as an array type!
326326

327-
if(type.subtype().id()==ID_cpp_name)
327+
if(to_array_type(type).element_type().id() == ID_cpp_name)
328328
{
329329
cpp_typecheck_fargst fargs;
330330

331-
exprt symbol_expr=resolve(
332-
to_cpp_name(static_cast<const irept &>(type.subtype())),
331+
exprt symbol_expr = resolve(
332+
to_cpp_name(
333+
static_cast<const irept &>(to_array_type(type).element_type())),
333334
cpp_typecheck_resolvet::wantt::BOTH,
334335
fargs);
335336

@@ -1652,7 +1653,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
16521653

16531654
// look for the right entry
16541655
irep_idt vtentry_component_name =
1655-
vt_compo.type().subtype().get_string(ID_identifier) +
1656+
to_pointer_type(vt_compo.type()).base_type().get_string(ID_identifier) +
16561657
"::" + expr.function().type().get_string(ID_C_virtual_name);
16571658

16581659
exprt vtentry_member(ID_ptrmember);
@@ -1719,14 +1720,14 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
17191720

17201721
assert(parameters.size()>=1);
17211722

1722-
const typet &this_type=parameters[0].type();
1723+
const auto &this_type = to_pointer_type(parameters[0].type());
17231724

17241725
// change type from 'constructor' to object type
1725-
expr.type()=this_type.subtype();
1726+
expr.type() = this_type.base_type();
17261727

17271728
// create temporary object
17281729
side_effect_exprt tmp_object_expr(
1729-
ID_temporary_object, this_type.subtype(), expr.source_location());
1730+
ID_temporary_object, this_type.base_type(), expr.source_location());
17301731
tmp_object_expr.set(ID_C_lvalue, true);
17311732
tmp_object_expr.set(ID_mode, ID_cpp);
17321733

@@ -1808,7 +1809,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
18081809

18091810
if(
18101811
operand.type().id() != ID_pointer &&
1811-
operand.type() == parameter.type().subtype())
1812+
operand.type() == to_pointer_type(parameter.type()).base_type())
18121813
{
18131814
address_of_exprt tmp(operand, pointer_type(operand.type()));
18141815
tmp.add_source_location()=operand.source_location();
@@ -1869,7 +1870,7 @@ void cpp_typecheckt::typecheck_function_call_arguments(
18691870
exprt temporary;
18701871
new_temporary(
18711872
arg_it->source_location(),
1872-
parameter.type().subtype(),
1873+
to_reference_type(parameter.type()).base_type(),
18731874
already_typechecked_exprt{*arg_it},
18741875
temporary);
18751876
arg_it->swap(temporary);

‎src/cpp/cpp_typecheck_resolve.cpp

Lines changed: 17 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -269,10 +269,14 @@ exprt cpp_typecheck_resolvet::convert_identifier(
269269
{
270270
// use this->...
271271
assert(this_expr.type().id()==ID_pointer);
272-
object=exprt(ID_dereference, this_expr.type().subtype());
272+
object =
273+
exprt(ID_dereference, to_pointer_type(this_expr.type()).base_type());
273274
object.copy_to_operands(this_expr);
274-
object.type().set(ID_C_constant,
275-
this_expr.type().subtype().get_bool(ID_C_constant));
275+
object.type().set(
276+
ID_C_constant,
277+
to_pointer_type(this_expr.type())
278+
.base_type()
279+
.get_bool(ID_C_constant));
276280
object.set(ID_C_lvalue, true);
277281
object.add_source_location()=source_location;
278282
}
@@ -1838,19 +1842,24 @@ void cpp_typecheck_resolvet::guess_template_args(
18381842
else if(is_reference(template_type) ||
18391843
is_rvalue_reference(template_type))
18401844
{
1841-
guess_template_args(template_type.subtype(), desired_type);
1845+
guess_template_args(
1846+
to_reference_type(template_type).base_type(), desired_type);
18421847
}
18431848
else if(template_type.id()==ID_pointer)
18441849
{
18451850
if(desired_type.id() == ID_pointer)
1846-
guess_template_args(template_type.subtype(), desired_type.subtype());
1851+
guess_template_args(
1852+
to_pointer_type(template_type).base_type(),
1853+
to_pointer_type(desired_type).base_type());
18471854
}
18481855
else if(template_type.id()==ID_array)
18491856
{
18501857
if(desired_type.id() == ID_array)
18511858
{
18521859
// look at subtype first
1853-
guess_template_args(template_type.subtype(), desired_type.subtype());
1860+
guess_template_args(
1861+
to_array_type(template_type).element_type(),
1862+
to_array_type(desired_type).element_type());
18541863

18551864
// size (e.g., buffer size guessing)
18561865
guess_template_args(
@@ -2134,7 +2143,8 @@ bool cpp_typecheck_resolvet::disambiguate_functions(
21342143
if(type.return_type().id() == ID_constructor)
21352144
{
21362145
// it's a constructor
2137-
const typet &object_type=parameter.type().subtype();
2146+
const typet &object_type =
2147+
to_pointer_type(parameter.type()).base_type();
21382148
symbol_exprt object(irep_idt(), object_type);
21392149
object.set(ID_C_lvalue, true);
21402150

‎src/goto-programs/string_abstraction.cpp

Lines changed: 30 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,8 @@ bool string_abstractiont::build_wrap(
4646
if(
4747
dest.type() != a_t &&
4848
!(dest.type().id() == ID_array && a_t.id() == ID_pointer &&
49-
dest.type().subtype() == a_t.subtype()))
49+
to_array_type(dest.type()).element_type() ==
50+
to_pointer_type(a_t).base_type()))
5051
{
5152
messaget log{message_handler};
5253
log.warning() << "warning: inconsistent abstract type for "
@@ -59,7 +60,8 @@ bool string_abstractiont::build_wrap(
5960

6061
bool string_abstractiont::is_ptr_string_struct(const typet &type) const
6162
{
62-
return type.id() == ID_pointer && type.subtype() == string_struct;
63+
return type.id() == ID_pointer &&
64+
to_pointer_type(type).base_type() == string_struct;
6365
}
6466

6567
static inline bool is_ptr_argument(const typet &type)
@@ -334,10 +336,16 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest,
334336
{
335337
if(symbol.type.id() == ID_array || symbol.type.id() == ID_pointer)
336338
{
337-
const typet &source_subt =
338-
is_ptr_string_struct(symbol.type) ? source_type : source_type.subtype();
339+
const typet &source_subt = is_ptr_string_struct(symbol.type)
340+
? source_type
341+
: to_type_with_subtype(source_type).subtype();
339342
symbol_exprt sym_expr = add_dummy_symbol_and_value(
340-
dest, ref_instr, symbol, irep_idt(), symbol.type.subtype(), source_subt);
343+
dest,
344+
ref_instr,
345+
symbol,
346+
irep_idt(),
347+
to_type_with_subtype(symbol.type).subtype(),
348+
source_subt);
341349

342350
if(symbol.type.id() == ID_array)
343351
return array_of_exprt(sym_expr, to_array_type(symbol.type));
@@ -429,7 +437,8 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
429437

430438
// set the value - may be nil
431439
if(
432-
source_type.id() == ID_array && is_char_type(source_type.subtype()) &&
440+
source_type.id() == ID_array &&
441+
is_char_type(to_array_type(source_type).element_type()) &&
433442
type == string_struct)
434443
{
435444
new_symbol.value = struct_exprt(
@@ -561,7 +570,8 @@ void string_abstractiont::abstract_function_call(
561570
abstract_type.id()==ID_pointer)
562571
{
563572
INVARIANT(
564-
str_args.back().type().subtype() == abstract_type.subtype(),
573+
to_array_type(str_args.back().type()).element_type() ==
574+
to_pointer_type(abstract_type).base_type(),
565575
"argument array type differs from formal parameter pointer type");
566576

567577
index_exprt idx(str_args.back(), from_integer(0, c_index_type()));
@@ -706,11 +716,14 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
706716
if(type.id() == ID_array || type.id() == ID_pointer)
707717
{
708718
// char* or void* or char[]
709-
if(is_char_type(type.subtype()) || type.subtype().id() == ID_empty)
719+
if(
720+
is_char_type(to_type_with_subtype(type).subtype()) ||
721+
to_type_with_subtype(type).subtype().id() == ID_empty)
710722
map_entry.first->second=pointer_type(string_struct);
711723
else
712724
{
713-
const typet &subt = build_abstraction_type_rec(type.subtype(), known);
725+
const typet &subt =
726+
build_abstraction_type_rec(to_type_with_subtype(type).subtype(), known);
714727
if(!subt.is_nil())
715728
{
716729
if(type.id() == ID_array)
@@ -787,7 +800,8 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
787800

788801
return dest.type() != abstract_type ||
789802
(dest.type().id() == ID_array && abstract_type.id() == ID_pointer &&
790-
dest.type().subtype() == abstract_type.subtype());
803+
to_array_type(dest.type()).element_type() ==
804+
to_pointer_type(abstract_type).base_type());
791805
}
792806

793807
if(object.id()==ID_string_constant)
@@ -801,7 +815,9 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
801815
return build_symbol_constant(str_len, str_len+1, dest);
802816
}
803817

804-
if(object.id()==ID_array && is_char_type(object.type().subtype()))
818+
if(
819+
object.id() == ID_array &&
820+
is_char_type(to_array_type(object.type()).element_type()))
805821
return build_array(to_array_expr(object), dest, write);
806822

807823
// other constants aren't useful
@@ -928,8 +944,9 @@ bool string_abstractiont::build_pointer(const exprt &object,
928944
dest=address_of_exprt(dest);
929945
return false;
930946
}
931-
else if(ptr.pointer.id()==ID_symbol &&
932-
is_char_type(object.type().subtype()))
947+
else if(
948+
ptr.pointer.id() == ID_symbol &&
949+
is_char_type(to_pointer_type(object.type()).base_type()))
933950
// recursive call; offset will be handled by pointer_offset in SIZE/LENGTH
934951
// checks
935952
return build_wrap(ptr.pointer, dest, write);

‎src/util/type.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,13 +45,17 @@ class typet:public irept
4545
}
4646
#endif
4747

48+
// Deliberately protected -- use type-specific accessor methods instead.
49+
protected:
4850
const typet &subtype() const
4951
{
5052
if(get_sub().empty())
5153
return static_cast<const typet &>(get_nil_irep());
5254
return static_cast<const typet &>(get_sub().front());
5355
}
5456

57+
public:
58+
// This method will be protected eventually.
5559
typet &subtype()
5660
{
5761
subt &sub=get_sub();

0 commit comments

Comments
 (0)
Please sign in to comment.