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