Make new LIFO path exploration the default

This commits adds the "lifo" strategy, which explores program paths
using depth-first search. This is now the default strategy due to its
favourable memory consumption compared to other strategies; tests on a
few benchmarks show that its memory usage is basically constant and
comparable to regular model-checking, since this strategy finishes paths
as quickly as possible rather than saving them for later.

Author: karkhaz

regression/cbmc-path-strategies/if/lifo.in

@@ -0,0 +1,27 @@
+CORE
+main.c
+--paths lifo
+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
+any lines
+path is successful
+end

regression/cbmc-path-strategies/loop-functional-correctness/lifo.in

@@ -0,0 +1,42 @@
+CORE
+main.c
+--unwind 2 --paths lifo
+activate-multi-line-match
+SIGNAL=0
+EXIT=10
+--
+^warning: ignoring
+--
+Test that the following happens in order:
+execute line 6
+save next 7
+save jump 9
+any lines
+execute line 6
+
+// The path where we skip the loop body. Successful because the path is
+// implausible, we cannot have skipped the body if x == 1.
+resume jump 9
+execute line 9
+any lines
+path is successful
+
+// The path where we execute the body once. x is 0 after that, so
+// assertion failure.
+any lines
+execute line 6
+resume next 7
+any lines
+save next 7
+save jump 9
+any lines
+resume jump 9
+any lines
+path is unsuccessful
+
+// The path where we execute the body twice. Successful because infeasible
+any lines
+execute line 6
+resume next 7
+any lines
+path is successful

regression/cbmc-path-strategies/nested-if/lifo.in

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

regression/cbmc-path-strategies/simple-loop/lifo.in

@@ -0,0 +1,42 @@
+CORE
+main.c
+--unwind 2 --paths lifo
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+--
+^warning: ignoring
+--
+Test that the following happens in order:
+
+// skip the loop body
+save next 6
+save jump 8
+any lines
+execute line 4
+resume jump 8
+execute line 8
+any lines
+path is successful
+
+// execute loop body once
+any lines
+execute line 4
+resume next 6
+execute line 6
+any lines
+save next 6
+save jump 8
+any lines
+resume jump 8
+execute line 8
+any lines
+path is successful
+
+// execute loop body twice
+any lines
+execute line 4
+resume next 6
+execute line 6
+any lines
+path is successful

src/goto-symex/path_storage.cpp

@@ -13,6 +13,39 @@ Author: Kareem Khazem <[email protected]>
 #include <util/exit_codes.h>
 #include <util/make_unique.h>
 
+// _____________________________________________________________________________
+// path_lifot
+
+path_storaget::patht &path_lifot::private_peek()
+{
+  last_peeked = paths.end();
+  --last_peeked;
+  return paths.back();
+}
+
+void path_lifot::push(
+  const path_storaget::patht &next_instruction,
+  const path_storaget::patht &jump_target)
+{
+  paths.push_back(next_instruction);
+  paths.push_back(jump_target);
+}
+
+void path_lifot::private_pop()
+{
+  PRECONDITION(last_peeked != paths.end());
+  paths.erase(last_peeked);
+  last_peeked = paths.end();
+}
+
+std::size_t path_lifot::size() const
+{
+  return paths.size();
+}
+
+// _____________________________________________________________________________
+// path_fifot
+
 path_storaget::patht &path_fifot::private_peek()
 {
   return paths.front();
@@ -36,6 +69,9 @@ std::size_t path_fifot::size() const
   return paths.size();
 }
 
+// _____________________________________________________________________________
+// path_strategy_choosert
+
 std::string path_strategy_choosert::show_strategies() const
 {
   std::stringstream ss;
@@ -69,10 +105,19 @@ void path_strategy_choosert::set_path_strategy_options(
 
 path_strategy_choosert::path_strategy_choosert()
   : strategies(
-      {{"fifo",
+      {{"lifo",
+        {" lifo                         next instruction is pushed before\n"
+         "                              goto target; paths are popped in\n"
+         "                              last-in, first-out order. Explores\n"
+         "                              the program tree depth-first.\n",
+         []() { // NOLINT(whitespace/braces)
+           return util_make_unique<path_lifot>();
+         }}},
+       {"fifo",
         {" fifo                         next instruction is pushed before\n"
          "                              goto target; paths are popped in\n"
-         "                              first-in, first-out order\n",
+         "                              first-in, first-out order. Explores\n"
+         "                              the program tree breadth-first.\n",
          []() { // NOLINT(whitespace/braces)
            return util_make_unique<path_fifot>();
          }}}})

src/goto-symex/path_storage.h

@@ -84,6 +84,22 @@ class path_storaget
   virtual void private_pop() = 0;
 };
 
+/// \brief LIFO save queue: depth-first search, try to finish paths
+class path_lifot : public path_storaget
+{
+public:
+  void push(const patht &, const patht &) override;
+  std::size_t size() const override;
+
+protected:
+  std::list<path_storaget::patht>::iterator last_peeked;
+  std::list<patht> paths;
+
+private:
+  patht &private_peek() override;
+  void private_pop() override;
+};
+
 /// \brief FIFO save queue: paths are resumed in the order that they were saved
 class path_fifot : public path_storaget
 {
@@ -134,7 +150,7 @@ class path_strategy_choosert
 protected:
   std::string default_strategy() const
   {
-    return "fifo";
+    return "lifo";
   }
 
   /// Map from the name of a strategy (to be supplied on the command line), to