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 <goto-programs/cfg.h>
22 
23 #include <util/exception_utils.h>
24 
25 #include "full_slicer_class.h"
27 
33 std::vector<reachability_slicert::cfgt::node_indext>
35  const is_threadedt &is_threaded,
36  const slicing_criteriont &criterion)
37 {
38  std::vector<cfgt::node_indext> sources;
39  for(const auto &e_it : cfg.entries())
40  {
41  if(
42  criterion(cfg[e_it.second].function_id, e_it.first) ||
43  is_threaded(e_it.first))
44  sources.push_back(e_it.second);
45  }
46 
47  if(sources.empty())
48  {
50  "no slicing criterion found",
51  "--property",
52  "provide at least one property using --property <property>"};
53  }
54 
55  return sources;
56 }
57 
61 {
62  // Avoid comparing iterators belonging to different functions, and therefore
63  // different std::lists.
64  const auto &node1 = cfg.get_node(it1);
65  const auto &node2 = cfg.get_node(it2);
66  return node1.function_id == node2.function_id && it1 == it2;
67 }
68 
75 std::vector<reachability_slicert::cfgt::node_indext>
77  std::vector<cfgt::node_indext> stack)
78 {
79  std::vector<cfgt::node_indext> return_sites;
80 
81  while(!stack.empty())
82  {
83  auto &node = cfg[stack.back()];
84  stack.pop_back();
85 
86  if(node.reaches_assertion)
87  continue;
88  node.reaches_assertion = true;
89 
90  for(const auto &edge : node.in)
91  {
92  const auto &pred_node = cfg[edge.first];
93 
94  if(pred_node.PC->is_end_function())
95  {
96  // This is an end-of-function -> successor-of-callsite edge.
97  // Record the return site for later investigation and step over it:
98  return_sites.push_back(edge.first);
99 
100  INVARIANT(
101  std::prev(node.PC)->is_function_call(),
102  "all function return edges should point to the successor of a "
103  "FUNCTION_CALL instruction");
104 
105  stack.push_back(cfg.get_node_index(std::prev(node.PC)));
106  }
107  else
108  {
109  stack.push_back(edge.first);
110  }
111  }
112  }
113 
114  return return_sites;
115 }
116 
127  std::vector<cfgt::node_indext> stack)
128 {
129  while(!stack.empty())
130  {
131  auto &node = cfg[stack.back()];
132  stack.pop_back();
133 
134  if(node.reaches_assertion)
135  continue;
136  node.reaches_assertion = true;
137 
138  for(const auto &edge : node.in)
139  {
140  const auto &pred_node = cfg[edge.first];
141 
142  if(pred_node.PC->is_end_function())
143  {
144  // This is an end-of-function -> successor-of-callsite edge.
145  // Walk into the called function, and then walk from the callsite
146  // backward:
147  stack.push_back(edge.first);
148 
149  INVARIANT(
150  std::prev(node.PC)->is_function_call(),
151  "all function return edges should point to the successor of a "
152  "FUNCTION_CALL instruction");
153 
154  stack.push_back(cfg.get_node_index(std::prev(node.PC)));
155  }
156  else if(pred_node.PC->is_function_call())
157  {
158  // Skip -- the callsite relevant to this function was already queued
159  // when we processed the return site.
160  }
161  else
162  {
163  stack.push_back(edge.first);
164  }
165  }
166  }
167 }
168 
176  const is_threadedt &is_threaded,
177  const slicing_criteriont &criterion)
178 {
179  std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
180 
181  // First walk outwards towards __CPROVER_start, visiting all possible callers
182  // and stepping over but recording callees as we go:
183  std::vector<cfgt::node_indext> return_sites =
185 
186  // Now walk into those callees, restricting our walk to the known callsites:
187  backward_inwards_walk_from(return_sites);
188 }
189 
199  const cfgt::nodet &call_node,
200  std::vector<cfgt::node_indext> &callsite_successor_stack,
201  std::vector<cfgt::node_indext> &callee_head_stack)
202 {
203  // Get the instruction's natural successor (function head, or next
204  // instruction if the function is bodyless)
205  INVARIANT(call_node.out.size() == 1, "Call sites should have one successor");
206  const auto successor_index = call_node.out.begin()->first;
207 
208  auto callsite_successor_pc = std::next(call_node.PC);
209 
210  auto successor_pc = cfg[successor_index].PC;
211  if(!is_same_target(successor_pc, callsite_successor_pc))
212  {
213  // Real call -- store the callee head node:
214  callee_head_stack.push_back(successor_index);
215 
216  // Check if it can return, and if so store the callsite's successor:
217  while(!successor_pc->is_end_function())
218  ++successor_pc;
219 
220  if(!cfg.get_node(successor_pc).out.empty())
221  callsite_successor_stack.push_back(
222  cfg.get_node_index(callsite_successor_pc));
223  }
224  else
225  {
226  // Bodyless function -- mark the successor instruction only.
227  callsite_successor_stack.push_back(successor_index);
228  }
229 }
230 
237 std::vector<reachability_slicert::cfgt::node_indext>
239  std::vector<cfgt::node_indext> stack)
240 {
241  std::vector<cfgt::node_indext> called_function_heads;
242 
243  while(!stack.empty())
244  {
245  auto &node = cfg[stack.back()];
246  stack.pop_back();
247 
248  if(node.reachable_from_assertion)
249  continue;
250  node.reachable_from_assertion = true;
251 
252  if(node.PC->is_function_call())
253  {
254  // Store the called function head for the later inwards walk;
255  // visit the call instruction's local successor now.
256  forward_walk_call_instruction(node, stack, called_function_heads);
257  }
258  else
259  {
260  // General case, including end of function: queue all successors.
261  for(const auto &edge : node.out)
262  stack.push_back(edge.first);
263  }
264  }
265 
266  return called_function_heads;
267 }
268 
277  std::vector<cfgt::node_indext> stack)
278 {
279  while(!stack.empty())
280  {
281  auto &node = cfg[stack.back()];
282  stack.pop_back();
283 
284  if(node.reachable_from_assertion)
285  continue;
286  node.reachable_from_assertion = true;
287 
288  if(node.PC->is_function_call())
289  {
290  // Visit both the called function head and the callsite successor:
291  forward_walk_call_instruction(node, stack, stack);
292  }
293  else if(node.PC->is_end_function())
294  {
295  // Special case -- the callsite successor was already queued when entering
296  // this function, more precisely than we can see from the function return
297  // edges (which lead to all possible callers), so nothing to do here.
298  }
299  else
300  {
301  // General case: queue all successors.
302  for(const auto &edge : node.out)
303  stack.push_back(edge.first);
304  }
305  }
306 }
307 
315  const is_threadedt &is_threaded,
316  const slicing_criteriont &criterion)
317 {
318  std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
319 
320  // First walk outwards towards __CPROVER_start, visiting all possible callers
321  // and stepping over but recording callees as we go:
322  std::vector<cfgt::node_indext> return_sites =
324 
325  // Now walk into those callees, restricting our walk to the known callsites:
326  forward_inwards_walk_from(return_sites);
327 }
328 
332 {
333  // now replace those instructions that do not reach any assertions
334  // by assume(false)
335 
336  for(auto &gf_entry : goto_functions.function_map)
337  {
338  if(gf_entry.second.body_available())
339  {
340  Forall_goto_program_instructions(i_it, gf_entry.second.body)
341  {
342  cfgt::nodet &e = cfg.get_node(i_it);
343  if(
344  !e.reaches_assertion && !e.reachable_from_assertion &&
345  !i_it->is_end_function())
346  {
348  false_exprt(), i_it->source_location());
349  }
350  }
351 
352  // replace unreachable code by skip
353  remove_unreachable(gf_entry.second.body);
354  }
355  }
356 
357  // remove the skips
358  remove_skip(goto_functions);
359 }
360 
368  goto_modelt &goto_model,
369  const bool include_forward_reachability)
370 {
373  s(goto_model.goto_functions, a, include_forward_reachability);
374 }
375 
384  goto_modelt &goto_model,
385  const std::list<std::string> &properties,
386  const bool include_forward_reachability)
387 {
389  properties_criteriont p(properties);
390  s(goto_model.goto_functions, p, include_forward_reachability);
391 }
392 
399  goto_modelt &goto_model,
400  const std::list<std::string> &functions_list)
401 {
402  for(const auto &function : functions_list)
403  {
404  in_function_criteriont matching_criterion(function);
405  reachability_slicert slicer;
406  slicer(goto_model.goto_functions, matching_criterion, true);
407  }
408 
409  remove_calls_no_bodyt remove_calls_no_body;
410  remove_calls_no_body(goto_model.goto_functions);
411 
412  goto_model.goto_functions.update();
414 }
415 
421 {
422  reachability_slicer(goto_model, false);
423 }
424 
431  goto_modelt &goto_model,
432  const std::list<std::string> &properties)
433 {
434  reachability_slicer(goto_model, properties, false);
435 }
Control Flow Graph.
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
Definition: cfg.h:259
base_grapht::nodet nodet
Definition: cfg.h:92
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
Definition: cfg.h:239
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
Definition: cfg.h:245
const source_locationt & source_location() const
Definition: expr.h:230
The Boolean constant false.
Definition: std_expr.h:2865
A collection of goto functions.
void compute_loop_numbers()
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:934
instructionst::const_iterator const_targett
Definition: goto_program.h:593
edgest out
Definition: graph.h:42
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
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,...
bool is_same_target(goto_programt::const_targett it1, goto_programt::const_targett it2) const
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,...
void backward_inwards_walk_from(std::vector< cfgt::node_indext >)
Perform backward 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,...
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,...
void forward_inwards_walk_from(std::vector< cfgt::node_indext >)
Perform forwards depth-first search of the control-flow graph of the goto program,...
void slice(goto_functionst &goto_functions)
This function removes all instructions that have the flag reaches_assertion or reachable_from_asserti...
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.
Goto Program Slicing.
#define Forall_goto_program_instructions(it, program)
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.
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.
Remove calls to functions without a body.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
Program Transformation.
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
Program Transformation.