Skip to content

Commit 1ea6f18

Browse files
authored
Merge pull request #5908 from diffblue/code_nonconst
protect instructiont::code
2 parents f28d4f2 + 99afbae commit 1ea6f18

File tree

89 files changed

+316
-302
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

89 files changed

+316
-302
lines changed

jbmc/src/java_bytecode/convert_java_nondet.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,7 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
9393
// We only expect to find nondets in the rhs of an assignments, and in return
9494
// statements if remove_returns has not been run, but we do a more general
9595
// check on all operands in case this changes
96-
for(exprt &op : target->code.operands())
96+
for(exprt &op : target->code_nonconst().operands())
9797
{
9898
if(!is_nondet_pointer(op))
9999
{

jbmc/src/java_bytecode/remove_exceptions.cpp

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -200,8 +200,7 @@ bool remove_exceptionst::function_or_callees_may_throw(
200200

201201
if(instruction.is_function_call())
202202
{
203-
const exprt &function_expr =
204-
to_code_function_call(instruction.code).function();
203+
const exprt &function_expr = instruction.get_function_call().function();
205204
DATA_INVARIANT(
206205
function_expr.id()==ID_symbol,
207206
"identifier expected to be a symbol");
@@ -235,8 +234,8 @@ void remove_exceptionst::instrument_exception_handler(
235234
if(may_catch)
236235
{
237236
// retrieve the exception variable
238-
const exprt &thrown_exception_local=
239-
to_code_landingpad(instr_it->code).catch_expr();
237+
const exprt &thrown_exception_local =
238+
to_code_landingpad(instr_it->get_code()).catch_expr();
240239

241240
const symbol_exprt thrown_global_symbol=
242241
get_inflight_exception_global();
@@ -408,8 +407,8 @@ bool remove_exceptionst::instrument_throw(
408407
{
409408
PRECONDITION(instr_it->type==THROW);
410409

411-
const exprt &exc_expr=
412-
uncaught_exceptions_domaint::get_exception_symbol(instr_it->code);
410+
const exprt &exc_expr =
411+
uncaught_exceptions_domaint::get_exception_symbol(instr_it->get_code());
413412

414413
add_exception_dispatch_sequence(
415414
function_identifier, goto_program, instr_it, stack_catch, locals);
@@ -424,7 +423,7 @@ bool remove_exceptionst::instrument_throw(
424423
typecast_exprt(exc_expr, exc_thrown.type()));
425424
// now turn the `throw' into `assignment'
426425
instr_it->type=ASSIGN;
427-
instr_it->code=assignment;
426+
instr_it->code_nonconst() = assignment;
428427

429428
return true;
430429
}
@@ -518,7 +517,7 @@ void remove_exceptionst::instrument_exceptions(
518517
// Is it a handler push/pop or catch landing-pad?
519518
else if(instr_it->type==CATCH)
520519
{
521-
const irep_idt &statement=instr_it->code.get_statement();
520+
const irep_idt &statement = instr_it->get_code().get_statement();
522521
// Is it an exception landing pad (start of a catch block)?
523522
if(statement==ID_exception_landingpad)
524523
{
@@ -558,8 +557,8 @@ void remove_exceptionst::instrument_exceptions(
558557
stack_catch.back();
559558

560559
// copy targets
561-
const code_push_catcht::exception_listt &exception_list=
562-
to_code_push_catch(instr_it->code).exception_list();
560+
const code_push_catcht::exception_listt &exception_list =
561+
to_code_push_catch(instr_it->get_code()).exception_list();
563562

564563
// The target list can be empty if `finish_catch_push_targets` found that
565564
// the targets were unreachable (in which case no exception can truly

jbmc/src/java_bytecode/remove_instanceof.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -244,8 +244,9 @@ bool remove_instanceoft::lower_instanceof(
244244
goto_programt &goto_program,
245245
goto_programt::targett target)
246246
{
247-
if(target->is_target() &&
248-
(contains_instanceof(target->code) || contains_instanceof(target->guard)))
247+
if(
248+
target->is_target() && (contains_instanceof(target->get_code()) ||
249+
contains_instanceof(target->guard)))
249250
{
250251
// If this is a branch target, add a skip beforehand so we can splice new
251252
// GOTO programs before the target instruction without inserting into the
@@ -257,7 +258,7 @@ bool remove_instanceoft::lower_instanceof(
257258
}
258259

259260
return lower_instanceof(
260-
function_identifier, target->code, goto_program, target) |
261+
function_identifier, target->code_nonconst(), goto_program, target) |
261262
lower_instanceof(
262263
function_identifier, target->guard, goto_program, target);
263264
}

jbmc/src/java_bytecode/replace_java_nondet.cpp

Lines changed: 12 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -88,11 +88,11 @@ is_nondet_returning_object(const code_function_callt &function_call)
8888
static nondet_instruction_infot
8989
get_nondet_instruction_info(const goto_programt::const_targett &instr)
9090
{
91-
if(!(instr->is_function_call() && instr->code.id() == ID_code))
91+
if(!(instr->is_function_call() && instr->get_code().id() == ID_code))
9292
{
9393
return nondet_instruction_infot();
9494
}
95-
const auto &code = instr->code;
95+
const auto &code = instr->get_code();
9696
INVARIANT(
9797
code.get_statement() == ID_function_call,
9898
"function_call should have ID_function_call");
@@ -146,7 +146,7 @@ static bool is_assignment_from(
146146
{
147147
return false;
148148
}
149-
const auto &rhs = to_code_assign(instr.code).rhs();
149+
const auto &rhs = instr.get_assign().rhs();
150150
return is_symbol_with_id(rhs, identifier) ||
151151
is_typecast_with_id(rhs, identifier);
152152
}
@@ -209,14 +209,13 @@ static goto_programt::targett check_and_replace_target(
209209
// If we haven't removed returns yet, our function call will have a variable
210210
// on its left hand side.
211211
const bool remove_returns_not_run =
212-
to_code_function_call(target->code).lhs().is_not_nil();
212+
target->get_function_call().lhs().is_not_nil();
213213

214214
irep_idt return_identifier;
215215
if(remove_returns_not_run)
216216
{
217217
return_identifier =
218-
to_symbol_expr(to_code_function_call(target->code).lhs())
219-
.get_identifier();
218+
to_symbol_expr(target->get_function_call().lhs()).get_identifier();
220219
}
221220
else
222221
{
@@ -227,8 +226,7 @@ static goto_programt::targett check_and_replace_target(
227226
"either have a variable for the return value in its lhs() or the next "
228227
"instruction should be an assignment of the return value to a temporary "
229228
"variable");
230-
const exprt &return_value_assignment =
231-
to_code_assign(next_instr->code).lhs();
229+
const exprt &return_value_assignment = next_instr->get_assign().lhs();
232230

233231
// If the assignment is null, return.
234232
if(
@@ -283,22 +281,23 @@ static goto_programt::targett check_and_replace_target(
283281
inserted_expr.set_nullable(
284282
instr_info.get_nullable_type() ==
285283
nondet_instruction_infot::is_nullablet::TRUE);
286-
target_instruction->code = code_returnt(inserted_expr);
287-
target_instruction->code.add_source_location() =
284+
target_instruction->code_nonconst() = code_returnt(inserted_expr);
285+
target_instruction->code_nonconst().add_source_location() =
288286
target_instruction->source_location;
289287
}
290288
else if(target_instruction->is_assign())
291289
{
292290
// Assume that the LHS of *this* assignment is the actual nondet variable
293-
const auto &nondet_var = to_code_assign(target_instruction->code).lhs();
291+
const auto &nondet_var = target_instruction->get_assign().lhs();
294292

295293
side_effect_expr_nondett inserted_expr(
296294
nondet_var.type(), target_instruction->source_location);
297295
inserted_expr.set_nullable(
298296
instr_info.get_nullable_type() ==
299297
nondet_instruction_infot::is_nullablet::TRUE);
300-
target_instruction->code = code_assignt(nondet_var, inserted_expr);
301-
target_instruction->code.add_source_location() =
298+
target_instruction->code_nonconst() =
299+
code_assignt(nondet_var, inserted_expr);
300+
target_instruction->code_nonconst().add_source_location() =
302301
target_instruction->source_location;
303302
}
304303

jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ static bool is_call_to(
6363
{
6464
if(!inst->is_function_call())
6565
return false;
66-
const exprt &callee_expr = to_code_function_call(inst->code).function();
66+
const exprt &callee_expr = inst->get_function_call().function();
6767
if(callee_expr.id() != ID_symbol)
6868
return false;
6969
return to_symbol_expr(callee_expr).get_identifier() == callee;

jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ static bool is_expected_virtualmethod_call(
2222
{
2323
if(instruction.type != FUNCTION_CALL)
2424
return false;
25-
const auto &virtual_call = to_code_function_call(instruction.code);
25+
const auto &virtual_call = instruction.get_function_call();
2626
const auto &called_function = virtual_call.function();
2727
if(!can_cast_expr<class_method_descriptor_exprt>(called_function))
2828
return false;
@@ -81,9 +81,10 @@ SCENARIO(
8181
instrend = main_function.body.instructions.end();
8282
instrit != instrend; ++instrit)
8383
{
84-
for(auto it = instrit->code.depth_begin(),
85-
itend = instrit->code.depth_end();
86-
it != itend; ++it)
84+
for(auto it = instrit->get_code().depth_begin(),
85+
itend = instrit->get_code().depth_end();
86+
it != itend;
87+
++it)
8788
{
8889
if(it->id() == ID_dereference)
8990
{

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ void validate_nondet_method_removed(
4141
// Check that our NONDET(<type>) exists on a rhs somewhere.
4242
if(inst.is_assign())
4343
{
44-
const code_assignt &assignment = to_code_assign(inst.code);
44+
const code_assignt &assignment = inst.get_assign();
4545
if(assignment.rhs().id() == ID_side_effect)
4646
{
4747
const side_effect_exprt &see = to_side_effect_expr(assignment.rhs());
@@ -68,8 +68,7 @@ void validate_nondet_method_removed(
6868
// And check to see that our nondet method call has been removed.
6969
if(inst.is_function_call())
7070
{
71-
const code_function_callt &function_call =
72-
to_code_function_call(inst.code);
71+
const code_function_callt &function_call = inst.get_function_call();
7372

7473
// Small check to make sure the instruction is a symbol.
7574
if(function_call.function().id() != ID_symbol)
@@ -101,9 +100,8 @@ void validate_nondets_converted(
101100
// Check that our NONDET(<type>) exists on a rhs somewhere.
102101
exprt target_expression =
103102
(inst.is_assign()
104-
? to_code_assign(inst.code).rhs()
105-
: inst.is_return() ? to_code_return(inst.code).return_value()
106-
: inst.code);
103+
? inst.get_assign().rhs()
104+
: inst.is_return() ? inst.return_value() : inst.get_code());
107105

108106
if(
109107
const auto side_effect =

jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ void check_function_call(
3232
for(const auto &target : targets)
3333
{
3434
REQUIRE(target->type == goto_program_instruction_typet::FUNCTION_CALL);
35-
const code_function_callt &call = to_code_function_call(target->code);
35+
const code_function_callt &call = target->get_function_call();
3636
REQUIRE(call.function().id() == ID_symbol);
3737
REQUIRE(to_symbol_expr(call.function()).get_identifier() == function_name);
3838
}

src/analyses/ai.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -398,7 +398,7 @@ bool ai_baset::visit_function_call(
398398
// it generates a synthetic goto_functions object for this
399399
if(!goto_functions.function_map.empty())
400400
{
401-
const code_function_callt &code = to_code_function_call(l_call->code);
401+
const code_function_callt &code = l_call->get_function_call();
402402
const exprt &callee_expression = code.function();
403403

404404
if(callee_expression.id() == ID_symbol)

src/analyses/call_graph.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ static void forall_callsites(
5656
{
5757
if(i_it->is_function_call())
5858
{
59-
const exprt &function_expr=to_code_function_call(i_it->code).function();
59+
const exprt &function_expr = i_it->get_function_call().function();
6060
if(function_expr.id()==ID_symbol)
6161
{
6262
const irep_idt &callee=to_symbol_expr(function_expr).get_identifier();

0 commit comments

Comments
 (0)