From e26cb346f7d09be61fe30fddad68072a27cae766 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 12 May 2016 11:20:14 +0100 Subject: [PATCH] symbolic execution: assumptions just alter the path condition --- src/cbmc/bmc.cpp | 16 ------- src/cbmc/bmc_cover.cpp | 13 ----- src/cbmc/show_vcc.cpp | 5 +- src/goto-programs/goto_trace.cpp | 18 +------ src/goto-programs/goto_trace.h | 4 +- src/goto-programs/graphml_witness.cpp | 2 - src/goto-symex/build_goto_trace.cpp | 1 - src/goto-symex/slice.cpp | 8 ---- src/goto-symex/slice_by_trace.cpp | 2 +- src/goto-symex/symex_goto.cpp | 6 +-- src/goto-symex/symex_main.cpp | 22 +++------ src/goto-symex/symex_target.h | 6 --- src/goto-symex/symex_target_equation.cpp | 61 +----------------------- src/goto-symex/symex_target_equation.h | 11 +---- src/path-symex/build_goto_trace.cpp | 4 -- 15 files changed, 16 insertions(+), 163 deletions(-) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index f92483d2441..45d55cf74c3 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -261,22 +261,6 @@ void bmct::show_program() count++; } - else if(step.is_assume()) - { - std::string string_value; - languages.from_expr(step.cond_expr, string_value); - std::cout << "(" << count << ") ASSUME(" - << string_value <<") " << "\n"; - - if(!step.guard.is_true()) - { - languages.from_expr(step.guard, string_value); - std::cout << std::string(std::to_string(count).size()+3, ' '); - std::cout << "guard: " << string_value << "\n"; - } - - count++; - } else if(step.is_constraint()) { std::string string_value; diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 4c101cc2159..be247b3a9d9 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -171,19 +171,6 @@ void bmc_covert::satisfying_assignment() build_goto_trace(bmc.equation, bmc.equation.SSA_steps.end(), solver, bmc.ns, test.goto_trace); - goto_tracet &goto_trace=test.goto_trace; - - // Now delete anything after first failed assumption - for(goto_tracet::stepst::iterator - s_it1=goto_trace.steps.begin(); - s_it1!=goto_trace.steps.end(); - s_it1++) - if(s_it1->is_assume() && !s_it1->cond_value) - { - goto_trace.steps.erase(++s_it1, goto_trace.steps.end()); - break; - } - #if 0 show_goto_trace(std::cout, bmc.ns, test.goto_trace); #endif diff --git a/src/cbmc/show_vcc.cpp b/src/cbmc/show_vcc.cpp index f7a777173ce..e2c8d12c670 100644 --- a/src/cbmc/show_vcc.cpp +++ b/src/cbmc/show_vcc.cpp @@ -53,7 +53,7 @@ void bmct::show_vcc_plain(std::ostream &out) last_it=has_threads?equation.SSA_steps.end():s_it; for(unsigned count=1; p_it!=last_it; p_it++) - if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint()) + if(p_it->is_assignment() || p_it->is_constraint()) { if(!p_it->ignore) { @@ -120,8 +120,7 @@ void bmct::show_vcc_json(std::ostream &out) =equation.SSA_steps.begin(); p_it!=last_it; p_it++) { - if((p_it->is_assume() || - p_it->is_assignment() || + if((p_it->is_assignment() || p_it->is_constraint()) && !p_it->ignore) { diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 4485aed5151..94ae795a703 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -39,7 +39,6 @@ void goto_trace_stept::output( switch(type) { case goto_trace_stept::typet::ASSERT: out << "ASSERT"; break; - case goto_trace_stept::typet::ASSUME: out << "ASSUME"; break; case goto_trace_stept::typet::LOCATION: out << "LOCATION"; break; case goto_trace_stept::typet::ASSIGNMENT: out << "ASSIGNMENT"; break; case goto_trace_stept::typet::GOTO: out << "GOTO"; break; @@ -56,7 +55,7 @@ void goto_trace_stept::output( default: assert(false); } - if(type==typet::ASSERT || type==typet::ASSUME || type==typet::GOTO) + if(type==typet::ASSERT || type==typet::GOTO) out << " (" << cond_value << ")"; if(hidden) @@ -268,21 +267,6 @@ void show_goto_trace( } break; - case goto_trace_stept::typet::ASSUME: - if(!step.cond_value) - { - out << "\n"; - out << "Violated assumption:" << "\n"; - if(!step.pc->source_location.is_nil()) - out << " " << step.pc->source_location << "\n"; - - if(step.pc->is_assume()) - out << " " << from_expr(ns, "", step.pc->guard) << "\n"; - - out << "\n"; - } - break; - case goto_trace_stept::typet::LOCATION: break; diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 4c8a3accc8a..0caa098aa8a 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -37,7 +37,6 @@ class goto_trace_stept unsigned step_nr; bool is_assignment() const { return type==typet::ASSIGNMENT; } - bool is_assume() const { return type==typet::ASSUME; } bool is_assert() const { return type==typet::ASSERT; } bool is_goto() const { return type==typet::GOTO; } bool is_constraint() const { return type==typet::CONSTRAINT; } @@ -59,7 +58,6 @@ class goto_trace_stept { NONE, ASSIGNMENT, - ASSUME, ASSERT, GOTO, LOCATION, @@ -92,7 +90,7 @@ class goto_trace_stept // this transition done by given thread number unsigned thread_nr; - // for assume, assert, goto + // for assert, goto bool cond_value; exprt cond_expr; diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 2362d8f1461..71f7180aaec 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -334,7 +334,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) case goto_trace_stept::typet::FUNCTION_CALL: case goto_trace_stept::typet::FUNCTION_RETURN: case goto_trace_stept::typet::LOCATION: - case goto_trace_stept::typet::ASSUME: case goto_trace_stept::typet::INPUT: case goto_trace_stept::typet::OUTPUT: case goto_trace_stept::typet::SHARED_READ: @@ -495,7 +494,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) case goto_trace_stept::typet::FUNCTION_CALL: case goto_trace_stept::typet::FUNCTION_RETURN: case goto_trace_stept::typet::LOCATION: - case goto_trace_stept::typet::ASSUME: case goto_trace_stept::typet::INPUT: case goto_trace_stept::typet::OUTPUT: case goto_trace_stept::typet::SHARED_READ: diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index 7b6a367f6b2..97b73482d93 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -250,7 +250,6 @@ void build_goto_trace( } if(SSA_step.is_assert() || - SSA_step.is_assume() || SSA_step.is_goto()) { goto_trace_step.cond_expr=SSA_step.cond_expr; diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp index a398264963e..93381b879df 100644 --- a/src/goto-symex/slice.cpp +++ b/src/goto-symex/slice.cpp @@ -60,10 +60,6 @@ void symex_slicet::slice(symex_target_equationt::SSA_stept &SSA_step) get_symbols(SSA_step.cond_expr); break; - case goto_trace_stept::typet::ASSUME: - get_symbols(SSA_step.cond_expr); - break; - case goto_trace_stept::typet::GOTO: get_symbols(SSA_step.cond_expr); break; @@ -162,10 +158,6 @@ void symex_slicet::collect_open_variables( get_symbols(SSA_step.cond_expr); break; - case goto_trace_stept::typet::ASSUME: - get_symbols(SSA_step.cond_expr); - break; - case goto_trace_stept::typet::LOCATION: // ignore break; diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp index f0dfccba4f5..0434d38eb09 100644 --- a/src/goto-symex/slice_by_trace.cpp +++ b/src/goto-symex/slice_by_trace.cpp @@ -110,7 +110,7 @@ void symex_slice_by_tracet::slice_by_trace( SSA_step.guard=t_guard.as_expr(); SSA_step.ssa_lhs.make_nil(); SSA_step.cond_expr.swap(trace_condition); - SSA_step.type=goto_trace_stept::typet::ASSUME; + SSA_step.type=goto_trace_stept::typet::CONSTRAINT; SSA_step.source=empty_source; assign_merges(equation); // Now add the merge variable assignments to eqn diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 03186a129b3..d34e194a7db 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -202,16 +202,14 @@ void goto_symext::symex_step_goto(statet &state, bool taken) const goto_programt::instructiont &instruction=*state.source.pc; exprt guard(instruction.guard); - dereference(guard, state, false); + clean_expr(guard, state, false); state.rename(guard, ns); if(!taken) guard.make_not(); - state.guard.guard_expr(guard); do_simplify(guard); - - target.assumption(state.guard.as_expr(), guard, state.source); + state.guard.add(guard); } void goto_symext::merge_gotos(statet &state) diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 501fdabea70..f011e1ba206 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -47,10 +47,13 @@ void goto_symext::vcc( if(expr.is_true()) return; - state.guard.guard_expr(expr); + exprt gexpr=expr; + state.guard.guard_expr(gexpr); remaining_vccs++; - target.assertion(state.guard.as_expr(), expr, msg, state.source); + target.assertion(state.guard.as_expr(), gexpr, msg, state.source); + + state.guard.add(expr); } void goto_symext::symex_assume(statet &state, const exprt &cond) @@ -62,20 +65,7 @@ void goto_symext::symex_assume(statet &state, const exprt &cond) if(simplified_cond.is_true()) return; - if(state.threads.size()==1) - { - exprt tmp=simplified_cond; - state.guard.guard_expr(tmp); - target.assumption(state.guard.as_expr(), tmp, state.source); - } - // symex_target_equationt::convert_assertions would fail to - // consider assumptions of threads that have a thread-id above that - // of the thread containing the assertion: - // T0 T1 - // x=0; assume(x==1); - // assert(x!=42); x=42; - else - state.guard.add(simplified_cond); + state.guard.add(simplified_cond); if(state.atomic_section_id!=0 && state.guard.is_false()) diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h index 24a8daee0e2..a62e02451db 100644 --- a/src/goto-symex/symex_target.h +++ b/src/goto-symex/symex_target.h @@ -135,12 +135,6 @@ class symex_targett const irep_idt &input_id, const std::list &args)=0; - // record an assumption - virtual void assumption( - const exprt &guard, - const exprt &cond, - const sourcet &source)=0; - // record an assertion virtual void assertion( const exprt &guard, diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index e0c8e86a42f..4feef1691a2 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -303,23 +303,6 @@ void symex_target_equationt::input( merge_ireps(SSA_step); } -/// record an assumption -void symex_target_equationt::assumption( - const exprt &guard, - const exprt &cond, - const sourcet &source) -{ - SSA_steps.push_back(SSA_stept()); - SSA_stept &SSA_step=SSA_steps.back(); - - SSA_step.guard=guard; - SSA_step.cond_expr=cond; - SSA_step.type=goto_trace_stept::typet::ASSUME; - SSA_step.source=source; - - merge_ireps(SSA_step); -} - /// record an assertion void symex_target_equationt::assertion( const exprt &guard, @@ -381,7 +364,6 @@ void symex_target_equationt::convert( convert_guards(prop_conv); convert_assignments(prop_conv); convert_decls(prop_conv); - convert_assumptions(prop_conv); convert_assertions(prop_conv); convert_goto_instructions(prop_conv); convert_io(prop_conv); @@ -431,23 +413,6 @@ void symex_target_equationt::convert_guards( } } -/// converts assumptions -/// \return - -void symex_target_equationt::convert_assumptions( - prop_convt &prop_conv) -{ - for(auto &step : SSA_steps) - { - if(step.is_assume()) - { - if(step.ignore) - step.cond_literal=const_literal(true); - else - step.cond_literal=prop_conv.convert(step.cond_expr); - } - } -} - /// converts goto instructions /// \return - void symex_target_equationt::convert_goto_instructions( @@ -499,16 +464,12 @@ void symex_target_equationt::convert_assertions( if(number_of_assertions==1) { for(auto &step : SSA_steps) - { if(step.is_assert()) { prop_conv.set_to_false(step.cond_expr); step.cond_literal=const_literal(false); return; // prevent further assumptions! } - else if(step.is_assume()) - prop_conv.set_to_true(step.cond_expr); - } assert(false); // unreachable } @@ -518,32 +479,16 @@ void symex_target_equationt::convert_assertions( or_exprt::operandst disjuncts; disjuncts.reserve(number_of_assertions); - exprt assumption=true_exprt(); - for(auto &step : SSA_steps) { if(step.is_assert()) { - implies_exprt implication( - assumption, - step.cond_expr); - // do the conversion - step.cond_literal=prop_conv.convert(implication); + step.cond_literal=prop_conv.convert(step.cond_expr); // store disjunct disjuncts.push_back(literal_exprt(!step.cond_literal)); } - else if(step.is_assume()) - { - // the assumptions have been converted before - // avoid deep nesting of ID_and expressions - if(assumption.id()==ID_and) - assumption.copy_to_operands(literal_exprt(step.cond_literal)); - else - assumption= - and_exprt(assumption, literal_exprt(step.cond_literal)); - } } // the below is 'true' if there are no assertions @@ -627,8 +572,6 @@ void symex_target_equationt::SSA_stept::output( { case goto_trace_stept::typet::ASSERT: out << "ASSERT " << from_expr(ns, "", cond_expr) << '\n'; break; - case goto_trace_stept::typet::ASSUME: - out << "ASSUME " << from_expr(ns, "", cond_expr) << '\n'; break; case goto_trace_stept::typet::LOCATION: out << "LOCATION" << '\n'; break; case goto_trace_stept::typet::INPUT: @@ -691,7 +634,7 @@ void symex_target_equationt::SSA_stept::output( default: assert(false); } - if(is_assert() || is_assume() || is_assignment() || is_constraint()) + if(is_assert() || is_assignment() || is_constraint()) out << from_expr(ns, "", cond_expr) << '\n'; if(is_assert() || is_constraint()) diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index abee81346a7..3b27ffc7a01 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -110,12 +110,6 @@ class symex_target_equationt:public symex_targett const irep_idt &input_id, const std::list &args); - // record an assumption - virtual void assumption( - const exprt &guard, - const exprt &cond, - const sourcet &source); - // record an assertion virtual void assertion( const exprt &guard, @@ -158,7 +152,6 @@ class symex_target_equationt:public symex_targett void convert(prop_convt &prop_conv); void convert_assignments(decision_proceduret &decision_procedure) const; void convert_decls(prop_convt &prop_conv) const; - void convert_assumptions(prop_convt &prop_conv); void convert_assertions(prop_convt &prop_conv); void convert_constraints(decision_proceduret &decision_procedure) const; void convert_goto_instructions(prop_convt &prop_conv); @@ -176,8 +169,6 @@ class symex_target_equationt:public symex_targett // NOLINTNEXTLINE(whitespace/line_length) bool is_assert() const { return type==goto_trace_stept::typet::ASSERT; } // NOLINTNEXTLINE(whitespace/line_length) - bool is_assume() const { return type==goto_trace_stept::typet::ASSUME; } - // NOLINTNEXTLINE(whitespace/line_length) bool is_assignment() const { return type==goto_trace_stept::typet::ASSIGNMENT; } // NOLINTNEXTLINE(whitespace/line_length) bool is_goto() const { return type==goto_trace_stept::typet::GOTO; } @@ -218,7 +209,7 @@ class symex_target_equationt:public symex_targett exprt ssa_rhs; assignment_typet assignment_type; - // for ASSUME/ASSERT/GOTO/CONSTRAINT + // for ASSERT/GOTO/CONSTRAINT exprt cond_expr; literalt cond_literal; std::string comment; diff --git a/src/path-symex/build_goto_trace.cpp b/src/path-symex/build_goto_trace.cpp index fed73f16457..f5f842ebd4d 100644 --- a/src/path-symex/build_goto_trace.cpp +++ b/src/path-symex/build_goto_trace.cpp @@ -57,10 +57,6 @@ void build_goto_trace( trace_step.type=goto_trace_stept::typet::DEAD; break; - case ASSUME: - trace_step.type=goto_trace_stept::typet::ASSUME; - break; - case FUNCTION_CALL: trace_step.type=goto_trace_stept::typet::FUNCTION_CALL; break;