Add path strategy chooser class

karkhaz · karkhaz · commit 17951c86c3ee · 2018-05-05T12:51:31.000+01:00
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.
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
@@ -598,6 +598,7 @@ void bmct::setup_unwind()
 /// \param callback_after_symex: optional callback to be run after symex.
 ///   See class member `bmct::driver_callback_after_symex` for details.
 int bmct::do_language_agnostic_bmc(
+  const path_strategy_choosert &path_strategy_chooser,
   const optionst &opts,
   abstract_goto_modelt &model,
   const ui_message_handlert::uit &ui,
@@ -609,8 +610,12 @@ int bmct::do_language_agnostic_bmc(
   safety_checkert::resultt tmp_result = safety_checkert::resultt::UNKNOWN;
   const symbol_tablet &symbol_table = model.get_symbol_table();
   message_handlert &mh = message.get_message_handler();
-  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
   {
     {
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
@@ -117,6 +117,7 @@ class bmct:public safety_checkert
   }
 
   static int do_language_agnostic_bmc(
+    const path_strategy_choosert &path_strategy_chooser,
     const optionst &opts,
     abstract_goto_modelt &goto_model,
     const ui_message_handlert::uit &ui,
@@ -294,15 +295,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"                         \
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -68,7 +68,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()
 {
 }
 
@@ -79,7 +80,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()
 {
 }
 
@@ -146,8 +148,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);
@@ -531,7 +538,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()
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
@@ -110,6 +110,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();
diff --git a/src/goto-symex/path_storage.cpp b/src/goto-symex/path_storage.cpp
@@ -8,16 +8,10 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>
 
 #include "path_storage.h"
 
-std::unique_ptr<path_storaget>
-path_storaget::make(path_storaget::disciplinet discipline)
-{
-  switch(discipline)
-  {
-  case path_storaget::disciplinet::FIFO:
-    return std::unique_ptr<path_fifot>(new path_fifot());
-  }
-  UNREACHABLE;
-}
+#include <sstream>
+
+#include <util/exit_codes.h>
+#include <util/make_unique.h>
 
 path_storaget::patht &path_fifot::private_peek()
 {
@@ -41,3 +35,46 @@ std::size_t path_fifot::size() const
 {
   return paths.size();
 }
+
+std::string path_strategy_choosert::show_strategies() const
+{
+  std::stringstream ss;
+  for(auto &pair : strategies)
+    ss << pair.second.first;
+  return ss.str();
+}
+
+void path_strategy_choosert::set_path_strategy_options(
+  const cmdlinet &cmdline,
+  optionst &options,
+  messaget &message) const
+{
+  if(cmdline.isset("paths"))
+  {
+    options.set_option("paths", true);
+    std::string strategy = cmdline.get_value("paths");
+    if(!is_valid_strategy(strategy))
+    {
+      message.error() << "Unknown strategy '" << strategy
+                      << "'. Pass the --show-symex-strategies flag to list "
+                         "available strategies."
+                      << message.eom;
+      exit(CPROVER_EXIT_USAGE_ERROR);
+    }
+    options.set_option("exploration-strategy", strategy);
+  }
+  else
+    options.set_option("exploration-strategy", default_strategy());
+}
+
+path_strategy_choosert::path_strategy_choosert()
+  : strategies(
+      {{"fifo",
+        {" fifo                         next instruction is pushed before\n"
+         "                              goto target; paths are popped in\n"
+         "                              first-in, first-out order\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
@@ -8,6 +8,11 @@
 #include "goto_symex_state.h"
 #include "symex_target_equation.h"
 
+#include <util/options.h>
+#include <util/cmdline.h>
+#include <util/ui_message.h>
+#include <util/invariant.h>
+
 #include <memory>
 
 /// \brief Storage for symbolic execution paths to be resumed later
@@ -19,13 +24,6 @@
 class path_storaget
 {
 public:
-  /// \brief Derived types of path_storaget
-  enum class disciplinet
-  {
-    /// path_fifot
-    FIFO
-  };
-
   /// \brief Information saved at a conditional goto to resume execution
   struct patht
   {
@@ -43,8 +41,6 @@ class path_storaget
     }
   };
 
-  /// \brief Factory method for building a subtype of path_storaget
-  static std::unique_ptr<path_storaget> make(disciplinet discipline);
   virtual ~path_storaget() = default;
 
   /// \brief Reference to the next path to resume
@@ -103,4 +99,51 @@ class path_fifot : public path_storaget
   void private_pop() override;
 };
 
+/// \brief Factory and information for path_storaget
+class path_strategy_choosert
+{
+public:
+  path_strategy_choosert();
+
+  /// \brief suitable for displaying as a front-end help message
+  std::string show_strategies() const;
+
+  /// \brief is there a factory constructor for the named strategy?
+  bool is_valid_strategy(const std::string strategy) const
+  {
+    return strategies.find(strategy) != strategies.end();
+  }
+
+  /// \brief Factory for a path_storaget
+  ///
+  /// Ensure that path_strategy_choosert::is_valid_strategy() returns true for a
+  /// particular string before calling this function on that string.
+  std::unique_ptr<path_storaget> get(const std::string strategy) const
+  {
+    auto found = strategies.find(strategy);
+    INVARIANT(
+      found != strategies.end(), "Unknown strategy '" + strategy + "'.");
+    return found->second.second();
+  }
+
+  /// \brief add `paths` and `exploration-strategy` option, suitable to be
+  /// invoked from front-ends.
+  void
+  set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const;
+
+protected:
+  std::string default_strategy() const
+  {
+    return "fifo";
+  }
+
+  /// Map from the name of a strategy (to be supplied on the command line), to
+  /// the help text for that strategy and a factory thunk returning a pointer to
+  /// a derived class of path_storaget that implements that strategy.
+  std::map<const std::string,
+           std::pair<const std::string,
+                     const std::function<std::unique_ptr<path_storaget>()>>>
+    strategies;
+};
+
 #endif /* CPROVER_GOTO_SYMEX_PATH_STORAGE_H */
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 #include <memory>
 
+#include <util/exit_codes.h>
 #include <util/string2int.h>
 #include <util/config.h>
 #include <util/unicode.h>
@@ -63,7 +64,8 @@ Author: Daniel Kroening, kroening@kroening.com
 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv):
   parse_options_baset(JBMC_OPTIONS, argc, argv),
   messaget(ui_message_handler),
-  ui_message_handler(cmdline, "JBMC " CBMC_VERSION)
+  ui_message_handler(cmdline, "JBMC " CBMC_VERSION),
+  path_strategy_chooser()
 {
 }
 
@@ -73,7 +75,8 @@ ::jbmc_parse_optionst::jbmc_parse_optionst(
   const std::string &extra_options):
   parse_options_baset(JBMC_OPTIONS+extra_options, argc, argv),
   messaget(ui_message_handler),
-  ui_message_handler(cmdline, "JBMC " CBMC_VERSION)
+  ui_message_handler(cmdline, "JBMC " CBMC_VERSION),
+  path_strategy_chooser()
 {
 }
 
@@ -100,6 +103,14 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(1); // should contemplate EX_USAGE from sysexits.h
   }
 
+  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);
 
@@ -533,7 +544,12 @@ int jbmc_parse_optionst::doit()
     // The `configure_bmc` callback passed will enable enum-unwind-static if
     // applicable.
     return bmct::do_language_agnostic_bmc(
-      options, goto_model, ui_message_handler.get_ui(), *this, configure_bmc);
+      path_strategy_chooser,
+      options,
+      goto_model,
+      ui_message_handler.get_ui(),
+      *this,
+      configure_bmc);
   }
   else
   {
@@ -573,6 +589,7 @@ int jbmc_parse_optionst::doit()
     // applicable.
     return
       bmct::do_language_agnostic_bmc(
+        path_strategy_chooser,
         options,
         lazy_goto_model,
         ui_message_handler.get_ui(),
diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h
@@ -27,6 +27,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/show_properties.h>
 #include <goto-instrument/cover.h>
 
+#include <goto-symex/path_storage.h>
+
 #include <java_bytecode/java_bytecode_language.h>
 
 class bmct;
@@ -103,6 +105,7 @@ class jbmc_parse_optionst:
 protected:
   ui_message_handlert ui_message_handler;
   std::unique_ptr<cover_configt> cover_config;
+  path_strategy_choosert path_strategy_chooser;
 
   void eval_verbosity();
   void get_command_line_options(optionst &);
