Symex: distinguish reachability from the state guard

Previously the state guard being false was taken to indicate unreachable code,
and different causes of unreachability were handled inconsistently:

* ASSUME false implied unreachability but had no effect on the guard
* --unwind or --depth being exceeded usually meant setting the guard false

This meant that expensive code downstream of an ASSUME false *was* executed, but the state
guard was maintained as usual including shrinking the guard when branches converge, while
--unwind or --depth limit breaks led to code *not* being executed (vital for these options
to function properly) but the state guard grew ever larger because the part that had gone
missing (been set to false) never got merged back in.

This commit distinguishes the two concepts: the "reachable" flag is set false whenever a
limit break OR and ASSUME false happens, but state guard maintenance continues as normal.
A new symex_unreachable_goto tries to find some way through the CFG back to reachable code;
when it can't due to loops *then* it sets the state guard to false, signifying our not
being able to figure out where the guard ought to be merged back in.

This means that ASSUME false instructions now correctly truncate execution and are
recognised as unreachable code for the purposes of state merging (leading to better
constant propagation downstream), but in some cases we may see more guard growth
because code downstream of an ASSUME false is executed less rigorously that before,
which could result in the guard not being merged or being merged later than it otherwise
would have been.

Depth and unwind limit breaks behave roughly as before, except that there is some chance
the state guard will be merged rather than discarded, reducing costs downstream.

Author: smowton

regression/cbmc/unreachable-goto1/test-vccs.desc

@@ -0,0 +1,12 @@
+CORE paths-lifo-expected-failure
+test.c
+--show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^\{1\} false$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Note: disabled for paths-lifo mode, which never merges state guards
+This checks that despite being unreachable due to an assume(false), the state guard
+is returned to TRUE by the time the assertion is executed.

regression/cbmc/unreachable-goto1/test.c

@@ -0,0 +1,12 @@
+int main(int argc, char **argv)
+{
+  if(argc == 1)
+  {
+    do
+    {
+      __CPROVER_assume(0);
+    } while(argc < 2);
+  }
+
+  assert(0);
+}

regression/cbmc/unreachable-goto1/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This tests that a __CPROVER_assume(0) prompts symex to assume that a conditional
+backward branch is not taken.

regression/cbmc/unreachable-goto2/test-vccs.desc

@@ -0,0 +1,13 @@
+CORE paths-lifo-expected-failure
+test.c
+--show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^\{1\} goto_symex::\\guard#1$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Note: disabled for paths-lifo mode, which never merges state guards
+This checks that the guard from a loop containing an assume(false), and with
+an unconditional backedge, is discarded as expected, resulting in a non-trivial
+guard at the assertion.

regression/cbmc/unreachable-goto2/test.c

@@ -0,0 +1,12 @@
+int main(int argc, char **argv)
+{
+  if(argc == 1)
+  {
+    while(argc < 2)
+    {
+      __CPROVER_assume(0);
+    }
+  }
+
+  assert(0);
+}

regression/cbmc/unreachable-goto2/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This tests that a __CPROVER_assume(0) in an infinite loop terminates the loop

regression/cbmc/unreachable-goto3/test-vccs.desc

@@ -0,0 +1,13 @@
+CORE paths-lifo-expected-failure
+test.c
+--show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^\{1\} false$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Note: disabled for paths-lifo mode, which never merges state guards
+This checks that an assume(false) prior to a loop correctly results
+in symex stepping around that loop, resulting in the state guard
+returning to true.

regression/cbmc/unreachable-goto3/test.c

@@ -0,0 +1,12 @@
+int main(int argc, char **argv)
+{
+  if(argc == 1)
+  {
+    __CPROVER_assume(0);
+    while(1)
+    {
+    }
+  }
+
+  assert(0);
+}

regression/cbmc/unreachable-goto3/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This tests that with a __CPROVER_assume(0) before an infinite loop,
+symex terminates without needing a `--unwind` setting.

regression/cbmc/unreachable-goto4/test-vccs.desc

@@ -0,0 +1,13 @@
+CORE paths-lifo-expected-failure
+test.c
+--show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^\{1\} false$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Note: disabled for paths-lifo mode, which never merges state guards
+This checks that an assume(false) prior to a do-while loop correctly results
+in symex stepping into a single iteration of that loop, and then out,
+resulting in the state guard returning to true.

regression/cbmc/unreachable-goto4/test.c

@@ -0,0 +1,12 @@
+int main(int argc, char **argv)
+{
+  if(argc == 1)
+  {
+    __CPROVER_assume(0);
+    do
+    {
+    } while(1);
+  }
+
+  assert(0);
+}

regression/cbmc/unreachable-goto4/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This tests that with a __CPROVER_assume(0) before an infinite loop,
+symex terminates without needing a `--unwind` setting.

regression/cbmc/unreachable-goto5/test-vccs.desc

