Skip to content

Commit 93970f2

Browse files
author
Matthias Güdemann
committed
Add unit test for mutually recursive generic parameters
1 parent 3bb3be5 commit 93970f2

File tree

5 files changed

+158
-0
lines changed

5 files changed

+158
-0
lines changed

‎jbmc/unit/Makefile

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

3637
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

465 Bytes
Binary file not shown.

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
class KeyValue<K, V> {
2+
KeyValue<K, V> next;
3+
KeyValue<V, K> reverse;
4+
K key;
5+
V value;
6+
}
7+
class MutuallyRecursiveGenerics {
8+
KeyValue<String, Integer> example1;
9+
void f() {
10+
}
11+
}

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

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,146 @@
1+
/*******************************************************************\
2+
3+
Module: Unit tests for parsing mutually generic classes
4+
5+
Author: Diffblue Ltd.
6+
7+
\*******************************************************************/
8+
#include <iostream>
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_programs_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+
}
146+
}

0 commit comments

Comments
 (0)