77\*******************************************************************/
88
99// / \file
10- // / Slicer
10+ // / Reachability Slicer
11+ // / Consider the control flow graph of the goto program and a criterion, and
12+ // / remove the parts of the graph from which the criterion is not reachable
13+ // / (and possibly, depending on the parameters, keep those that can be reached
14+ // / from the criterion).
1115
1216#include " reachability_slicer.h"
1317
2024#include " full_slicer_class.h"
2125#include " reachability_slicer_class.h"
2226
23- void reachability_slicert::fixedpoint_assertions (
27+ // / Get the set of nodes that correspond to the given criterion, or that can
28+ // / appear in concurrent execution. None of these should be sliced away so
29+ // / they are used as a basis for the search.
30+ // / \param is_threaded Instructions that might be executed concurrently
31+ // / \param criterion The criterion we care about
32+ std::vector<reachability_slicert::cfgt::node_indext>
33+ reachability_slicert::get_sources (
2434 const is_threadedt &is_threaded,
2535 slicing_criteriont &criterion)
2636{
27- queuet queue;
37+ std::vector<cfgt::node_indext> sources;
38+ for (const auto &e_it : cfg.entry_map )
39+ {
40+ if (criterion (e_it.first ) || is_threaded (e_it.first ))
41+ sources.push_back (e_it.second );
42+ }
2843
29- for (cfgt::entry_mapt::iterator
30- e_it=cfg.entry_map .begin ();
31- e_it!=cfg.entry_map .end ();
32- e_it++)
33- if (criterion (e_it->first ) ||
34- is_threaded (e_it->first ))
35- queue.push (e_it->second );
44+ return sources;
45+ }
3646
37- while (!queue.empty ())
38- {
39- cfgt::entryt e=queue.top ();
40- cfgt::nodet &node=cfg[e];
41- queue.pop ();
47+ // / Perform backwards depth-first search of the control-flow graph of the
48+ // / goto program, starting from the nodes corresponding to the criterion and
49+ // / the instructions that might be executed concurrently. Set reaches_assertion
50+ // / to true for every instruction visited.
51+ // / \param is_threaded Instructions that might be executed concurrently
52+ // / \param criterion the criterion we are trying to hit
53+ void reachability_slicert::fixedpoint_to_assertions (
54+ const is_threadedt &is_threaded,
55+ slicing_criteriont &criterion)
56+ {
57+ std::vector<cfgt::node_indext> src = get_sources (is_threaded, criterion);
4258
43- if (node.reaches_assertion )
44- continue ;
59+ std::vector<cfgt::node_indext> reachable = cfg.get_reachable (src, false );
60+ for (const auto index : reachable)
61+ cfg[index ].reaches_assertion = true ;
62+ }
4563
46- node.reaches_assertion =true ;
64+ // / Perform forwards depth-first search of the control-flow graph of the
65+ // / goto program, starting from the nodes corresponding to the criterion and
66+ // / the instructions that might be executed concurrently. Set reaches_assertion
67+ // / to true for every instruction visited.
68+ // / \param is_threaded Instructions that might be executed concurrently
69+ // / \param criterion the criterion we are trying to hit
70+ void reachability_slicert::fixedpoint_from_assertions (
71+ const is_threadedt &is_threaded,
72+ slicing_criteriont &criterion)
73+ {
74+ std::vector<cfgt::node_indext> src = get_sources (is_threaded, criterion);
4775
48- for (cfgt::edgest::const_iterator
49- p_it=node.in .begin ();
50- p_it!=node.in .end ();
51- p_it++)
52- {
53- queue.push (p_it->first );
54- }
55- }
76+ const std::vector<cfgt::node_indext> reachable = cfg.get_reachable (src, true );
77+ for (const auto index : reachable)
78+ cfg[index ].reachable_from_assertion = true ;
5679}
5780
81+ // / This function removes all instructions that have the flag
82+ // / reaches_assertion or reachable_from_assertion set to true;
5883void reachability_slicert::slice (goto_functionst &goto_functions)
5984{
6085 // now replace those instructions that do not reach any assertions
@@ -66,8 +91,9 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
6691 Forall_goto_program_instructions (i_it, f_it->second .body )
6792 {
6893 const cfgt::nodet &e=cfg[cfg.entry_map [i_it]];
69- if (!e.reaches_assertion &&
70- !i_it->is_end_function ())
94+ if (
95+ !e.reaches_assertion && !e.reachable_from_assertion &&
96+ !i_it->is_end_function ())
7197 i_it->make_assumption (false_exprt ());
7298 }
7399
@@ -80,18 +106,55 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
80106 goto_functions.update ();
81107}
82108
83- void reachability_slicer (goto_modelt &goto_model)
109+ // / Perform reachability slicing on goto_model, with respect to the
110+ // / criterion given by all properties.
111+ // / \param goto_model Goto program to slice
112+ // / \param include_forward_reachability Determines if only instructions
113+ // / from which the criterion is reachable should be kept (false) or also
114+ // / those reachable from the criterion (true)
115+ void reachability_slicer (
116+ goto_modelt &goto_model,
117+ const bool include_forward_reachability)
84118{
85119 reachability_slicert s;
86120 assert_criteriont a;
87- s (goto_model.goto_functions , a);
121+ s (goto_model.goto_functions , a, include_forward_reachability );
88122}
89123
124+ // / Perform reachability slicing on goto_model for selected properties.
125+ // / \param goto_model Goto program to slice
126+ // / \param properties The properties relevant for the slicing (i.e. starting
127+ // / point for the search in the cfg)
128+ // / \param include_forward_reachability Determines if only instructions
129+ // / from which the criterion is reachable should be kept (false) or also
130+ // / those reachable from the criterion (true)
90131void reachability_slicer (
91132 goto_modelt &goto_model,
92- const std::list<std::string> &properties)
133+ const std::list<std::string> &properties,
134+ const bool include_forward_reachability)
93135{
94136 reachability_slicert s;
95137 properties_criteriont p (properties);
96- s (goto_model.goto_functions , p);
138+ s (goto_model.goto_functions , p, include_forward_reachability);
139+ }
140+
141+ // / Perform reachability slicing on goto_model, with respect to criterion
142+ // / comprising all properties. Only instructions from which the criterion
143+ // / is reachable will be kept.
144+ // / \param goto_model Goto program to slice
145+ void reachability_slicer (goto_modelt &goto_model)
146+ {
147+ reachability_slicer (goto_model, false );
148+ }
149+
150+ // / Perform reachability slicing on goto_model for selected properties. Only
151+ // / instructions from which the criterion is reachable will be kept.
152+ // / \param goto_model Goto program to slice
153+ // / \param properties The properties relevant for the slicing (i.e. starting
154+ // / point for the search in the cfg)
155+ void reachability_slicer (
156+ goto_modelt &goto_model,
157+ const std::list<std::string> &properties)
158+ {
159+ reachability_slicer (goto_model, properties, false );
97160}
0 commit comments