Output distances to property from every reachable program location

Author: polgreen

src/path-symex/locs.cpp

@@ -82,6 +82,39 @@ 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;

src/path-symex/locs.h

@@ -59,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/symex/symex_parse_options.cpp

@@ -57,6 +57,7 @@ Author: Daniel Kroening, [email protected]
 #include <path-symex/locs.h>
 
 #include "path_search.h"
+#include "shortest_path_graph.h"
 
 symex_parse_optionst::symex_parse_optionst(int argc, const char **argv):
   parse_options_baset(SYMEX_OPTIONS, argc, argv),
@@ -180,6 +181,18 @@ int symex_parse_optionst::doit()
     return 0;
   }
 
+  if(cmdline.isset("show-distances-to-property"))
+  {
+    const namespacet ns(goto_model.symbol_table);
+    locst locs(ns);
+    locs.build(goto_model.goto_functions);
+
+    shortest_path_grapht path_search_graph(goto_model.goto_functions, locs);
+
+    locs.output_reachable(std::cout);
+    return 0;
+  }
+
   // do actual Symex
 
   try
@@ -636,6 +649,8 @@ void symex_parse_optionst::help()
     " --eager-infeasibility        query solver early to determine whether a path is infeasible before searching it\n" // NOLINT(*)
     "\n"
     "Other options:\n"
+    " --show-distances-to-property\n"
+    "                              shows the (context free) shortest path from every reachable program location to a single property" // NOLINT(*)
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
     " --verbosity #                verbosity level\n"

src/symex/symex_parse_options.h

@@ -48,6 +48,7 @@ class optionst;
   "(show-locs)(show-vcc)(show-properties)" \
   "(drop-unused-functions)" \
   "(object-bits):" \
+  "(show-distances-to-property)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \
   "(no-simplify)(no-unwinding-assertions)(no-propagation)" \