Skip to content

Commit a01a0f2

Browse files
author
thk123
committed
Extend the specialisation code to handle generic fields
Previously we didn't handle generic fields when we were doing specialisation, meaning they were missed. This resolves this and adds a unit test to demonstrate it.
1 parent 1ccbf83 commit a01a0f2

File tree

3 files changed

+68
-13
lines changed

3 files changed

+68
-13
lines changed

src/java_bytecode/generate_java_generic_type.cpp

Lines changed: 51 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -117,22 +117,61 @@ typet generate_java_generic_typet::substitute_type(
117117
return parameter_type;
118118
}
119119
}
120-
else if(
121-
parameter_type.id() == ID_pointer &&
122-
parameter_type.subtype().id() == ID_symbol)
120+
else if(parameter_type.id() == ID_pointer)
123121
{
124-
const symbol_typet &array_subtype =
125-
to_symbol_type(parameter_type.subtype());
126-
if(is_java_array_tag(array_subtype.get_identifier()))
122+
if(is_java_generic_type(parameter_type))
127123
{
128-
const typet &array_element_type = java_array_element_type(array_subtype);
124+
const java_generic_typet &generic_type =
125+
to_java_generic_type(parameter_type);
126+
127+
java_generic_typet::generic_type_variablest replaced_type_variables;
128+
129+
// Swap each parameter
130+
std::transform(
131+
generic_type.generic_type_variables().begin(),
132+
generic_type.generic_type_variables().end(),
133+
std::back_inserter(replaced_type_variables),
134+
[&](const java_generic_parametert &generic_param)
135+
-> java_generic_parametert {
136+
const typet &replacement_type =
137+
substitute_type(generic_param, generic_class, generic_reference);
138+
139+
// This code will be simplified when references aren't considered to
140+
// be generic parameters
141+
if(is_java_generic_parameter(replacement_type))
142+
{
143+
return to_java_generic_parameter(replacement_type);
144+
}
145+
else
146+
{
147+
INVARIANT(
148+
is_reference(replacement_type),
149+
"All generic parameters should be references");
150+
return java_generic_inst_parametert(
151+
to_symbol_type(replacement_type.subtype()));
152+
}
153+
});
154+
155+
java_generic_typet new_type = generic_type;
156+
new_type.generic_type_variables() = replaced_type_variables;
157+
return new_type;
158+
}
159+
else if(parameter_type.subtype().id() == ID_symbol)
160+
{
161+
const symbol_typet &array_subtype =
162+
to_symbol_type(parameter_type.subtype());
163+
if(is_java_array_tag(array_subtype.get_identifier()))
164+
{
165+
const typet &array_element_type =
166+
java_array_element_type(array_subtype);
129167

130-
const typet &new_array_type =
131-
substitute_type(array_element_type, generic_class, generic_reference);
168+
const typet &new_array_type =
169+
substitute_type(array_element_type, generic_class, generic_reference);
132170

133-
typet replacement_array_type = java_array_type('a');
134-
replacement_array_type.subtype().set(ID_C_element_type, new_array_type);
135-
return replacement_array_type;
171+
typet replacement_array_type = java_array_type('a');
172+
replacement_array_type.subtype().set(ID_C_element_type, new_array_type);
173+
return replacement_array_type;
174+
}
136175
}
137176
}
138177
return parameter_type;

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -292,9 +292,9 @@ SCENARIO(
292292
const symbolt test_class_symbol =
293293
new_symbol_table.lookup_ref(specialised_class_name);
294294

295+
REQUIRE(test_class_symbol.type.id() == ID_struct);
295296
THEN("The array field should be specialised to be an array of floats")
296297
{
297-
REQUIRE(test_class_symbol.type.id() == ID_struct);
298298
const struct_typet::componentt &field_component =
299299
require_type::require_component(
300300
to_struct_type(test_class_symbol.type), "arrayField");
@@ -310,6 +310,20 @@ SCENARIO(
310310
require_type::require_pointer(
311311
array_type, symbol_typet("java::java.lang.Float"));
312312
}
313+
314+
THEN(
315+
"The generic class field should be specialised to be a generic "
316+
"class with the appropriate type")
317+
{
318+
const struct_typet::componentt &field_component =
319+
require_type::require_component(
320+
to_struct_type(test_class_symbol.type), "genericClassField");
321+
322+
require_type::require_java_generic_type(
323+
field_component.type(),
324+
{{require_type::type_parameter_kindt::Inst,
325+
"java::java.lang.Float"}});
326+
}
313327
}
314328
}
315329
}

unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@ class generic<T> {
66

77
class genericArray<T> {
88
T [] arrayField;
9+
10+
generic<T> genericClassField;
911
}
1012

1113
generic<Float []> f;

0 commit comments

Comments
 (0)