11
11
#include < java_bytecode/java_types.h>
12
12
#include < java_bytecode/java_utils.h>
13
13
14
-
15
14
generate_java_generic_typet::generate_java_generic_typet (
16
15
message_handlert &message_handler):
17
16
message_handler(message_handler)
@@ -33,41 +32,26 @@ symbolt generate_java_generic_typet::operator()(
33
32
34
33
INVARIANT (
35
34
pointer_subtype.id ()==ID_struct, " Only pointers to classes in java" );
35
+ INVARIANT (
36
+ is_java_generic_class_type (pointer_subtype),
37
+ " Generic references type must be a generic class" );
36
38
37
- const java_class_typet &replacement_type=
38
- to_java_class_type (pointer_subtype);
39
- const irep_idt new_tag=build_generic_tag (
40
- existing_generic_type, replacement_type);
41
- struct_union_typet::componentst replacement_components=
42
- replacement_type.components ();
39
+ const java_generic_class_typet &generic_class_definition =
40
+ to_java_generic_class_type (to_java_class_type (pointer_subtype));
41
+
42
+ const irep_idt new_tag =
43
+ build_generic_tag (existing_generic_type, generic_class_definition);
44
+ struct_union_typet::componentst replacement_components =
45
+ generic_class_definition.components ();
43
46
44
47
// Small auxiliary function, to perform the inplace
45
48
// modification of the generic fields.
46
- auto replace_type_for_generic_field=
47
- [&](struct_union_typet::componentt &component)
48
- {
49
- if (is_java_generic_parameter (component.type ()))
50
- {
51
- auto replacement_type_param=
52
- to_java_generics_class_type (replacement_type);
53
-
54
- auto component_identifier=
55
- to_java_generic_parameter (component.type ()).type_variable ()
56
- .get_identifier ();
57
-
58
- optionalt<size_t > results=java_generics_get_index_for_subtype (
59
- replacement_type_param, component_identifier);
49
+ auto replace_type_for_generic_field =
50
+ [&](struct_union_typet::componentt &component) {
60
51
61
- INVARIANT (
62
- results.has_value (),
63
- " generic component type not found" );
52
+ component.type () = substitute_type (
53
+ component.type (), generic_class_definition, existing_generic_type);
64
54
65
- if (results)
66
- {
67
- component.type ()=
68
- existing_generic_type.generic_type_variables ()[*results];
69
- }
70
- }
71
55
return component;
72
56
};
73
57
@@ -79,8 +63,8 @@ symbolt generate_java_generic_typet::operator()(
79
63
replacement_components.end (),
80
64
replace_type_for_generic_field);
81
65
82
- std::size_t after_modification_size=
83
- replacement_type .components ().size ();
66
+ std::size_t after_modification_size =
67
+ generic_class_definition .components ().size ();
84
68
85
69
INVARIANT (
86
70
pre_modification_size==after_modification_size,
@@ -98,6 +82,95 @@ symbolt generate_java_generic_typet::operator()(
98
82
return *symbol;
99
83
}
100
84
85
+ // / For a given type, if the type contains a Java generic parameter, we look
86
+ // / that parameter up and return the relevant type. This works recursively on
87
+ // / arrays so that T [] is converted to RelevantType [].
88
+ // / \param parameter_type: The type under consideration
89
+ // / \param generic_class: The generic class that the \p parameter_type
90
+ // / belongs to (e.g. the type of a component of the class). This is used to
91
+ // / look up the mapping from name of generic parameter to its index.
92
+ // / \param generic_reference: The instantiated version of the generic class
93
+ // / used to look up the instantiated type. This is expected to be fully
94
+ // / instantiated.
95
+ // / \return A newly constructed type with generic parameters replaced, or if
96
+ // / there are none to replace, the original type.
97
+ typet generate_java_generic_typet::substitute_type (
98
+ const typet ¶meter_type,
99
+ const java_generic_class_typet &generic_class,
100
+ const java_generic_typet &generic_reference) const
101
+ {
102
+ if (is_java_generic_parameter (parameter_type))
103
+ {
104
+ auto component_identifier = to_java_generic_parameter (parameter_type)
105
+ .type_variable ()
106
+ .get_identifier ();
107
+
108
+ optionalt<size_t > results =
109
+ java_generics_get_index_for_subtype (generic_class, component_identifier);
110
+
111
+ INVARIANT (results.has_value (), " generic component type not found" );
112
+ return generic_reference.generic_type_variables ()[*results];
113
+ }
114
+ else if (parameter_type.id () == ID_pointer)
115
+ {
116
+ if (is_java_generic_type (parameter_type))
117
+ {
118
+ const java_generic_typet &generic_type =
119
+ to_java_generic_type (parameter_type);
120
+
121
+ java_generic_typet::generic_type_variablest replaced_type_variables;
122
+
123
+ // Swap each parameter
124
+ std::transform (
125
+ generic_type.generic_type_variables ().begin (),
126
+ generic_type.generic_type_variables ().end (),
127
+ std::back_inserter (replaced_type_variables),
128
+ [&](const java_generic_parametert &generic_param)
129
+ -> java_generic_parametert {
130
+ const typet &replacement_type =
131
+ substitute_type (generic_param, generic_class, generic_reference);
132
+
133
+ // This code will be simplified when references aren't considered to
134
+ // be generic parameters
135
+ if (is_java_generic_parameter (replacement_type))
136
+ {
137
+ return to_java_generic_parameter (replacement_type);
138
+ }
139
+ else
140
+ {
141
+ INVARIANT (
142
+ is_reference (replacement_type),
143
+ " All generic parameters should be references" );
144
+ return java_generic_inst_parametert (
145
+ to_symbol_type (replacement_type.subtype ()));
146
+ }
147
+ });
148
+
149
+ java_generic_typet new_type = generic_type;
150
+ new_type.generic_type_variables () = replaced_type_variables;
151
+ return new_type;
152
+ }
153
+ else if (parameter_type.subtype ().id () == ID_symbol)
154
+ {
155
+ const symbol_typet &array_subtype =
156
+ to_symbol_type (parameter_type.subtype ());
157
+ if (is_java_array_tag (array_subtype.get_identifier ()))
158
+ {
159
+ const typet &array_element_type =
160
+ java_array_element_type (array_subtype);
161
+
162
+ const typet &new_array_type =
163
+ substitute_type (array_element_type, generic_class, generic_reference);
164
+
165
+ typet replacement_array_type = java_array_type (' a' );
166
+ replacement_array_type.subtype ().set (ID_C_element_type, new_array_type);
167
+ return replacement_array_type;
168
+ }
169
+ }
170
+ }
171
+ return parameter_type;
172
+ }
173
+
101
174
// / Build a unique tag for the generic to be instantiated.
102
175
// / \param existing_generic_type The type we want to concretise
103
176
// / \param original_class
0 commit comments