Add progressive path exploration strategy

Path exploration can now be run with a new strategy: "progressive-fifo".
This strategy prefers to pop the jumps of a goto instruction rather than
the next instruction. This is intended to make forward progress through
a program rather than dwelling on loops. This commit adds tests for this
strategy also.

A new class is introduced to hold the names, descriptions and
constructor thunks for all path exploration strategies. This provides a
uniform way for strategy descriptions to be displayed, which can be done
with the --show-symex-strategies flag.

Author: karkhaz

.gitignore

@@ -59,6 +59,7 @@ regression/**/*.smt2
 
 # These files are generated from the test.in file in their directories
 regression/cbmc-path-fifo/*/test.desc
+regression/cbmc-path-progressive/*/test.desc
 
 # files stored by editors
 *~

regression/cbmc-path-progressive/Makefile

@@ -0,0 +1,23 @@
+default: tests.log
+
+test: gen-desc
+	@../test.pl -p -c "../../../src/cbmc/cbmc --paths progressive-fifo --verbosity 10"
+
+tests.log: ../test.pl gen-desc
+	@../test.pl -p -c "../../../src/cbmc/cbmc --paths progressive-fifo --verbosity 10"
+
+gen-desc:
+	@../../scripts/make_descs.py
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name 'test.desc' -execdir $(RM) '{}' \;
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/cbmc-path-progressive/if/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  int x;
+  if(x)
+    x = 1;
+  else
+    x = 0;
+}

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

@@ -0,0 +1,27 @@
+CORE
+main.c
+
+activate-multi-line-match
+EXIT=0
+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 next 5
+save jump 7
+any lines
+execute line 4
+resume jump 7
+execute line 7
+any lines
+path is successful
+any lines
+execute line 4
+resume next 5
+execute line 5
+any lines
+path is successful

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

@@ -0,0 +1,10 @@
+int main()
+{
+  int x;
+  __CPROVER_assume(x == 1);
+
+  while(x)
+    --x;
+
+  assert(x);
+}

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

@@ -0,0 +1,56 @@
+CORE
+main.c
+--unwind 2
+activate-multi-line-match
+SIGNAL=0
+EXIT=10
+--
+^warning: ignoring
+--
+This strategy differs from 'fifo' because the failed path is the second
+one, not the last one.
+
+Test that the following happens in order:
+execute line 6
+save next 7
+save jump 9
+
+// We skip the loop first with this strategy. This path is infeasible,
+// since x is 1 so we must have entered the loop; so the solver is happy.
+any lines
+execute line 6
+resume jump 9
+execute line 9
+any lines
+path is successful
+
+// We now enter the loop and execute it; we then save "entering the loop
+// twice" and "bailing out after the first spin".
+any lines
+execute line 6
+resume next 7
+execute line 7
+any lines
+save next 7
+save jump 9
+
+// Since the just saved "bailing out after the first spin" is a jump,
+// execute that path. That path makes the assertion fail, since we
+// decremented x from 1 to 0.
+any lines
+execute line 6
+resume jump 9
+execute line 9
+any lines
+path is unsuccessful
+
+// Finally, execute "entering the loop twice". This path is infeasible
+// because we cannot actually have entered the loop twice if x was only
+// 1 to begin with, so the solver is happy.
+any lines
+execute line 6
+resume next 7
+execute line 7
+any lines
+path is successful
+end

regression/cbmc-path-progressive/nested-if/main.c

@@ -0,0 +1,18 @@
+int main()
+{
+  int x, y;
+  if(x)
+  {
+    if(y)
+      y = 1;
+    else
+      y = 0;
+  }
+  else
+  {
+    if(y)
+      y = 1;
+    else
+      y = 0;
+  }
+}

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

@@ -0,0 +1,56 @@
+CORE
+main.c
+
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+--
+^warning: ignoring
+--
+Test that the following happens in order:
+execute line 4
+save next 6
+save jump 13
+
+any lines
+execute line 4
+resume jump 13
+execute line 13
+save next 14
+save jump 16
+
+any lines
+execute line 13
+resume jump 16
+execute line 16
+any lines
+path is successful
+
+any lines
+execute line 4
+resume next 6
+execute line 6
+save next 7
+save jump 9
+
+any lines
+execute line 6
+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 6
+resume next 7
+execute line 7
+any lines
+path is successful
+end

regression/cbmc-path-progressive/simple-loop/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  int x;
+  while(x)
+  {
+    int y;
+  }
+  int y;
+}

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

@@ -0,0 +1,47 @@
+CORE
+main.c
+--unwind 2
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+--
+^warning: ignoring
+--
+Test that the following happens in order:
+execute line 4
+save next 6
+save jump 8
+
+// Bail out without having entered loop, ever
+any lines
+execute line 4
+resume jump 8
+execute line 8
+any lines
+path is successful
+
+// Enter loop body for the first time
+any lines
+execute line 4
+resume next 6
+execute line 6
+any lines
+save next 6
+save jump 8
+
+// Bail out after executing loop once
+any lines
+execute line 4
+resume jump 8
+execute line 8
+any lines
+path is successful
+
+// Execute loop for the second time
+any lines
+execute line 4
+resume next 6
+execute line 6
+any lines
+path is successful
+end

