10
10
#include < iterator>
11
11
12
12
#include " generate_java_generic_type.h"
13
+ #include " generic_arguments_name_builder.h"
13
14
#include < util/namespace.h>
14
15
#include < java_bytecode/java_types.h>
15
16
#include < java_bytecode/java_utils.h>
@@ -19,6 +20,36 @@ generate_java_generic_typet::generate_java_generic_typet(
19
20
message_handler(message_handler)
20
21
{}
21
22
23
+ // / Small auxiliary function, to print a single generic argument name.
24
+ // / \param argument argument type
25
+ // / \return printed name of the argument
26
+ static std::string argument_name_printer (const reference_typet &argument)
27
+ {
28
+ const irep_idt &id (id2string (argument.subtype ().get (ID_identifier)));
29
+ if (is_java_array_tag (id))
30
+ {
31
+ std::string name = pretty_print_java_type (id2string (id));
32
+ const typet &element_type =
33
+ java_array_element_type (to_symbol_type (argument.subtype ()));
34
+
35
+ // If this is an array of references then we will specialize its
36
+ // identifier using the type of the objects in the array. Else, there
37
+ // can be a problem with the same symbols for different instantiations
38
+ // using arrays with different types.
39
+ if (element_type.id () == ID_pointer)
40
+ {
41
+ const symbol_typet element_symbol =
42
+ to_symbol_type (element_type.subtype ());
43
+ name.append (" of_" + id2string (element_symbol.get_identifier ()));
44
+ }
45
+ return name;
46
+ }
47
+ else
48
+ {
49
+ return id2string (id);
50
+ }
51
+ }
52
+
22
53
// / Generate a concrete instantiation of a generic type.
23
54
// / \param existing_generic_type The type to be concretised
24
55
// / \param symbol_table The symbol table that the concrete type will be
@@ -43,8 +74,8 @@ symbolt generate_java_generic_typet::operator()(
43
74
const java_class_typet &class_definition =
44
75
to_java_class_type (pointer_subtype);
45
76
46
- const irep_idt generic_name =
47
- build_generic_name ( existing_generic_type, class_definition);
77
+ const std::string generic_name = build_generic_name (
78
+ existing_generic_type, class_definition, argument_name_printer );
48
79
struct_union_typet::componentst replacement_components =
49
80
class_definition.components ();
50
81
@@ -204,172 +235,96 @@ typet generate_java_generic_typet::substitute_type(
204
235
return parameter_type;
205
236
}
206
237
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
238
// / Build a unique name for the generic to be instantiated.
239
+ // / Example: if \p existing_generic_type is a pointer to `Outer<T>.Inner`
240
+ // / (\p original_class) with parameter `T` being specialized with argument
241
+ // / `Integer`, then the function returns a string `Outer<\p
242
+ // / argument_name_printer(Integer)>$Inner`.
296
243
// / \param existing_generic_type The type we want to concretise
297
- // / \param original_class
298
- // / \return A name for the new generic we want a unique name for.
299
- irep_idt generate_java_generic_typet::build_generic_name (
244
+ // / \param original_class The original class type for \p existing_generic_type
245
+ // / \param argument_name_printer A custom function to print names of individual
246
+ // / arguments (such as `Integer`, `Integer[]` for concise names or `java::java
247
+ // / .lang.Integer`, `array[reference]of_java::java.lang.Integer`)
248
+ // / \return A name for the new specialized generic class we want a unique name
249
+ // / for.
250
+ std::string generate_java_generic_typet::build_generic_name (
300
251
const java_generic_typet &existing_generic_type,
301
- const java_class_typet &original_class) const
252
+ const java_class_typet &original_class,
253
+ const generic_arguments_name_buildert::name_printert &argument_name_printer)
254
+ const
302
255
{
303
256
std::ostringstream generic_name_buffer;
304
257
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
258
+
259
+ // gather together all implicit generic types and generic types
260
+ std::vector<java_generic_parametert> generic_types;
314
261
if (is_java_implicitly_generic_class_type (original_class))
315
262
{
316
263
const java_implicitly_generic_class_typet
317
264
&implicitly_generic_original_class =
318
265
to_java_implicitly_generic_class_type (original_class);
319
-
320
- INVARIANT (
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)
331
- {
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);
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;
266
+ generic_types.insert (
267
+ generic_types.end (),
268
+ implicitly_generic_original_class.implicit_generic_types ().begin (),
269
+ implicitly_generic_original_class.implicit_generic_types ().end ());
347
270
}
348
-
349
- // if the original class is generic, add tag for the class itself
350
271
if (is_java_generic_class_type (original_class))
351
272
{
352
273
const java_generic_class_typet &generic_original_class =
353
274
to_java_generic_class_type (original_class);
354
-
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);
275
+ generic_types.insert (
276
+ generic_types.end (),
277
+ generic_original_class.generic_types ().begin (),
278
+ generic_original_class.generic_types ().end ());
368
279
}
369
280
370
281
INVARIANT (
371
- generic_argument_p == existing_generic_type.generic_type_arguments ().end (),
372
- " All type arguments must have been added to the name" );
282
+ generic_types.size () ==
283
+ existing_generic_type.generic_type_arguments ().size (),
284
+ " All generic types must be concretized" );
285
+
286
+ auto generic_type_p = generic_types.begin ();
287
+ std::string previous_class_name;
288
+ std::string current_class_name;
289
+ generic_arguments_name_buildert build_generic_arguments (
290
+ argument_name_printer);
291
+
292
+ // add generic arguments to each generic (outer) class
293
+ for (const auto &generic_argument :
294
+ existing_generic_type.generic_type_arguments ())
295
+ {
296
+ previous_class_name = current_class_name;
297
+ current_class_name = generic_type_p->get_parameter_class_name ();
298
+
299
+ // if the class names do not match, it means that the next generic
300
+ // (outer) class is being handled
301
+ if (current_class_name != previous_class_name)
302
+ {
303
+ // add the arguments of the previous generic class to the buffer
304
+ // and reset the builder
305
+ generic_name_buffer << build_generic_arguments.finalize ();
306
+
307
+ INVARIANT (
308
+ has_prefix (current_class_name, previous_class_name),
309
+ " Generic types are ordered from the outermost outer class inwards" );
310
+
311
+ // add the remaining part of the current generic class name to the buffer
312
+ // example: if current_outer_class = A$B$C, previous_outer_class = A,
313
+ // then substr of current, starting at the length of previous is $B$C
314
+ generic_name_buffer << current_class_name.substr (
315
+ previous_class_name.length ());
316
+ }
317
+
318
+ // add an argument to the current generic class
319
+ build_generic_arguments.add_argument (generic_argument);
320
+ ++generic_type_p;
321
+ }
322
+ generic_name_buffer << build_generic_arguments.finalize ();
323
+
324
+ // add the remaining part of the original class name to the buffer
325
+ generic_name_buffer << original_class_name.substr (
326
+ current_class_name.length ());
327
+
373
328
return generic_name_buffer.str ();
374
329
}
375
330
0 commit comments