Skip to content

Commit c31abd0

Browse files
author
Owen
committed
Make convert_java_nondet more general
1 parent 0c20014 commit c31abd0

File tree

2 files changed

+157
-67
lines changed

2 files changed

+157
-67
lines changed

‎jbmc/src/java_bytecode/convert_java_nondet.cpp

Lines changed: 71 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -39,71 +39,83 @@ static goto_programt::targett insert_nondet_init_code(
3939
object_factory_parameterst object_factory_parameters,
4040
const irep_idt &mode)
4141
{
42-
// Return if the instruction isn't an assignment
43-
const auto next_instr=std::next(target);
44-
if(!target->is_assign())
45-
{
46-
return next_instr;
47-
}
42+
const auto next_instr = std::next(target);
4843

49-
// Return if the rhs of the assignment isn't a side effect expression
50-
const auto &assign=to_code_assign(target->code);
51-
if(assign.rhs().id()!=ID_side_effect)
44+
// We only expect to find nondets in the rhs of an assignments or in return
45+
// statements
46+
for(exprt &op : target->code.operands())
5247
{
53-
return next_instr;
54-
}
48+
if(op.id() != ID_side_effect)
49+
{
50+
continue;
51+
}
5552

56-
// Return if the rhs isn't nondet
57-
const auto &side_effect=to_side_effect_expr(assign.rhs());
58-
if(side_effect.get_statement()!=ID_nondet)
59-
{
60-
return next_instr;
61-
}
53+
const auto &side_effect = to_side_effect_expr(op);
54+
if(side_effect.get_statement() != ID_nondet)
55+
{
56+
continue;
57+
}
6258

63-
const auto lhs=assign.lhs();
64-
// If the lhs type doesn't have a subtype then I guess it's primitive and
65-
// we want to bail out now
66-
if(!lhs.type().has_subtype())
67-
{
68-
return next_instr;
69-
}
59+
const typet &type = side_effect.type();
60+
// If the lhs type doesn't have a subtype then I guess it's primitive and
61+
// we want to bail out now
62+
if(!(type.id() == ID_pointer && type.has_subtype()))
63+
{
64+
continue;
65+
}
7066

71-
// Although, if the type is a ptr-to-void then we also want to bail
72-
if(lhs.type().subtype().id()==ID_empty ||
73-
lhs.type().subtype().id()==ID_code)
74-
{
75-
return next_instr;
76-
}
67+
// Although, if the type is a ptr-to-void then we also want to bail
68+
if(type.subtype().id() == ID_empty || type.subtype().id() == ID_code)
69+
{
70+
continue;
71+
}
7772

78-
// Check whether the nondet object may be null
79-
if(!to_side_effect_expr_nondet(side_effect).get_nullable())
80-
object_factory_parameters.max_nonnull_tree_depth = 1;
81-
// Get the symbol to nondet-init
82-
const auto source_loc=target->source_location;
83-
84-
// Erase the nondet assignment
85-
target->make_skip();
86-
87-
// Generate nondet init code
88-
code_blockt init_code;
89-
gen_nondet_init(
90-
lhs,
91-
init_code,
92-
symbol_table,
93-
source_loc,
94-
true,
95-
allocation_typet::DYNAMIC,
96-
object_factory_parameters,
97-
update_in_placet::NO_UPDATE_IN_PLACE);
98-
99-
// Convert this code into goto instructions
100-
goto_programt new_instructions;
101-
goto_convert(
102-
init_code, symbol_table, new_instructions, message_handler, mode);
103-
104-
// Insert the new instructions into the instruction list
105-
goto_program.destructive_insert(next_instr, new_instructions);
106-
goto_program.update();
73+
// Check whether the nondet object may be null
74+
if(!to_side_effect_expr_nondet(side_effect).get_nullable())
75+
object_factory_parameters.max_nonnull_tree_depth = 1;
76+
// Get the symbol to nondet-init
77+
const auto source_loc = target->source_location;
78+
79+
// Create aux symbol for nondet object
80+
symbolt &aux_symbol = get_fresh_aux_symbol(
81+
type,
82+
id2string(goto_programt::get_function_id(goto_program)),
83+
"nondet_tmp",
84+
source_loc,
85+
ID_java,
86+
symbol_table);
87+
aux_symbol.is_static_lifetime = false;
88+
89+
const symbol_exprt aux_symbol_expr = aux_symbol.symbol_expr();
90+
code_declt decl(aux_symbol_expr);
91+
decl.add_source_location() = source_loc;
92+
93+
// Generate nondet init code
94+
code_blockt init_code;
95+
init_code.add(decl);
96+
97+
gen_nondet_init(
98+
aux_symbol_expr,
99+
init_code,
100+
symbol_table,
101+
source_loc,
102+
true,
103+
allocation_typet::DYNAMIC,
104+
object_factory_parameters,
105+
update_in_placet::NO_UPDATE_IN_PLACE);
106+
107+
// Convert this code into goto instructions
108+
goto_programt new_instructions;
109+
goto_convert(
110+
init_code, symbol_table, new_instructions, message_handler, mode);
111+
112+
// Insert the new instructions into the instruction list before target
113+
goto_program.destructive_insert(target, new_instructions);
114+
goto_program.update();
115+
116+
// Replace op with aux symbol
117+
op = aux_symbol_expr;
118+
}
107119

