symbolic execution: assumptions just alter the path condition

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;

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

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)
       {

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;
 

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;
 

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:

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;

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;

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

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)

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())

src/goto-symex/symex_target.h

@@ -135,12 +135,6 @@ class symex_targett
     const irep_idt &input_id,
     const std::list<exprt> &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,

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())