Regularise the style and division of responsibilities in symex dispatch

Specifically: symex_step always dispatches without running either clean_expr or renaming, symex_step
always takes care of the if-unreachable case (usually means skip instruction, but end-of-function has
work to do regardless), symex_step takes care of advancing to the successor instruction after a simple
instruction executes.

No behavioural changes intended here except avoiding a little bit of redundant renaming / simplification
when functions other than symex_step call symex_assume or vcc.

Author: smowton

src/goto-symex/goto_symex.h

@@ -223,12 +223,14 @@ class goto_symext
   virtual void symex_dead(statet &);
   virtual void symex_other(statet &);
 
+  void symex_assert(const goto_programt::instructiont &, statet &);
   virtual void vcc(
     const exprt &,
     const std::string &msg,
     statet &);
 
   virtual void symex_assume(statet &, const exprt &cond);
+  void symex_assume_l2(statet &, const exprt &cond);
 
   // gotos
   void merge_gotos(statet &);

src/goto-symex/symex_function_call.cpp

@@ -194,8 +194,18 @@ void goto_symext::symex_function_call(
 void goto_symext::symex_function_call_symbol(
   const get_goto_functiont &get_goto_function,
   statet &state,
-  const code_function_callt &code)
+  const code_function_callt &original_code)
 {
+  code_function_callt code = original_code;
+
+  if(code.lhs().is_not_nil())
+    clean_expr(code.lhs(), state, true);
+
+  clean_expr(code.function(), state, false);
+
+  Forall_expr(it, code.arguments())
+    clean_expr(*it, state, false);
+
   target.location(state.guard.as_expr(), state.source);
 
   PRECONDITION(code.function().id() == ID_symbol);
@@ -437,4 +447,3 @@ static void locality(
     state.l1_history.insert(l1_name);
   }
 }
-

src/goto-symex/symex_goto.cpp

@@ -27,13 +27,6 @@ void goto_symext::symex_goto(statet &state)
   const goto_programt::instructiont &instruction=*state.source.pc;
   framet &frame = state.top();
 
-  if(state.guard.is_false())
-  {
-    // next instruction
-    symex_transition(state);
-    return; // nothing to do
-  }
-
   exprt new_guard = instruction.get_condition();
   clean_expr(new_guard, state, false);
 
@@ -75,9 +68,9 @@ void goto_symext::symex_goto(statet &state)
       // generate assume(false) or a suitable negation if this
       // instruction is a conditional goto
       if(new_guard.is_true())
-        symex_assume(state, false_exprt());
+        symex_assume_l2(state, false_exprt());
       else
-        symex_assume(state, not_exprt(new_guard));
+        symex_assume_l2(state, not_exprt(new_guard));
 
       // next instruction
       symex_transition(state);
@@ -559,17 +552,18 @@ void goto_symext::loop_bound_exceeded(
     if(symex_config.unwinding_assertions)
     {
       // Generate VCC for unwinding assertion.
-      vcc(negated_cond,
-          "unwinding assertion loop "+std::to_string(loop_number),
-          state);
+      vcc(
+        negated_cond,
+        "unwinding assertion loop " + std::to_string(loop_number),
+        state);
 
       // add to state guard to prevent further assignments
       state.guard.add(negated_cond);
     }
     else
     {
       // generate unwinding assumption, unless we permit partial loops
-      symex_assume(state, negated_cond);
+      symex_assume_l2(state, negated_cond);
     }
   }
 }

src/goto-symex/symex_main.cpp

@@ -76,51 +76,71 @@ void symex_transition(goto_symext::statet &state)
   symex_transition(state, next, false);
 }
 
