Skip to content

Commit e26cb34

Browse files
tautschnigtautschnig
committed
symbolic execution: assumptions just alter the path condition
1 parent e2afe93 commit e26cb34

15 files changed

+16
-163
lines changed

‎src/cbmc/bmc.cpp

Lines changed: 0 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -261,22 +261,6 @@ void bmct::show_program()
261261

262262
count++;
263263
}
264-
else if(step.is_assume())
265-
{
266-
std::string string_value;
267-
languages.from_expr(step.cond_expr, string_value);
268-
std::cout << "(" << count << ") ASSUME("
269-
<< string_value <<") " << "\n";
270-
271-
if(!step.guard.is_true())
272-
{
273-
languages.from_expr(step.guard, string_value);
274-
std::cout << std::string(std::to_string(count).size()+3, ' ');
275-
std::cout << "guard: " << string_value << "\n";
276-
}
277-
278-
count++;
279-
}
280264
else if(step.is_constraint())
281265
{
282266
std::string string_value;

‎src/cbmc/bmc_cover.cpp

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -171,19 +171,6 @@ void bmc_covert::satisfying_assignment()
171171
build_goto_trace(bmc.equation, bmc.equation.SSA_steps.end(),
172172
solver, bmc.ns, test.goto_trace);
173173

174-
goto_tracet &goto_trace=test.goto_trace;
175-
176-
// Now delete anything after first failed assumption
177-
for(goto_tracet::stepst::iterator
178-
s_it1=goto_trace.steps.begin();
179-
s_it1!=goto_trace.steps.end();
180-
s_it1++)
181-
if(s_it1->is_assume() && !s_it1->cond_value)
182-
{
183-
goto_trace.steps.erase(++s_it1, goto_trace.steps.end());
184-
break;
185-
}
186-
187174
#if 0
188175
show_goto_trace(std::cout, bmc.ns, test.goto_trace);
189176
#endif

‎src/cbmc/show_vcc.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ void bmct::show_vcc_plain(std::ostream &out)
5353
last_it=has_threads?equation.SSA_steps.end():s_it;
5454

5555
for(unsigned count=1; p_it!=last_it; p_it++)
56-
if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint())
56+
if(p_it->is_assignment() || p_it->is_constraint())
5757
{
5858
if(!p_it->ignore)
5959
{
@@ -120,8 +120,7 @@ void bmct::show_vcc_json(std::ostream &out)
120120
=equation.SSA_steps.begin();
121121
p_it!=last_it; p_it++)
122122
{
123-
if((p_it->is_assume() ||
124-
p_it->is_assignment() ||
123+
if((p_it->is_assignment() ||
125124
p_it->is_constraint()) &&
126125
!p_it->ignore)
127126
{

‎src/goto-programs/goto_trace.cpp

Lines changed: 1 addition & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,6 @@ void goto_trace_stept::output(
3939
switch(type)
4040
{
4141
case goto_trace_stept::typet::ASSERT: out << "ASSERT"; break;
42-
case goto_trace_stept::typet::ASSUME: out << "ASSUME"; break;
4342
case goto_trace_stept::typet::LOCATION: out << "LOCATION"; break;
4443
case goto_trace_stept::typet::ASSIGNMENT: out << "ASSIGNMENT"; break;
4544
case goto_trace_stept::typet::GOTO: out << "GOTO"; break;
@@ -56,7 +55,7 @@ void goto_trace_stept::output(
5655
default: assert(false);
5756
}
5857

59-
if(type==typet::ASSERT || type==typet::ASSUME || type==typet::GOTO)
58+
if(type==typet::ASSERT || type==typet::GOTO)
6059
out << " (" << cond_value << ")";
6160

6261
if(hidden)
@@ -268,21 +267,6 @@ void show_goto_trace(
268267
}
269268
break;
270269

271-
case goto_trace_stept::typet::ASSUME:
272-
if(!step.cond_value)
273-
{
274-
out << "\n";
275-
out << "Violated assumption:" << "\n";
276-
if(!step.pc->source_location.is_nil())
277-
out << " " << step.pc->source_location << "\n";
278-
279-
if(step.pc->is_assume())
280-
out << " " << from_expr(ns, "", step.pc->guard) << "\n";
281-
282-
out << "\n";
283-
}
284-
break;
285-
286270
case goto_trace_stept::typet::LOCATION:
287271
break;
288272

‎src/goto-programs/goto_trace.h

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,6 @@ class goto_trace_stept
3737
unsigned step_nr;
3838

3939
bool is_assignment() const { return type==typet::ASSIGNMENT; }
40-
bool is_assume() const { return type==typet::ASSUME; }
4140
bool is_assert() const { return type==typet::ASSERT; }
4241
bool is_goto() const { return type==typet::GOTO; }
4342
bool is_constraint() const { return type==typet::CONSTRAINT; }
@@ -59,7 +58,6 @@ class goto_trace_stept
5958
{
6059
NONE,
6160
ASSIGNMENT,
62-
ASSUME,
6361
ASSERT,
6462
GOTO,
6563
LOCATION,
@@ -92,7 +90,7 @@ class goto_trace_stept
9290
// this transition done by given thread number
9391
unsigned thread_nr;
9492

95-
// for assume, assert, goto
93+
// for assert, goto
9694
bool cond_value;
9795
exprt cond_expr;
9896

‎src/goto-programs/graphml_witness.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -334,7 +334,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
334334
case goto_trace_stept::typet::FUNCTION_CALL:
335335
case goto_trace_stept::typet::FUNCTION_RETURN:
336336
case goto_trace_stept::typet::LOCATION:
337-
case goto_trace_stept::typet::ASSUME:
338337
case goto_trace_stept::typet::INPUT:
339338
case goto_trace_stept::typet::OUTPUT:
340339
case goto_trace_stept::typet::SHARED_READ:
@@ -495,7 +494,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
495494
case goto_trace_stept::typet::FUNCTION_CALL:
496495
case goto_trace_stept::typet::FUNCTION_RETURN:
497496
case goto_trace_stept::typet::LOCATION:
498-
case goto_trace_stept::typet::ASSUME:
499497
case goto_trace_stept::typet::INPUT:
500498
case goto_trace_stept::typet::OUTPUT:
501499
case goto_trace_stept::typet::SHARED_READ:

‎src/goto-symex/build_goto_trace.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -250,7 +250,6 @@ void build_goto_trace(
250250
}
251251

252252
if(SSA_step.is_assert() ||
253-
SSA_step.is_assume() ||
254253
SSA_step.is_goto())
255254
{
256255
goto_trace_step.cond_expr=SSA_step.cond_expr;

‎src/goto-symex/slice.cpp

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -60,10 +60,6 @@ void symex_slicet::slice(symex_target_equationt::SSA_stept &SSA_step)
6060
get_symbols(SSA_step.cond_expr);
6161
break;
6262

63-
case goto_trace_stept::typet::ASSUME:
64-
get_symbols(SSA_step.cond_expr);
65-
break;
66-
6763
case goto_trace_stept::typet::GOTO:
6864
get_symbols(SSA_step.cond_expr);
6965
break;
@@ -162,10 +158,6 @@ void symex_slicet::collect_open_variables(
162158
get_symbols(SSA_step.cond_expr);
163159
break;
164160

165-
case goto_trace_stept::typet::ASSUME:
166-
get_symbols(SSA_step.cond_expr);
167-
break;
168-
169161
case goto_trace_stept::typet::LOCATION:
170162
// ignore
171163
break;

‎src/goto-symex/slice_by_trace.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,7 @@ void symex_slice_by_tracet::slice_by_trace(
110110
SSA_step.guard=t_guard.as_expr();
111111
SSA_step.ssa_lhs.make_nil();
112112
SSA_step.cond_expr.swap(trace_condition);
113-
SSA_step.type=goto_trace_stept::typet::ASSUME;
113+
SSA_step.type=goto_trace_stept::typet::CONSTRAINT;
114114
SSA_step.source=empty_source;
115115

116116
assign_merges(equation); // Now add the merge variable assignments to eqn

‎src/goto-symex/symex_goto.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -202,16 +202,14 @@ void goto_symext::symex_step_goto(statet &state, bool taken)
202202
const goto_programt::instructiont &instruction=*state.source.pc;
203203

204204
exprt guard(instruction.guard);
205-
dereference(guard, state, false);
205+
clean_expr(guard, state, false);
206206
state.rename(guard, ns);
207207

208208
if(!taken)
209209
guard.make_not();
210210

211-
state.guard.guard_expr(guard);
212211
do_simplify(guard);
213-
214-
target.assumption(state.guard.as_expr(), guard, state.source);
212+
state.guard.add(guard);
215213
}
216214

217215
void goto_symext::merge_gotos(statet &state)

‎src/goto-symex/symex_main.cpp

Lines changed: 6 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -47,10 +47,13 @@ void goto_symext::vcc(
4747
if(expr.is_true())
4848
return;
4949

50-
state.guard.guard_expr(expr);
50+
exprt gexpr=expr;
51+
state.guard.guard_expr(gexpr);
5152

5253
remaining_vccs++;
53-
target.assertion(state.guard.as_expr(), expr, msg, state.source);
54+
target.assertion(state.guard.as_expr(), gexpr, msg, state.source);
55+
56+
state.guard.add(expr);
5457
}
5558

5659
void goto_symext::symex_assume(statet &state, const exprt &cond)
@@ -62,20 +65,7 @@ void goto_symext::symex_assume(statet &state, const exprt &cond)
6265
if(simplified_cond.is_true())
6366
return;
6467

65-
if(state.threads.size()==1)
66-
{
67-
exprt tmp=simplified_cond;
68-
state.guard.guard_expr(tmp);
69-
target.assumption(state.guard.as_expr(), tmp, state.source);
70-
}
71-
// symex_target_equationt::convert_assertions would fail to
72-
// consider assumptions of threads that have a thread-id above that
73-
// of the thread containing the assertion:
74-
// T0 T1
75-
// x=0; assume(x==1);
76-
// assert(x!=42); x=42;
77-
else
78-
state.guard.add(simplified_cond);
68+
state.guard.add(simplified_cond);
7969

8070
if(state.atomic_section_id!=0 &&
8171
state.guard.is_false())

‎src/goto-symex/symex_target.h

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -135,12 +135,6 @@ class symex_targett
135135
const irep_idt &input_id,
136136
const std::list<exprt> &args)=0;
137137

138-
// record an assumption
139-
virtual void assumption(
140-
const exprt &guard,
141-
const exprt &cond,
142-
const sourcet &source)=0;
143-
144138
// record an assertion
145139
virtual void assertion(
146140
const exprt &guard,

‎src/goto-symex/symex_target_equation.cpp

Lines changed: 2 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -303,23 +303,6 @@ void symex_target_equationt::input(
303303
merge_ireps(SSA_step);
304304
}
305305

306-
/// record an assumption
307-
void symex_target_equationt::assumption(
308-
const exprt &guard,
309-
const exprt &cond,
310-
const sourcet &source)
311-
{
312-
SSA_steps.push_back(SSA_stept());
313-
SSA_stept &SSA_step=SSA_steps.back();
314-
315-
SSA_step.guard=guard;
316-
SSA_step.cond_expr=cond;
317-
SSA_step.type=goto_trace_stept::typet::ASSUME;
318-
SSA_step.source=source;
319-
320-
merge_ireps(SSA_step);
321-
}
322-
323306
/// record an assertion
324307
void symex_target_equationt::assertion(
325308
const exprt &guard,
@@ -381,7 +364,6 @@ void symex_target_equationt::convert(
381364
convert_guards(prop_conv);
382365
convert_assignments(prop_conv);
383366
convert_decls(prop_conv);
384-
convert_assumptions(prop_conv);
385367
convert_assertions(prop_conv);
386368
convert_goto_instructions(prop_conv);
387369
convert_io(prop_conv);
@@ -431,23 +413,6 @@ void symex_target_equationt::convert_guards(
431413
}
432414
}
433415

434-
/// converts assumptions
435-
/// \return -
436-
void symex_target_equationt::convert_assumptions(
437-
prop_convt &prop_conv)
438-
{
439-
for(auto &step : SSA_steps)
440-
{
441-
if(step.is_assume())
442-
{
443-
if(step.ignore)
444-
step.cond_literal=const_literal(true);
445-
else
446-
step.cond_literal=prop_conv.convert(step.cond_expr);
447-
}
448-
}
449-
}
450-
451416
/// converts goto instructions
452417
/// \return -
453418
void symex_target_equationt::convert_goto_instructions(
@@ -499,16 +464,12 @@ void symex_target_equationt::convert_assertions(
499464
if(number_of_assertions==1)
500465
{
501466
for(auto &step : SSA_steps)
502-
{
503467
if(step.is_assert())
504468
{
505469
prop_conv.set_to_false(step.cond_expr);
506470
step.cond_literal=const_literal(false);
507471
return; // prevent further assumptions!
508472
}
509-
else if(step.is_assume())
510-
prop_conv.set_to_true(step.cond_expr);
511-
}
512473

513474
assert(false); // unreachable
514475
}
@@ -518,32 +479,16 @@ void symex_target_equationt::convert_assertions(
518479
or_exprt::operandst disjuncts;
519480
disjuncts.reserve(number_of_assertions);
520481

521-
exprt assumption=true_exprt();
522-
523482
for(auto &step : SSA_steps)
524483
{
525484
if(step.is_assert())
526485
{
527-
implies_exprt implication(
528-
assumption,
529-
step.cond_expr);
530-
531486
// do the conversion
532-
step.cond_literal=prop_conv.convert(implication);
487+
step.cond_literal=prop_conv.convert(step.cond_expr);
533488

534489
// store disjunct
535490
disjuncts.push_back(literal_exprt(!step.cond_literal));
536491
}
537-
else if(step.is_assume())
538-
{
539-
// the assumptions have been converted before
540-
// avoid deep nesting of ID_and expressions
541-
if(assumption.id()==ID_and)
542-
assumption.copy_to_operands(literal_exprt(step.cond_literal));
543-
else
544-
assumption=
545-
and_exprt(assumption, literal_exprt(step.cond_literal));
546-
}
547492
}
548493

549494
// the below is 'true' if there are no assertions
@@ -627,8 +572,6 @@ void symex_target_equationt::SSA_stept::output(
627572
{
628573
case goto_trace_stept::typet::ASSERT:
629574
out << "ASSERT " << from_expr(ns, "", cond_expr) << '\n'; break;
630-
case goto_trace_stept::typet::ASSUME:
631-
out << "ASSUME " << from_expr(ns, "", cond_expr) << '\n'; break;
632575
case goto_trace_stept::typet::LOCATION:
633576
out << "LOCATION" << '\n'; break;
634577
case goto_trace_stept::typet::INPUT:
@@ -691,7 +634,7 @@ void symex_target_equationt::SSA_stept::output(
691634
default: assert(false);
692635
}
693636

694-
if(is_assert() || is_assume() || is_assignment() || is_constraint())
637+
if(is_assert() || is_assignment() || is_constraint())
695638
out << from_expr(ns, "", cond_expr) << '\n';
696639

697640
if(is_assert() || is_constraint())

0 commit comments

Comments
 (0)