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 
20 #include <goto-programs/cfg.h>
24 
25 #include "util/message.h"
26 
27 #include "full_slicer_class.h"
29 
35 std::vector<reachability_slicert::cfgt::node_indext>
37  const is_threadedt &is_threaded,
38  const slicing_criteriont &criterion)
39 {
40  std::vector<cfgt::node_indext> sources;
41  for(const auto &e_it : cfg.entry_map)
42  {
43  if(criterion(e_it.first) || is_threaded(e_it.first))
44  sources.push_back(e_it.second);
45  }
46 
47  return sources;
48 }
49 
50 static bool is_same_target(
53 {
54  // Avoid comparing iterators belonging to different functions, and therefore
55  // different std::lists.
56  return it1->function == it2->function && it1 == it2;
57 }
58 
65 std::vector<reachability_slicert::cfgt::node_indext>
67  std::vector<cfgt::node_indext> stack)
68 {
69  std::vector<cfgt::node_indext> return_sites;
70 
71  while(!stack.empty())
72  {
73  auto &node = cfg[stack.back()];
74  stack.pop_back();
75 
76  if(node.reaches_assertion)
77  continue;
78  node.reaches_assertion = true;
79 
80  for(const auto &edge : node.in)
81  {
82  const auto &pred_node = cfg[edge.first];
83 
84  if(pred_node.PC->is_end_function())
85  {
86  // This is an end-of-function -> successor-of-callsite edge.
87  // Record the return site for later investigation and step over it:
88  return_sites.push_back(edge.first);
89 
90  INVARIANT(
91  std::prev(node.PC)->is_function_call(),
92  "all function return edges should point to the successor of a "
93  "FUNCTION_CALL instruction");
94 
95  stack.push_back(cfg.entry_map[std::prev(node.PC)]);
96  }
97  else
98  {
99  stack.push_back(edge.first);
100  }
101  }
102  }
103 
104  return return_sites;
105 }
106 
117  std::vector<cfgt::node_indext> stack)
118 {
119  while(!stack.empty())
120  {
121  auto &node = cfg[stack.back()];
122  stack.pop_back();
123 
124  if(node.reaches_assertion)
125  continue;
126  node.reaches_assertion = true;
127 
128  for(const auto &edge : node.in)
129  {
130  const auto &pred_node = cfg[edge.first];
131 
132  if(pred_node.PC->is_end_function())
133  {
134  // This is an end-of-function -> successor-of-callsite edge.
135  // Walk into the called function, and then walk from the callsite
136  // backward:
137  stack.push_back(edge.first);
138 
139  INVARIANT(
140  std::prev(node.PC)->is_function_call(),
141  "all function return edges should point to the successor of a "
142  "FUNCTION_CALL instruction");
143 
144  stack.push_back(cfg.entry_map[std::prev(node.PC)]);
145  }
146  else if(pred_node.PC->is_function_call())
147  {
148  // Skip -- the callsite relevant to this function was already queued
149  // when we processed the return site.
150  }
151  else
152  {
153  stack.push_back(edge.first);
154  }
155  }
156  }
157 }
158 
166  const is_threadedt &is_threaded,
167  const slicing_criteriont &criterion)
168 {
169  std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
170 
171  // First walk outwards towards __CPROVER_start, visiting all possible callers
172  // and stepping over but recording callees as we go:
173  std::vector<cfgt::node_indext> return_sites =
175 
176  // Now walk into those callees, restricting our walk to the known callsites:
177  backward_inwards_walk_from(return_sites);
178 }
179 
189  const cfgt::nodet &call_node,
190  std::vector<cfgt::node_indext> &callsite_successor_stack,
191  std::vector<cfgt::node_indext> &callee_head_stack)
192 {
193  // Get the instruction's natural successor (function head, or next
194  // instruction if the function is bodyless)
195  INVARIANT(call_node.out.size() == 1, "Call sites should have one successor");
196  const auto successor_index = call_node.out.begin()->first;
197 
198  auto callsite_successor_pc = std::next(call_node.PC);
199 
200  auto successor_pc = cfg[successor_index].PC;
201  if(!is_same_target(successor_pc, callsite_successor_pc))
202  {
203  // Real call -- store the callee head node:
204  callee_head_stack.push_back(successor_index);
205 
206  // Check if it can return, and if so store the callsite's successor:
207  while(!successor_pc->is_end_function())
208  ++successor_pc;
209 
210  if(!cfg[cfg.entry_map[successor_pc]].out.empty())
211  callsite_successor_stack.push_back(cfg.entry_map[callsite_successor_pc]);
212  }
213  else
214  {
215  // Bodyless function -- mark the successor instruction only.
216  callsite_successor_stack.push_back(successor_index);
217  }
218 }
219 
226 std::vector<reachability_slicert::cfgt::node_indext>
228  std::vector<cfgt::node_indext> stack)
229 {
230  std::vector<cfgt::node_indext> called_function_heads;
231 
232  while(!stack.empty())
233  {
234  auto &node = cfg[stack.back()];
235  stack.pop_back();
236 
237  if(node.reachable_from_assertion)
238  continue;
239  node.reachable_from_assertion = true;
240 
241  if(node.PC->is_function_call())
242  {
243  // Store the called function head for the later inwards walk;
244  // visit the call instruction's local successor now.
245  forward_walk_call_instruction(node, stack, called_function_heads);
246  }
247  else
248  {
249  // General case, including end of function: queue all successors.
250  for(const auto &edge : node.out)
251  stack.push_back(edge.first);
252  }
253  }
254 
255  return called_function_heads;
256 }
257 
266  std::vector<cfgt::node_indext> stack)
267 {
268  while(!stack.empty())
269  {
270  auto &node = cfg[stack.back()];
271  stack.pop_back();
272 
273  if(node.reachable_from_assertion)
274  continue;
275  node.reachable_from_assertion = true;
276 
277  if(node.PC->is_function_call())
278  {
279  // Visit both the called function head and the callsite successor:
281  }
282  else if(node.PC->is_end_function())
283  {
284  // Special case -- the callsite successor was already queued when entering
285  // this function, more precisely than we can see from the function return
286  // edges (which lead to all possible callers), so nothing to do here.
287  }
288  else
289  {
290  // General case: queue all successors.
291  for(const auto &edge : node.out)
292  stack.push_back(edge.first);
293  }
294  }
295 }
296 
304  const is_threadedt &is_threaded,
305  const slicing_criteriont &criterion)
306 {
307  std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
308 
309  // First walk outwards towards __CPROVER_start, visiting all possible callers
310  // and stepping over but recording callees as we go:
311  std::vector<cfgt::node_indext> return_sites =
313 
314  // Now walk into those callees, restricting our walk to the known callsites:
315  forward_inwards_walk_from(return_sites);
316 }
317 
321 {
322  // now replace those instructions that do not reach any assertions
323  // by assume(false)
324 
325  Forall_goto_functions(f_it, goto_functions)
326  if(f_it->second.body_available())
327  {
328  Forall_goto_program_instructions(i_it, f_it->second.body)
329  {
330  cfgt::nodet &e = cfg[cfg.entry_map[i_it]];
331  if(
332  !e.reaches_assertion && !e.reachable_from_assertion &&
333  !i_it->is_end_function())
334  i_it->make_assumption(false_exprt());
335  }
336 
337  // replace unreachable code by skip
338  remove_unreachable(f_it->second.body);
339  }
340 
341  // remove the skips
342  remove_skip(goto_functions);
343 }
344 
352  goto_modelt &goto_model,
353  const bool include_forward_reachability)
354 {
357  s(goto_model.goto_functions, a, include_forward_reachability);
358 }
359 
368  goto_modelt &goto_model,
369  const std::list<std::string> &properties,
370  const bool include_forward_reachability)
371 {
373  properties_criteriont p(properties);
374  s(goto_model.goto_functions, p, include_forward_reachability);
375 }
376 
383  goto_modelt &goto_model,
384  const std::list<std::string> &functions_list)
385 {
386  for(const auto &function : functions_list)
387  {
388  in_function_criteriont matching_criterion(function);
389  reachability_slicert slicer;
390  slicer(goto_model.goto_functions, matching_criterion, true);
391  }
392 
393  remove_calls_no_bodyt remove_calls_no_body;
394  remove_calls_no_body(goto_model.goto_functions);
395 
396  goto_model.goto_functions.update();
398 }
399 
405 {
406  reachability_slicer(goto_model, false);
407 }
408 
415  goto_modelt &goto_model,
416  const std::list<std::string> &properties)
417 {
418  reachability_slicer(goto_model, properties, false);
419 }
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.
std::vector< cfgt::node_indext > backward_outwards_walk_from(std::vector< cfgt::node_indext >)
Perform backward depth-first search of the control-flow graph of the goto program,...
Goto Program Slicing.
Control Flow Graph.
entry_mapt entry_map
Definition: cfg.h:106
void compute_loop_numbers()
Remove calls to functions without a body.
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
void forward_inwards_walk_from(std::vector< cfgt::node_indext >)
Perform forwards depth-first search of the control-flow graph of the goto program,...
std::vector< cfgt::node_indext > get_sources(const is_threadedt &is_threaded, const slicing_criteriont &criterion)
Get the set of nodes that correspond to the given criterion, or that can appear in concurrent executi...
void fixedpoint_to_assertions(const is_threadedt &is_threaded, const slicing_criteriont &criterion)
Perform backward depth-first search of the control-flow graph of the goto program,...
cfg_base_nodet< slicer_entryt, goto_programt::const_targett > nodet
Definition: graph.h:170
const edgest & out(node_indext n) const
Definition: graph.h:227
instructionst::const_iterator const_targett
Definition: goto_program.h:415
void slice(goto_functionst &goto_functions)
This function removes all instructions that have the flag reaches_assertion or reachable_from_asserti...
A collection of goto functions.
The Boolean constant false.
Definition: std_expr.h:4452
void forward_walk_call_instruction(const cfgt::nodet &call_node, std::vector< cfgt::node_indext > &callsite_successor_stack, std::vector< cfgt::node_indext > &callee_head_stack)
Process a call instruction during a forwards reachability walk.
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)
static bool is_same_target(goto_programt::const_targett it1, goto_programt::const_targett it2)
Program Transformation.
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
void fixedpoint_from_assertions(const is_threadedt &is_threaded, const slicing_criteriont &criterion)
Perform forwards depth-first search of the control-flow graph of the goto program,...
Goto Program Slicing.
std::vector< cfgt::node_indext > forward_outwards_walk_from(std::vector< cfgt::node_indext >)
Perform forwards depth-first search of the control-flow graph of the goto program,...
Program Transformation.
#define stack(x)
Definition: parser.h:144
void backward_inwards_walk_from(std::vector< cfgt::node_indext >)
Perform backward depth-first search of the control-flow graph of the goto program,...
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
void function_path_reachability_slicer(goto_modelt &goto_model, const std::list< std::string > &functions_list)
Perform reachability slicing on goto_model for selected functions.