Skip to content

Commit 4f135cc

Browse files
kroeningkroening
committed
introduce pointer_typet::base_type()
The type of the data that a pointer points to is usually referred to as the 'base type' of the pointer. This commit introduces a method with that name, to supersede the generic 'subtype' method, whose name is misleading in the case of pointers.
1 parent 90bcd52 commit 4f135cc

File tree

56 files changed

+173
-155
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

56 files changed

+173
-155
lines changed

‎jbmc/src/java_bytecode/assignments_from_json.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -66,8 +66,8 @@ static java_class_typet
6666
followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
6767
{
6868
const pointer_typet &pointer_type = to_pointer_type(expr.type());
69-
const java_class_typet &java_class_type =
70-
to_java_class_type(namespacet{symbol_table}.follow(pointer_type.subtype()));
69+
const java_class_typet &java_class_type = to_java_class_type(
70+
namespacet{symbol_table}.follow(pointer_type.base_type()));
7171
return java_class_type;
7272
}
7373

@@ -602,7 +602,7 @@ static code_with_references_listt assign_non_enum_pointer_from_json(
602602
code_blockt output_code;
603603
exprt dereferenced_symbol_expr =
604604
info.allocate_objects.allocate_dynamic_object(
605-
output_code, expr, to_pointer_type(expr.type()).subtype());
605+
output_code, expr, to_pointer_type(expr.type()).base_type());
606606
for(codet &code : output_code.statements())
607607
result.add(std::move(code));
608608
result.append(assign_struct_from_json(dereferenced_symbol_expr, json, info));
@@ -754,7 +754,7 @@ static get_or_create_reference_resultt get_or_create_reference(
754754
{
755755
code_blockt block;
756756
reference.expr = info.allocate_objects.allocate_dynamic_object_symbol(
757-
block, expr, pointer_type.subtype());
757+
block, expr, pointer_type.base_type());
758758
code.add(block);
759759
}
760760
auto iterator_inserted_pair = info.references.insert({id, reference});

