Symex: restore guards on function exit

Executing a function may have a cumulative effect on the state guard. For example, if the
callee contained ASSUME statements that rendered one or more control-flow options unviable
then the guard might still embody that restriction (i.e. for if(x) ASSUME(false) the guard might
still be `!x`). However, on function return we know that all control-flow paths have converged
or been shown to be unviable, so we can restore the simpler guard as it was when we entered
the callee function.

Exceptions:
(a) if the guard is false it would be correct but inefficient to restore it; keep it false until
    we find a convergeance with another viable path
(b) if we're doing path-sensitive symex then we do tail duplication, and there are no control-flow
    convergeances. Keep the guard as-was.
(c) if we're executing a multi-threaded program then symex_assume_l2 uses the guard to accumulate
    assumptions, which we must not discard.

In truth this optimisation is applicable whenever a block postdominates another, but function
structure gives us a cheap way to establish postdominance without analysis (in the absence of
setjmp/longjmp at least)

Author: smowton

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

@@ -303,7 +303,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 +332,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 +349,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 +409,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