Skip to content

Commit 3d39655

Browse files
author
Owen Jones
committed
Try 4
Respond to review comments
1 parent 1b7cfe9 commit 3d39655

File tree

2 files changed

+69
-53
lines changed

2 files changed

+69
-53
lines changed

‎jbmc/src/java_bytecode/convert_java_nondet.cpp‎

Lines changed: 63 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,47 @@ Author: Reuben Thomas, [email protected]
2222

2323
#include "java_object_factory.h" // gen_nondet_init
2424

25+
/// Return whether `expr` is a nondet pointer that we should convert
26+
static bool is_nondet_pointer(exprt expr)
27+
{
28+
// If the expression type doesn't have a subtype then I guess it's primitive
29+
// and we do not want to convert it. If the type is a ptr-to-void or a
30+
// function pointer then we also do not want to convert it.
31+
const typet &type = expr.type();
32+
const bool non_void_non_function_pointer = type.id() == ID_pointer &&
33+
type.subtype().id() != ID_empty &&
34+
type.subtype().id() != ID_code;
35+
return can_cast_expr<side_effect_expr_nondett>(expr) &&
36+
non_void_non_function_pointer;
37+
}
38+
39+
/// Populate `instructions` with goto instructions to nondet init
40+
/// `aux_symbol_expr`
41+
static void get_gen_nondet_init_instructions(
42+
goto_programt &instructions,
43+
const symbol_exprt &aux_symbol_expr,
44+
const source_locationt &source_loc,
45+
symbol_table_baset &symbol_table,
46+
message_handlert &message_handler,
47+
const object_factory_parameterst &object_factory_parameters,
48+
const irep_idt &mode)
49+
{
50+
code_blockt gen_nondet_init_code;
51+
const bool skip_classid = true;
52+
gen_nondet_init(
53+
aux_symbol_expr,
54+
gen_nondet_init_code,
55+
symbol_table,
56+
source_loc,
57+
skip_classid,
58+
allocation_typet::DYNAMIC,
59+
object_factory_parameters,
60+
update_in_placet::NO_UPDATE_IN_PLACE);
61+
62+
goto_convert(
63+
gen_nondet_init_code, symbol_table, instructions, message_handler, mode);
64+
}
65+
2566
/// Checks an instruction to see whether it contains an assignment from
2667
/// side_effect_expr_nondet. If so, replaces the instruction with a range of
2768
/// instructions to properly nondet-initialize the lhs.
@@ -44,94 +85,70 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
4485
{
4586
const auto next_instr = std::next(target);
4687

47-
// We only expect to find nondets in the rhs of an assignments or in return
48-
// statements
88+
// We only expect to find nondets in the rhs of an assignments, and in return
89+
// statements if remove_returns has not been run, but we do a more general
90+
// check on all operands in case this changes
4991
for(exprt &op : target->code.operands())
5092
{
51-
if(!can_cast_expr<side_effect_expr_nondett>(op))
93+
if(!is_nondet_pointer(op))
5294
{
5395
continue;
5496
}
5597

56-
const auto &nondet_expr = to_side_effect_expr_nondet(op);
57-
58-
// If the lhs type doesn't have a subtype then I guess it's primitive and
59-
// we want to bail out now. If the type is a ptr-to-void or a function
60-
// pointer then we also want to bail.
61-
const typet &type = nondet_expr.type();
62-
if(
63-
type.id() != ID_pointer || type.subtype().id() == ID_empty ||
64-
type.subtype().id() == ID_code)
65-
{
66-
continue;
67-
}
98+
const auto &nondet_expr = to_side_effect_expr_nondet(op);
6899

69100
if(!nondet_expr.get_nullable())
70101
object_factory_parameters.max_nonnull_tree_depth = 1;
71102

72-
const auto source_loc = target->source_location;
103+
const source_locationt &source_loc = target->source_location;
73104

74105
// Currently the code looks like this
75-
// target: original instruction
106+
// target: instruction containing op
76107
// When we are done it will look like this
77108
// target : declare aux_symbol
78109
// . <gen_nondet_init_instructions - many lines>
79110
// . <gen_nondet_init_instructions - many lines>
80111
// . <gen_nondet_init_instructions - many lines>
81-
// target2: orig instruction with op replaced by aux_symbol
112+
// target2: instruction containing op, with op replaced by aux_symbol
82113
// dead aux_symbol
83114

84115
symbolt &aux_symbol = get_fresh_aux_symbol(
85-
type,
116+
op.type(),
86117
id2string(goto_programt::get_function_id(goto_program)),
87118
"nondet_tmp",
88119
source_loc,
89120
ID_java,
90121
symbol_table);
91-
aux_symbol.is_static_lifetime = false;
92122

93123
const symbol_exprt aux_symbol_expr = aux_symbol.symbol_expr();
94124
op = aux_symbol_expr;
95125

96-
// It is simplest to insert the final instruction first, before everything
97-
// gets moved around
98-
goto_programt::targett dead_aux_symbol = goto_program.insert_after(target);
99-
dead_aux_symbol->type = DEAD;
100-
dead_aux_symbol->code = code_deadt(aux_symbol_expr);
101-
dead_aux_symbol->source_location = source_loc;
102-
103126
// Insert an instruction declaring `aux_symbol` before `target`, being
104127
// careful to preserve jumps to `target`
105-
goto_programt::instructiont decl_aux_symbol(DECL);
106-
decl_aux_symbol.code = code_declt(aux_symbol_expr);
128+
goto_programt::instructiont decl_aux_symbol;
129+
decl_aux_symbol.make_decl(code_declt(aux_symbol_expr));
107130
decl_aux_symbol.source_location = source_loc;
108131
goto_program.insert_before_swap(target, decl_aux_symbol);
109132

110-
// Keep track of the new location of the original instruction.
133+
// Keep track of the new location of the instruction containing op.
111134
const goto_programt::targett target2 = std::next(target);
112135

113-
code_blockt gen_nondet_init_code;
114-
const bool skip_classid = true;
115-
gen_nondet_init(
136+
goto_programt gen_nondet_init_instructions;
137+
get_gen_nondet_init_instructions(
138+
gen_nondet_init_instructions,
116139
aux_symbol_expr,
117-
gen_nondet_init_code,
118-
symbol_table,
119140
source_loc,
120-
skip_classid,
121-
allocation_typet::DYNAMIC,
122-
object_factory_parameters,
123-
update_in_placet::NO_UPDATE_IN_PLACE);
124-
125-
goto_programt gen_nondet_init_instructions;
126-
goto_convert(
127-
gen_nondet_init_code,
128141
symbol_table,
129-
gen_nondet_init_instructions,
130142
message_handler,
143+
object_factory_parameters,
131144
mode);
132-
133145
goto_program.destructive_insert(target2, gen_nondet_init_instructions);
134146

147+
goto_programt::targett dead_aux_symbol = goto_program.insert_after(target2);
148+
dead_aux_symbol->make_dead();
149+
dead_aux_symbol->code = code_deadt(aux_symbol_expr);
150+
dead_aux_symbol->source_location = source_loc;
151+
135152
// In theory target could have more than one operand which should be
136153
// replaced by convert_nondet, so we return target2 so that it
137154
// will be checked again
@@ -159,9 +176,8 @@ void convert_nondet(
159176
{
160177
bool changed = false;
161178
auto instruction_iterator = goto_program.instructions.begin();
162-
auto end = goto_program.instructions.end();
163179

164-
while(instruction_iterator != end)
180+
while(instruction_iterator != goto_program.instructions.end())
165181
{
166182
auto ret = insert_nondet_init_code(
167183
goto_program,

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -106,15 +106,16 @@ void validate_nondets_converted(
106106
: inst.is_return() ? to_code_return(inst.code).return_value()
107107
: inst.code);
108108

109-
if(target_expression.id() == ID_side_effect)
109+
if(
110+
const auto side_effect =
111+
expr_try_dynamic_cast<side_effect_exprt>(target_expression))
110112
{
111-
auto side_effect = to_side_effect_expr(target_expression);
112-
if(side_effect.get_statement() == ID_nondet)
113+
if(side_effect->get_statement() == ID_nondet)
113114
{
114115
nondet_exists = true;
115116
}
116117

117-
if(side_effect.get_statement() == ID_allocate)
118+
if(side_effect->get_statement() == ID_allocate)
118119
{
119120
allocate_exists = true;
120121
}
@@ -124,8 +125,7 @@ void validate_nondets_converted(
124125
REQUIRE_FALSE(nondet_exists);
125126
REQUIRE(allocate_exists);
126127
}
127-
#include<iostream>
128-
#include<cout_message.h>
128+
129129
void load_and_test_method(
130130
const std::string &method_signature,
131131
goto_functionst &functions,

0 commit comments

Comments
 (0)