Merge pull request #5097 from smowton/smowton/feature/symex-truncate-on-assume-false

Symex: distinguish reachability from the state guard

Author: smowton

jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_indirect_enum_initalization.desc

@@ -1,7 +1,6 @@
 CORE
 indirect/IndirectVirtualCall.class
 --function indirect.IndirectVirtualCall.main
-function java::indirect\.TestEnum\.<clinit>:\(\)V$
 ^EXIT=10$
 ^SIGNAL=0$
 --

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/analyses/guard_bdd.h

@@ -65,6 +65,13 @@ class guard_bddt
     return guard_bddt(manager, bdd.bdd_not());
   }
 
+  /// Returns true if `operator|=` with \p other_guard may result in a simpler
+  /// expression. For `bdd_exprt` we always simplify maximally.
+  bool disjunction_may_simplify(const guard_bddt &other_guard)
+  {
+    return true;
+  }
+
 private:
   bdd_exprt &manager;
   bddt bdd;

src/analyses/guard_expr.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <ostream>
 
-#include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/simplify_utils.h>
 #include <util/std_expr.h>
@@ -91,6 +90,17 @@ guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2)
   return g1;
 }
 
+bool guard_exprt::disjunction_may_simplify(const guard_exprt &other_guard)
+{
+  if(is_true() || is_false() || other_guard.is_true() || other_guard.is_false())
+    return true;
+  if(expr.id() == ID_and && other_guard.expr.id() == ID_and)
+    return true;
+  if(other_guard.expr == boolean_negate(expr))
+    return true;
+  return false;
+}
+
 guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2)
 {
   if(g2.is_false() || g1.is_true())

src/analyses/guard_expr.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <iosfwd>
 
+#include <util/expr_util.h>
 #include <util/std_expr.h>
 
 /// This is unused by this implementation of guards, but can be used by other
@@ -72,6 +73,11 @@ class guard_exprt
   friend guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2);
   friend guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2);
 
+  /// Returns true if `operator|=` with \p other_guard may result in a simpler
+  /// expression. For `guard_exprt` in practice this means they're both
+  /// conjunctions, since for other things we just OR them together.
+  bool disjunction_may_simplify(const guard_exprt &other_guard);
+
 private:
   exprt expr;
 };

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;
     }