Merge pull request #5003 from smowton/smowton/feature/revert-guards-after-calls

[TG-9002] Symex: revert guards after call return

Author: Daniel Kroening

regression/cbmc/residual-guards-1/test.c

@@ -0,0 +1,19 @@
+void g()
+{
+  g();
+}
+
+void f(int y)
+{
+  if(y == 5)
+  {
+    g();
+    y = 10;
+  }
+}
+
+int main(int argc, char **argv)
+{
+  f(argc);
+  assert(argc == 1);
+}

regression/cbmc/residual-guards-1/test.desc

@@ -0,0 +1,14 @@
+CORE paths-lifo-expected-failure
+test.c
+--show-vcc --unwind 10
+^\{1\} main::argc!0@1#1 = 1$
+^EXIT=0$
+^SIGNAL=0$
+--
+^\{-[0-9]+\} f::y!0@1#[0-9]+ = 10$
+--
+This checks that the assertion, argc == 1, is unguarded (i.e. is not of the form 
+'guard => condition'). Such a guard is redundant, but could be added before goto-symex
+made sure to restore guards to their state at function entry.
+We also check that no VCC is created for the unreachable code 'y = 10;'
+--paths mode is excluded as it currently always accrues large guards as it proceeds through execution

regression/cbmc/residual-guards-1/test_execution.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--unwind 10
+^\[main\.assertion\.[0-9]+\] line [0-9]+ assertion argc == 1: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The main test is in test.desc; this just checks that the test is executable and
+the assertion fails as expected.

regression/cbmc/residual-guards-2/test.c

@@ -0,0 +1,16 @@
+void f(int y)
+{
+  if(y == 5)
+  {
+    for(int i = 0; i < 20; ++i)
+    {
+    }
+    y = 10;
+  }
+}
+
+int main(int argc, char **argv)
+{
+  f(argc);
+  assert(argc == 1);
+}

regression/cbmc/residual-guards-2/test.desc

@@ -0,0 +1,12 @@
+CORE paths-lifo-expected-failure
+test.c
+--show-vcc --unwind 10
+^\{1\} main::argc!0@1#1 = 1$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This checks that the assertion, argc == 1, is unguarded (i.e. is not of the form 
+'guard => condition'). Such a guard is redundant, but could be added before goto-symex
+made sure to restore guards to their state at function entry.
+--paths mode is excluded as it currently always accrues large guards as it proceeds through execution

regression/cbmc/residual-guards-2/test_execution.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--unwind 10
+^\[main\.assertion\.[0-9]+\] line [0-9]+ assertion argc == 1: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The main test is in test.desc; this just checks that the test is executable and
+the assertion fails as expected.

regression/cbmc/residual-guards-2/unreachable-code.desc

@@ -0,0 +1,9 @@
+FUTURE
+test.c
+--show-vcc --unwind 10
+^EXIT=0$
+^SIGNAL=0$
+--
+^\{-[0-9]+\} f::y!0@1#[0-9]+ = 10$
+--
+We also check that no VCC is created for the unreachable code 'y = 10;'

regression/cbmc/residual-guards-3/test.c

@@ -0,0 +1,19 @@
+void g(int x)
+{
+  return g(x + 1);
+}
+
+void f(int y)
+{
+  if(y == 5)
+  {
+    g(1);
+    y = 10;
+  }
+}
+
+int main(int argc, char **argv)
+{
+  f(argc);
+  assert(argc == 1);
+}

regression/cbmc/residual-guards-3/test.desc

@@ -0,0 +1,14 @@
+CORE paths-lifo-expected-failure
+test.c
+--show-vcc --depth 1000
+^\{1\} main::argc!0@1#1 = 1$
+^EXIT=0$
+^SIGNAL=0$
+--
+^\{-[0-9]+\} f::y!0@1#[0-9]+ = 10$
+--
+This checks that the assertion, argc == 1, is unguarded (i.e. is not of the form 
+'guard => condition'). Such a guard is redundant, but could be added before goto-symex
+made sure to restore guards to their state at function entry.
+We also check that no VCC is created for the unreachable code 'y = 10;'
+--paths mode is excluded as it currently always accrues large guards as it proceeds through execution

regression/cbmc/residual-guards-3/test_execution.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--depth 1000
+^\[main\.assertion\.[0-9]+\] line [0-9]+ assertion argc == 1: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The main test is in test.desc; this just checks that the test is executable and
+the assertion fails as expected.

regression/cbmc/residual-guards-4/test.c

@@ -0,0 +1,14 @@
+void f(int y)
+{
+  if(y == 5)
+  {
+    __CPROVER_assume(0);
+    y = 10;
+  }
+}
+
+int main(int argc, char **argv)
+{
+  f(argc);
+  assert(argc == 1);
+}

regression/cbmc/residual-guards-4/test.desc

@@ -0,0 +1,12 @@
+CORE paths-lifo-expected-failure
+test.c
+--show-vcc
+^\{1\} main::argc!0@1#1 = 1$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This checks that the assertion, argc == 1, is unguarded (i.e. is not of the form 
+'guard => condition'). Such a guard is redundant, but could be added before goto-symex
+made sure to restore guards to their state at function entry.
+--paths mode is excluded as it currently always accrues large guards as it proceeds through execution

