Skip to content

Commit 606a83a

Browse files
tautschnigtautschnig
authored
Merge pull request #4144 from diffblue/instructiont-guard
avoid accesses to instructiont::guard
2 parents e3ff246 + d1c2749 commit 606a83a

33 files changed

+165
-86
lines changed

‎src/analyses/constant_propagator.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -756,11 +756,13 @@ void constant_propagator_ait::replace(
756756
continue;
757757

758758
replace_types_rec(d.values.replace_const, it->code);
759-
replace_types_rec(d.values.replace_const, it->guard);
760759

761760
if(it->is_goto() || it->is_assume() || it->is_assert())
762761
{
763-
constant_propagator_domaint::partial_evaluate(d.values, it->guard, ns);
762+
exprt c = it->get_condition();
763+
replace_types_rec(d.values.replace_const, c);
764+
constant_propagator_domaint::partial_evaluate(d.values, c, ns);
765+
it->set_condition(c);
764766
}
765767
else if(it->is_assign())
766768
{

‎src/analyses/dirty.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,9 @@ void dirtyt::build(const goto_functiont &goto_function)
2020
forall_goto_program_instructions(it, goto_function.body)
2121
{
2222
find_dirty(it->code);
23-
find_dirty(it->guard);
23+
24+
if(it->has_condition())
25+
find_dirty(it->get_condition());
2426
}
2527
}
2628

‎src/analyses/goto_check.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1671,7 +1671,8 @@ void goto_checkt::goto_check(
16711671
i.is_target())
16721672
assertions.clear();
16731673

1674-
check(i.guard);
1674+
if(i.has_condition())
1675+
check(i.get_condition());
16751676

16761677
// magic ERROR label?
16771678
for(const auto &label : error_labels)

‎src/analyses/goto_rw.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -762,7 +762,10 @@ void goto_rw(
762762
case ASSUME:
763763
case ASSERT:
764764
rw_set.get_objects_rec(
765-
function, target, rw_range_sett::get_modet::READ, target->guard);
765+
function,
766+
target,
767+
rw_range_sett::get_modet::READ,
768+
target->get_condition());
766769
break;
767770

768771
case RETURN:

‎src/analyses/local_cfg.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ void local_cfgt::build(const goto_programt &goto_program)
4848
switch(instruction.type)
4949
{
5050
case GOTO:
51-
if(!instruction.guard.is_true())
51+
if(!instruction.get_condition().is_true())
5252
node.successors.push_back(loc_nr+1);
5353

5454
for(const auto &target : instruction.targets)

‎src/goto-analyzer/static_verifier.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -256,7 +256,7 @@ bool static_verifier(
256256
if(!i_it->is_assert())
257257
continue;
258258

259-
exprt e(i_it->guard);
259+
exprt e(i_it->get_condition());
260260
auto dp = ai.abstract_state_before(i_it);
261261
const ai_domain_baset &domain(*dp);
262262
domain.ai_simplify(e, ns);

‎src/goto-analyzer/taint_analysis.cpp

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -334,13 +334,18 @@ bool taint_analysist::operator()(
334334
{
335335
if(!i_it->is_assert())
336336
continue;
337-
if(!custom_bitvector_domaint::has_get_must_or_may(i_it->guard))
337+
338+
if(!custom_bitvector_domaint::has_get_must_or_may(
339+
i_it->get_condition()))
340+
{
338341
continue;
342+
}
339343

340344
if(custom_bitvector_analysis[i_it].has_values.is_false())
341345
continue;
342346

343-
exprt result=custom_bitvector_analysis.eval(i_it->guard, i_it);
347+
exprt result =
348+
custom_bitvector_analysis.eval(i_it->get_condition(), i_it);
344349
exprt result2=simplify_expr(result, ns);
345350

346351
if(result2.is_true())

‎src/goto-instrument/accelerate/accelerate.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -43,11 +43,10 @@ goto_programt::targett acceleratet::find_back_jump(
4343
++it)
4444
{
4545
goto_programt::targett t=*it;
46-
if(t->is_goto() &&
47-
t->guard.is_true() &&
48-
t->targets.size()==1 &&
49-
t->targets.front()==loop_header &&
50-
t->location_number > back_jump->location_number)
46+
if(
47+
t->is_goto() && t->get_condition().is_true() && t->targets.size() == 1 &&
48+
t->targets.front() == loop_header &&
49+
t->location_number > back_jump->location_number)
5150
{
5251
back_jump=t;
5352
}
@@ -394,7 +393,8 @@ void acceleratet::add_dirty_checks()
394393
// the right hand side of an assignment. Assume each is not dirty.
395394
find_symbols_sett read;
396395

397-
find_symbols(it->guard, read);
396+
if(it->has_condition())
397+
find_symbols(it->get_condition(), read);
398398

399399
if(it->is_assign())
400400
{

‎src/goto-instrument/accelerate/acceleration_utils.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -276,7 +276,7 @@ exprt acceleration_utilst::precondition(patht &path)
276276
}
277277
else if(t->is_assume() || t->is_assert())
278278
{
279-
ret=implies_exprt(t->guard, ret);
279+
ret = implies_exprt(t->get_condition(), ret);
280280
}
281281
else
282282
{

‎src/goto-instrument/accelerate/all_paths_enumerator.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -136,15 +136,15 @@ void all_paths_enumeratort::extend_path(
136136

137137
if(t->is_goto())
138138
{
139-
guard=not_exprt(t->guard);
139+
guard = not_exprt(t->get_condition());
140140

141141
for(goto_programt::targetst::iterator it=t->targets.begin();
142142
it != t->targets.end();
143143
++it)
144144
{
145145
if(next == *it)
146146
{
147-
guard=t->guard;
147+
guard = t->get_condition();
148148
break;
149149
}
150150
}

‎src/goto-instrument/accelerate/cone_of_influence.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ void cone_of_influencet::get_succs(
8787

8888
if(rit->is_goto())
8989
{
90-
if(!rit->guard.is_false())
90+
if(!rit->get_condition().is_false())
9191
{
9292
// Branch can be taken.
9393
for(goto_programt::targetst::const_iterator t=rit->targets.begin();
@@ -100,14 +100,14 @@ void cone_of_influencet::get_succs(
100100
}
101101
}
102102

103-
if(rit->guard.is_true())
103+
if(rit->get_condition().is_true())
104104
{
105105
return;
106106
}
107107
}
108108
else if(rit->is_assume() || rit->is_assert())
109109
{
110-
if(rit->guard.is_false())
110+
if(rit->get_condition().is_false())
111111
{
112112
return;
113113
}

‎src/goto-instrument/branch.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -45,11 +45,10 @@ void branch(
4545
// T': id("not-taken"); t3
4646
// ...
4747

48-
if(i_it->is_goto() &&
49-
!i_it->guard.is_constant())
48+
if(i_it->is_goto() && !i_it->get_condition().is_constant())
5049
{
5150
// negate condition
52-
i_it->guard = boolean_negate(i_it->guard);
51+
i_it->set_condition(boolean_negate(i_it->get_condition()));
5352

5453
goto_programt::targett t1=body.insert_after(i_it);
5554
t1->make_function_call(

‎src/goto-programs/adjust_float_expressions.cpp

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -200,7 +200,13 @@ void adjust_float_expressions(
200200
Forall_goto_program_instructions(it, goto_function.body)
201201
{
202202
adjust_float_expressions(it->code, ns);
203-
adjust_float_expressions(it->guard, ns);
203+
204+
if(it->has_condition())
205+
{
206+
exprt c = it->get_condition();
207+
adjust_float_expressions(c, ns);
208+
it->set_condition(c);
209+
}
204210
}
205211
}
206212

‎src/goto-programs/compute_called_functions.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,9 @@ void compute_address_taken_functions(
5656
{
5757
forall_goto_program_instructions(it, goto_program)
5858
{
59-
compute_address_taken_functions(it->guard, address_taken);
59+
if(it->has_condition())
60+
compute_address_taken_functions(it->get_condition(), address_taken);
61+
6062
compute_address_taken_functions(it->code, address_taken);
6163
}
6264
}

‎src/goto-programs/goto_convert.cpp

Lines changed: 16 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -254,8 +254,10 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest)
254254

255255
if(
256256
it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() ||
257-
!it_goto_y->guard.is_true() || it_goto_y->is_target())
257+
!it_goto_y->get_condition().is_true() || it_goto_y->is_target())
258+
{
258259
continue;
260+
}
259261

260262
auto it_z = std::next(it_goto_y);
261263

@@ -266,7 +268,7 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest)
266268
if(it->get_target()->target_number == it_z->target_number)
267269
{
268270
it->set_target(it_goto_y->get_target());
269-
it->guard = boolean_negate(it->guard);
271+
it->set_condition(boolean_negate(it->get_condition()));
270272
it_goto_y->make_skip();
271273
}
272274
}
@@ -554,9 +556,9 @@ void goto_convertt::convert_block(
554556

555557
// see if we need to do any destructors -- may have been processed
556558
// in a prior break/continue/return already, don't create dead code
557-
if(!dest.empty() &&
558-
dest.instructions.back().is_goto() &&
559-
dest.instructions.back().guard.is_true())
559+
if(
560+
!dest.empty() && dest.instructions.back().is_goto() &&
561+
dest.instructions.back().get_condition().is_true())
560562
{
561563
// don't do destructors when we are unreachable
562564
}
@@ -1474,10 +1476,10 @@ void goto_convertt::generate_ifthenelse(
14741476
}
14751477

14761478
// do guarded assertions directly
1477-
if(is_size_one(true_case) &&
1478-
true_case.instructions.back().is_assert() &&
1479-
true_case.instructions.back().guard.is_false() &&
1480-
true_case.instructions.back().labels.empty())
1479+
if(
1480+
is_size_one(true_case) && true_case.instructions.back().is_assert() &&
1481+
true_case.instructions.back().get_condition().is_false() &&
1482+
true_case.instructions.back().labels.empty())
14811483
{
14821484
// The above conjunction deliberately excludes the instance
14831485
// if(some) { label: assert(false); }
@@ -1492,10 +1494,10 @@ void goto_convertt::generate_ifthenelse(
14921494
}
14931495

14941496
// similarly, do guarded assertions directly
1495-
if(is_size_one(false_case) &&
1496-
false_case.instructions.back().is_assert() &&
1497-
false_case.instructions.back().guard.is_false() &&
1498-
false_case.instructions.back().labels.empty())
1497+
if(
1498+
is_size_one(false_case) && false_case.instructions.back().is_assert() &&
1499+
false_case.instructions.back().get_condition().is_false() &&
1500+
false_case.instructions.back().labels.empty())
14991501
{
15001502
// The above conjunction deliberately excludes the instance
15011503
// if(some) ... else { label: assert(false); }
@@ -1514,7 +1516,7 @@ void goto_convertt::generate_ifthenelse(
15141516
if(
15151517
is_empty(false_case) && true_case.instructions.size() == 2 &&
15161518
true_case.instructions.front().is_assert() &&
1517-
true_case.instructions.front().guard.is_false() &&
1519+
true_case.instructions.front().get_condition().is_false() &&
15181520
true_case.instructions.front().labels.empty() &&
15191521
true_case.instructions.back().labels.empty())
15201522
{

‎src/goto-programs/goto_convert_functions.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -109,9 +109,12 @@ void goto_convert_functionst::add_return(
109109
while(true)
110110
{
111111
// unconditional goto, say from while(1)?
112-
if(last_instruction->is_goto() &&
113-
last_instruction->guard.is_true())
112+
if(
113+
last_instruction->is_goto() &&
114+
last_instruction->get_condition().is_true())
115+
{
114116
return;
117+
}
115118

116119
// return?
117120
if(last_instruction->is_return())

‎src/goto-programs/goto_inline_class.cpp

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -315,8 +315,14 @@ void goto_inlinet::insert_function_body(
315315
Forall_goto_program_instructions(it, tmp)
316316
{
317317
replace_location(it->source_location, target->source_location);
318-
replace_location(it->guard, target->source_location);
319318
replace_location(it->code, target->source_location);
319+
320+
if(it->has_condition())
321+
{
322+
exprt c = it->get_condition();
323+
replace_location(c, target->source_location);
324+
it->set_condition(c);
325+
}
320326
}
321327
}
322328

‎src/goto-programs/goto_program.cpp

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -73,10 +73,9 @@ std::ostream &goto_programt::output_instruction(
7373
break;
7474

7575
case GOTO:
76-
if(!instruction.guard.is_true())
76+
if(!instruction.get_condition().is_true())
7777
{
78-
out << "IF "
79-
<< from_expr(ns, identifier, instruction.guard)
78+
out << "IF " << from_expr(ns, identifier, instruction.get_condition())
8079
<< " THEN ";
8180
}
8281

@@ -112,7 +111,7 @@ std::ostream &goto_programt::output_instruction(
112111
out << "ASSERT ";
113112

114113
{
115-
out << from_expr(ns, identifier, instruction.guard);
114+
out << from_expr(ns, identifier, instruction.get_condition());
116115

117116
const irep_idt &comment=instruction.source_location.get_comment();
118117
if(comment!="")
@@ -276,7 +275,7 @@ std::list<exprt> expressions_read(
276275
case ASSUME:
277276
case ASSERT:
278277
case GOTO:
279-
dest.push_back(instruction.guard);
278+
dest.push_back(instruction.get_condition());
280279
break;
281280

282281
case RETURN:
@@ -416,9 +415,9 @@ std::string as_string(
416415
return "(NO INSTRUCTION TYPE)";
417416

418417
case GOTO:
419-
if(!i.guard.is_true())
418+
if(!i.get_condition().is_true())
420419
{
421-
result += "IF " + from_expr(ns, function, i.guard) + " THEN ";
420+
result += "IF " + from_expr(ns, function, i.get_condition()) + " THEN ";
422421
}
423422

424423
result+="GOTO ";
@@ -449,7 +448,7 @@ std::string as_string(
449448
else
450449
result+="ASSERT ";
451450

452-
result += from_expr(ns, function, i.guard);
451+
result += from_expr(ns, function, i.get_condition());
453452

454453
{
455454
const irep_idt &comment=i.source_location.get_comment();
@@ -634,7 +633,7 @@ void goto_programt::copy_from(const goto_programt &src)
634633
bool goto_programt::has_assertion() const
635634
{
636635
for(const auto &i : instructions)
637-
if(i.is_assert() && !i.guard.is_true())
636+
if(i.is_assert() && !i.get_condition().is_true())
638637
return true;
639638

640639
return false;

0 commit comments

Comments
 (0)