Shortest path grapht

Builds CFG of all program locations and computes the shortest distance from all locations in the graph to a single property.
WARNING: if more than one property is given, we use the first one only.

Writes these distances to the corresponding node in a locs structure passed as argument to the constructor, in order for this to be used to guide the symex search

Author: polgreen

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)/ansi-c/ansi-c$(LIBEXT) \

src/symex/shortest_path_graph.cpp

@@ -0,0 +1,88 @@
+/*******************************************************************\
+
+Module: Shortest path graph
+
+Author: [email protected]
+
+\*******************************************************************/
+
+#include "shortest_path_graph.h"
+
+#include <algorithm>
+void shortest_path_grapht::bfs(node_indext property_index)
+{
+  // does BFS, not Dijkstra
+  // we hope the graph is sparse
+  std::vector<node_indext> frontier_set;
+
+  frontier_set.reserve(nodes.size());
+
+  frontier_set.push_back(property_index);
+  nodes[property_index].visited = true;
+
+  for(std::size_t d = 1; !frontier_set.empty(); ++d)
+  {
+    std::vector<node_indext> new_frontier_set;
+
+    for(const auto &node_index : frontier_set)
+    {
+      const nodet &n = nodes[node_index];
+
+      // do all neighbors
+      // we go backwards through the graph
+      for(const auto &edge_in : n.in)
+      {
+        node_indext node_in = edge_in.first;
+
+        if(!nodes[node_in].visited)
+        {
+          nodes[node_in].shortest_path_to_property = d;
+          nodes[node_in].visited = true;
+          new_frontier_set.push_back(node_in);
+        }
+      }
+    }
+
+    frontier_set.swap(new_frontier_set);
+  }
+}
+
+void shortest_path_grapht::write_lengths_to_locs()
+{
+  for(const auto &n : nodes)
+  {
+    loc_reft l = target_to_loc_map[n.PC];
+    locs.loc_vector[l.loc_number].distance_to_property
+        = n.shortest_path_to_property;
+  }
+}
+
+void shortest_path_grapht::get_path_lengths_to_property()
+{
+  node_indext property_index;
+  bool found_property=false;
+  for(node_indext n=0; n<nodes.size(); n++)
+  {
+    if(nodes[n].PC->is_assert())
+    {
+      if(found_property == false)
+      {
+        nodes[n].is_property = true;
+        nodes[n].shortest_path_to_property = 0;
+        working_set.insert(n);
+        property_index = n;
+        found_property = true;
+      }
+      else
+        throw "shortest path search cannot be used for multiple properties";
+    }
+  }
+  if(!found_property)
+    throw "unable to find property";
+
+  bfs(property_index);
+
+  write_lengths_to_locs();
+}
+
+

src/symex/shortest_path_graph.h

@@ -0,0 +1,72 @@
+/*******************************************************************\
+
+Module: Shortest path graph
+
+Author: [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_SYMEX_SHORTEST_PATH_GRAPH_H
+#define CPROVER_SYMEX_SHORTEST_PATH_GRAPH_H
+
+#include <goto-programs/cfg.h>
+#include <path-symex/locs.h>
+#include <goto-programs/goto_model.h>
+#include <limits>
+
+
+struct shortest_path_nodet
+{
+  bool visited;
+  std::size_t shortest_path_to_property;
+  bool is_property;
+  shortest_path_nodet():
+    visited(false),
+    is_property(false)
+  {
+    shortest_path_to_property = std::numeric_limits<std::size_t>::max();
+  }
+};
+
+/// \brief constructs a CFG of all program locations. Then computes
+/// the shortest path from every program location to a single property.
+/// WARNING: if more than one property is present in the graph, we will
+/// use the first property found
+/// 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 CFG from, locs struct made from the
+/// same goto_functions
+class shortest_path_grapht: public cfg_baset<shortest_path_nodet>
+{
+public:
+  explicit shortest_path_grapht(
+      const goto_functionst &_goto_functions, locst &_locs):
+    locs(_locs),
+    target_to_loc_map(_locs)
+    {
+    cfg_baset<shortest_path_nodet>::operator()(_goto_functions);
+    get_path_lengths_to_property();
+    }
+
+protected:
+  /// \brief writes the computed shortest path for every node
+  /// in the graph to the corresponding location in locst.
+  /// This is done so that we can use these numbers to guide
+  /// a search heuristic for symex
+  void write_lengths_to_locs();
+  /// \brief computes the shortest path from every node in
+  /// the graph to a single property. WARNING: if more than one property
+  /// is present, we use the first one discovered.
+  /// Calls bfs() to do this.
+  void get_path_lengths_to_property();
+  /// \brief implements backwards BFS to compute distance from every node in
+  /// the graph to the node index given as parameter
+  /// \param destination node index
+  void bfs(node_indext property_index);
+  std::set<node_indext> working_set;
+  locst &locs;
+  target_to_loc_mapt target_to_loc_map;
+};
+
+#endif /* CPROVER_SYMEX_SHORTEST_PATH_GRAPH_H */