regression/cbmc/residual-guards-4/test_execution.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+
+^\[main\.assertion\.[0-9]+\] line [0-9]+ assertion argc == 1: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The main test is in test.desc; this just checks that the test is executable and
+the assertion fails as expected.

regression/cbmc/residual-guards-4/unreachable-code.desc

@@ -0,0 +1,9 @@
+FUTURE
+test.c
+--show-vcc
+^EXIT=0$
+^SIGNAL=0$
+--
+^\{-[0-9]+\} f::y!0@1#[0-9]+ = 10$
+--
+We also check that no VCC is created for the unreachable code 'y = 10;'

src/goto-symex/call_stack.h

@@ -26,9 +26,10 @@ class call_stackt : public std::vector<framet>
     return back();
   }
 
-  framet &new_frame(symex_targett::sourcet calling_location)
+  framet &
+  new_frame(symex_targett::sourcet calling_location, const guardt &guard)
   {
-    emplace_back(calling_location);
+    emplace_back(calling_location, guard);
     return back();
   }
 

src/goto-symex/frame.h

@@ -27,7 +27,7 @@ struct framet
   std::map<goto_programt::const_targett, goto_state_listt> goto_state_map;
   symex_targett::sourcet calling_location;
   std::vector<irep_idt> parameter_names;
-
+  guardt guard_at_function_start;
   goto_programt::const_targett end_of_function;
   exprt return_value = nil_exprt();
   bool hidden_function = false;
@@ -48,8 +48,9 @@ struct framet
 
   std::unordered_map<irep_idt, loop_infot> loop_iterations;
 
-  explicit framet(symex_targett::sourcet _calling_location)
-    : calling_location(std::move(_calling_location))
+  framet(symex_targett::sourcet _calling_location, const guardt &state_guard)
+    : calling_location(std::move(_calling_location)),
+      guard_at_function_start(state_guard)
   {
   }
 };

src/goto-symex/goto_symex_state.cpp

@@ -44,7 +44,7 @@ goto_symex_statet::goto_symex_statet(
     fresh_l2_name_provider(fresh_l2_name_provider)
 {
   threads.emplace_back(guard_manager);
-  call_stack().new_frame(source);
+  call_stack().new_frame(source, guardt(true_exprt(), manager));
 }
 
 goto_symex_statet::~goto_symex_statet()=default;

src/goto-symex/symex_function_call.cpp

@@ -258,7 +258,10 @@ 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
+      // 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());
     }
 
@@ -303,7 +306,7 @@ void goto_symext::symex_function_call_code(
 
   // produce a new frame
   PRECONDITION(!state.call_stack().empty());
-  framet &frame = state.call_stack().new_frame(state.source);
+  framet &frame = state.call_stack().new_frame(state.source, state.guard);
 
   // preserve locality of local variables
   locality(identifier, state, path_storage, goto_function, ns);
@@ -332,8 +335,10 @@ void goto_symext::symex_function_call_code(
 }
 
 /// pop one call frame
-static void
-pop_frame(goto_symext::statet &state, const path_storaget &path_storage)
+static void pop_frame(
+  goto_symext::statet &state,
+  const path_storaget &path_storage,
+  bool doing_path_exploration)
 {
   PRECONDITION(!state.call_stack().empty());
 
@@ -347,6 +352,26 @@ pop_frame(goto_symext::statet &state, const path_storaget &path_storage)
     // restore L1 renaming
     state.level1.restore_from(frame.old_level1);
 
+    // If the program is multi-threaded then the state guard is used to
+    // 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`),
+    // 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)
+    {
+      state.guard = frame.guard_at_function_start;
+    }
+
     symex_renaming_levelt::viewt view;
     state.get_level2().current_names.get_view(view);
 
@@ -387,7 +412,7 @@ void goto_symext::symex_end_of_function(statet &state)
     state.guard.as_expr(), state.source.function_id, state.source, hidden);
 
   // then get rid of the frame
-  pop_frame(state, path_storage);
+  pop_frame(state, path_storage, symex_config.doing_path_exploration);
 }
 
 /// Preserves locality of parameters of a given function by applying L1

src/goto-symex/symex_goto.cpp

@@ -795,15 +795,16 @@ void goto_symext::loop_bound_exceeded(
         negated_cond,
         "unwinding assertion loop " + std::to_string(loop_number),
         state);
+    }
+
+    // generate unwinding assumption, unless we permit partial loops
+    symex_assume_l2(state, negated_cond);
 
+    if(symex_config.unwinding_assertions)
+    {
       // 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);
-    }
   }
 }
 

src/goto-symex/symex_main.cpp

@@ -528,7 +528,13 @@ void goto_symext::execute_next_instruction(
 
   // depth exceeded?
   if(symex_config.max_depth != 0 && state.depth > symex_config.max_depth)
+  {
+    // 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());
+  }
   state.depth++;
 
   // actually do instruction