-void goto_symext::vcc(
-  const exprt &vcc_expr,
-  const std::string &msg,
+void goto_symext::symex_assert(
+  const goto_programt::instructiont &instruction,
   statet &state)
 {
-  state.total_vccs++;
-  path_segment_vccs++;
-
-  exprt expr=vcc_expr;
+  exprt condition = instruction.get_condition();
+  clean_expr(condition, state, false);
 
   // we are willing to re-write some quantified expressions
-  if(has_subexpr(expr, ID_exists) || has_subexpr(expr, ID_forall))
+  if(has_subexpr(condition, ID_exists) || has_subexpr(condition, ID_forall))
   {
     // have negation pushed inwards as far as possible
-    do_simplify(expr);
-    rewrite_quantifiers(expr, state);
+    do_simplify(condition);
+    rewrite_quantifiers(condition, state);
   }
 
   // now rename, enables propagation
-  exprt l2_expr = state.rename(std::move(expr), ns);
+  exprt l2_condition = state.rename(std::move(condition), ns);
 
   // now try simplifier on it
-  do_simplify(l2_expr);
+  do_simplify(l2_condition);
 
-  if(l2_expr.is_true())
+  std::string msg = id2string(instruction.source_location.get_comment());
+  if(msg == "")
+    msg = "assertion";
+
+  vcc(l2_condition, msg, state);
+}
+
+void goto_symext::vcc(
+  const exprt &condition,
+  const std::string &msg,
+  statet &state)
+{
+  state.total_vccs++;
+  path_segment_vccs++;
+
+  if(condition.is_true())
     return;
 
-  state.guard.guard_expr(l2_expr);
+  exprt guarded_condition = condition;
+  state.guard.guard_expr(guarded_condition);
 
   state.remaining_vccs++;
-  target.assertion(state.guard.as_expr(), l2_expr, msg, state.source);
+  target.assertion(state.guard.as_expr(), guarded_condition, msg, state.source);
 }
 
 void goto_symext::symex_assume(statet &state, const exprt &cond)
 {
   exprt simplified_cond=cond;
 
+  clean_expr(simplified_cond, state, false);
+  simplified_cond = state.rename(std::move(simplified_cond), ns);
   do_simplify(simplified_cond);
 
-  if(simplified_cond.is_true())
+  symex_assume_l2(state, simplified_cond);
+}
+
+void goto_symext::symex_assume_l2(statet &state, const exprt &cond)
+{
+  if(cond.is_true())
     return;
 
   if(state.threads.size()==1)
   {
-    exprt tmp=simplified_cond;
+    exprt tmp = cond;
     state.guard.guard_expr(tmp);
     target.assumption(state.guard.as_expr(), tmp, state.source);
   }
@@ -131,7 +151,7 @@ void goto_symext::symex_assume(statet &state, const exprt &cond)
   // x=0;                   assume(x==1);
   // assert(x!=42);         x=42;
   else
-    state.guard.add(simplified_cond);
+    state.guard.add(cond);
 
   if(state.atomic_section_id!=0 &&
      state.guard.is_false())
@@ -402,31 +422,21 @@ void goto_symext::symex_step(
     break;
 
   case GOTO:
-    symex_goto(state);
+    if(!state.guard.is_false())
+      symex_goto(state);
+    else
+      symex_transition(state);
     break;
 
   case ASSUME:
     if(!state.guard.is_false())
-    {
-      exprt tmp = instruction.get_condition();
-      clean_expr(tmp, state, false);
-      symex_assume(state, state.rename(std::move(tmp), ns));
-    }
-
+      symex_assume(state, instruction.get_condition());
     symex_transition(state);
     break;
 
   case ASSERT:
     if(!state.guard.is_false())
-    {
-      std::string msg=id2string(state.source.pc->source_location.get_comment());
-      if(msg=="")
-        msg="assertion";
-      exprt tmp(instruction.get_condition());
-      clean_expr(tmp, state, false);
-      vcc(tmp, msg, state);
-    }
-
+      symex_assert(instruction, state);
     symex_transition(state);
     break;
 
@@ -445,17 +455,8 @@ void goto_symext::symex_step(
   case FUNCTION_CALL:
     if(!state.guard.is_false())
     {
-      code_function_callt deref_code = instruction.get_function_call();
-
-      if(deref_code.lhs().is_not_nil())
-        clean_expr(deref_code.lhs(), state, true);
-
-      clean_expr(deref_code.function(), state, false);
-
-      Forall_expr(it, deref_code.arguments())
-        clean_expr(*it, state, false);
-
-      symex_function_call(get_goto_function, state, deref_code);
+      symex_function_call(
+        get_goto_function, state, instruction.get_function_call());
     }
     else
       symex_transition(state);
@@ -464,14 +465,12 @@ void goto_symext::symex_step(
   case OTHER:
     if(!state.guard.is_false())
       symex_other(state);
-
     symex_transition(state);
     break;
 
   case DECL:
     if(!state.guard.is_false())
       symex_decl(state);
-
     symex_transition(state);
     break;
 

src/goto-symex/symex_throw.cpp

@@ -49,5 +49,5 @@ void goto_symext::symex_throw(statet &state)
   #endif
 
   // An un-caught exception. Behaves like assume(0);
-  symex_assume(state, false_exprt());
+  symex_assume_l2(state, false_exprt());
 }