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  forall_goto_functions(f_it, goto_functions)
32  {
33  forall_goto_program_instructions(i_it, f_it->second.body)
34  cfg[cfg.entry_map[i_it]].function_id = f_it->first;
35  }
36 
37  is_threadedt is_threaded(goto_functions);
38  fixedpoint_to_assertions(is_threaded, criterion);
39  if(include_forward_reachability)
40  fixedpoint_from_assertions(is_threaded, criterion);
41  slice(goto_functions);
42  }
43 
44 protected:
46  {
48  {
49  }
50 
54  };
55 
56  bool is_same_target(
59 
62 
63  typedef std::stack<cfgt::entryt> queuet;
64 
69  {
72 
81 
84  {
85  }
86  };
87 
89  const is_threadedt &is_threaded,
90  const slicing_criteriont &criterion);
91 
93  const is_threadedt &is_threaded,
94  const slicing_criteriont &criterion);
95 
96  void slice(goto_functionst &goto_functions);
97 
98 private:
99  std::vector<cfgt::node_indext>
100  backward_outwards_walk_from(std::vector<cfgt::node_indext>);
101 
102  void backward_inwards_walk_from(std::vector<cfgt::node_indext>);
103 
104  std::vector<cfgt::node_indext>
105  forward_outwards_walk_from(std::vector<cfgt::node_indext>);
106 
107  void forward_inwards_walk_from(std::vector<cfgt::node_indext>);
108 
110  const cfgt::nodet &call_node,
111  std::vector<cfgt::node_indext> &callsite_successor_stack,
112  std::vector<cfgt::node_indext> &callee_head_stack);
113 
114  std::vector<cfgt::node_indext> get_sources(
115  const is_threadedt &is_threaded,
116  const slicing_criteriont &criterion);
117 };
118 
119 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
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_slicert::search_stack_entryt::node_index
cfgt::node_indext node_index
CFG node to mark reachable.
Definition: reachability_slicer_class.h:71
reachability_slicert::cfgt
cfg_baset< slicer_entryt > cfgt
Definition: reachability_slicer_class.h:60
slicing_criteriont
Definition: full_slicer.h:33
reachability_slicert::slicer_entryt::reachable_from_assertion
bool reachable_from_assertion
Definition: reachability_slicer_class.h:53
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_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
reachability_slicert::slicer_entryt::reaches_assertion
bool reaches_assertion
Definition: reachability_slicer_class.h:52
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
reachability_slicert::search_stack_entryt::search_stack_entryt
search_stack_entryt(cfgt::node_indext node_index, bool caller_is_known)
Definition: reachability_slicer_class.h:82
grapht< cfg_base_nodet< slicer_entryt, goto_programt::const_targett > >::node_indext
nodet::node_indext node_indext
Definition: graph.h:174
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
reachability_slicert::search_stack_entryt::caller_is_known
bool caller_is_known
If true, this function's caller is known and has already been queued to mark reachable,...
Definition: reachability_slicer_class.h:80
reachability_slicert::slicer_entryt::slicer_entryt
slicer_entryt()
Definition: reachability_slicer_class.h:47
is_threaded.h
Over-approximate Concurrency for Threaded Goto Programs.
reachability_slicert::operator()
void operator()(goto_functionst &goto_functions, const slicing_criteriont &criterion, bool include_forward_reachability)
Definition: reachability_slicer_class.h:25
reachability_slicert::slicer_entryt
Definition: reachability_slicer_class.h:46
cfg_baset::entry_map
entry_mapt entry_map
Definition: cfg.h:152
cfg_baset< slicer_entryt >
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
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
reachability_slicert::slicer_entryt::function_id
irep_idt function_id
Definition: reachability_slicer_class.h:51
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
goto_functions.h
Goto Programs with Functions.
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
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
reachability_slicert::queuet
std::stack< cfgt::entryt > queuet
Definition: reachability_slicer_class.h:63
reachability_slicert::search_stack_entryt
A search stack entry, used in tracking nodes to mark reachable when walking over the CFG in fixedpoin...
Definition: reachability_slicer_class.h:69
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
reachability_slicert::cfg
cfgt cfg
Definition: reachability_slicer_class.h:61
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196