Shortest path search heuristic

Shortest path search heuristic computes the shortest path from all program locations to a single property. This metric is used to guide the symex search.

We also introduce randomized shortest path based search, which makes a random choice when picking the next state every 1000 choices in order to avoid local minima

Author: polgreen

src/symex/path_search.cpp

@@ -20,8 +20,51 @@ Author: Daniel Kroening, [email protected]
 #include <path-symex/path_symex.h>
 #include <path-symex/build_goto_trace.h>
 
+#include "shortest_path_graph.h"
+
 #include <random>
 
+
+void path_searcht::sort_queue()
+{
+  debug()<< " get shortest path, queue.size = " <<queue.size() <<eom;
+  if(queue.size()==1)
+  {
+    current_distance = queue.front().get_shortest_path();
+    return;
+  }
+
+  unsigned shortest_path = std::numeric_limits<unsigned>::max();
+
+  std::list<statet>::iterator it;
+  std::list<statet>::iterator closest_state;
+
+  for(it=queue.begin(); it!=queue.end(); ++it)
+  {
+    if(it->get_shortest_path() < shortest_path)
+    {
+      shortest_path = it->get_shortest_path();
+      closest_state = it;
+    }
+  }
+
+  if(shortest_path != std::numeric_limits<unsigned>::max())
+  {
+    current_distance = shortest_path;
+    statet tmp = *closest_state;
+    queue.erase(closest_state);
+    queue.push_front(tmp);
+  }
+  else
+  {
+    error() << "all states have shortest path length = MAX_UNSIGNED_INT, "
+             << "try removing function pointers with goto-instrument next time."
+             << "randomly picking state instead"
+             << eom;
+    shuffle_queue(queue);
+  }
+}
+
 void path_searcht::shuffle_queue(queuet &queue)
 {
   if(queue.size()<=1)
@@ -54,9 +97,8 @@ path_searcht::resultt path_searcht::operator()(
   // this is the container for the history-forest
   path_symex_historyt history;
 
-  queue.push_back(initial_state(var_map, locs, history));
-
   // set up the statistics
+  current_distance = std::numeric_limits<unsigned>::max();
   number_of_dropped_states=0;
   number_of_paths=0;
   number_of_VCCs=0;
@@ -72,6 +114,15 @@ path_searcht::resultt path_searcht::operator()(
   absolute_timet last_reported_time=start_time;
 
   initialize_property_map(goto_functions);
+  if(search_heuristic == search_heuristict::SHORTEST_PATH ||
+      search_heuristic == search_heuristict::RAN_SHORTEST_PATH )
+  {
+    status()<<"Building shortest path graph" << eom;
+    shortest_path_grapht shortest_path_graph(goto_functions, locs);
+  }
+  statet init_state = initial_state(var_map, locs, history);
+  queue.push_back(init_state);
+  initial_distance_to_property=init_state.get_shortest_path();
 
   while(!queue.empty())
   {
@@ -135,8 +186,13 @@ path_searcht::resultt path_searcht::operator()(
                    << " thread " << state.get_current_thread()+1
                    << '/' << state.threads.size()
                    << " PC " << state.pc()
-                   << " depth " << state.get_depth()
-                   << " [" << number_of_steps << " steps, "
+                   << " depth " << state.get_depth();
+
+          if(search_heuristic == search_heuristict::SHORTEST_PATH
+              || search_heuristic == search_heuristict::RAN_SHORTEST_PATH)
+            status() << " distance to property " << state.get_shortest_path();
+
+          status() << " [" << number_of_steps << " steps, "
                    << running_time << "s]" << messaget::eom;
         }
       }
@@ -243,6 +299,15 @@ void path_searcht::pick_state()
       queue.splice(queue.begin(), queue, --queue.end(), queue.end());
     return;
 
+  case search_heuristict::RAN_SHORTEST_PATH:
+    if(number_of_steps%1000==0)
+      shuffle_queue(queue);
+    else
+      sort_queue();
+    return;
+  case search_heuristict::SHORTEST_PATH:
+    sort_queue();
+    return;
   case search_heuristict::LOCS:
     return;
   }

src/symex/path_search.h

@@ -80,6 +80,8 @@ class path_searcht:public safety_checkert
   bool stop_on_fail;
 
   // statistics
+  unsigned current_distance;
+  unsigned initial_distance_to_property;
   std::size_t number_of_dropped_states;
   std::size_t number_of_paths;
   std::size_t number_of_steps;
@@ -110,6 +112,10 @@ class path_searcht:public safety_checkert
   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; }
+  void set_shortest_path()
+    { search_heuristic=search_heuristict::SHORTEST_PATH; }
+  void set_ran_shortest_path()
+    { search_heuristic=search_heuristict::RAN_SHORTEST_PATH; }
 
   typedef std::map<irep_idt, property_entryt> property_mapt;
   property_mapt property_map;
@@ -124,6 +130,9 @@ class path_searcht:public safety_checkert
   /// Pick random element of queue and move to front
   /// \param queue  queue to be shuffled
   void shuffle_queue(queuet &queue);
+  /// Move element with shortest distance to property
+  /// to the front of the queue
+  void sort_queue();
   // search heuristic
   void pick_state();
 
@@ -155,7 +164,7 @@ class path_searcht:public safety_checkert
   unsigned time_limit;
 
   enum class search_heuristict
-  { DFS, RAN_DFS, BFS, LOCS } search_heuristic;
+  { DFS, RAN_DFS, BFS, LOCS, SHORTEST_PATH, RAN_SHORTEST_PATH } search_heuristic;
 
   source_locationt last_source_location;
 };

src/symex/symex_parse_options.cpp

@@ -236,6 +236,13 @@ int symex_parse_optionst::doit()
     if(cmdline.isset("locs"))
       path_search.set_locs();
 
+    if(cmdline.isset("shortest-path"))
+    {
+      if(cmdline.isset("randomize"))
+        path_search.set_ran_shortest_path();
+      else
+        path_search.set_shortest_path();
+    }
     if(cmdline.isset("show-vcc"))
     {
       path_search.show_vcc=true;
@@ -645,7 +652,9 @@ 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(*)
+    "--shortest-path               use shortest path guided search\n"
+    " --randomize                  in conjunction with dfs to use randomized dfs\n" // NOLINT(*)
+	  "                              in conjunction with shortest path to use randomized shortest path guided search\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

@@ -38,7 +38,7 @@ class optionst;
   "(little-endian)(big-endian)" \
   "(error-label):(verbosity):(no-library)" \
   "(version)" \
-  "(bfs)(dfs)(locs)" \
+  "(bfs)(dfs)(locs)(shortest-path)" \
   "(randomize)" \
   "(cover):" \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \