cprover
reachability_slicer_class.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Program Slicing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
13 #define CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
14 
16 #include <goto-programs/cfg.h>
17 
18 #include <analyses/is_threaded.h>
19 
20 class slicing_criteriont;
21 
23 {
24 public:
25  void operator()(
26  goto_functionst &goto_functions,
27  const slicing_criteriont &criterion,
28  bool include_forward_reachability)
29  {
30  cfg(goto_functions);
31  is_threadedt is_threaded(goto_functions);
32  fixedpoint_to_assertions(is_threaded, criterion);
33  if(include_forward_reachability)
34  fixedpoint_from_assertions(is_threaded, criterion);
35  slice(goto_functions);
36  }
37 
38 protected:
40  {
42  {
43  }
44 
47  };
48 
51 
52  typedef std::stack<cfgt::entryt> queuet;
53 
58  {
61 
70 
73  {
74  }
75  };
76 
78  const is_threadedt &is_threaded,
79  const slicing_criteriont &criterion);
80 
82  const is_threadedt &is_threaded,
83  const slicing_criteriont &criterion);
84 
85  void slice(goto_functionst &goto_functions);
86 
87 private:
88  std::vector<cfgt::node_indext>
89  backward_outwards_walk_from(std::vector<cfgt::node_indext>);
90 
91  void backward_inwards_walk_from(std::vector<cfgt::node_indext>);
92 
93  std::vector<cfgt::node_indext>
94  forward_outwards_walk_from(std::vector<cfgt::node_indext>);
95 
96  void forward_inwards_walk_from(std::vector<cfgt::node_indext>);
97 
99  const cfgt::nodet &call_node,
100  std::vector<cfgt::node_indext> &callsite_successor_stack,
101  std::vector<cfgt::node_indext> &callee_head_stack);
102 
103  std::vector<cfgt::node_indext> get_sources(
104  const is_threadedt &is_threaded,
105  const slicing_criteriont &criterion);
106 };
107 
108 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
Over-approximate Concurrency for Threaded Goto Programs.
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,...
Control Flow Graph.
search_stack_entryt(cfgt::node_indext node_index, bool caller_is_known)
Goto Programs with Functions.
cfgt::node_indext node_index
CFG node to mark reachable.
std::stack< cfgt::entryt > queuet
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
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.
bool caller_is_known
If true, this function's caller is known and has already been queued to mark reachable,...
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.
cfg_baset< slicer_entryt > cfgt
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,...
A search stack entry, used in tracking nodes to mark reachable when walking over the CFG in fixedpoin...
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,...
void operator()(goto_functionst &goto_functions, const slicing_criteriont &criterion, bool include_forward_reachability)