cprover
Loading...
Searching...
No Matches
reachability_slicer.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Slicer
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
15
16#include "reachability_slicer.h"
17
18#include <goto-programs/cfg.h>
22
24
25#include "full_slicer_class.h"
27
33std::vector<reachability_slicert::cfgt::node_indext>
35 const is_threadedt &is_threaded,
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
75std::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,
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:
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
212 {
213 // Real call -- store the callee head node:
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(
223 }
224 else
225 {
226 // Bodyless function -- mark the successor instruction only.
228 }
229}
230
237std::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.
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
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,
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:
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 {
341 {
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
375
384 goto_modelt &goto_model,
385 const std::list<std::string> &properties,
387{
389 properties_criteriont p(properties);
391}
392
399 goto_modelt &goto_model,
400 const std::list<std::string> &functions_list)
401{
402 for(const auto &function : functions_list)
403 {
406 slicer(goto_model.goto_functions, matching_criterion, true);
407 }
408
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
Definition cfg.h:259
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
Definition cfg.h:245
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
Definition cfg.h:239
The Boolean constant false.
Definition std_expr.h:2865
A collection of goto functions.
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())
instructionst::const_iterator const_targett
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
Program Transformation.
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
Program Transformation.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423