Per function shortest path graph

Builds a CFG for every goto_program in goto_functions, and computes the distance for every location in the CFGs to the property, if one exists in taht CFG, or to the end of the function

Writes these numbers to locst passed as argument to the constructor, in order to use numbers to guide symex search

Author: polgreen

src/symex/shortest_path_graph.cpp

@@ -9,6 +9,56 @@ Author: [email protected]
 #include "shortest_path_graph.h"
 
 #include <algorithm>
+
+void shortest_path_grapht::get_path_lengths_in_function()
+{
+  bool found_property = false;
+  bool found_end = false;
+  node_indext end_index;
+  node_indext property_index;
+  node_indext index = 0;
+  for(auto &n : nodes)
+  {
+    if(n.PC->is_assert())
+    {
+      if(found_property == false)
+      {
+        n.is_property = true;
+        n.shortest_path_to_property = 0;
+        found_property = true;
+        property_index = index;
+      }
+      else
+        throw "shortest path search cannot be used with multiple properties";
+    }
+    if(n.PC->is_end_function())
+    {
+      end_index = index;
+      found_end = true;
+    }
+    index++;
+  }
+
+  if(!found_property)
+  {
+    nodes[end_index].shortest_path_to_property = 0;
+    bfs(end_index);
+  }
+  else
+    bfs(property_index);
+
+  write_lengths_to_locs();
+}
+
+void per_function_shortest_patht::build(const goto_functionst &goto_functions)
+{
+  forall_goto_functions(it, goto_functions)
+    if(it->second.body_available())
+    {
+      shortest_path_grapht path_graph(it->second.body, locs);
+    }
+}
+
 void shortest_path_grapht::bfs(node_indext property_index)
 {
   // does BFS, not Dijkstra

src/symex/shortest_path_graph.h

@@ -49,6 +49,15 @@ class shortest_path_grapht: public cfg_baset<shortest_path_nodet>
     get_path_lengths_to_property();
     }
 
+  explicit shortest_path_grapht(
+      const goto_programt &_goto_program, locst &_locs):
+    locs(_locs),
+    target_to_loc_map(_locs)
+    {
+    cfg_baset<shortest_path_nodet>::operator()(_goto_program);
+    get_path_lengths_in_function();
+    }
+
 protected:
   /// \brief writes the computed shortest path for every node
   /// in the graph to the corresponding location in locst.
@@ -60,6 +69,11 @@ class shortest_path_grapht: public cfg_baset<shortest_path_nodet>
   /// is present, we use the first one discovered.
   /// Calls bfs() to do this.
   void get_path_lengths_to_property();
+  /// \brief computes the shortest path from every node in a
+  /// graph to the property, or the end of the funciton if
+  /// there is no property.
+  /// we assume the graph is a graph of a single function.
+  void get_path_lengths_in_function();
   /// \brief implements backwards BFS to compute distance from every node in
   /// the graph to the node index given as parameter
   /// \param destination node index
@@ -69,4 +83,27 @@ class shortest_path_grapht: public cfg_baset<shortest_path_nodet>
   target_to_loc_mapt target_to_loc_map;
 };
 
+/// \brief class contains CFG of program locations
+/// for every function with the shortest distance to a
+/// property, or the end of a function, calculated for each location
+/// The distances computed for each node are written to the corresponding
+/// loct in the locst passed as param to the constructor. This allows us
+/// to use these numbers to guide a symex search
+/// \param goto functions to create the CFGs from, locs struct made from the
+/// same goto_functions
+class per_function_shortest_patht
+{
+public:
+  explicit per_function_shortest_patht(
+      const goto_functionst &_goto_functions, locst &_locs):
+  locs(_locs)
+  {
+    build(_goto_functions);
+  }
+
+protected:
+  locst &locs;
+  void build(const goto_functionst & goto_functions);
+};
+
 #endif /* CPROVER_SYMEX_SHORTEST_PATH_GRAPH_H */