src/cbmc/bmc.cpp

@@ -598,6 +598,7 @@ void bmct::setup_unwind()
 }
 
 int bmct::do_language_agnostic_bmc(
+  const path_strategy_choosert &path_strategy_chooser,
   const optionst &opts,
   const goto_modelt &goto_model,
   const ui_message_handlert::uit &ui,
@@ -606,8 +607,12 @@ int bmct::do_language_agnostic_bmc(
 {
   message_handlert &mh = message.get_message_handler();
   safety_checkert::resultt final_result = safety_checkert::resultt::UNKNOWN;
-  std::unique_ptr<path_storaget> worklist = path_storaget::make(
-    path_storaget::disciplinet::FIFO);
+  std::unique_ptr<path_storaget> worklist;
+  std::string strategy = opts.get_option("exploration-strategy");
+  INVARIANT(
+    path_strategy_chooser.is_valid_strategy(strategy),
+    "Front-end passed us invalid path strategy '" + strategy + "'");
+  worklist = path_strategy_chooser.get(strategy);
   try
   {
     {

src/cbmc/bmc.h

@@ -130,6 +130,7 @@ class bmct:public safety_checkert
   /// function object will be called with every \ref bmct object that
   /// is constructed by `do_language_agnostic_bmc`.
   static int do_language_agnostic_bmc(
+    const path_strategy_choosert &path_strategy_chooser,
     const optionst &opts,
     const goto_modelt &goto_model,
     const ui_message_handlert::uit &ui,
@@ -299,15 +300,17 @@ class path_explorert : public bmct
   "(no-unwinding-assertions)"                                                  \
   "(no-pretty-names)"                                                          \
   "(partial-loops)"                                                            \
-  "(paths)"                                                                    \
+  "(paths):"                                                                   \
+  "(show-symex-strategies)"                                                    \
   "(depth):"                                                                   \
   "(unwind):"                                                                  \
   "(unwindset):"                                                               \
   "(graphml-witness):"                                                         \
   "(unwindset):"
 
 #define HELP_BMC                                                               \
-  " --paths                      explore paths one at a time\n"                \
+  " --paths [strategy]           explore paths one at a time\n"                \
+  " --show-symex-strategies      list strategies for use with --paths\n"       \
   " --program-only               only show program expression\n"               \
   " --show-loops                 show the loops in the program\n"              \
   " --depth nr                   limit search depth\n"                         \

src/cbmc/cbmc_parse_options.cpp

@@ -69,7 +69,8 @@ cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):
   parse_options_baset(CBMC_OPTIONS, argc, argv),
   xml_interfacet(cmdline),
   messaget(ui_message_handler),
-  ui_message_handler(cmdline, "CBMC " CBMC_VERSION)
+  ui_message_handler(cmdline, "CBMC " CBMC_VERSION),
+  path_strategy_chooser()
 {
 }
 
@@ -80,7 +81,8 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
   parse_options_baset(CBMC_OPTIONS+extra_options, argc, argv),
   xml_interfacet(cmdline),
   messaget(ui_message_handler),
-  ui_message_handler(cmdline, "CBMC " CBMC_VERSION)
+  ui_message_handler(cmdline, "CBMC " CBMC_VERSION),
+  path_strategy_chooser()
 {
 }
 
@@ -107,8 +109,13 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
-  if(cmdline.isset("paths"))
-    options.set_option("paths", true);
+  if(cmdline.isset("show-symex-strategies"))
+  {
+    std::cout << path_strategy_chooser.show_strategies();
+    exit(CPROVER_EXIT_SUCCESS);
+  }
+
+  path_strategy_chooser.set_path_strategy_options(cmdline, options, *this);
 
   if(cmdline.isset("program-only"))
     options.set_option("program-only", true);
@@ -543,7 +550,11 @@ int cbmc_parse_optionst::doit()
     return CPROVER_EXIT_SET_PROPERTIES_FAILED;
 
   return bmct::do_language_agnostic_bmc(
-    options, goto_model, ui_message_handler.get_ui(), *this);
+    path_strategy_chooser,
+    options,
+    goto_model,
+    ui_message_handler.get_ui(),
+    *this);
 }
 
 bool cbmc_parse_optionst::set_properties()

src/cbmc/cbmc_parse_options.h

@@ -93,6 +93,7 @@ class cbmc_parse_optionst:
 protected:
   goto_modelt goto_model;
   ui_message_handlert ui_message_handler;
+  const path_strategy_choosert path_strategy_chooser;
 
   void eval_verbosity();
   void register_languages();