Skip to content

Commit f9ab8c0

Browse files
kroeningkroening
committed
protect goto_instructiont::guard
This protects a field of goto_instructiont, in favor of using the recommended accessor methods.
1 parent 58d64d8 commit f9ab8c0

18 files changed

+89
-70
lines changed

‎jbmc/src/java_bytecode/remove_exceptions.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -368,7 +368,7 @@ void remove_exceptionst::add_exception_dispatch_sequence(
368368
struct_tag_typet type(stack_catch[i][j].first);
369369

370370
java_instanceof_exprt check(exc_thrown, type);
371-
t_exc->guard=check;
371+
t_exc->condition_nonconst() = check;
372372

373373
if(remove_added_instanceof)
374374
{

‎jbmc/src/java_bytecode/remove_instanceof.cpp

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -242,8 +242,9 @@ bool remove_instanceoft::lower_instanceof(
242242
goto_programt::targett target)
243243
{
244244
if(
245-
target->is_target() && (contains_instanceof(target->get_code()) ||
246-
contains_instanceof(target->guard)))
245+
target->is_target() &&
246+
(contains_instanceof(target->get_code()) ||
247+
(target->has_condition() && contains_instanceof(target->condition()))))
247248
{
248249
// If this is a branch target, add a skip beforehand so we can splice new
249250
// GOTO programs before the target instruction without inserting into the
@@ -256,8 +257,12 @@ bool remove_instanceoft::lower_instanceof(
256257

257258
return lower_instanceof(
258259
function_identifier, target->code_nonconst(), goto_program, target) |
259-
lower_instanceof(
260-
function_identifier, target->guard, goto_program, target);
260+
(target->has_condition() ? lower_instanceof(
261+
function_identifier,
262+
target->condition_nonconst(),
263+
goto_program,
264+
target)
265+
: false);
261266
}
262267

263268
/// Replace every instanceof in the passed function body with an explicit

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ static bool is_call_to(
7171

7272
static bool is_assume_false(goto_programt::const_targett inst)
7373
{
74-
return inst->is_assume() && inst->guard.is_false();
74+
return inst->is_assume() && inst->condition().is_false();
7575
}
7676

7777
/// Interpret `program`, resolving classid comparisons assuming any actual
@@ -90,7 +90,7 @@ static goto_programt::const_targett interpret_classid_comparison(
9090
{
9191
if(pc->type() == GOTO)
9292
{
93-
exprt guard = pc->guard;
93+
exprt guard = pc->condition();
9494
guard = resolve_classid_test(guard, actual_class_id, ns);
9595
if(guard.is_true())
9696
{

‎jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp

Lines changed: 12 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -92,15 +92,20 @@ SCENARIO(
9292
}
9393
}
9494

95-
for(auto it = instrit->guard.depth_begin(),
96-
itend = instrit->guard.depth_end();
97-
it != itend; ++it)
95+
if(instrit->has_condition())
9896
{
99-
if(it->id() == ID_dereference)
97+
const auto &condition = instrit->condition();
98+
99+
for(auto it = condition.depth_begin(),
100+
itend = condition.depth_end();
101+
it != itend;
102+
++it)
100103
{
101-
const auto &deref = to_dereference_expr(*it);
102-
REQUIRE(
103-
safe_pointers.is_safe_dereference(deref, instrit));
104+
if(it->id() == ID_dereference)
105+
{
106+
const auto &deref = to_dereference_expr(*it);
107+
REQUIRE(safe_pointers.is_safe_dereference(deref, instrit));
108+
}
104109
}
105110
}
106111
}

‎jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -71,11 +71,12 @@ SCENARIO(
7171
// branching for class C and one for class D or O.
7272
if(instruction.type() == goto_program_instruction_typet::GOTO)
7373
{
74-
if(instruction.guard.id() == ID_equal)
74+
if(instruction.condition().id() == ID_equal)
7575
{
7676
THEN("Class C should call its specific method")
7777
{
78-
const equal_exprt &eq_expr = to_equal_expr(instruction.guard);
78+
const equal_exprt &eq_expr =
79+
to_equal_expr(instruction.condition());
7980
check_function_call(
8081
eq_expr,
8182
"java::C",
@@ -84,11 +85,12 @@ SCENARIO(
8485
}
8586
}
8687

87-
else if(instruction.guard.id() == ID_or)
88+
else if(instruction.condition().id() == ID_or)
8889
{
8990
THEN("Classes D and O should both call O.toString()")
9091
{
91-
const or_exprt &disjunction = to_or_expr(instruction.guard);
92+
const or_exprt &disjunction =
93+
to_or_expr(instruction.condition());
9294
REQUIRE(
9395
(disjunction.op0().id() == ID_equal &&
9496
disjunction.op1().id() == ID_equal));

‎src/analyses/interval_analysis.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ void instrument_intervals(
5050
{
5151
// we follow a branch, instrument
5252
}
53-
else if(previous->is_function_call() && !previous->guard.is_true())
53+
else if(previous->is_function_call() && !previous->condition().is_true())
5454
{
5555
// we follow a function call, instrument
5656
}

‎src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -79,13 +79,13 @@ void variable_sensitivity_domaint::transform(
7979
if(to == from->get_target())
8080
{
8181
// The AI is exploring the branch where the jump is taken
82-
assume(instruction.guard, ns);
82+
assume(instruction.condition(), ns);
8383
}
8484
else
8585
{
8686
// Exploring the path where the jump is not taken - therefore assume
8787
// the condition is false
88-
assume(not_exprt(instruction.guard), ns);
88+
assume(not_exprt(instruction.condition()), ns);
8989
}
9090
}
9191
// ignore jumps to the next line, we can assume nothing
@@ -94,7 +94,7 @@ void variable_sensitivity_domaint::transform(
9494
break;
9595

9696
case ASSUME:
97-
assume(instruction.guard, ns);
97+
assume(instruction.condition(), ns);
9898
break;
9999

100100
case FUNCTION_CALL:

‎src/goto-cc/linker_script_merge.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -258,8 +258,11 @@ int linker_script_merget::pointerize_linker_defined_symbols(
258258
goto_programt &program=gf.second.body;
259259
for(auto &instruction : program.instructions)
260260
{
261-
for(exprt *insts : std::list<exprt *>(
262-
{&(instruction.code_nonconst()), &(instruction.guard)}))
261+
std::list<exprt *> expressions = {&instruction.code_nonconst()};
262+
if(instruction.has_condition())
263+
expressions.push_back(&instruction.condition_nonconst());
264+
265+
for(exprt *insts : expressions)
263266
{
264267
std::list<symbol_exprt> to_pointerize;
265268
symbols_to_pointerize(linker_values, *insts, to_pointerize);

‎src/goto-checker/symex_coverage.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -214,7 +214,7 @@ void goto_program_coverage_recordt::compute_coverage_lines(
214214
it->is_end_function())
215215
continue;
216216

217-
const bool is_branch = it->is_goto() && !it->guard.is_constant();
217+
const bool is_branch = it->is_goto() && !it->condition().is_constant();
218218

219219
unsigned l =
220220
safe_string2unsigned(id2string(it->source_location().get_line()));

‎src/goto-harness/memory_snapshot_harness_generator.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -165,7 +165,7 @@ void memory_snapshot_harness_generatort::add_init_section(
165165
auto ins_it1 = goto_program.insert_before(
166166
start_it,
167167
goto_programt::make_goto(goto_program.const_cast_target(start_it)));
168-
ins_it1->guard = func_init_done_var;
168+
ins_it1->condition_nonconst() = func_init_done_var;
169169

170170
auto ins_it2 = goto_program.insert_after(
171171
ins_it1,

‎src/goto-instrument/cover_basic_blocks.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,9 @@ optionalt<std::size_t> cover_basic_blockst::continuation_of_block(
2121
return {};
2222

2323
const goto_programt::targett in_t = *instruction->incoming_edges.cbegin();
24-
if(in_t->is_goto() && !in_t->is_backwards_goto() && in_t->guard.is_true())
24+
if(
25+
in_t->is_goto() && !in_t->is_backwards_goto() &&
26+
in_t->condition().is_true())
2527
return block_map[in_t];
2628

2729
return {};

‎src/goto-instrument/cover_instrument_other.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ void cover_assertion_instrumentert::instrument(
4040
// turn into 'assert(false)' to avoid simplification
4141
if(is_non_cover_assertion(i_it))
4242
{
43-
i_it->guard = false_exprt();
43+
i_it->condition_nonconst() = false_exprt();
4444
initialize_source_location(
4545
i_it, id2string(i_it->source_location().get_comment()), function_id);
4646
}

‎src/goto-instrument/goto_program2code.cpp

Lines changed: 38 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -199,7 +199,7 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
199199
return target;
200200

201201
case ASSUME:
202-
dest.add(code_assumet(target->guard));
202+
dest.add(code_assumet(target->condition()));
203203
return target;
204204

205205
case GOTO:
@@ -514,7 +514,7 @@ goto_programt::const_targett goto_program2codet::convert_do_while(
514514
{
515515
assert(loop_end->is_goto() && loop_end->is_backwards_goto());
516516

517-
code_dowhilet d(loop_end->guard, code_blockt());
517+
code_dowhilet d(loop_end->condition(), code_blockt());
518518
simplify(d.cond(), ns);
519519

520520
copy_source_location(loop_end->targets.front(), d);
@@ -547,7 +547,7 @@ goto_programt::const_targett goto_program2codet::convert_goto(
547547
(upper_bound==goto_program.instructions.end() ||
548548
upper_bound->location_number > loop_entry->second->location_number))
549549
return convert_goto_while(target, loop_entry->second, dest);
550-
else if(!target->guard.is_true())
550+
else if(!target->condition().is_true())
551551
return convert_goto_switch(target, upper_bound, dest);
552552
else if(!loop_last_stack.empty())
553553
return convert_goto_break_continue(target, upper_bound, dest);
@@ -574,10 +574,10 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
574574

575575
if(target->get_target()==after_loop)
576576
{
577-
w.cond()=not_exprt(target->guard);
577+
w.cond() = not_exprt(target->condition());
578578
simplify(w.cond(), ns);
579579
}
580-
else if(target->guard.is_true())
580+
else if(target->condition().is_true())
581581
{
582582
target = convert_goto_goto(target, to_code_block(w.body()));
583583
}
@@ -594,13 +594,13 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
594594
loop_last_stack.pop_back();
595595

596596
convert_labels(loop_end, to_code_block(w.body()));
597-
if(loop_end->guard.is_false())
597+
if(loop_end->condition().is_false())
598598
{
599599
to_code_block(w.body()).add(code_breakt());
600600
}
601-
else if(!loop_end->guard.is_true())
601+
else if(!loop_end->condition().is_true())
602602
{
603-
code_ifthenelset i(not_exprt(loop_end->guard), code_breakt());
603+
code_ifthenelset i(not_exprt(loop_end->condition()), code_breakt());
604604
simplify(i.cond(), ns);
605605

606606
copy_source_location(target, i);
@@ -661,9 +661,9 @@ goto_programt::const_targett goto_program2codet::get_cases(
661661
cases_it!=upper_bound && cases_it!=first_target;
662662
++cases_it)
663663
{
664-
if(cases_it->is_goto() &&
665-
!cases_it->is_backwards_goto() &&
666-
cases_it->guard.is_true())
664+
if(
665+
cases_it->is_goto() && !cases_it->is_backwards_goto() &&
666+
cases_it->condition().is_true())
667667
{
668668
default_target=cases_it->get_target();
669669

@@ -684,16 +684,16 @@ goto_programt::const_targett goto_program2codet::get_cases(
684684
++cases_it;
685685
break;
686686
}
687-
else if(cases_it->is_goto() &&
688-
!cases_it->is_backwards_goto() &&
689-
(cases_it->guard.id()==ID_equal ||
690-
cases_it->guard.id()==ID_or))
687+
else if(
688+
cases_it->is_goto() && !cases_it->is_backwards_goto() &&
689+
(cases_it->condition().id() == ID_equal ||
690+
cases_it->condition().id() == ID_or))
691691
{
692692
exprt::operandst eqs;
693-
if(cases_it->guard.id()==ID_equal)
694-
eqs.push_back(cases_it->guard);
693+
if(cases_it->condition().id() == ID_equal)
694+
eqs.push_back(cases_it->condition());
695695
else
696-
eqs=cases_it->guard.operands();
696+
eqs = cases_it->condition().operands();
697697

698698
// goto conversion builds disjunctions in reverse order
699699
// to ensure convergence, we turn this around again
@@ -839,9 +839,9 @@ bool goto_program2codet::remove_default(
839839
}
840840

841841
// jumps to default are ok
842-
if(it->case_last->is_goto() &&
843-
it->case_last->guard.is_true() &&
844-
it->case_last->get_target()==default_target)
842+
if(
843+
it->case_last->is_goto() && it->case_last->condition().is_true() &&
844+
it->case_last->get_target() == default_target)
845845
continue;
846846

847847
// fall-through is ok
@@ -860,7 +860,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
860860
code_blockt &dest)
861861
{
862862
// try to figure out whether this was a switch/case
863-
exprt eq_cand=target->guard;
863+
exprt eq_cand = target->condition();
864864
if(eq_cand.id()==ID_or)
865865
eq_cand = to_or_expr(eq_cand).op0();
866866

@@ -985,7 +985,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
985985
{
986986
UNREACHABLE;
987987
goto_programt::instructiont i=*(it->case_selector);
988-
i.guard=true_exprt();
988+
i.condition_nonconst() = true_exprt();
989989
goto_programt tmp;
990990
tmp.insert_before_swap(tmp.insert_before(tmp.instructions.end()), i);
991991
convert_goto_goto(tmp.instructions.begin(), c);
@@ -1048,13 +1048,13 @@ goto_programt::const_targett goto_program2codet::convert_goto_if(
10481048
return target;
10491049
}
10501050

1051-
has_else=
1051+
has_else =
10521052
before_else->is_goto() &&
10531053
before_else->get_target()->location_number > end_if->location_number &&
1054-
before_else->guard.is_true() &&
1055-
(upper_bound==goto_program.instructions.end() ||
1056-
upper_bound->location_number>=
1057-
before_else->get_target()->location_number);
1054+
before_else->condition().is_true() &&
1055+
(upper_bound == goto_program.instructions.end() ||
1056+
upper_bound->location_number >=
1057+
before_else->get_target()->location_number);
10581058

10591059
if(has_else)
10601060
end_if=before_else->get_target();
@@ -1071,7 +1071,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_if(
10711071
return convert_goto_goto(target, dest);
10721072
}
10731073

1074-
code_ifthenelset i(not_exprt(target->guard), code_blockt());
1074+
code_ifthenelset i(not_exprt(target->condition()), code_blockt());
10751075
copy_source_location(target, i);
10761076
simplify(i.cond(), ns);
10771077

@@ -1132,7 +1132,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
11321132
if(target->get_target()==loop_end &&
11331133
loop_last_stack.back().second)
11341134
{
1135-
code_ifthenelset i(target->guard, code_continuet());
1135+
code_ifthenelset i(target->condition(), code_continuet());
11361136
simplify(i.cond(), ns);
11371137

11381138
copy_source_location(target, i);
@@ -1156,7 +1156,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
11561156

11571157
if(target->get_target()==after_loop)
11581158
{
1159-
code_ifthenelset i(target->guard, code_breakt());
1159+
code_ifthenelset i(target->condition(), code_breakt());
11601160
simplify(i.cond(), ns);
11611161

11621162
copy_source_location(target, i);
@@ -1214,7 +1214,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_goto(
12141214

12151215
code_gotot goto_code(label.str());
12161216

1217-
code_ifthenelset i(target->guard, std::move(goto_code));
1217+
code_ifthenelset i(target->condition(), std::move(goto_code));
12181218
simplify(i.cond(), ns);
12191219

12201220
copy_source_location(target, i);
@@ -1281,9 +1281,12 @@ goto_programt::const_targett goto_program2codet::convert_start_thread(
12811281
// END THREAD
12821282
// 2: code in existing thread
12831283
/* check the structure and compute the iterators */
1284-
assert(next->is_goto() && next->guard.is_true());
1285-
assert(!next->is_backwards_goto());
1286-
assert(thread_start->location_number < next->get_target()->location_number);
1284+
DATA_INVARIANT(
1285+
next->is_goto() && next->condition().is_true(), "START THREAD pattern");
1286+
DATA_INVARIANT(!next->is_backwards_goto(), "START THREAD pattern");
1287+
DATA_INVARIANT(
1288+
thread_start->location_number < next->get_target()->location_number,
1289+
"START THREAD pattern");
12871290
goto_programt::const_targett after_thread_start=thread_start;
12881291
++after_thread_start;
12891292

0 commit comments

Comments
 (0)