Path exploration pushes both successors onto queue

When doing path exploration and encountering a conditional goto
instruction, both successors of the goto (the next instruction, and the
target) are pushed onto the path exploration workqueue. This allows the
symbolic execution caller to have complete control over which path to
execute next.

Prior to this commit, symex would push one successor onto the workqueue
and continue executing the path of the other successor until the path
was terminated. This commit introduces the possibility that symbolic
execution pauses without reaching the end of a path, and needs to be
resumed by the caller. Thus, new safety checker results are introduced
(SUSPENDED and UNKNOWN); the former signals to the caller of symex that
symex has not reached the end of a branch, and therefore no safety check
has been performed.

The (currently only) path exploration strategy still pops paths in the
order that they were pushed. This behaviour means that the paths that it
pops will always alternate between the next instruction of a goto, and
the target of that same goto. The test suite is updated to reflect this
strategy.

Author: karkhaz

regression/cbmc-path-fifo/Makefile

@@ -1,10 +1,10 @@
 default: tests.log
 
 test: gen-desc
-	@../test.pl -j 12 -p -c "../../../src/cbmc/cbmc --paths --verbosity 10"
+	@../test.pl -p -c "../../../src/cbmc/cbmc --paths fifo --verbosity 10"
 
 tests.log: ../test.pl gen-desc
-	@../test.pl -j 12 -p -c "../../../src/cbmc/cbmc --paths --verbosity 10"
+	@../test.pl -p -c "../../../src/cbmc/cbmc --paths fifo --verbosity 10"
 
 gen-desc:
 	@../../scripts/make_descs.py

regression/cbmc-path-fifo/if/test.in

@@ -7,16 +7,21 @@ SIGNAL=0
 --
 ^warning: ignoring
 --
+This tests that the next path is resumed before the jump path.
+
 Test that the following happens in order:
 execute line 4
-save line 7
+save next 5
+save jump 7
+any lines
+execute line 4
+resume next 5
 execute line 5
 any lines
 path is successful
 any lines
 execute line 4
-resume line 7
+resume jump 7
 execute line 7
 any lines
 path is successful
-end

regression/cbmc-path-fifo/loop-functional-correctness/main.c

@@ -1,7 +1,7 @@
 int main()
 {
   int x;
-  __CPROVER_assume(x > 0);
+  __CPROVER_assume(x == 1);
 
   while(x)
     --x;

regression/cbmc-path-fifo/loop-functional-correctness/test.in

@@ -7,25 +7,50 @@ EXIT=10
 --
 ^warning: ignoring
 --
-This tests the following:
-
-- Symex saves the path that traverses the loop once, then the path that
-  traverses the loop twice;
-
-- Symex pops the path that traverses the loop once, then the path that
-  traverses the loop twice.
+Test that the following happens in order:
+execute line 6
+// Enter loop
+save next 7
+// Skip loop
+save jump 9
+any lines
+execute line 6
+resume next 7
+execute line 7
+any lines
+// Enter loop twice
+save next 7
+// Enter loop once & bail
+save jump 9
 
-The path that traverses the loop twice is the one that would cause an
-assertion failure, thus that result must appear last rather than second
-last.
+// From this point on, we start hitting the end of paths.
 
-Test that the following happens in order:
-// Loop 0 times
+// The path where we skipped over the loop completely. The path is
+// nonsense, because we assume x == 1 and yet do not enter the loop;
+// thus the path is infeasible and verification succeeds.
+any lines
+execute line 6
+resume jump 9
+execute line 9
+any lines
 path is successful
+
+// The path where we enter the loop twice and then hit the assertion.
+// The path is infeasible because we cannot execute the loop twice if x
+// started out as 1.
+any lines
+execute line 6
+resume next 7
+execute line 7
 any lines
-// Loop once
 path is successful
+
+// The path where we enter the loop once and then bail out. Here, x has
+// been decremented to zero, so the assertion must fail.
+any lines
+execute line 6
+resume jump 9
+execute line 9
 any lines
-// Loop twice
 path is unsuccessful
 end

regression/cbmc-path-fifo/nested-if/test.in

@@ -9,29 +9,47 @@ SIGNAL=0
 --
 Test that the following happens in order:
 execute line 4
-save line 13
-execute line 6
-save line 9
-execute line 7
+save next 6
+save jump 13
+
 any lines
-path is successful
+execute line 4
+resume next 6
+execute line 6
+save next 7
+save jump 9
+
 any lines
 execute line 4
-resume line 13
+resume jump 13
 execute line 13
-save line 16
-execute line 14
+save next 14
+save jump 16
+
+any lines
+execute line 6
+resume next 7
+execute line 7
 any lines
 path is successful
+
 any lines
 execute line 6
-resume line 9
+resume jump 9
 execute line 9
 any lines
 path is successful
+
+any lines
+execute line 13
+resume next 14
+execute line 14
+any lines
+path is successful
+
 any lines
 execute line 13
-resume line 16
+resume jump 16
 execute line 16
 any lines
 path is successful

regression/cbmc-path-fifo/simple-loop/test.in

@@ -8,43 +8,39 @@ SIGNAL=0
 ^warning: ignoring
 --
 Test that the following happens in order:
-execute line 4
-//
-// Save that the loop condition was never satisfied
-//
-save line 8
-execute line 6
+save next 6
+save jump 8
 any lines
 execute line 4
-unwind
-//
-// Save that the loop condition was satisfied once but not twice
-//
-save line 8
+resume next 6
 execute line 6
+
+// Now go back to the top of the loop
 any lines
-//
-// Escape the loop
-//
-execute line 8
+save next 6
+save jump 8
+
+// Before doing the instructions that assume we've already been through
+// the loop once, explore the path corresponding to never having been
+// through the loop
+any lines
+execute line 4
+resume jump 8
 any lines
 path is successful
-//
-// Now do the first break out of the loop...
-//
+
+// Enter loop twice
 any lines
 execute line 4
-resume line 8
-execute line 8
+resume next 6
+execute line 6
 any lines
 path is successful
-//
-// ...and the second.
-//
+
+// Bail out after having entered loop once
 any lines
 execute line 4
-resume line 8
+resume jump 8
 execute line 8
 any lines
 path is successful
-end

scripts/make_descs.py

@@ -99,16 +99,28 @@ def interpret(command_list, in_file):
                     % int(m.group("l")))
             continue
 
