Skip to content

Commit aec9e89

Browse files
NathanJPhillipsNathanJPhillips
committed
Change naming of implicit type parameters for inner classes
Previously they duplicated the names for the type parameters of the outer classes
1 parent b90abb3 commit aec9e89

File tree

3 files changed

+53
-31
lines changed

3 files changed

+53
-31
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

Lines changed: 18 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
2525
#include <util/c_types.h>
2626
#include <util/expr_initializer.h>
2727
#include <util/namespace.h>
28+
#include <util/prefix.h>
2829
#include <util/std_expr.h>
2930
#include <util/suffix.h>
3031

@@ -1037,12 +1038,10 @@ static void find_and_replace_parameter(
10371038
const std::string &replacement_parameter_full_name =
10381039
id2string(replacement_parameter_it->type_variable().get_identifier());
10391040

1040-
// the replacement parameter is a viable one, i.e., it comes from an outer
1041-
// class
1042-
PRECONDITION(
1043-
get_without_final_name_component(parameter_full_name)
1044-
.compare(
1045-
get_without_final_name_component(replacement_parameter_full_name)) > 0);
1041+
// Check the replacement parameter comes from an outer class
1042+
PRECONDITION(has_prefix(
1043+
replacement_parameter_full_name,
1044+
get_without_final_name_component(parameter_full_name)));
10461045

10471046
parameter.type_variable_ref().set_identifier(replacement_parameter_full_name);
10481047
}
@@ -1176,12 +1175,19 @@ void mark_java_implicitly_generic_class_type(
11761175
to_java_class_type(outer_class_symbol.type);
11771176
if(is_java_generic_class_type(outer_class_type))
11781177
{
1179-
const auto &outer_generic_type_parameters =
1180-
to_java_generic_class_type(outer_class_type).generic_types();
1181-
implicit_generic_type_parameters.insert(
1182-
implicit_generic_type_parameters.begin(),
1183-
outer_generic_type_parameters.begin(),
1184-
outer_generic_type_parameters.end());
1178+
for(const java_generic_parametert &outer_generic_type_parameter :
1179+
to_java_generic_class_type(outer_class_type).generic_types())
1180+
{
1181+
// Create a new generic type parameter with name in the form:
1182+
// java::Outer$Inner::Outer::T
1183+
irep_idt identifier = qualified_class_name + "::" +
1184+
id2string(strip_java_namespace_prefix(
1185+
outer_generic_type_parameter.get_name()));
1186+
java_generic_parameter_tagt bound = to_java_generic_parameter_tag(
1187+
outer_generic_type_parameter.subtype());
1188+
bound.type_variable_ref().set_identifier(identifier);
1189+
implicit_generic_type_parameters.emplace_back(identifier, bound);
1190+
}
11851191
}
11861192
outer_class_delimiter = outer_class_name.rfind('$');
11871193
}

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

Lines changed: 15 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -187,7 +187,9 @@ SCENARIO(
187187

188188
const class_typet &derived_class_type =
189189
require_type::require_complete_java_implicitly_generic_class(
190-
derived_symbol.type, {"java::ContainsInnerClassGeneric::T"});
190+
derived_symbol.type,
191+
{"java::ContainsInnerClassGeneric$InnerClass::"
192+
"ContainsInnerClassGeneric::T"});
191193

192194
THEN("The base for superclass has the correct generic type information")
193195
{
@@ -197,7 +199,8 @@ SCENARIO(
197199
base_type,
198200
"java::Generic",
199201
{{require_type::type_argument_kindt::Var,
200-
"java::ContainsInnerClassGeneric::T"}});
202+
"java::ContainsInnerClassGeneric$InnerClass::"
203+
"ContainsInnerClassGeneric::T"}});
201204
}
202205
}
203206

@@ -552,7 +555,8 @@ SCENARIO(
552555
require_type::require_java_generic_struct_tag_type(
553556
base_type,
554557
"java::GenericBase$ImplicitGeneric",
555-
{{require_type::type_argument_kindt::Var, "java::GenericBase::T"}});
558+
{{require_type::type_argument_kindt::Var,
559+
"java::GenericBase$ExtendImplicit::GenericBase::T"}});
556560
}
557561
}
558562

@@ -573,7 +577,8 @@ SCENARIO(
573577
require_type::require_java_generic_struct_tag_type(
574578
base_type,
575579
"java::GenericBase$ImplicitAndExplicitGeneric",
576-
{{require_type::type_argument_kindt::Var, "java::GenericBase::T"},
580+
{{require_type::type_argument_kindt::Var,
581+
"java::GenericBase$ExtendImplicitAndExplicit::GenericBase::T"},
577582
{require_type::type_argument_kindt::Var,
578583
"java::GenericBase$ExtendImplicitAndExplicit::S"}});
579584
}
@@ -596,9 +601,12 @@ SCENARIO(
596601
require_type::require_java_generic_struct_tag_type(
597602
base_type,
598603
"java::GenericBase2$ImplicitAndExplicitGeneric",
599-
{{require_type::type_argument_kindt::Var, "java::GenericBase2::T"},
600-
{require_type::type_argument_kindt::Var, "java::GenericBase2::S"},
601-
{require_type::type_argument_kindt::Var, "java::GenericBase2::S"}});
604+
{{require_type::type_argument_kindt::Var,
605+
"java::GenericBase2$ExtendImplicitAndExplicit::GenericBase2::T"},
606+
{require_type::type_argument_kindt::Var,
607+
"java::GenericBase2$ExtendImplicitAndExplicit::GenericBase2::S"},
608+
{require_type::type_argument_kindt::Var,
609+
"java::GenericBase2$ExtendImplicitAndExplicit::GenericBase2::S"}});
602610
}
603611
}
604612
}

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

