Skip to content

Commit 26e5433

Browse files
author
Matthias Güdemann
committed
Add unit test for mutually recursive generic parameters
1 parent 6ff2993 commit 26e5433

8 files changed

+308
-0
lines changed

‎jbmc/unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
3232
util/simplify_expr.cpp \
3333
java_bytecode/java_virtual_functions/virtual_functions.cpp \
3434
java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \
35+
java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \
3536
# Empty last line
3637

3738
INCLUDES= -I ../src/ -I. -I $(CPROVER_DIR)/src -I $(CPROVER_DIR)/unit

‎jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class

562 Bytes
Binary file not shown.

‎jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class

671 Bytes
Binary file not shown.

‎jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
class Outer<K, V, U> {
2+
class Inner<U> {
3+
Outer<V, K, U> o;
4+
U u;
5+
}
6+
Inner<U> inner;
7+
K key;
8+
V value;
9+
}
10+
class Three<X, E, U> {
11+
Three<U, X, E> rotate;
12+
Three<X, E, U> normal;
13+
X x;
14+
E e;
15+
U u;
16+
}
17+
class KeyValue<K, V> {
18+
KeyValue<K, V> next;
19+
KeyValue<V, K> reverse;
20+
K key;
21+
V value;
22+
}
23+
class MutuallyRecursiveGenerics {
24+
KeyValue<String, Integer> example1;
25+
Three<Byte, Character, Integer> example2;
26+
Outer<Boolean, Byte, Short> example3;
27+
void f() {
28+
}
29+
}

‎jbmc/unit/java_bytecode/goto_program_generics/Outer$Inner.class

613 Bytes
Binary file not shown.

‎jbmc/unit/java_bytecode/goto_program_generics/Outer.class

634 Bytes
Binary file not shown.

‎jbmc/unit/java_bytecode/goto_program_generics/Three.class

597 Bytes
Binary file not shown.

‎jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp

