1010#include < iterator>
1111
1212#include " generate_java_generic_type.h"
13+ #include " generic_arguments_name_builder.h"
1314#include < util/namespace.h>
1415#include < java_bytecode/java_types.h>
1516#include < java_bytecode/java_utils.h>
@@ -19,6 +20,36 @@ generate_java_generic_typet::generate_java_generic_typet(
1920 message_handler(message_handler)
2021{}
2122
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+
2253// / Generate a concrete instantiation of a generic type.
2354// / \param existing_generic_type The type to be concretised
2455// / \param symbol_table The symbol table that the concrete type will be
@@ -43,8 +74,8 @@ symbolt generate_java_generic_typet::operator()(
4374 const java_class_typet &class_definition =
4475 to_java_class_type (pointer_subtype);
4576
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 );
4879 struct_union_typet::componentst replacement_components =
4980 class_definition.components ();
5081
@@ -204,172 +235,96 @@ typet generate_java_generic_typet::substitute_type(
204235 return parameter_type;
205236}
206237
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-
295238// / 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`.
296243// / \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 (
300251 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
302255{
303256 std::ostringstream generic_name_buffer;
304257 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;
314261 if (is_java_implicitly_generic_class_type (original_class))
315262 {
316263 const java_implicitly_generic_class_typet
317264 &implicitly_generic_original_class =
318265 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 ());
347270 }
348-
349- // if the original class is generic, add tag for the class itself
350271 if (is_java_generic_class_type (original_class))
351272 {
352273 const java_generic_class_typet &generic_original_class =
353274 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 ());
368279 }
369280
370281 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+
373328 return generic_name_buffer.str ();
374329}
375330
0 commit comments