Skip to content

Commit fef1b6d

Browse files
committed
Output distances to property from every reachable program location
1 parent 489e0c0 commit fef1b6d

File tree

4 files changed

+50
-0
lines changed

4 files changed

+50
-0
lines changed

src/path-symex/locs.cpp

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,39 @@ void locst::build(const goto_functionst &goto_functions)
8282
}
8383
}
8484

85+
void locst::output_reachable(std::ostream &out) const
86+
{
87+
irep_idt function;
88+
int reachable_count = 0;
89+
int unreachable_count = 0;
90+
91+
for(unsigned l = 0; l < loc_vector.size(); l++)
92+
{
93+
const loct &loc = loc_vector[l];
94+
if(loc.distance_to_property != -1)
95+
{
96+
reachable_count++;
97+
if(function != loc.function)
98+
{
99+
function = loc.function;
100+
out << "*** " << function << "\n";
101+
}
102+
103+
out << " L" << l << ": " << " " << as_string(ns, *loc.target)
104+
<< " path length: " << loc_vector[l].distance_to_property << "\n";
105+
106+
if(!loc.branch_target.is_nil())
107+
out << " T: " << loc.branch_target << "\n";
108+
}
109+
else
110+
unreachable_count++;
111+
}
112+
out << "\n";
113+
out << "The entry location is L" << entry_loc << ".\n";
114+
out << "Number of reachable locs " << reachable_count << "\n";
115+
out << "Number of unreachable locs " << unreachable_count << "\n";
116+
}
117+
85118
void locst::output(std::ostream &out) const
86119
{
87120
irep_idt function;

src/path-symex/locs.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,7 @@ class locst
5959
explicit locst(const namespacet &_ns);
6060
void build(const goto_functionst &goto_functions);
6161
void output(std::ostream &out) const;
62+
void output_reachable(std::ostream &out) const;
6263

6364
loct &operator[] (loc_reft l)
6465
{

src/symex/symex_parse_options.cpp

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,7 @@ Author: Daniel Kroening, [email protected]
5858
#include <path-symex/locs.h>
5959

6060
#include "path_search.h"
61+
#include "shortest_path_graph.h"
6162

6263
symex_parse_optionst::symex_parse_optionst(int argc, const char **argv):
6364
parse_options_baset(SYMEX_OPTIONS, argc, argv),
@@ -202,6 +203,18 @@ int symex_parse_optionst::doit()
202203
return 0;
203204
}
204205

206+
if(cmdline.isset("show-distances-to-property"))
207+
{
208+
const namespacet ns(goto_model.symbol_table);
209+
locst locs(ns);
210+
locs.build(goto_model.goto_functions);
211+
212+
shortest_path_grapht path_search_graph(goto_model.goto_functions, locs);
213+
214+
locs.output_reachable(std::cout);
215+
return 0;
216+
}
217+
205218
// do actual Symex
206219

207220
try
@@ -647,6 +660,8 @@ void symex_parse_optionst::help()
647660
" --eager-infeasibility query solver early to determine whether a path is infeasible before searching it\n" // NOLINT(*)
648661
"\n"
649662
"Other options:\n"
663+
" --show-distances-to-property\n"
664+
" shows the (context free) shortest path from every reachable program location to a single property" // NOLINT(*)
650665
" --version show version and exit\n"
651666
" --xml-ui use XML-formatted output\n"
652667
" --verbosity # verbosity level\n"

src/symex/symex_parse_options.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,7 @@ class optionst;
5151
"(show-locs)(show-vcc)(show-properties)(show-symbol-table)" \
5252
"(drop-unused-functions)" \
5353
"(object-bits):" \
54+
"(show-distances-to-property)" \
5455
OPT_SHOW_GOTO_FUNCTIONS \
5556
"(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \
5657
"(no-simplify)(no-unwinding-assertions)(no-propagation)" \

0 commit comments

Comments
 (0)