Make new LIFO path exploration the default

karkhaz · karkhaz · commit 85aba52313c0 · 2018-05-05T12:51:31.000+01:00
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.
diff --git a/src/goto-symex/path_storage.cpp b/src/goto-symex/path_storage.cpp
@@ -13,6 +13,39 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>
 #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>();
          }}}})
diff --git a/src/goto-symex/path_storage.h b/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
