Regularise and optimise symex path truncating

There are various situations where symex wishes to mark the current path non-viable:
* On a __CPROVER_ASSUME(false), or an expression which simplifies to false
* When --depth is exceeded
* When --unwind is exceeded

However these situations were handled in slightly varying ways, some using the symex_assume
mechanism and others directly hacking the state guard. In the ASSUME(false) case, we also failed
to actually falsify the guard, meaning we continued pointlessly generating constraints for
unreachable code.

This commit directs all such paths through either symex_assume_l2, if they wish to assert a
non-false condition, or the new utility function truncate_current_path when unconditionally
truncating the current execution path. We also mutate the state guard *in the specific case
where it becomes false*, as this enables us to save execution time that would otherwise be
spent on unreachable code, similar to how we treat conditional GOTOs with statically decidable
conditions.

This should mean that (a) all sorts of path truncation result in the guard becoming false and
corresponding work-saving, and (b) the different kinds of truncation are handled uniformly,
making future maintenance simpler.

Author: smowton

regression/cbmc/assume-false/test.c

@@ -0,0 +1,11 @@
+int main(int argc, char **argv) {
+  int i = 0;
+  if(argc % 2)
+    i = argc;
+  else {
+    __CPROVER_assume(0);
+    i = 2;
+  }
+
+  assert(i == argc);
+}

regression/cbmc/assume-false/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--show-vcc
+main::1::i!0@1#[0-9]+ = 0
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::i!0@1#[0-9]+ = 2
+--
+This checks that code rendered unreachable by a __CPROVER_assume(0) does not generate constraints.
+

regression/cbmc/assume-false/test_execution.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The main test is in test.desc; this just checks that the program
+has the expected result

src/goto-symex/goto_symex.h

@@ -411,6 +411,17 @@ class goto_symext
   virtual void symex_assume(statet &state, const exprt &cond);
   void symex_assume_l2(statet &, const exprt &cond);
 
+  /// Mark the current execution path unviable, due to an ASSUME(FALSE),
+  /// exceeding depth or unwind limits, or anything else that means we
+  /// statically know we can't possibly execute this path. Symex will use this
+  /// to cease executing instructions (on this thread) until we next merge with
+  /// a viable path
+  /// \param state: state to alter
+  void truncate_current_path(statet &state)
+  {
+    symex_assume_l2(state, false_exprt());
+  }
+
   /// Merge all branches joining at the current program point. Applies
   /// \ref merge_goto for each goto state (each of which corresponds to previous
   /// branch).

src/goto-symex/symex_function_call.cpp

@@ -258,8 +258,7 @@ void goto_symext::symex_function_call_code(
       if(symex_config.unwinding_assertions)
         vcc(false_exprt(), "recursion unwinding assertion", state);
 
-      // add to state guard to prevent further assignments
-      state.guard.add(false_exprt());
+      truncate_current_path(state);
     }
 
     symex_transition(state);

src/goto-symex/symex_goto.cpp

@@ -268,7 +268,7 @@ 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_l2(state, false_exprt());
+        truncate_current_path(state);
       else
         symex_assume_l2(state, not_exprt(new_guard));
 
@@ -796,14 +796,9 @@ void goto_symext::loop_bound_exceeded(
         "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_l2(state, negated_cond);
     }
+    // generate unwinding assumption, unless we permit partial loops
+    symex_assume_l2(state, negated_cond);
   }
 }
 

src/goto-symex/symex_main.cpp

@@ -160,8 +160,14 @@ void goto_symext::symex_assume_l2(statet &state, const exprt &cond)
 
   if(state.threads.size()==1)
   {
+    exprt unguarded_cond = rewritten_cond;
     exprt tmp = state.guard.guard_expr(rewritten_cond);
     target.assumption(state.guard.as_expr(), tmp, state.source);
+    // There's no need to drag assumptions in general around in the guard, but
+    // when it's obvious that this branch is no longer viable we might as well
+    // avoid the cost of executing other instructions on this branch:
+    if(unguarded_cond.is_false())
+      state.guard.add(unguarded_cond);
   }
   // symex_target_equationt::convert_assertions would fail to
   // consider assumptions of threads that have a thread-id above that
@@ -527,8 +533,11 @@ void goto_symext::execute_next_instruction(
     merge_gotos(state);
 
   // depth exceeded?
-  if(symex_config.max_depth != 0 && state.depth > symex_config.max_depth)
-    state.guard.add(false_exprt());
+  if(symex_config.max_depth != 0 && state.depth > symex_config.max_depth &&
+     !state.guard.is_false())
+  {
+    truncate_current_path(state);
+  }
   state.depth++;
 
   // actually do instruction
@@ -619,7 +628,7 @@ void goto_symext::execute_next_instruction(
   case END_THREAD:
     // behaves like assume(0);
     if(!state.guard.is_false())
-      state.guard.add(false_exprt());
+      truncate_current_path(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_l2(state, false_exprt());
+  truncate_current_path(state);
 }

unit/path_strategies.cpp

@@ -202,10 +202,9 @@ SCENARIO("path strategies")
         symex_eventt::resume(symex_eventt::enumt::JUMP, 9),
         symex_eventt::result(symex_eventt::enumt::FAILURE),
 
-        // The path where we enter the loop body twice. Successful because
+        // The path where we enter the loop body twice. No result because
         // infeasible.
         symex_eventt::resume(symex_eventt::enumt::NEXT, 7),
-        symex_eventt::result(symex_eventt::enumt::SUCCESS),
 
         // Overall we fail.
         symex_eventt::result(symex_eventt::enumt::FAILURE),
@@ -235,9 +234,8 @@ SCENARIO("path strategies")
         symex_eventt::result(symex_eventt::enumt::SUCCESS),
 
         // Pop line 7 that we saved from above, and execute the loop a second
-        // time. Successful, since this path is infeasible.
+        // time. No result, since this path is infeasible.
         symex_eventt::resume(symex_eventt::enumt::NEXT, 7),
-        symex_eventt::result(symex_eventt::enumt::SUCCESS),
 
         // Pop line 7 that we saved from above and bail out. That corresponds to
         // executing the loop once, decrementing x to 0; assert(x) should fail.