108120
return next_instr;
109121
}

‎jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

Lines changed: 86 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@
1515
#include <goto-programs/remove_virtual_functions.h>
1616
#include <goto-programs/remove_returns.h>
1717

18+
#include <java_bytecode/convert_java_nondet.h>
19+
#include <java_bytecode/object_factory_parameters.h>
1820
#include <java_bytecode/remove_instanceof.h>
1921
#include <java_bytecode/replace_java_nondet.h>
2022

@@ -26,7 +28,7 @@
2628
#include <iostream>
2729
#include <java-testing-utils/load_java_class.h>
2830

29-
void validate_method_removal(
31+
void validate_nondet_method_removed(
3032
std::list<goto_programt::instructiont> instructions)
3133
{
3234
bool method_removed = true, replacement_nondet_exists = false;
@@ -90,6 +92,38 @@ void validate_method_removal(
9092
REQUIRE(replacement_nondet_exists);
9193
}
9294

95+
void validate_nondets_converted(
96+
std::list<goto_programt::instructiont> instructions)
97+
{
98+
bool nondetExists = false, allocateExists = false;
99+
for(const auto &inst : instructions)
100+
{
101+
// Check that our NONDET(<type>) exists on a rhs somewhere.
102+
exprt target_expression =
103+
(inst.is_assign()
104+
? to_code_assign(inst.code).rhs()
105+
: inst.is_return() ? to_code_return(inst.code).return_value()
106+
: inst.code);
107+
108+
if(target_expression.id() == ID_side_effect)
109+
{
110+
auto side_effect = to_side_effect_expr(target_expression);
111+
if(side_effect.get_statement() == ID_nondet)
112+
{
113+
nondetExists = true;
114+
}
115+
116+
if(side_effect.get_statement() == ID_allocate)
117+
{
118+
allocateExists = true;
119+
}
120+
}
121+
}
122+
123+
REQUIRE(!nondetExists);
124+
REQUIRE(allocateExists);
125+
}
126+
93127
void load_and_test_method(
94128
const std::string &method_signature,
95129
goto_functionst &functions,
@@ -110,26 +144,70 @@ void load_and_test_method(
110144
remove_virtual_functions(model_function);
111145

112146
// Then test both situations.
113-
THEN(
114-
"Code should work when remove returns is called before "
115-
"replace_java_nondet.")
147+
THEN("Replace nondet should work when remove returns has been called.")
148+
{
149+
remove_returns(model_function, [](const irep_idt &) { return false; });
150+
151+
replace_java_nondet(model_function);
152+
153+
validate_nondet_method_removed(goto_function.body.instructions);
154+
}
155+
156+
THEN("Replace nondet should work when remove returns hasn't been called.")
116157
{
158+
replace_java_nondet(model_function);
159+
117160
remove_returns(model_function, [](const irep_idt &) { return false; });
118161

162+
validate_nondet_method_removed(goto_function.body.instructions);
163+
}
164+
165+
object_factory_parameterst params{};
166+
167+
THEN(
168+
"Replace and convert nondet should work when remove returns has been "
169+
"called.")
170+
{
119171
replace_java_nondet(model_function);
120172

121-
validate_method_removal(goto_function.body.instructions);
173+
convert_nondet(model_function, null_message_handler, params, ID_java);
174+
175+
remove_returns(model_function, [](const irep_idt &) { return false; });
176+
177+
std::string output = "";
178+
for(auto instruction : model_function.get_goto_function().body.instructions)
179+
{
180+
output += instruction.code.pretty(0, 0) + "\n\n\n";
181+
}
182+
183+
std::stringstream out;
184+
goto_function.body.output(namespacet(symbol_table), "", out);
185+
std::string res = out.str();
186+
187+
validate_nondets_converted(goto_function.body.instructions);
122188
}
123189

124190
THEN(
125-
"Code should work when remove returns is called after "
126-
"replace_java_nondet.")
191+
"Replace and convert nondet should work when remove returns hasn't been "
192+
"called.")
127193
{
128194
replace_java_nondet(model_function);
129195

196+
convert_nondet(model_function, null_message_handler, params, ID_java);
197+
130198
remove_returns(model_function, [](const irep_idt &) { return false; });
131199

132-
validate_method_removal(goto_function.body.instructions);
200+
std::string output = "";
201+
for(auto instruction : model_function.get_goto_function().body.instructions)
202+
{
203+
output += instruction.code.pretty(0, 0) + "\n\n\n";
204+
}
205+
206+
std::stringstream out;
207+
goto_function.body.output(namespacet(symbol_table), "", out);
208+
std::string res = out.str();
209+
210+
validate_nondets_converted(goto_function.body.instructions);
133211
}
134212
}
135213

0 commit comments

Comments
 (0)