Skip to content

Commit 26c1bae

Browse files
tautschnigtautschnig
committed
symbolic execution: assumptions just alter the path condition
1 parent 985f1a7 commit 26c1bae

15 files changed

+22
-184
lines changed

‎src/cbmc/bmc.cpp

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

354354
count++;
355355
}
356-
else if(step.is_assume())
357-
{
358-
std::string string_value;
359-
languages.from_expr(step.cond_expr, string_value);
360-
std::cout << "(" << count << ") ASSUME("
361-
<< string_value <<") " << "\n";
362-
363-
if(!step.guard.is_true())
364-
{
365-
languages.from_expr(step.guard, string_value);
366-
std::cout << std::string(std::to_string(count).size()+3, ' ');
367-
std::cout << "guard: " << string_value << "\n";
368-
}
369-
370-
count++;
371-
}
372356
else if(step.is_constraint())
373357
{
374358
std::string string_value;

‎src/cbmc/bmc_cover.cpp

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

195-
goto_tracet &goto_trace=test.goto_trace;
196-
197-
// Now delete anything after first failed assumption
198-
for(goto_tracet::stepst::iterator
199-
s_it1=goto_trace.steps.begin();
200-
s_it1!=goto_trace.steps.end();
201-
s_it1++)
202-
if(s_it1->is_assume() && !s_it1->cond_value)
203-
{
204-
goto_trace.steps.erase(++s_it1, goto_trace.steps.end());
205-
break;
206-
}
207-
208195
#if 0
209196
show_goto_trace(std::cout, bmc.ns, test.goto_trace);
210197
#endif

‎src/cbmc/show_vcc.cpp

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

6464
for(unsigned count=1; p_it!=last_it; p_it++)
65-
if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint())
65+
if(p_it->is_assignment() || p_it->is_constraint())
6666
{
6767
if(!p_it->ignore)
6868
{
@@ -141,8 +141,7 @@ void bmct::show_vcc_json(std::ostream &out)
141141
=equation.SSA_steps.begin();
142142
p_it!=last_it; p_it++)
143143
{
144-
if((p_it->is_assume() ||
145-
p_it->is_assignment() ||
144+
if((p_it->is_assignment() ||
146145
p_it->is_constraint()) &&
147146
!p_it->ignore)
148147
{

‎src/goto-programs/goto_trace.cpp

Lines changed: 6 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,6 @@ void goto_trace_stept::output(
6060
switch(type)
6161
{
6262
case goto_trace_stept::ASSERT: out << "ASSERT"; break;
63-
case goto_trace_stept::ASSUME: out << "ASSUME"; break;
6463
case goto_trace_stept::LOCATION: out << "LOCATION"; break;
6564
case goto_trace_stept::ASSIGNMENT: out << "ASSIGNMENT"; break;
6665
case goto_trace_stept::GOTO: out << "GOTO"; break;
@@ -73,10 +72,14 @@ void goto_trace_stept::output(
7372
case goto_trace_stept::SHARED_WRITE: out << "SHARED WRITE"; break;
7473
case goto_trace_stept::FUNCTION_CALL: out << "FUNCTION CALL"; break;
7574
case goto_trace_stept::FUNCTION_RETURN: out << "FUNCTION RETURN"; break;
76-
default: assert(false);
75+
case goto_trace_stept::DEAD: assert(false);
76+
case goto_trace_stept::CONSTRAINT: assert(false);
77+
case goto_trace_stept::MEMORY_BARRIER: assert(false);
78+
case goto_trace_stept::SPAWN: assert(false);
79+
case goto_trace_stept::NONE: assert(false);
7780
}
7881

79-
if(type==ASSERT || type==ASSUME || type==GOTO)
82+
if(type==ASSERT || type==GOTO)
8083
out << " (" << cond_value << ")";
8184

8285
if(hidden)
@@ -348,21 +351,6 @@ void show_goto_trace(
348351
}
349352
break;
350353

351-
case goto_trace_stept::ASSUME:
352-
if(!step.cond_value)
353-
{
354-
out << "\n";
355-
out << "Violated assumption:" << "\n";
356-
if(!step.pc->source_location.is_nil())
357-
out << " " << step.pc->source_location << "\n";
358-
359-
if(step.pc->is_assume())
360-
out << " " << from_expr(ns, "", step.pc->guard) << "\n";
361-
362-
out << "\n";
363-
}
364-
break;
365-
366354
case goto_trace_stept::LOCATION:
367355
break;
368356

‎src/goto-programs/goto_trace.h

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,6 @@ class goto_trace_stept
3434
unsigned step_nr;
3535

3636
bool is_assignment() const { return type==ASSIGNMENT; }
37-
bool is_assume() const { return type==ASSUME; }
3837
bool is_assert() const { return type==ASSERT; }
3938
bool is_goto() const { return type==GOTO; }
4039
bool is_constraint() const { return type==CONSTRAINT; }
@@ -52,7 +51,7 @@ class goto_trace_stept
5251
bool is_atomic_begin() const { return type==ATOMIC_BEGIN; }
5352
bool is_atomic_end() const { return type==ATOMIC_END; }
5453

55-
typedef enum { NONE, ASSIGNMENT, ASSUME, ASSERT, GOTO,
54+
typedef enum { NONE, ASSIGNMENT, ASSERT, GOTO,
5655
LOCATION, INPUT, OUTPUT, DECL, DEAD,
5756
FUNCTION_CALL, FUNCTION_RETURN,
5857
CONSTRAINT,
@@ -72,7 +71,7 @@ class goto_trace_stept
7271
// this transition done by given thread number
7372
unsigned thread_nr;
7473

75-
// for assume, assert, goto
74+
// for assert, goto
7675
bool cond_value;
7776
exprt cond_expr;
7877

‎src/goto-programs/graphml_witness.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -378,7 +378,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
378378
case goto_trace_stept::FUNCTION_CALL:
379379
case goto_trace_stept::FUNCTION_RETURN:
380380
case goto_trace_stept::LOCATION:
381-
case goto_trace_stept::ASSUME:
382381
case goto_trace_stept::INPUT:
383382
case goto_trace_stept::OUTPUT:
384383
case goto_trace_stept::SHARED_READ:
@@ -550,7 +549,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
550549
case goto_trace_stept::FUNCTION_CALL:
551550
case goto_trace_stept::FUNCTION_RETURN:
552551
case goto_trace_stept::LOCATION:
553-
case goto_trace_stept::ASSUME:
554552
case goto_trace_stept::INPUT:
555553
case goto_trace_stept::OUTPUT:
556554
case goto_trace_stept::SHARED_READ:

‎src/goto-symex/build_goto_trace.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -279,7 +279,6 @@ void build_goto_trace(
279279
}
280280

281281
if(SSA_step.is_assert() ||
282-
SSA_step.is_assume() ||
283282
SSA_step.is_goto())
284283
{
285284
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
@@ -117,10 +117,6 @@ void symex_slicet::slice(symex_target_equationt::SSA_stept &SSA_step)
117117
get_symbols(SSA_step.cond_expr);
118118
break;
119119

120-
case goto_trace_stept::ASSUME:
121-
get_symbols(SSA_step.cond_expr);
122-
break;
123-
124120
case goto_trace_stept::GOTO:
125121
get_symbols(SSA_step.cond_expr);
126122
break;
@@ -252,10 +248,6 @@ void symex_slicet::collect_open_variables(
252248
get_symbols(SSA_step.cond_expr);
253249
break;
254250

255-
case goto_trace_stept::ASSUME:
256-
get_symbols(SSA_step.cond_expr);
257-
break;
258-
259251
case goto_trace_stept::LOCATION:
260252
// ignore
261253
break;

‎src/goto-symex/slice_by_trace.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,7 @@ void symex_slice_by_tracet::slice_by_trace(
119119
SSA_step.guard=t_guard.as_expr();
120120
SSA_step.ssa_lhs.make_nil();
121121
SSA_step.cond_expr.swap(trace_condition);
122-
SSA_step.type=goto_trace_stept::ASSUME;
122+
SSA_step.type=goto_trace_stept::CONSTRAINT;
123123
SSA_step.source=empty_source;
124124

125125
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
@@ -223,16 +223,14 @@ void goto_symext::symex_step_goto(statet &state, bool taken)
223223
const goto_programt::instructiont &instruction=*state.source.pc;
224224

225225
exprt guard(instruction.guard);
226-
dereference(guard, state, false);
226+
clean_expr(guard, state, false);
227227
state.rename(guard, ns);
228228

229229
if(!taken)
230230
guard.make_not();
231231

232-
state.guard.guard_expr(guard);
233232
do_simplify(guard);
234-
235-
target.assumption(state.guard.as_expr(), guard, state.source);
233+
state.guard.add(guard);
236234
}
237235

238236
/*******************************************************************\

‎src/goto-symex/symex_main.cpp

Lines changed: 6 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -68,10 +68,13 @@ void goto_symext::vcc(
6868
if(expr.is_true())
6969
return;
7070

71-
state.guard.guard_expr(expr);
71+
exprt gexpr=expr;
72+
state.guard.guard_expr(gexpr);
7273

7374
remaining_vccs++;
74-
target.assertion(state.guard.as_expr(), expr, msg, state.source);
75+
target.assertion(state.guard.as_expr(), gexpr, msg, state.source);
76+
77+
state.guard.add(expr);
7578
}
7679

7780
/*******************************************************************\
@@ -95,20 +98,7 @@ void goto_symext::symex_assume(statet &state, const exprt &cond)
9598
if(simplified_cond.is_true())
9699
return;
97100

98-
if(state.threads.size()==1)
99-
{
100-
exprt tmp=simplified_cond;
101-
state.guard.guard_expr(tmp);
102-
target.assumption(state.guard.as_expr(), tmp, state.source);
103-
}
104-
// symex_target_equationt::convert_assertions would fail to
105-
// consider assumptions of threads that have a thread-id above that
106-
// of the thread containing the assertion:
107-
// T0 T1
108-
// x=0; assume(x==1);
109-
// assert(x!=42); x=42;
110-
else
111-
state.guard.add(simplified_cond);
101+
state.guard.add(simplified_cond);
112102

113103
if(state.atomic_section_id!=0 &&
114104
state.guard.is_false())

‎src/goto-symex/symex_target.h

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

135-
// record an assumption
136-
virtual void assumption(
137-
const exprt &guard,
138-
const exprt &cond,
139-
const sourcet &source)=0;
140-
141135
// record an assertion
142136
virtual void assertion(
143137
const exprt &guard,

0 commit comments

Comments
 (0)