Shortest path search heuristic

src/path-symex/locs.cpp

@@ -82,23 +82,60 @@ void locst::build(const goto_functionst &goto_functions)
   }
 }
 
+void locst::output_reachable(std::ostream &out) const
+{
+  irep_idt function;
+  int reachable_count = 0;
+  int unreachable_count = 0;
+
+  for(unsigned l = 0; l < loc_vector.size(); l++)
+  {
+    const loct &loc = loc_vector[l];
+    if(loc.distance_to_property != -1)
+    {
+      reachable_count++;
+      if(function != loc.function)
+      {
+        function = loc.function;
+        out << "*** " << function << "\n";
+      }
+
+      out << "  L" << l << ": " << " " << as_string(ns, *loc.target)
+          << " path length: " << loc_vector[l].distance_to_property << "\n";
+
+      if(!loc.branch_target.is_nil())
+        out << "    T: " << loc.branch_target << "\n";
+    }
+    else
+      unreachable_count++;
+  }
+  out << "\n";
+  out << "The entry location is L" << entry_loc << ".\n";
+  out << "Number of reachable locs " << reachable_count << "\n";
+  out << "Number of unreachable locs " << unreachable_count << "\n";
+}
+
 void locst::output(std::ostream &out) const
 {
   irep_idt function;
 
-  for(unsigned l=0; l<loc_vector.size(); l++)
+  for(std::size_t l = 0; l < loc_vector.size(); l++)
   {
-    const loct &loc=loc_vector[l];
-    if(function!=loc.function)
+    const loct &loc = loc_vector[l];
+    if(function != loc.function)
     {
-      function=loc.function;
+      function = loc.function;
       out << "*** " << function << "\n";
     }
 
     out << "  L" << l << ": "
 //        << loc.target->type << " "
 //        << loc.target->location
-        << " " << as_string(ns, *loc.target) << "\n";
+        << " " << as_string(ns, *loc.target);
+    if(loc_vector[l].distance_to_property
+        != std::numeric_limits<std::size_t>::max())
+      out << " path length: " << loc_vector[l].distance_to_property;
+    out << "\n";
 
     if(!loc.branch_target.is_nil())
       out << "    T: " << loc.branch_target << "\n";

src/path-symex/locs.h

@@ -27,11 +27,12 @@ struct loct
     target(_target),
     function(_function)
   {
+    distance_to_property=std::numeric_limits<std::size_t>::max();
   }
 
   goto_programt::const_targett target;
   irep_idt function;
-
+  std::size_t distance_to_property;
   // we only support a single branch target
   loc_reft branch_target;
 };
@@ -58,6 +59,7 @@ class locst
   explicit locst(const namespacet &_ns);
   void build(const goto_functionst &goto_functions);
   void output(std::ostream &out) const;
+  void output_reachable(std::ostream &out) const;
 
   loct &operator[] (loc_reft l)
   {

src/path-symex/path_symex_state.h

@@ -208,6 +208,11 @@ struct path_symex_statet
     return depth;
   }
 
+  unsigned get_shortest_path() const
+  {
+    return locs.loc_vector[pc().loc_number].distance_to_property;
+  }
+
   void increase_depth()
   {
     depth++;

src/symex/Makefile

@@ -2,6 +2,7 @@ SRC = path_search.cpp \
       symex_cover.cpp \
       symex_main.cpp \
       symex_parse_options.cpp \
+      shortest_path_graph.cpp \
       # Empty last line
 
 OBJ += ../../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \

src/symex/path_search.cpp

@@ -20,6 +20,106 @@ 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);
+  }
+}
+
+// We prioritise remaining in the same function, but if there is no choice
+// we take the next state with the shortest path
+void path_searcht::sort_queue_per_function()
+{
+  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;
+
+  // pick the first state in the queue that is a direct successor, i.e.,
+  // has a path length 1 less than the current path length
+  for(it=queue.begin(); it!=queue.end(); ++it)
+  {
+    if(it->get_shortest_path()+1 == current_distance)
+    {
+      shortest_path = it->get_shortest_path();
+      current_distance = shortest_path;
+      statet tmp = *it;
+      queue.erase(it);
+      queue.push_front(tmp);
+      return;
+    }
+  }
+
+  // if we get here there was no direct successor, we revert to
+  // picking the shortest path
+  sort_queue();
+}
+
+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)
 {
@@ -30,12 +130,36 @@ path_searcht::resultt path_searcht::operator()(
 
   status() << "Starting symbolic simulation" << eom;
 
+  switch(search_heuristic)
+  {
+  case search_heuristict::DFS:
+    status() << "Search heuristic: DFS" << eom;
+    break;
+  case search_heuristict::RAN_DFS:
+    status() << "Search heuristic: randomized DFS" << eom;
+    break;
+  case search_heuristict::BFS:
+    status() << "Search heuristic: BFS" << eom;
+    break;
+  case search_heuristict::SHORTEST_PATH:
+    status() << "Search heuristic: shortest path" << eom;
+    break;
+  case search_heuristict::SHORTEST_PATH_PER_FUNC:
+    status() << "Search heuristic: shortest path per function" << eom;
+    break;
+  case search_heuristict::RAN_SHORTEST_PATH:
+    status() << "Search heuristic: randomized shortest path" << eom;
+    break;
+  case search_heuristict::LOCS:
+    status() << "Search heuristic: LOCS" << eom;
+    break;
+  }
+
   // 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;
@@ -51,6 +175,26 @@ 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);
+  }
+  else if(search_heuristic == search_heuristict::SHORTEST_PATH_PER_FUNC)
+  {
+    status()<<"Building shortest path graph per function" << eom;
+    per_function_shortest_patht 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();
+
+  time_periodt initialisation_time=current_time()-start_time;
+  status() << "Initialisation took "<< initialisation_time << "s" << eom;
+  start_time=current_time();
+  last_reported_time=start_time;
 
   while(!queue.empty())
   {
@@ -114,8 +258,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;
         }
       }
@@ -142,6 +291,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 +360,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;
 
@@ -218,6 +371,18 @@ 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::SHORTEST_PATH_PER_FUNC:
+    sort_queue_per_function();
+    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;
@@ -107,8 +109,15 @@ 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; }
+  void set_shortest_path()
+    { search_heuristic=search_heuristict::SHORTEST_PATH; }
+  void set_ran_shortest_path()
+    { search_heuristic=search_heuristict::RAN_SHORTEST_PATH; }
+  void set_shortest_path_per_function()
+    { search_heuristic=search_heuristict::SHORTEST_PATH_PER_FUNC; }
 
   typedef std::map<irep_idt, property_entryt> property_mapt;
   property_mapt property_map;
@@ -120,7 +129,13 @@ 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);
+  /// Move element with shortest distance to property
+  /// to the front of the queue
+  void sort_queue();
+  void sort_queue_per_function();
   // search heuristic
   void pick_state();
 
@@ -151,7 +166,9 @@ 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, SHORTEST_PATH,
+    RAN_SHORTEST_PATH , SHORTEST_PATH_PER_FUNC } search_heuristic;
 
   source_locationt last_source_location;
 };