Skip to content

Commit 28b633c

Browse files
romainbrenguierromainbrenguier
committed
Add unit test for assign_from_json
This in particular check that an array field (which is not marked nondet and not a reference) is allocated with a constant size.
1 parent 204da89 commit 28b633c

File tree

2 files changed

+272
-0
lines changed

2 files changed

+272
-0
lines changed

‎jbmc/unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
4848
java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
4949
java_bytecode/java_object_factory/struct_tag_types.cpp \
5050
java_bytecode/java_replace_nondet/replace_nondet.cpp \
51+
java_bytecode/java_static_initializers/assignments_from_json.cpp \
5152
java_bytecode/java_static_initializers/java_static_initializers.cpp \
5253
java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
5354
java_bytecode/java_trace_validation/java_trace_validation.cpp \

‎jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp

Lines changed: 271 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,271 @@
1+
/*******************************************************************\
2+
3+
Module: Unit tests for assign_from_json
4+
5+
Author: Romain Brenguier, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include <java_bytecode/assignments_from_json.h>
10+
11+
#include <java_bytecode/ci_lazy_methods_needed.h>
12+
#include <java_bytecode/java_bytecode_convert_class.h>
13+
#include <java_bytecode/java_types.h>
14+
#include <java_bytecode/java_utils.h>
15+
#include <testing-utils/expr_query.h>
16+
#include <testing-utils/use_catch.h>
17+
#include <util/arith_tools.h>
18+
#include <util/json.h>
19+
#include <util/symbol_table.h>
20+
21+
/// Add `clinit` function symbol to the table
22+
/// \return its identifier in the symbol table
23+
static irep_idt
24+
add_clinit(symbol_tablet &symbol_table, const std::string &class_name)
25+
{
26+
symbolt clinit_symbol;
27+
clinit_symbol.name = "java::" + class_name + ".<clinit>:()V";
28+
set_declaring_class(clinit_symbol, "java::" + class_name);
29+
symbol_table.insert(clinit_symbol);
30+
return clinit_symbol.name;
31+
}
32+
33+
static void add_class_with_components(
34+
symbol_tablet &symbol_table,
35+
const std::string &class_name,
36+
const std::vector<std::pair<std::string, typet>> &components)
37+
{
38+
symbolt test_class_symbol;
39+
test_class_symbol.name = "java::" + class_name;
40+
test_class_symbol.is_type = true;
41+
test_class_symbol.type = [&] {
42+
java_class_typet type;
43+
// TODO java_class_typet constructors should ensure there is always a
44+
// @class_identifier field, and that name is always set
45+
type.set_name("java::" + class_name);
46+
for(const auto &pair : components)
47+
type.components().emplace_back(pair.first, pair.second);
48+
return type;
49+
}();
50+
symbol_table.insert(test_class_symbol);
51+
}
52+
53+
#include <iostream>
54+
55+
SCENARIO(
56+
"assign_from_json",
57+
"[core][java_static_initializers][assign_from_json]")
58+
{
59+
symbol_tablet symbol_table;
60+
const std::size_t max_user_array_length = 100;
61+
std::unordered_map<std::string, object_creation_referencet> references;
62+
std::unordered_multimap<irep_idt, symbolt> class_to_declared_symbols;
63+
64+
GIVEN("A class which has a static number in the provided JSON")
65+
{
66+
const json_objectt json = [] {
67+
json_objectt entry{};
68+
entry["field_name"] = [] {
69+
json_objectt int_json;
70+
int_json["value"] = json_numbert{"42"};
71+
int_json["@type"] = json_stringt{"int"};
72+
return int_json;
73+
}();
74+
entry["@type"] = json_stringt{"TestClass"};
75+
return entry;
76+
}();
77+
class_to_declared_symbols.emplace("java::TestClass", [] {
78+
symbolt field_symbol;
79+
field_symbol.base_name = "field_name";
80+
field_symbol.name = "field_name_for_codet";
81+
field_symbol.type = java_int_type();
82+
field_symbol.is_static_lifetime = true;
83+
return field_symbol;
84+
}());
85+
add_clinit(symbol_table, "TestClass");
86+
add_class_with_components(
87+
symbol_table,
88+
"TestClass",
89+
{std::pair<std::string, typet>("@class_identifier", string_typet{}),
90+
std::pair<std::string, typet>("field_name", java_int_type())});
91+
92+
const reference_typet test_class_type =
93+
reference_type(struct_tag_typet{"java::TestClass"});
94+
code_blockt block;
95+
optionalt<ci_lazy_methods_neededt> option{};
96+
assign_from_json(
97+
symbol_exprt{"symbol_to_assign", test_class_type},
98+
json,
99+
"java::TestClass.<clinit>:()V",
100+
block,
101+
symbol_table,
102+
option,
103+
max_user_array_length,
104+
references);
105+
THEN(
106+
"The first instruction is the declaration of a symbol of TestClass* type")
107+
{
108+
const symbol_exprt declared_symbol =
109+
make_query(block)[0].as<code_declt>()[0].as<symbol_exprt>().get();
110+
REQUIRE(declared_symbol.type() == test_class_type);
111+
THEN("The second instruction allocates the symbol")
112+
{
113+
REQUIRE(
114+
make_query(block)[1].as<code_assignt>()[0].as<symbol_exprt>().get() ==
115+
declared_symbol);
116+
}
117+
}
118+
THEN("The third instruction assigns the symbol to `symbol_to_assign`")
119+
{
120+
REQUIRE(
121+
make_query(block)[2]
122+
.as<code_assignt>()[0]
123+
.as<symbol_exprt>()
124+
.get()
125+
.get_identifier() == "symbol_to_assign");
126+
}
127+
THEN("The fourth instruction zero-initializes the struct")
128+
{
129+
REQUIRE(
130+
make_query(block)[3].as<code_assignt>()[1].get().type() ==
131+
test_class_type.subtype());
132+
}
133+
THEN("The fifth instruction assigns the field to 42")
134+
{
135+
REQUIRE(
136+
make_query(block)[4]
137+
.as<code_assignt>()[0]
138+
.as<member_exprt>()
139+
.get()
140+
.get_component_name() == "field_name");
141+
REQUIRE(
142+
numeric_cast_v<mp_integer>(make_query(block)[4]
143+
.as<code_assignt>()[1]
144+
.as<constant_exprt>()
145+
.get()) == 42);
146+
}
147+
}
148+
149+
GIVEN("A class with an array field")
150+
{
151+
const json_objectt json = [] {
152+
json_objectt entry{};
153+
entry["array_field"] = [] {
154+
json_objectt int_json;
155+
int_json["@items"] = json_arrayt{json_numbert{"42"}};
156+
int_json["@type"] = json_stringt{"[I"};
157+
return int_json;
158+
}();
159+
entry["@type"] = json_stringt{"TestClass"};
160+
return entry;
161+
}();
162+
class_to_declared_symbols.emplace("java::TestClass", [] {
163+
symbolt field_symbol;
164+
field_symbol.base_name = "array_field";
165+
field_symbol.name = "field_name_for_codet";
166+
field_symbol.type = java_int_type();
167+
field_symbol.is_static_lifetime = true;
168+
return field_symbol;
169+
}());
170+
const irep_idt clinit_name = add_clinit(symbol_table, "TestClass");
171+
add_class_with_components(
172+
symbol_table,
173+
"TestClass",
174+
{std::pair<std::string, typet>("@class_identifier", string_typet{}),
175+
std::pair<std::string, typet>("array_field", java_array_type('i'))});
176+
// For array[int]
177+
add_java_array_types(symbol_table);
178+
179+
const reference_typet test_class_type =
180+
reference_type(struct_tag_typet{"java::TestClass"});
181+
code_blockt block;
182+
optionalt<ci_lazy_methods_neededt> option{};
183+
assign_from_json(
184+
symbol_exprt{"symbol_to_assign", test_class_type},
185+
json,
186+
clinit_name,
187+
block,
188+
symbol_table,
189+
option,
190+
max_user_array_length,
191+
references);
192+
193+
THEN(
194+
"The first instruction is the declaration of a symbol of TestClass* type")
195+
{
196+
const symbol_exprt allocation_symbol =
197+
make_query(block)[0].as<code_declt>()[0].as<symbol_exprt>().get();
198+
REQUIRE(allocation_symbol.type() == test_class_type);
199+
THEN("The second instruction declares the array data")
200+
{
201+
REQUIRE(
202+
make_query(block)[1]
203+
.as<code_declt>()[0]
204+
.as<symbol_exprt>()
205+
.get()
206+
.type() == java_reference_type(java_int_type()));
207+
}
208+
THEN("The third instruction allocates the struct")
209+
{
210+
REQUIRE(
211+
make_query(block)[2].as<code_assignt>()[0].as<symbol_exprt>().get() ==
212+
allocation_symbol);
213+
}
214+
}
215+
THEN("The fourth instruction assigns the symbol to \"symbol_to_assign\"")
216+
{
217+
REQUIRE(
218+
make_query(block)[3]
219+
.as<code_assignt>()[0]
220+
.as<symbol_exprt>()
221+
.get()
222+
.get_identifier() == "symbol_to_assign");
223+
}
224+
225+
THEN("The fifth instruction zero-initializes the struct")
226+
{
227+
REQUIRE(
228+
make_query(block)[4].as<code_assignt>()[0].get().type() ==
229+
test_class_type.subtype());
230+
}
231+
THEN(
232+
"The sixth instruction allocates the array field, with a size of "
233+
"exactly 1")
234+
{
235+
REQUIRE(
236+
make_query(block)[5]
237+
.as<code_assignt>()[0]
238+
.as<member_exprt>()
239+
.get()
240+
.get_component_name() == "array_field");
241+
auto side_effect = make_query(block)[5]
242+
.as<code_assignt>()[1]
243+
.as<side_effect_exprt>()
244+
.get();
245+
REQUIRE(side_effect.get_statement() == ID_java_new_array);
246+
REQUIRE(
247+
numeric_cast_v<mp_integer>(
248+
make_query(side_effect)[0].as<constant_exprt>().get()) == 1);
249+
}
250+
THEN(
251+
"The seventh instruction copies the data to "
252+
"user_specified_array_data_init")
253+
{
254+
REQUIRE(
255+
make_query(block)[6]
256+
.as<code_assignt>()[0]
257+
.as<symbol_exprt>()
258+
.get()
259+
.get_identifier() ==
260+
"java::TestClass.<clinit>:()V::user_specified_array_data_init");
261+
}
262+
THEN("The eighth instruction assigns the array cell to 42")
263+
{
264+
REQUIRE(
265+
numeric_cast_v<mp_integer>(make_query(block)[7]
266+
.as<code_assignt>()[1]
267+
.as<constant_exprt>()
268+
.get()) == 42);
269+
}
270+
}
271+
}

0 commit comments

Comments
 (0)