cprover
reachability_slicer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Slicer
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
15 
16 #include "reachability_slicer.h"
17 
18 #include <stack>
19 
22 #include <goto-programs/cfg.h>
23 
24 #include "full_slicer_class.h"
26 
32 std::vector<reachability_slicert::cfgt::node_indext>
34  const is_threadedt &is_threaded,
36 {
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  }
43 
44  return sources;
45 }
46 
47 static bool is_same_target(
50 {
51  // Avoid comparing iterators belonging to different functions, and therefore
52  // different std::lists.
53  return it1->function == it2->function && it1 == it2;
54 }
55 
63  const is_threadedt &is_threaded,
65 {
66  std::vector<search_stack_entryt> stack;
67  std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
68  for(const auto source : sources)
69  stack.emplace_back(source, false);
70 
71  while(!stack.empty())
72  {
73  auto &node = cfg[stack.back().node_index];
74  const auto caller_is_known = stack.back().caller_is_known;
75  stack.pop_back();
76 
77  if(node.reaches_assertion)
78  continue;
79  node.reaches_assertion = true;
80 
81  for(const auto &edge : node.in)
82  {
83  const auto &pred_node = cfg[edge.first];
84 
85  if(pred_node.PC->is_end_function())
86  {
87  // This is an end-of-function -> successor-of-callsite edge.
88  // Queue both the caller and the end of the callee.
89  INVARIANT(
90  std::prev(node.PC)->is_function_call(),
91  "all function return edges should point to the successor of a "
92  "FUNCTION_CALL instruction");
93  stack.emplace_back(edge.first, true);
94  stack.emplace_back(
95  cfg.entry_map[std::prev(node.PC)], caller_is_known);
96  }
97  else if(pred_node.PC->is_function_call())
98  {
99  // Skip this predecessor, unless this is a bodyless function, or we
100  // don't know who our callee was:
101  if(!caller_is_known || is_same_target(std::next(pred_node.PC), node.PC))
102  stack.emplace_back(edge.first, caller_is_known);
103  }
104  else
105  {
106  stack.emplace_back(edge.first, caller_is_known);
107  }
108  }
109  }
110 }
111 
119  const is_threadedt &is_threaded,
121 {
122  std::vector<search_stack_entryt> stack;
123  std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
124  for(const auto source : sources)
125  stack.emplace_back(source, false);
126 
127  while(!stack.empty())
128  {
129  auto &node = cfg[stack.back().node_index];
130  const auto caller_is_known = stack.back().caller_is_known;
131  stack.pop_back();
132 
133  if(node.reachable_from_assertion)
134  continue;
135  node.reachable_from_assertion = true;
136 
137  if(node.PC->is_function_call())
138  {
139  // Queue the instruction's natural successor (function head, or next
140  // instruction if the function is bodyless)
141  INVARIANT(node.out.size() == 1, "Call sites should have one successor");
142  const auto successor_index = node.out.begin()->first;
143 
144  // If the function has a body, mark the function head, but note that we
145  // have already taken care of the return site.
146  const auto &callee_head_node = cfg[successor_index];
147  auto callee_it = callee_head_node.PC;
148  if(!is_same_target(callee_it, std::next(node.PC)))
149  {
150  stack.emplace_back(successor_index, true);
151 
152  // Check if it can return, and if so mark the callsite's successor:
153  while(!callee_it->is_end_function())
154  ++callee_it;
155 
156  if(!cfg[cfg.entry_map[callee_it]].out.empty())
157  {
158  stack.emplace_back(
159  cfg.entry_map[std::next(node.PC)], caller_is_known);
160  }
161  }
162  else
163  {
164  // Bodyless function -- mark the successor instruction only.
165  stack.emplace_back(successor_index, caller_is_known);
166  }
167  }
168  else if(node.PC->is_end_function() && caller_is_known)
169  {
170  // Special case -- the callsite successor was already queued when entering
171  // this function, more precisely than we can see from the function return
172  // edges (which lead to all possible callers), so nothing to do here.
173  }
174  else
175  {
176  // General case, including end-of-function where we don't know our caller.
177  // Queue all successors.
178  for(const auto &edge : node.out)
179  stack.emplace_back(edge.first, caller_is_known);
180  }
181  }
182 }
183 
187 {
188  // now replace those instructions that do not reach any assertions
189  // by assume(false)
190 
191  Forall_goto_functions(f_it, goto_functions)
192  if(f_it->second.body_available())
193  {
194  Forall_goto_program_instructions(i_it, f_it->second.body)
195  {
196  const cfgt::nodet &e=cfg[cfg.entry_map[i_it]];
197  if(
198  !e.reaches_assertion && !e.reachable_from_assertion &&
199  !i_it->is_end_function())
200  i_it->make_assumption(false_exprt());
201  }
202 
203  // replace unreachable code by skip
204  remove_unreachable(f_it->second.body);
205  }
206 
207  // remove the skips
208  remove_skip(goto_functions);
209 }
210 
218  goto_modelt &goto_model,
219  const bool include_forward_reachability)
220 {
223  s(goto_model.goto_functions, a, include_forward_reachability);
224 }
225 
234  goto_modelt &goto_model,
235  const std::list<std::string> &properties,
236  const bool include_forward_reachability)
237 {
239  properties_criteriont p(properties);
240  s(goto_model.goto_functions, p, include_forward_reachability);
241 }
242 
248 {
249  reachability_slicer(goto_model, false);
250 }
251 
258  goto_modelt &goto_model,
259  const std::list<std::string> &properties)
260 {
261  reachability_slicer(goto_model, properties, false);
262 }
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties...
Goto Program Slicing.
Control Flow Graph.
entry_mapt entry_map
Definition: cfg.h:106
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
const edgest & out(node_indext n) const
Definition: graph.h:193
instructionst::const_iterator const_targett
Definition: goto_program.h:398
void slice(goto_functionst &goto_functions)
This function removes all instructions that have the flag reaches_assertion or reachable_from_asserti...
The boolean constant false.
Definition: std_expr.h:4499
std::vector< cfgt::node_indext > get_sources(const is_threadedt &is_threaded, slicing_criteriont &criterion)
Get the set of nodes that correspond to the given criterion, or that can appear in concurrent executi...
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
#define Forall_goto_functions(it, functions)
void fixedpoint_from_assertions(const is_threadedt &is_threaded, slicing_criteriont &criterion)
Perform forwards depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently.
goto_programt coverage_criteriont criterion
Definition: cover.cpp:63
static bool is_same_target(goto_programt::const_targett it1, goto_programt::const_targett it2)
Program Transformation.
void fixedpoint_to_assertions(const is_threadedt &is_threaded, slicing_criteriont &criterion)
Perform backwards depth-first search of the control-flow graph of the goto program, starting from the nodes corresponding to the criterion and the instructions that might be executed concurrently.
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Goto Program Slicing.
Program Transformation.
#define stack(x)
Definition: parser.h:144
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32