Shortest path per function search heuristic

Computes the shortest path per function on the shortest path graph and uses this heuristic to guide the symex search

Author: polgreen

src/symex/path_search.cpp

@@ -65,6 +65,42 @@ void path_searcht::sort_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)
@@ -120,6 +156,12 @@ path_searcht::resultt path_searcht::operator()(
     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();
@@ -308,6 +350,9 @@ void path_searcht::pick_state()
   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

@@ -116,6 +116,8 @@ class path_searcht:public safety_checkert
     { 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;
@@ -133,6 +135,7 @@ class path_searcht:public safety_checkert
   /// 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();
 
@@ -164,7 +167,8 @@ class path_searcht:public safety_checkert
   unsigned time_limit;
 
   enum class search_heuristict
-  { DFS, RAN_DFS, BFS, LOCS, SHORTEST_PATH, RAN_SHORTEST_PATH } search_heuristic;
+  { DFS, RAN_DFS, BFS, LOCS, SHORTEST_PATH,
+    RAN_SHORTEST_PATH , SHORTEST_PATH_PER_FUNC } search_heuristic;
 
   source_locationt last_source_location;
 };

src/symex/symex_parse_options.cpp

@@ -243,6 +243,10 @@ int symex_parse_optionst::doit()
       else
         path_search.set_shortest_path();
     }
+
+    if(cmdline.isset("shortest-path-per-function"))
+      path_search.set_shortest_path_per_function();
+
     if(cmdline.isset("show-vcc"))
     {
       path_search.show_vcc=true;
@@ -653,6 +657,7 @@ void symex_parse_optionst::help()
     " --dfs                        use depth first search\n"
     " --bfs                        use breadth first search\n"
     "--shortest-path               use shortest path guided search\n"
+    "--shortest-path-per-function  computes shortest path locally and uses to guide symex search\n" // NOLINT(*)
     " --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(*)

src/symex/symex_parse_options.h

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