Lines changed: 278 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,278 @@
1+
/*******************************************************************\
2+
3+
Module: Unit tests for parsing mutually generic classes
4+
5+
Author: Diffblue Ltd.
6+
7+
\*******************************************************************/
8+
9+
#include <java-testing-utils/load_java_class.h>
10+
#include <java-testing-utils/require_goto_statements.h>
11+
#include <java-testing-utils/require_type.h>
12+
#include <testing-utils/catch.hpp>
13+
14+
SCENARIO(
15+
"Generics class with mutually recursive_generic parameters",
16+
"[core][java_bytecode][goto_programs_generics]")
17+
{
18+
const symbol_tablet &symbol_table = load_java_class(
19+
"MutuallyRecursiveGenerics",
20+
"./java_bytecode/goto_program_generics",
21+
"MutuallyRecursiveGenerics.f");
22+
23+
std::string class_prefix = "java::MutuallyRecursiveGenerics";
24+
25+
REQUIRE(symbol_table.has_symbol(class_prefix));
26+
27+
WHEN(
28+
"parsing class which has generic type parameters and two field with those"
29+
"parameters in use")
30+
{
31+
const auto &root = symbol_table.lookup_ref(class_prefix);
32+
const typet &type = root.type;
33+
REQUIRE(type.id() == ID_struct);
34+
35+
// needs an `example1` local variable ...
36+
const struct_union_typet::componentt &example1 =
37+
require_type::require_component(to_struct_type(type), "example1");
38+
39+
// ... which is generic and has two explicit generic parameter
40+
// instantiations, String and Integer ...
41+
const java_generic_typet &gen_type =
42+
require_type::require_java_generic_type(
43+
example1.type(),
44+
{{require_type::type_argument_kindt::Inst, "java::java.lang.String"},
45+
{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}});
46+
47+
// ... which is of type `KeyValue` ...
48+
const auto &subtype = gen_type.subtype();
49+
const auto &key_value =
50+
symbol_table.lookup_ref(to_symbol_type(subtype).get_identifier());
51+
REQUIRE(key_value.type.id() == ID_struct);
52+
REQUIRE(key_value.name == "java::KeyValue");
53+
54+
// ... and contains two local variables of type `KeyValue` ...
55+
const auto &next =
56+
require_type::require_component(to_struct_type(key_value.type), "next");
57+
const auto &reverse = require_type::require_component(
58+
to_struct_type(key_value.type), "reverse");
59+
60+
// ... where `next` has the same generic parameter instantiations ...
61+
const java_generic_typet &next_type =
62+
require_type::require_java_generic_type(
63+
next.type(),
64+
{{require_type::type_argument_kindt::Var, "java::KeyValue::K"},
65+
{require_type::type_argument_kindt::Var, "java::KeyValue::V"}});
66+
REQUIRE(next_type.subtype().id() == ID_symbol);
67+
const symbol_typet &next_symbol = to_symbol_type(next_type.subtype());
68+
REQUIRE(
69+
symbol_table.lookup_ref(next_symbol.get_identifier()).name ==
70+
"java::KeyValue");
71+
72+
// ... and `reverse` has the same but in reversed order
73+
const java_generic_typet &reverse_type =
74+
require_type::require_java_generic_type(
75+
reverse.type(),
76+
{{require_type::type_argument_kindt::Var, "java::KeyValue::V"},
77+
{require_type::type_argument_kindt::Var, "java::KeyValue::K"}});
78+
REQUIRE(next_type.subtype().id() == ID_symbol);
79+
const symbol_typet &reverse_symbol = to_symbol_type(reverse_type.subtype());
80+
REQUIRE(
81+
symbol_table.lookup_ref(next_symbol.get_identifier()).name ==
82+
"java::KeyValue");
83+
}
84+
WHEN("The class of type `MutuallyRecursiveGenerics` is created")
85+
{
86+
const std::vector<codet> &entry_point_code =
87+
require_goto_statements::require_entry_point_statements(symbol_table);
88+
89+
auto has_key_and_value_field = [&](
90+
const irep_idt &field,
91+
const irep_idt &key_type,
92+
const irep_idt &val_type) {
93+
require_goto_statements::require_struct_component_assignment(
94+
field, {}, "key", key_type, {}, entry_point_code);
95+
require_goto_statements::require_struct_component_assignment(
96+
field, {}, "value", val_type, {}, entry_point_code);
97+
};
98+
99+
const irep_idt &tmp_object_name =
100+
require_goto_statements::require_entry_point_argument_assignment(
101+
"this", entry_point_code);
102+
103+
THEN(
104+
"The Object has a field `example1` of type `KeyValue<String, Integer>`")
105+
{
106+
const auto &example1_field =
107+
require_goto_statements::require_struct_component_assignment(
108+
tmp_object_name,
109+
{},
110+
"example1",
111+
"java::KeyValue",
112+
{},
113+
entry_point_code);
114+
115+
THEN(
116+
"Object 'example1' has field 'key' of type `String` and field `value` "
117+
"of type `Integer`")
118+
{
119+
has_key_and_value_field(
120+
example1_field, "java::java.lang.String", "java::java.lang.Integer");
121+
}
122+
123+
THEN("`example1` has field next")
124+
{
125+
const auto &next_field =
126+
require_goto_statements::require_struct_component_assignment(
127+
example1_field, {}, "next", "java::KeyValue", {}, entry_point_code);
128+
has_key_and_value_field(
129+
next_field, "java::java.lang.String", "java::java.lang.Integer");
130+
}
131+
THEN("`example1` has field `reverse`")
132+
{
133+
const auto &reverse_field =
134+
require_goto_statements::require_struct_component_assignment(
135+
example1_field,
136+
{},
137+
"reverse",
138+
"java::KeyValue",
139+
{},
140+
entry_point_code);
141+
has_key_and_value_field(
142+
reverse_field, "java::java.lang.Integer", "java::java.lang.String");
143+
}
144+
}
145+
THEN(
146+
"The Object has a field `example2` of type `Three<Byte, Character, "
147+
"Integer>`")
148+
{
149+
const auto &example2_field =
150+
require_goto_statements::require_struct_component_assignment(
151+
tmp_object_name, {}, "example2", "java::Three", {}, entry_point_code);
152+
153+
auto has_x_u_e_fields = [&](
154+
const irep_idt &field,
155+
const irep_idt &x_type,
156+
const irep_idt &e_type,
157+
const irep_idt &u_type) {
158+
require_goto_statements::require_struct_component_assignment(
159+
field, {}, "x", x_type, {}, entry_point_code);
160+
require_goto_statements::require_struct_component_assignment(
161+
field, {}, "e", e_type, {}, entry_point_code);
162+
require_goto_statements::require_struct_component_assignment(
163+
field, {}, "u", u_type, {}, entry_point_code);
164+
};
165+
166+
THEN(
167+
"Object 'example2' has field 'x' of type `Byte`, field `u` of type "
168+
"`Character` and a field `e` of type `Integer`.")
169+
{
170+
has_x_u_e_fields(
171+
example2_field,
172+
"java::java.lang.Byte",
173+
"java::java.lang.Character",
174+
"java::java.lang.Integer");
175+
176+
THEN("`example2` has field `rotate`")
177+
{
178+
const auto &rotate_field =
179+
require_goto_statements::require_struct_component_assignment(
180+
example2_field,
181+
{},
182+
"rotate",
183+
"java::Three",
184+
{},
185+
entry_point_code);
186+
has_x_u_e_fields(
187+
rotate_field,
188+
"java::java.lang.Integer",
189+
"java::java.lang.Byte",
190+
"java::java.lang.Character");
191+
192+
THEN("`rotate` has itself a field `rotate` ... ")
193+
{
194+
const auto &rotate_rec_field =
195+
require_goto_statements::require_struct_component_assignment(
196+
rotate_field,
197+
{},
198+
"rotate",
199+
"java::Three",
200+
{},
201+
entry_point_code);
202+
has_x_u_e_fields(
203+
rotate_rec_field,
204+
"java::java.lang.Character",
205+
"java::java.lang.Integer",
206+
"java::java.lang.Byte");
207+
}
208+
THEN("`rotate` has also a field `normal` ... ")
209+
{
210+
const auto &rotate_normal_field =
211+
require_goto_statements::require_struct_component_assignment(
212+
rotate_field,
213+
{},
214+
"normal",
215+
"java::Three",
216+
{},
217+
entry_point_code);
218+
has_x_u_e_fields(
219+
rotate_normal_field,
220+
"java::java.lang.Integer",
221+
"java::java.lang.Byte",
222+
"java::java.lang.Character");
223+
}
224+
}
225+
THEN("`example2` has field `normal`")
226+
{
227+
const auto &normal_field =
228+
require_goto_statements::require_struct_component_assignment(
229+
example2_field,
230+
{},
231+
"normal",
232+
"java::Three",
233+
{},
234+
entry_point_code);
235+
has_x_u_e_fields(
236+
normal_field,
237+
"java::java.lang.Byte",
238+
"java::java.lang.Character",
239+
"java::java.lang.Integer");
240+
THEN("`normal` has itself a field `normal`")
241+
{
242+
const auto &normal_rec_field =
243+
require_goto_statements::require_struct_component_assignment(
244+
example2_field,
245+
{},
246+
"normal",
247+
"java::Three",
248+
{},
249+
entry_point_code);
250+
has_x_u_e_fields(
251+
normal_rec_field,
252+
"java::java.lang.Byte",
253+
"java::java.lang.Character",
254+
"java::java.lang.Integer");
255+
}
256+
THEN("`normal` has also a field `rotate`")
257+
{
258+
const auto &normal_rotate_field =
259+
require_goto_statements::require_struct_component_assignment(
260+
example2_field,
261+
{},
262+
"rotate",
263+
"java::Three",
264+
{},
265+
entry_point_code);
266+
has_x_u_e_fields(
267+
normal_rotate_field,
268+
"java::java.lang.Integer",
269+
"java::java.lang.Byte",
270+
"java::java.lang.Character");
271+
}
272+
}
273+
}
274+
}
275+
}
276+
277+
// TODO: add test for TG-3828
278+
}

0 commit comments

Comments
 (0)