Introduce randomized DFS

Randomized DFS shuffles the queue of successor states

Author: polgreen

src/symex/path_search.cpp

@@ -20,6 +20,27 @@ Author: Daniel Kroening, [email protected]
 #include <path-symex/path_symex.h>
 #include <path-symex/build_goto_trace.h>
 
+#include <random>
+
+void path_searcht::shuffle_queue(queuet &queue)
+{
+  if(queue.size()<=1)
+    return;
+
+  INVARIANT(queue.size()<std::numeric_limits<int>::max(),
+      "Queue size must be less than maximum integer");
+  // pick random state and move to front
+  int rand_i = rand() % queue.size();
+
+  std::list<statet>::iterator it = queue.begin();
+  for(int i=0; i<rand_i; i++)
+    it++;
+
+  statet tmp = *it;
+  queue.push_front(tmp);
+  queue.erase(it);
+}
+
 path_searcht::resultt path_searcht::operator()(
   const goto_functionst &goto_functions)
 {
@@ -142,6 +163,9 @@ path_searcht::resultt path_searcht::operator()(
       // execute
       path_symex(state, tmp_queue);
 
+      if(search_heuristic == search_heuristict::RAN_DFS)
+        shuffle_queue(tmp_queue);
+
       // put at head of main queue
       queue.splice(queue.begin(), tmp_queue);
     }
@@ -208,6 +232,7 @@ void path_searcht::pick_state()
   switch(search_heuristic)
   {
   case search_heuristict::DFS:
+  case search_heuristict::RAN_DFS:
     // Picking the first one (most recently added) is a DFS.
     return;
 

src/symex/path_search.h

@@ -107,6 +107,7 @@ class path_searcht:public safety_checkert
   };
 
   void set_dfs() { search_heuristic=search_heuristict::DFS; }
+  void set_randomized_dfs() { search_heuristic=search_heuristict::RAN_DFS; }
   void set_bfs() { search_heuristic=search_heuristict::BFS; }
   void set_locs() { search_heuristic=search_heuristict::LOCS; }
 
@@ -120,7 +121,9 @@ class path_searcht:public safety_checkert
   // The states most recently executed are at the head.
   typedef std::list<statet> queuet;
   queuet queue;
-
+  /// Pick random element of queue and move to front
+  /// \param queue  queue to be shuffled
+  void shuffle_queue(queuet &queue);
   // search heuristic
   void pick_state();
 
@@ -151,7 +154,8 @@ class path_searcht:public safety_checkert
   unsigned unwind_limit;
   unsigned time_limit;
 
-  enum class search_heuristict { DFS, BFS, LOCS } search_heuristic;
+  enum class search_heuristict
+  { DFS, RAN_DFS, BFS, LOCS } search_heuristic;
 
   source_locationt last_source_location;
 };

src/symex/symex_parse_options.cpp

@@ -210,7 +210,12 @@ int symex_parse_optionst::doit()
         safe_string2unsigned(cmdline.get_value("max-search-time")));
 
     if(cmdline.isset("dfs"))
-      path_search.set_dfs();
+    {
+      if(cmdline.isset("randomize"))
+        path_search.set_randomized_dfs();
+      else
+        path_search.set_dfs();
+    }
 
     if(cmdline.isset("bfs"))
       path_search.set_bfs();
@@ -627,6 +632,7 @@ void symex_parse_optionst::help()
     " --max-search-time s          limit search to approximately s seconds\n"
     " --dfs                        use depth first search\n"
     " --bfs                        use breadth first search\n"
+    " --randomize                  used in conjunction with dfs, to search by randomized dfs\n" // NOLINT(*)
     " --eager-infeasibility        query solver early to determine whether a path is infeasible before searching it\n" // NOLINT(*)
     "\n"
     "Other options:\n"

src/symex/symex_parse_options.h

@@ -39,6 +39,7 @@ class optionst;
   "(error-label):(verbosity):(no-library)" \
   "(version)" \
   "(bfs)(dfs)(locs)" \
+  "(randomize)" \
   "(cover):" \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
   "(ppc-macos)(unsigned-char)" \