‎jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -117,14 +117,14 @@ void ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer(
117117
const pointer_typet &pointer_type,
118118
const namespacet &ns)
119119
{
120-
const auto &class_type = to_struct_tag_type(pointer_type.subtype());
120+
const auto &class_type = to_struct_tag_type(pointer_type.base_type());
121121
const auto &param_classid = class_type.get_identifier();
122122

123123
// Note here: different arrays may have different element types, so we should
124124
// explore again even if we've seen this classid before in the array case.
125125
if(add_needed_class(param_classid) || is_java_array_tag(param_classid))
126126
{
127-
gather_field_types(pointer_type.subtype(), ns);
127+
gather_field_types(pointer_type.base_type(), ns);
128128
}
129129

130130
if(is_java_generic_type(pointer_type))
@@ -159,7 +159,7 @@ void ci_lazy_methods_neededt::gather_field_types(
159159
java_array_element_type(to_struct_tag_type(class_type));
160160
if(
161161
element_type.id() == ID_pointer &&
162-
element_type.subtype().id() != ID_empty)
162+
to_pointer_type(element_type).base_type().id() != ID_empty)
163163
{
164164
// This is a reference array -- mark its element type available.
165165
add_all_needed_classes(to_pointer_type(element_type));

‎jbmc/src/java_bytecode/code_with_references.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,8 @@ codet allocate_array(
2020
{
2121
pointer_typet pointer_type = to_pointer_type(expr.type());
2222
const auto &element_type =
23-
java_array_element_type(to_struct_tag_type(pointer_type.subtype()));
24-
pointer_type.subtype().set(ID_element_type, element_type);
23+
java_array_element_type(to_struct_tag_type(pointer_type.base_type()));
24+
pointer_type.base_type().set(ID_element_type, element_type);
2525
side_effect_exprt java_new_array{
2626
ID_java_new_array, {array_length_expr}, pointer_type, loc};
2727
return code_frontend_assignt{expr, java_new_array, loc};

‎jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ void generic_parameter_specialization_map_keyst::insert(
1818
return;
1919
// The supplied type must be the full type of the pointer's subtype
2020
PRECONDITION(
21-
pointer_type.subtype().get(ID_identifier) ==
21+
pointer_type.base_type().get(ID_identifier) ==
2222
pointer_subtype_struct.get(ID_name));
2323

2424
// If the pointer points to:

‎jbmc/src/java_bytecode/goto_check_java.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1148,7 +1148,7 @@ bool goto_check_javat::check_rec_member(const member_exprt &member)
11481148
if(member_offset_opt.has_value())
11491149
{
11501150
pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
1151-
new_pointer_type.subtype() = member.type();
1151+
new_pointer_type.base_type() = member.type();
11521152

11531153
const exprt char_pointer = typecast_exprt::conditional_cast(
11541154
deref.pointer(), pointer_type(char_type()));

‎jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -412,7 +412,7 @@ static void instrument_get_monitor_count(
412412

413413
const namespacet ns(symbol_table);
414414
const auto &followed_type =
415-
ns.follow(to_pointer_type(f_code.arguments()[0].type()).subtype());
415+
ns.follow(to_pointer_type(f_code.arguments()[0].type()).base_type());
416416
const auto &object_type = to_struct_type(followed_type);
417417
code_assignt code_assign(
418418
f_code.lhs(),

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1235,7 +1235,7 @@ void mark_java_implicitly_generic_class_type(
12351235
id2string(strip_java_namespace_prefix(
12361236
outer_generic_type_parameter.get_name()));
12371237
java_generic_parameter_tagt bound = to_java_generic_parameter_tag(
1238-
outer_generic_type_parameter.subtype());
1238+
outer_generic_type_parameter.base_type());
12391239
bound.type_variable_ref().set_identifier(identifier);
12401240
implicit_generic_type_parameters.emplace_back(identifier, bound);
12411241
}

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2711,10 +2711,10 @@ void java_bytecode_convert_methodt::convert_getstatic(
27112711
else if(arg0.type().id() == ID_pointer)
27122712
{
27132713
const auto &pointer_type = to_pointer_type(arg0.type());
2714-
if(pointer_type.subtype().id() == ID_struct_tag)
2714+
if(pointer_type.base_type().id() == ID_struct_tag)
27152715
{
27162716
needed_lazy_methods->add_needed_class(
2717-
to_struct_tag_type(pointer_type.subtype()).get_identifier());
2717+
to_struct_tag_type(pointer_type.base_type()).get_identifier());
27182718
}
27192719
}
27202720
else if(is_assertions_disabled_field)

‎jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1486,7 +1486,7 @@ bool java_bytecode_languaget::convert_single_method_code(
14861486
// TODO(tkiley): investigation
14871487
namespacet ns{symbol_table};
14881488
const java_class_typet &underlying_type =
1489-
to_java_class_type(ns.follow(pointer_return_type->subtype()));
1489+
to_java_class_type(ns.follow(pointer_return_type->base_type()));
14901490

14911491
if(!underlying_type.is_abstract())
14921492
needed_lazy_methods->add_all_needed_classes(*pointer_return_type);

‎jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -480,7 +480,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
480480
{
481481
PRECONDITION(expr.type().id()==ID_pointer);
482482
const namespacet ns(symbol_table);
483-
const typet &subtype = pointer_type.subtype();
483+
const typet &subtype = pointer_type.base_type();
484484
const typet &followed_subtype = ns.follow(subtype);
485485
PRECONDITION(followed_subtype.id() == ID_struct);
486486
const pointer_typet &replacement_pointer_type =
@@ -499,7 +499,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
499499
generic_parameter_specialization_map_keys(
500500
generic_parameter_specialization_map);
501501
generic_parameter_specialization_map_keys.insert(
502-
replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
502+
replacement_pointer_type,
503+
ns.follow(replacement_pointer_type.base_type()));
503504

504505
const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
505506
assignments, lifetime, replacement_pointer_type, depth, location);
@@ -1019,7 +1020,7 @@ void java_object_factoryt::gen_nondet_init(
10191020
generic_parameter_specialization_map_keys(
10201021
generic_parameter_specialization_map);
10211022
generic_parameter_specialization_map_keys.insert(
1022-
pointer_type, ns.follow(pointer_type.subtype()));
1023+
pointer_type, ns.follow(pointer_type.base_type()));
10231024

10241025
gen_nondet_pointer_init(
10251026
assignments,

‎jbmc/src/java_bytecode/java_pointer_casts.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -82,19 +82,21 @@ exprt make_clean_pointer_cast(
8282
return ptr;
8383

8484
if(
85-
ptr.type().subtype() == java_void_type() ||
86-
target_type.subtype() == java_void_type())
85+
to_pointer_type(ptr.type()).base_type() == java_void_type() ||
86+
target_type.base_type() == java_void_type())
87+
{
8788
return typecast_exprt(ptr, target_type);
89+
}
8890

89-
const typet &target_base=ns.follow(target_type.subtype());
91+
const typet &target_base = ns.follow(target_type.base_type());
9092

9193
exprt bare_ptr=ptr;
9294
while(bare_ptr.id()==ID_typecast)
9395
{
9496
assert(
9597
bare_ptr.type().id()==ID_pointer &&
9698
"Non-pointer in make_clean_pointer_cast?");
97-
if(bare_ptr.type().subtype() == java_void_type())
99+
if(to_pointer_type(bare_ptr.type()).base_type() == java_void_type())
98100
bare_ptr = to_typecast_expr(bare_ptr).op();
99101
}
100102

‎jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -64,8 +64,8 @@ bool java_string_library_preprocesst::is_java_string_pointer_type(
6464
if(type.id()==ID_pointer)
6565
{
6666
const pointer_typet &pt=to_pointer_type(type);
67-
const typet &subtype=pt.subtype();
68-
return is_java_string_type(subtype);
67+
const typet &base_type = pt.base_type();
68+
return is_java_string_type(base_type);
6969
}
7070
return false;
7171
}
@@ -95,8 +95,8 @@ bool java_string_library_preprocesst::is_java_string_builder_pointer_type(
9595
if(type.id()==ID_pointer)
9696
{
9797
const pointer_typet &pt=to_pointer_type(type);
98-
const typet &subtype=pt.subtype();
99-
return is_java_string_builder_type(subtype);
98+
const typet &base_type = pt.base_type();
99+
return is_java_string_builder_type(base_type);
100100
}
101101
return false;
102102
}
@@ -118,8 +118,8 @@ bool java_string_library_preprocesst::is_java_string_buffer_pointer_type(
118118
if(type.id()==ID_pointer)
119119
{
120120
const pointer_typet &pt=to_pointer_type(type);
121-
const typet &subtype=pt.subtype();
122-
return is_java_string_buffer_type(subtype);
121+
const typet &base_type = pt.base_type();
122+
return is_java_string_buffer_type(base_type);
123123
}
124124
return false;
125125
}
@@ -141,8 +141,8 @@ bool java_string_library_preprocesst::is_java_char_sequence_pointer_type(
141141
if(type.id()==ID_pointer)
142142
{
143143
const pointer_typet &pt=to_pointer_type(type);
144-
const typet &subtype=pt.subtype();
145-
return is_java_char_sequence_type(subtype);
144+
const typet &base_type = pt.base_type();
145+
return is_java_char_sequence_type(base_type);
146146
}
147147
return false;
148148
}
@@ -164,8 +164,8 @@ bool java_string_library_preprocesst::is_java_char_array_pointer_type(
164164
if(type.id()==ID_pointer)
165165
{
166166
const pointer_typet &pt=to_pointer_type(type);
167-
const typet &subtype=pt.subtype();
168-
return is_java_char_array_type(subtype);
167+
const typet &base_type = pt.base_type();
168+
return is_java_char_array_type(base_type);
169169
}
170170
return false;
171171
}

‎jbmc/src/java_bytecode/java_types.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1049,9 +1049,9 @@ java_generic_struct_tag_typet::java_generic_struct_tag_typet(
10491049
const java_generic_typet &gen_base_type = to_java_generic_type(*base_type);
10501050
INVARIANT(
10511051
type.get_identifier() ==
1052-
to_struct_tag_type(gen_base_type.subtype()).get_identifier(),
1052+
to_struct_tag_type(gen_base_type.base_type()).get_identifier(),
10531053
"identifier of " + type.pretty() + "\n and identifier of type " +
1054-
gen_base_type.subtype().pretty() +
1054+
gen_base_type.base_type().pretty() +
10551055
"\ncreated by java_type_from_string for " + base_ref +
10561056
" should be equal");
10571057
generic_types().insert(

‎jbmc/src/java_bytecode/java_types.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1056,7 +1056,7 @@ inline const typet &java_generic_class_type_bound(size_t index, const typet &t)
10561056
PRECONDITION(index<gen_types.size());
10571057
const java_generic_parametert &gen_type=gen_types[index];
10581058

1059-
return gen_type.subtype();
1059+
return gen_type.base_type();
10601060
}
10611061

10621062
/// Type to hold a Java class that is implicitly generic, e.g., an inner

‎jbmc/src/java_bytecode/java_utils.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -273,7 +273,7 @@ pointer_typet pointer_to_replacement_type(
273273
const pointer_typet &given_pointer_type,
274274
const java_class_typet &replacement_class_type)
275275
{
276-
if(can_cast_type<struct_tag_typet>(given_pointer_type.subtype()))
276+
if(can_cast_type<struct_tag_typet>(given_pointer_type.base_type()))
277277
{
278278
struct_tag_typet struct_tag_subtype{replacement_class_type.get_name()};
279279
return pointer_type(struct_tag_subtype);

‎jbmc/src/java_bytecode/select_pointer_type.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -59,21 +59,21 @@ pointer_typet select_pointer_typet::specialize_generics(
5959
}
6060
}
6161

62-
auto subtype =
63-
type_try_dynamic_cast<struct_tag_typet>(pointer_type.subtype());
64-
if(subtype != nullptr && is_java_array_tag(subtype->get_identifier()))
62+
auto base_type =
63+
type_try_dynamic_cast<struct_tag_typet>(pointer_type.base_type());
64+
if(base_type != nullptr && is_java_array_tag(base_type->get_identifier()))
6565
{
6666
// if the pointer is an array, recursively specialize its element type
6767
const auto *array_element_type =
68-
type_try_dynamic_cast<pointer_typet>(java_array_element_type(*subtype));
68+
type_try_dynamic_cast<pointer_typet>(java_array_element_type(*base_type));
6969
if(array_element_type == nullptr)
7070
return pointer_type;
7171

7272
const pointer_typet &new_array_type = specialize_generics(
7373
*array_element_type, generic_parameter_specialization_map);
7474

7575
pointer_typet replacement_array_type = java_array_type('a');
76-
replacement_array_type.subtype().set(ID_element_type, new_array_type);
76+
replacement_array_type.base_type().set(ID_element_type, new_array_type);
7777
return replacement_array_type;
7878
}
7979

‎jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -319,7 +319,7 @@ SCENARIO(
319319
// Trace the assignments back to the declaration of the generic type
320320
// and verify that it is what we expect.
321321
const auto &tmp_object_struct_tag = to_struct_tag_type(
322-
to_pointer_type(tmp_object_declaration.symbol().type()).subtype());
322+
to_pointer_type(tmp_object_declaration.symbol().type()).base_type());
323323
REQUIRE(tmp_object_struct_tag.get_identifier() == "java::Wrapper");
324324

325325
THEN("Object 'v' has field 'field' of type IWrapper")
@@ -369,7 +369,7 @@ SCENARIO(
369369
// Trace the assignments back to the declaration of the generic type
370370
// and verify that it is what we expect.
371371
const auto &tmp_object_struct_tag = to_struct_tag_type(
372-
to_pointer_type(tmp_object_declaration.symbol().type()).subtype());
372+
to_pointer_type(tmp_object_declaration.symbol().type()).base_type());
373373
REQUIRE(tmp_object_struct_tag.get_identifier() == "java::Wrapper");
374374

375375
THEN(
@@ -419,7 +419,7 @@ SCENARIO(
419419
// Trace the assignments back to the declaration of the generic type
420420
// and verify that it is what we expect.
421421
const auto &tmp_object_struct_tag = to_struct_tag_type(
422-
to_pointer_type(tmp_object_declaration.symbol().type()).subtype());
422+
to_pointer_type(tmp_object_declaration.symbol().type()).base_type());
423423
REQUIRE(
424424
tmp_object_struct_tag.get_identifier() ==
425425
"java::GenericFields$GenericInnerOuter$Outer");
@@ -484,7 +484,7 @@ SCENARIO(
484484
// Trace the assignments back to the declaration of the generic type
485485
// and verify that it is what we expect.
486486
const auto &tmp_object_struct_tag = to_struct_tag_type(
487-
to_pointer_type(tmp_object_declaration.symbol().type()).subtype());
487+
to_pointer_type(tmp_object_declaration.symbol().type()).base_type());
488488
REQUIRE(
489489
tmp_object_struct_tag.get_identifier() ==
490490
"java::GenericFields$GenericRewriteParameter$A");

‎jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ SCENARIO(
4848
{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}});
4949

5050
// ... which is of type `KeyValue` ...
51-
const auto &subtype = gen_type.subtype();
51+
const auto &subtype = gen_type.base_type();
5252
const auto &key_value =
5353
symbol_table.lookup_ref(to_struct_tag_type(subtype).get_identifier());
5454
REQUIRE(key_value.type.id() == ID_struct);
@@ -66,9 +66,9 @@ SCENARIO(
6666
next.type(),
6767
{{require_type::type_argument_kindt::Var, "java::KeyValue::K"},
6868
{require_type::type_argument_kindt::Var, "java::KeyValue::V"}});
69-
REQUIRE(next_type.subtype().id() == ID_struct_tag);
69+
REQUIRE(next_type.base_type().id() == ID_struct_tag);
7070
const struct_tag_typet &next_symbol =
71-
to_struct_tag_type(next_type.subtype());
71+
to_struct_tag_type(next_type.base_type());
7272
REQUIRE(
7373
symbol_table.lookup_ref(next_symbol.get_identifier()).name ==
7474
"java::KeyValue");
@@ -79,9 +79,9 @@ SCENARIO(
7979
reverse.type(),
8080
{{require_type::type_argument_kindt::Var, "java::KeyValue::V"},
8181
{require_type::type_argument_kindt::Var, "java::KeyValue::K"}});
82-
REQUIRE(reverse_type.subtype().id() == ID_struct_tag);
82+
REQUIRE(reverse_type.base_type().id() == ID_struct_tag);
8383
const struct_tag_typet &reverse_symbol =
84-
to_struct_tag_type(reverse_type.subtype());
84+
to_struct_tag_type(reverse_type.base_type());
8585
REQUIRE(
8686
symbol_table.lookup_ref(reverse_symbol.get_identifier()).name ==
8787
"java::KeyValue");

‎jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ void validate_lambda_assignment(
7272
require_type::require_pointer(side_effect_expr.type(), {});
7373

7474
const struct_tag_typet &lambda_implementor_type =
75-
require_type::require_struct_tag(lambda_temp_type.subtype());
75+
require_type::require_struct_tag(lambda_temp_type.base_type());
7676

7777
const irep_idt &tmp_class_identifier =
7878
lambda_implementor_type.get_identifier();

‎jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ SCENARIO(
3737
field_t.type(), JAVA_REFERENCE_ARRAY_CLASSID);
3838

3939
const struct_tag_typet &field_t_subtype =
40-
to_struct_tag_type(field_t_pointer.subtype());
40+
to_struct_tag_type(field_t_pointer.base_type());
4141
const struct_typet &subtype_type = to_struct_type(
4242
new_symbol_table.lookup_ref(field_t_subtype.get_identifier()).type);
4343
REQUIRE(is_valid_java_array(subtype_type));
@@ -63,7 +63,7 @@ SCENARIO(
6363
field_t2.type(), JAVA_REFERENCE_ARRAY_CLASSID);
6464

6565
const struct_tag_typet &field_t2_subtype =
66-
to_struct_tag_type(field_t2_pointer.subtype());
66+
to_struct_tag_type(field_t2_pointer.base_type());
6767
const struct_typet &subtype_struct = to_struct_type(
6868
new_symbol_table.lookup_ref(field_t2_subtype.get_identifier()).type);
6969
REQUIRE(is_valid_java_array(subtype_struct));
@@ -91,7 +91,7 @@ SCENARIO(
9191
field_t3.type(), JAVA_REFERENCE_ARRAY_CLASSID);
9292

9393
const struct_tag_typet &field_t3_subtype =
94-
to_struct_tag_type(field_t3_pointer.subtype());
94+
to_struct_tag_type(field_t3_pointer.base_type());
9595
const struct_typet &subtype_struct = to_struct_type(
9696
new_symbol_table.lookup_ref(field_t3_subtype.get_identifier()).type);
9797
REQUIRE(is_valid_java_array(subtype_struct));

0 commit comments

Comments
 (0)