@@ -36,24 +36,25 @@ symbolt generate_java_generic_typet::operator()(
36
36
INVARIANT (
37
37
pointer_subtype.id ()==ID_struct, " Only pointers to classes in java" );
38
38
INVARIANT (
39
- is_java_generic_class_type (pointer_subtype),
39
+ is_java_generic_class_type (pointer_subtype) ||
40
+ is_java_implicitly_generic_class_type (pointer_subtype),
40
41
" Generic references type must be a generic class" );
41
42
42
- const java_generic_class_typet &generic_class_definition =
43
- to_java_generic_class_type ( to_java_class_type (pointer_subtype) );
43
+ const java_class_typet &class_definition =
44
+ to_java_class_type (pointer_subtype);
44
45
45
46
const irep_idt generic_name =
46
- build_generic_name (existing_generic_type, generic_class_definition );
47
+ build_generic_name (existing_generic_type, class_definition );
47
48
struct_union_typet::componentst replacement_components =
48
- generic_class_definition .components ();
49
+ class_definition .components ();
49
50
50
51
// Small auxiliary function, to perform the inplace
51
52
// modification of the generic fields.
52
53
auto replace_type_for_generic_field =
53
54
[&](struct_union_typet::componentt &component) {
54
55
55
56
component.type () = substitute_type (
56
- component.type (), generic_class_definition , existing_generic_type);
57
+ component.type (), class_definition , existing_generic_type);
57
58
58
59
return component;
59
60
};
@@ -66,16 +67,15 @@ symbolt generate_java_generic_typet::operator()(
66
67
replacement_components.end (),
67
68
replace_type_for_generic_field);
68
69
69
- std::size_t after_modification_size =
70
- generic_class_definition.components ().size ();
70
+ std::size_t after_modification_size = class_definition.components ().size ();
71
71
72
72
INVARIANT (
73
73
pre_modification_size==after_modification_size,
74
74
" All components in the original class should be in the new class" );
75
75
76
76
const java_specialized_generic_class_typet new_java_class{
77
77
generic_name,
78
- generic_class_definition .get_tag (),
78
+ class_definition .get_tag (),
79
79
replacement_components,
80
80
existing_generic_type.generic_type_arguments ()};
81
81
@@ -110,7 +110,7 @@ symbolt generate_java_generic_typet::operator()(
110
110
// / there are none to replace, the original type.
111
111
typet generate_java_generic_typet::substitute_type (
112
112
const typet ¶meter_type,
113
- const java_generic_class_typet &generic_class ,
113
+ const java_class_typet &class_definition ,
114
114
const java_generic_typet &generic_reference) const
115
115
{
116
116
if (is_java_generic_parameter (parameter_type))
@@ -119,8 +119,28 @@ typet generate_java_generic_typet::substitute_type(
119
119
.type_variable ()
120
120
.get_identifier ();
121
121
122
- optionalt<size_t > results =
123
- java_generics_get_index_for_subtype (generic_class, component_identifier);
122
+ // see if it is a generic parameter introduced by this class
123
+ optionalt<size_t > results;
124
+ if (is_java_generic_class_type (class_definition))
125
+ {
126
+ const java_generic_class_typet &generic_class =
127
+ to_java_generic_class_type (class_definition);
128
+
129
+ results = java_generics_get_index_for_subtype (
130
+ generic_class.generic_types (), component_identifier);
131
+ }
132
+ // see if it is an implicit generic parameter introduced by an outer class
133
+ if (!results.has_value ())
134
+ {
135
+ INVARIANT (
136
+ is_java_implicitly_generic_class_type (class_definition),
137
+ " The parameter must either be a generic type or implicit generic type" );
138
+ const java_implicitly_generic_class_typet &implicitly_generic_class =
139
+ to_java_implicitly_generic_class_type (class_definition);
140
+ results = java_generics_get_index_for_subtype (
141
+ implicitly_generic_class.implicit_generic_types (),
142
+ component_identifier);
143
+ }
124
144
125
145
INVARIANT (results.has_value (), " generic component type not found" );
126
146
return generic_reference.generic_type_arguments ()[*results];
@@ -142,7 +162,7 @@ typet generate_java_generic_typet::substitute_type(
142
162
[&](const reference_typet &generic_param) -> reference_typet
143
163
{
144
164
const typet &replacement_type =
145
- substitute_type (generic_param, generic_class , generic_reference);
165
+ substitute_type (generic_param, class_definition , generic_reference);
146
166
147
167
// This code will be simplified when references aren't considered to
148
168
// be generic parameters
@@ -172,8 +192,8 @@ typet generate_java_generic_typet::substitute_type(
172
192
const typet &array_element_type =
173
193
java_array_element_type (array_subtype);
174
194
175
- const typet &new_array_type =
176
- substitute_type ( array_element_type, generic_class , generic_reference);
195
+ const typet &new_array_type = substitute_type (
196
+ array_element_type, class_definition , generic_reference);
177
197
178
198
typet replacement_array_type = java_array_type (' a' );
179
199
replacement_array_type.subtype ().set (ID_C_element_type, new_array_type);
@@ -184,51 +204,173 @@ typet generate_java_generic_typet::substitute_type(
184
204
return parameter_type;
185
205
}
186
206
187
- // / Build a unique tag for the generic to be instantiated.
207
+ // / Creates a name for an argument that is an array, e.g., for an array of
208
+ // / Integers it returns a string `array[reference]of_java::java.lang.Integer`
209
+ // / \param id argument of type array
210
+ // / \param generic_argument_p array reference type
211
+ // / \return name as a string
212
+ static irep_idt build_name_for_array_argument (
213
+ const irep_idt &id,
214
+ const reference_typet &generic_argument_p)
215
+ {
216
+ PRECONDITION (is_java_array_tag (id));
217
+ std::ostringstream name_buffer;
218
+ name_buffer << pretty_print_java_type (id2string (id));
219
+ const typet &element_type =
220
+ java_array_element_type (to_symbol_type (generic_argument_p.subtype ()));
221
+
222
+ // If this is an array of references then we will specialize its
223
+ // identifier using the type of the objects in the array. Else, there
224
+ // can be a problem with the same symbols for different instantiations
225
+ // using arrays with different types.
226
+ if (element_type.id () == ID_pointer)
227
+ {
228
+ const symbol_typet element_symbol = to_symbol_type (element_type.subtype ());
229
+ name_buffer << " of_" + id2string (element_symbol.get_identifier ());
230
+ }
231
+ return name_buffer.str ();
232
+ }
233
+
234
+ // / Build a generic name for a generic class, from given generic arguments.
235
+ // / For example, given a class `Class` with two generic type parameters
236
+ // / `java::Class::T` and `java::Class::U`, and two arguments
237
+ // / `java::java.lang.Integer` and `java::Outer$Inner`, the returned string is
238
+ // / `<java::java.lang.Integer, java::Outer$Inner>`.
239
+ // / \param generic_argument_p iterator over generic arguments
240
+ // / \param generic_type_p iterator over generic types, starts with types for
241
+ // / the given class, may continue with generic types of its inner classes
242
+ // / \param generic_types_end end of the vector of generic types
243
+ // / \param class_name name of the class for which the tag is being built
244
+ // / \return name as a string of the form `<*, *, ..., *>`
245
+ static irep_idt build_generic_name_for_class_arguments (
246
+ std::vector<reference_typet>::const_iterator &generic_argument_p,
247
+ std::vector<java_generic_parametert>::const_iterator &generic_type_p,
248
+ const std::vector<java_generic_parametert>::const_iterator &generic_types_end,
249
+ const std::string &class_name)
250
+ {
251
+ std::ostringstream name_buffer;
252
+ bool first = true ;
253
+ std::string parameter_class_name =
254
+ (*generic_type_p).get_parameter_class_name ();
255
+ PRECONDITION (parameter_class_name == class_name);
256
+
257
+ while (parameter_class_name == class_name)
258
+ {
259
+ if (first)
260
+ {
261
+ name_buffer << " <" ;
262
+ first = false ;
263
+ }
264
+ else
265
+ {
266
+ name_buffer << " , " ;
267
+ }
268
+
269
+ const irep_idt &id (
270
+ id2string ((*generic_argument_p).subtype ().get (ID_identifier)));
271
+ if (is_java_array_tag (id))
272
+ {
273
+ name_buffer << build_name_for_array_argument (id, *generic_argument_p);
274
+ }
275
+ else
276
+ {
277
+ name_buffer << id2string (id);
278
+ }
279
+
280
+ ++generic_argument_p;
281
+ ++generic_type_p;
282
+ if (generic_type_p != generic_types_end)
283
+ {
284
+ parameter_class_name = (*generic_type_p).get_parameter_class_name ();
285
+ }
286
+ else
287
+ {
288
+ break ;
289
+ }
290
+ }
291
+ name_buffer << " >" ;
292
+ return name_buffer.str ();
293
+ }
294
+
295
+ // / Build a unique name for the generic to be instantiated.
188
296
// / \param existing_generic_type The type we want to concretise
189
297
// / \param original_class
190
- // / \return A tag for the new generic we want a unique tag for.
298
+ // / \return A name for the new generic we want a unique name for.
191
299
irep_idt generate_java_generic_typet::build_generic_name (
192
300
const java_generic_typet &existing_generic_type,
193
301
const java_class_typet &original_class) const
194
302
{
195
- std::ostringstream new_tag_buffer;
196
- new_tag_buffer << original_class.get_tag ();
197
- new_tag_buffer << " <" ;
198
- bool first=true ;
199
- for (const typet &type_argument : existing_generic_type
200
- .generic_type_arguments ())
303
+ std::ostringstream generic_name_buffer;
304
+ const std::string &original_class_name = original_class.get_tag ().c_str ();
305
+ auto generic_argument_p =
306
+ existing_generic_type.generic_type_arguments ().begin ();
307
+
308
+ // if the original class is implicitly generic, add tags for all generic
309
+ // outer classes
310
+ // NOTE here we assume that the implicit generic types are ordered from the
311
+ // outermost outer class inwards, this is currently guaranteed by the way
312
+ // this vector is constructed in
313
+ // java_bytecode_convert_class:mark_java_implicitly_generic_class_type
314
+ if (is_java_implicitly_generic_class_type (original_class))
201
315
{
202
- if (!first)
203
- new_tag_buffer << " , " ;
204
- first= false ;
316
+ const java_implicitly_generic_class_typet
317
+ &implicitly_generic_original_class =
318
+ to_java_implicitly_generic_class_type (original_class) ;
205
319
206
320
INVARIANT (
207
- !is_java_generic_parameter (type_argument),
208
- " Only create full concretized generic types" );
209
- const irep_idt &id (id2string (type_argument.subtype ().get (ID_identifier)));
210
- new_tag_buffer << pretty_print_java_type (id2string (id));
211
- if (is_java_array_tag (id))
321
+ existing_generic_type.generic_type_arguments ().size () >=
322
+ implicitly_generic_original_class.implicit_generic_types ().size (),
323
+ " All implicit generic types must be concretised" );
324
+ auto implicit_generic_type_p =
325
+ implicitly_generic_original_class.implicit_generic_types ().begin ();
326
+ const auto &implicit_generic_types_end =
327
+ implicitly_generic_original_class.implicit_generic_types ().end ();
328
+ std::string current_outer_class_name;
329
+
330
+ while (implicit_generic_type_p != implicit_generic_types_end)
212
331
{
213
- const typet &element_type =
214
- java_array_element_type (to_symbol_type (type_argument.subtype ()));
215
-
216
- // If this is an array of references then we will specialize its
217
- // identifier using the type of the objects in the array. Else, there can
218
- // be a problem with the same symbols for different instantiations using
219
- // arrays with different types.
220
- if (element_type.id () == ID_pointer)
221
- {
222
- const symbol_typet element_symbol =
223
- to_symbol_type (element_type.subtype ());
224
- new_tag_buffer << " of_" << id2string (element_symbol.get_identifier ());
225
- }
332
+ current_outer_class_name =
333
+ (*implicit_generic_type_p).get_parameter_class_name ();
334
+ generic_name_buffer << current_outer_class_name;
335
+ generic_name_buffer << build_generic_name_for_class_arguments (
336
+ generic_argument_p,
337
+ implicit_generic_type_p,
338
+ implicit_generic_types_end,
339
+ current_outer_class_name);
226
340
}
341
+ generic_name_buffer << original_class_name.substr (
342
+ current_outer_class_name.length (), std::string::npos);
343
+ }
344
+ else
345
+ {
346
+ generic_name_buffer << original_class_name;
227
347
}
228
348
229
- new_tag_buffer << " >" ;
349
+ // if the original class is generic, add tag for the class itself
350
+ if (is_java_generic_class_type (original_class))
351
+ {
352
+ const java_generic_class_typet &generic_original_class =
353
+ to_java_generic_class_type (original_class);
230
354
231
- return new_tag_buffer.str ();
355
+ INVARIANT (
356
+ std::distance (
357
+ generic_argument_p,
358
+ existing_generic_type.generic_type_arguments ().end ()) ==
359
+ static_cast <int >(generic_original_class.generic_types ().size ()),
360
+ " All generic types must be concretised" );
361
+ auto generic_type_p = generic_original_class.generic_types ().begin ();
362
+
363
+ generic_name_buffer << build_generic_name_for_class_arguments (
364
+ generic_argument_p,
365
+ generic_type_p,
366
+ generic_original_class.generic_types ().end (),
367
+ original_class_name);
368
+ }
369
+
370
+ INVARIANT (
371
+ generic_argument_p == existing_generic_type.generic_type_arguments ().end (),
372
+ " All type arguments must have been added to the name" );
373
+ return generic_name_buffer.str ();
232
374
}
233
375
234
376
// / Construct the symbol to be moved into the symbol table
0 commit comments