-        m = re.match(r"^save line (?P<l>\d+)$", line)
+        m = re.match(r"^save jump (?P<l>\d+)$", line)
         if m:
-            ret += ("Saving 'file[^\\n]+line %d function \\w+'\\n"
+            ret += ("Saving jump target 'file[^\\n]+line %d function \\w+'\\n"
                     % int(m.group("l")))
             continue
 
-        m = re.match(r"^resume line (?P<l>\d+)$", line)
+        m = re.match(r"^save next (?P<l>\d+)$", line)
         if m:
-            ret += ("Resuming from 'file[^\\n]+line %d function \\w+'\\n"
-                    % int(m.group("l")))
+            ret += ("Saving next instruction 'file[^\\n]+line %d function "
+                    "\\w+'\\n" % int(m.group("l")))
+            continue
+
+        m = re.match(r"^resume next (?P<l>\d+)$", line)
+        if m:
+            ret += ("Resuming from next instruction 'file[^\\n]+line %d "
+                    "function \\w+'\\n" % int(m.group("l")))
+            continue
+
+        m = re.match(r"^resume jump (?P<l>\d+)$", line)
+        if m:
+            ret += ("Resuming from jump target 'file[^\\n]+line %d function "
+                    "\\w+'\\n" % int(m.group("l")))
             continue
 
         m = re.match(r"^unwind$", line)

src/cbmc/bmc.cpp

@@ -362,6 +362,8 @@ safety_checkert::resultt bmct::execute(const goto_functionst &goto_functions)
   try
   {
     perform_symbolic_execution(goto_functions);
+    if(symex.states_pushed)
+      return safety_checkert::resultt::SUSPENDED;
 
     // add a partial ordering, if required
     if(equation.has_threads())
@@ -603,7 +605,7 @@ int bmct::do_language_agnostic_bmc(
   std::function<void(bmct &, const goto_modelt &)> frontend_configure_bmc)
 {
   message_handlert &mh = message.get_message_handler();
-  safety_checkert::resultt result;
+  safety_checkert::resultt final_result = safety_checkert::resultt::UNKNOWN;
   std::unique_ptr<path_storaget> worklist = path_storaget::make(
     path_storaget::disciplinet::FIFO);
   try
@@ -618,7 +620,10 @@ int bmct::do_language_agnostic_bmc(
       bmct bmc(opts, goto_model.symbol_table, mh, pc, *worklist);
       bmc.set_ui(ui);
       frontend_configure_bmc(bmc, goto_model);
-      result = bmc.run(goto_model.goto_functions);
+      const safety_checkert::resultt tmp_result =
+        bmc.run(goto_model.goto_functions);
+      if(tmp_result != safety_checkert::resultt::SUSPENDED)
+        final_result = tmp_result;
     }
     INVARIANT(
       opts.get_bool_option("paths") || worklist->empty(),
@@ -627,8 +632,8 @@ int bmct::do_language_agnostic_bmc(
         std::to_string(worklist->size()) + " unexplored branches.");
 
     // When model checking, the bmc.run() above will already have explored
-    // the entire program, and result contains the verification result. The
-    // worklist (containing paths that have not yet been explored) is thus
+    // the entire program, and final_result contains the verification result.
+    // The worklist (containing paths that have not yet been explored) is thus
     // empty, and we don't enter this loop.
     //
     // When doing path exploration, there will be some saved paths left to
@@ -663,7 +668,10 @@ int bmct::do_language_agnostic_bmc(
         resume.state,
         *worklist);
       frontend_configure_bmc(pe, goto_model);
-      result &= pe.run(goto_model.goto_functions);
+      const safety_checkert::resultt tmp_result =
+        pe.run(goto_model.goto_functions);
+      if(tmp_result != safety_checkert::resultt::SUSPENDED)
+        final_result &= tmp_result;
       worklist->pop();
     }
   }
@@ -683,14 +691,18 @@ int bmct::do_language_agnostic_bmc(
     throw std::current_exception();
   }
 
-  switch(result)
+  switch(final_result)
   {
   case safety_checkert::resultt::SAFE:
     return CPROVER_EXIT_VERIFICATION_SAFE;
   case safety_checkert::resultt::UNSAFE:
     return CPROVER_EXIT_VERIFICATION_UNSAFE;
   case safety_checkert::resultt::ERROR:
     return CPROVER_EXIT_INTERNAL_ERROR;
+  case safety_checkert::resultt::UNKNOWN:
+    return CPROVER_EXIT_INTERNAL_ERROR;
+  case safety_checkert::resultt::SUSPENDED:
+    UNREACHABLE;
   }
   UNREACHABLE;
 }