@@ -0,0 +1,12 @@
+CORE paths-lifo-expected-failure
+test.c
+--show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^\{1\} false$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Note: disabled for paths-lifo mode, which never merges state guards
+This checks that an assume(false) within a branch correctly results
+in symex returning the state guard to true when control flow converges.

regression/cbmc/unreachable-goto5/test.c

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

regression/cbmc/unreachable-goto5/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This tests that with a __CPROVER_assume(0) within conditional control flow,
+symex still executes the assertion as expected.

regression/cbmc/unreachable-goto6/test-vccs.desc

@@ -0,0 +1,13 @@
+CORE paths-lifo-expected-failure
+test.c
+--show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^\{1\} false$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Note: disabled for paths-lifo mode, which never merges state guards
+This checks that an assume(false) prior to a branch correctly results
+in symex picking some arbitrary path through the unreachable CFG, and so
+it returns the state guard to true when control flow converges.

regression/cbmc/unreachable-goto6/test.c

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

regression/cbmc/unreachable-goto6/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This tests that with a __CPROVER_assume(0) prior to conditional control flow,
+symex executes the final assertion as expected.

src/goto-symex/goto_state.h

@@ -49,6 +49,10 @@ class goto_statet
   // of the condition of the if).
   guardt guard;
 
+  /// Is this code reachable? If not we can take shortcuts such as not entering
+  /// function calls, but we still conduct guard arithmetic as usual.
+  bool reachable;
+
   // Map L1 names to (L2) constants. Values will be evicted from this map
   // when they become non-constant. This is used to propagate values that have
   // been worked out to only have one possible value.
@@ -73,7 +77,7 @@ class goto_statet
   explicit goto_statet(const class goto_symex_statet &s);
 
   explicit goto_statet(guard_managert &guard_manager)
-    : guard(true_exprt(), guard_manager)
+    : guard(true_exprt(), guard_manager), reachable(true)
   {
   }
 

src/goto-symex/goto_symex.h

@@ -332,6 +332,9 @@ class goto_symext
   /// Symbolically execute a GOTO instruction
   /// \param state: Symbolic execution state for current instruction
   virtual void symex_goto(statet &state);
+  /// Symbolically execute a GOTO instruction in the context of unreachable code
+  /// \param state: Symbolic execution state for current instruction
+  void symex_unreachable_goto(statet &state);
   /// Symbolically execute a START_THREAD instruction
   /// \param state: Symbolic execution state for current instruction
   virtual void symex_start_thread(statet &state);

src/goto-symex/goto_symex_state.h

@@ -277,6 +277,7 @@ inline goto_statet::goto_statet(const class goto_symex_statet &s)
     level2(s.level2),
     value_set(s.value_set),
     guard(s.guard),
+    reachable(s.reachable),
     propagation(s.propagation),
     atomic_section_id(s.atomic_section_id)
 {

src/goto-symex/symex_atomic_section.cpp

@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
 
 void goto_symext::symex_atomic_begin(statet &state)
 {
-  if(state.guard.is_false())
+  if(!state.reachable)
     return;
 
   if(state.atomic_section_id != 0)
@@ -35,7 +35,7 @@ void goto_symext::symex_atomic_begin(statet &state)
 
 void goto_symext::symex_atomic_end(statet &state)
 {
-  if(state.guard.is_false())
+  if(!state.reachable)
     return;
 
   if(state.atomic_section_id == 0)

src/goto-symex/symex_function_call.cpp

@@ -260,9 +260,6 @@ void goto_symext::symex_function_call_code(
 
       // Rule out this path:
       symex_assume_l2(state, false_exprt());
-      // Disable processing instructions until we next encounter one reachable
-      // without passing this instruction:
-      state.guard.add(false_exprt());
     }
 
     symex_transition(state);
@@ -356,18 +353,15 @@ static void pop_frame(
     // accumulate assumptions (in symex_assume_l2) and must be left alone.
     // If however it is single-threaded then we should restore the guard, as the
     // guard coming out of the function may be more complex (e.g. if the callee
-    // was { if(x) __CPROVER_assume(false); } then the guard may still be `!x`),
+    // was { if(x) while(true) { } } then the guard may still be `!x`),
     // but at this point all control-flow paths have either converged or been
     // proven unviable, so we can stop specifying the callee's constraints when
     // we generate an assumption or VCC.
 
-    // If the guard is false, *this* path is unviable and we shouldn't discard
-    // that knowledge. If we're doing path exploration then we do
-    // tail-duplication, and we actually *are* in a more-restricted context
-    // than we were when the function began.
-    if(
-      state.threads.size() == 1 && !state.guard.is_false() &&
-      !doing_path_exploration)
+    // If we're doing path exploration then we do tail-duplication, and we
+    // actually *are* in a more-restricted context than we were when the
+    // function began.
+    if(state.threads.size() == 1 && !doing_path_exploration)
     {
       state.guard = frame.guard_at_function_start;
     }