Lines changed: 20 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,8 @@ SCENARIO(
1818
"GenericClassWithInnerClasses",
1919
"./java_bytecode/java_bytecode_parse_generics");
2020

21-
std::string outer_class_prefix = "java::GenericClassWithInnerClasses";
21+
std::string outer_class_name = "GenericClassWithInnerClasses";
22+
std::string outer_class_prefix = "java::" + outer_class_name;
2223

2324
WHEN("Generic outer class has fields which are objects of the inner classes")
2425
{
@@ -69,15 +70,16 @@ SCENARIO(
6970
{
7071
const java_implicitly_generic_class_typet &java_class =
7172
require_type::require_complete_java_implicitly_generic_class(
72-
class_symbol.type, {outer_class_prefix + "::T"});
73+
class_symbol.type,
74+
{inner_class_prefix + "::" + outer_class_name + "::T"});
7375

7476
THEN(
7577
"There is a field t1 which is the generic parameter of the outer "
7678
"class")
7779
{
7880
const auto &field = require_type::require_component(java_class, "t1");
7981
require_type::require_java_generic_parameter(
80-
field.type(), outer_class_prefix + "::T");
82+
field.type(), inner_class_prefix + "::" + outer_class_name + "::T");
8183
}
8284
THEN(
8385
"There is a field t2 of generic type with the generic "
@@ -88,7 +90,7 @@ SCENARIO(
8890
require_type::require_java_generic_type(
8991
field.type(),
9092
{{require_type::type_argument_kindt::Var,
91-
outer_class_prefix + "::T"}});
93+
inner_class_prefix + "::" + outer_class_name + "::T"}});
9294
}
9395
}
9496
}
@@ -105,15 +107,17 @@ SCENARIO(
105107
{
106108
const java_implicitly_generic_class_typet &java_class =
107109
require_type::require_complete_java_implicitly_generic_class(
108-
class_symbol.type, {outer_class_prefix + "::T"});
110+
class_symbol.type,
111+
{inner_inner_class_prefix + "::" + outer_class_name + "::T"});
109112

110113
THEN(
111114
"There is a field tt1 which is the generic parameter of the outer "
112115
"class")
113116
{
114117
const auto &field = require_type::require_component(java_class, "tt1");
115118
require_type::require_java_generic_parameter(
116-
field.type(), outer_class_prefix + "::T");
119+
field.type(),
120+
inner_inner_class_prefix + "::" + outer_class_name + "::T");
117121
}
118122
THEN(
119123
"There is a field tt2 of nested generic type with the generic "
@@ -132,7 +136,7 @@ SCENARIO(
132136
require_type::require_java_generic_type(
133137
type_argument,
134138
{{require_type::type_argument_kindt::Var,
135-
outer_class_prefix + "::T"}});
139+
inner_inner_class_prefix + "::" + outer_class_name + "::T"}});
136140
}
137141
}
138142
}
@@ -148,7 +152,8 @@ SCENARIO(
148152
THEN("It has correct generic types and implicit generic types")
149153
{
150154
require_type::require_complete_java_implicitly_generic_class(
151-
class_symbol.type, {outer_class_prefix + "::T"});
155+
class_symbol.type,
156+
{generic_inner_class_prefix + "::" + outer_class_name + "::T"});
152157
const java_generic_class_typet &generic_class =
153158
require_type::require_complete_java_generic_class(
154159
class_symbol.type, {generic_inner_class_prefix + "::U"});
@@ -160,7 +165,8 @@ SCENARIO(
160165
const auto &field =
161166
require_type::require_component(generic_class, "gt1");
162167
require_type::require_java_generic_parameter(
163-
field.type(), outer_class_prefix + "::T");
168+
field.type(),
169+
generic_inner_class_prefix + "::" + outer_class_name + "::T");
164170
}
165171
THEN(
166172
"There is a field gt2 of generic type with the generic "
@@ -173,9 +179,9 @@ SCENARIO(
173179
require_type::require_java_generic_type(
174180
field.type(),
175181
{{require_type::type_argument_kindt::Var,
176-
outer_class_prefix + "::T"},
182+
generic_inner_class_prefix + "::" + outer_class_name + "::T"},
177183
{require_type::type_argument_kindt::Var,
178-
generic_inner_class_prefix + "::U"}});
184+
generic_inner_class_prefix + "::U"}});
179185
}
180186
}
181187
}
@@ -194,7 +200,9 @@ SCENARIO(
194200
{
195201
require_type::require_complete_java_implicitly_generic_class(
196202
class_symbol.type,
197-
{outer_class_prefix + "::T", outer_class_prefix + "$GenericInner::U"});
203+
{generic_inner_inner_class_prefix + "::" + outer_class_name +
204+
"$GenericInner::U",
205+
generic_inner_inner_class_prefix + "::" + outer_class_name + "::T"});
198206
require_type::require_complete_java_generic_class(
199207
class_symbol.type, {generic_inner_inner_class_prefix + "::V"});
200208
}

0 commit comments

Comments
 (0)