cprover
full_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_FULL_SLICER_CLASS_H
13 #define CPROVER_GOTO_INSTRUMENT_FULL_SLICER_CLASS_H
14 
15 #include <stack>
16 #include <vector>
17 #include <list>
18 
20 #include <goto-programs/cfg.h>
21 
23 
24 #include "full_slicer.h"
25 
26 // #define DEBUG_FULL_SLICERT
27 #if 0
28 useful for debugging (remove NOLINT)
29 goto-instrument --full-slice a.out c.out
30 goto-instrument --show-goto-functions c.out > c.goto
31 echo 'digraph g {' > c.dot ; cat c.goto | \
32  NOLINT(*) grep 'ins:[[:digit:]]\+ req by' | grep '^[[:space:]]*//' | \
33  NOLINT(*) perl -n -e '/file .*(.) line (\d+) column ins:(\d+) req by:([\d,]+).*/; $f=$3; $t=$4; @tt=split(",",$t); print "n$f [label=\"$f\"];\n"; print "n$f -> n$_;\n" foreach(@tt);' >> c.dot ; \
34  echo '}' >> c.dot ; tred c.dot > c-red.dot ; \
35  dot -Tpdf -oc-red.pdf c-red.dot
36 #endif
37 
39 {
40 public:
41  void operator()(
42  goto_functionst &goto_functions,
43  const namespacet &ns,
44  const slicing_criteriont &criterion);
45 
46 protected:
47  struct cfg_nodet
48  {
50  {
51  }
52 
54 #ifdef DEBUG_FULL_SLICERT
55  std::set<unsigned> required_by;
56 #endif
57  };
58 
61 
62  typedef std::vector<cfgt::entryt> dep_node_to_cfgt;
63  typedef std::stack<cfgt::entryt> queuet;
64  typedef std::list<cfgt::entryt> jumpst;
65  typedef std::unordered_map<irep_idt, queuet> decl_deadt;
66 
67  void fixedpoint(
68  goto_functionst &goto_functions,
69  queuet &queue,
70  jumpst &jumps,
71  decl_deadt &decl_dead,
72  const dependence_grapht &dep_graph);
73 
74  void add_dependencies(
75  const cfgt::nodet &node,
76  queuet &queue,
77  const dependence_grapht &dep_graph,
78  const dep_node_to_cfgt &dep_node_to_cfg);
79 
80  void add_function_calls(
81  const cfgt::nodet &node,
82  queuet &queue,
83  const goto_functionst &goto_functions);
84 
85  void add_decl_dead(
86  const cfgt::nodet &node,
87  queuet &queue,
88  decl_deadt &decl_dead);
89 
90  void add_jumps(
91  queuet &queue,
92  jumpst &jumps,
93  const dependence_grapht::post_dominators_mapt &post_dominators);
94 
96  queuet &queue,
97  const cfgt::entryt &entry,
99  {
100 #ifdef DEBUG_FULL_SLICERT
101  cfg[entry].required_by.insert(reason->location_number);
102 #else
103  (void)reason; // unused parameter
104 #endif
105  queue.push(entry);
106  }
107 };
108 
110 {
111 public:
112  virtual bool operator()(goto_programt::const_targett target) const
113  {
114  return target->is_assert();
115  }
116 };
117 
119 {
120 public:
121  explicit in_function_criteriont(const std::string &function_name)
122  : target_function(function_name)
123  {
124  }
125 
126  virtual bool operator()(goto_programt::const_targett target) const
127  {
128  return target->function == target_function;
129  }
130 
131 protected:
133 };
134 
136 {
137 public:
139  const std::list<std::string> &properties):
140  property_ids(properties)
141  {
142  }
143 
144  virtual bool operator()(goto_programt::const_targett target) const
145  {
146  if(!target->is_assert())
147  return false;
148 
149  const std::string &p_id=
150  id2string(target->source_location.get_property_id());
151 
152  for(std::list<std::string>::const_iterator
153  it=property_ids.begin();
154  it!=property_ids.end();
155  ++it)
156  if(p_id==*it)
157  return true;
158 
159  return false;
160  }
161 
162 protected:
163  const std::list<std::string> &property_ids;
164 };
165 
166 #endif // CPROVER_GOTO_INSTRUMENT_FULL_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:35
cfg.h
dependence_grapht
Definition: dependence_graph.h:217
properties_criteriont::operator()
virtual bool operator()(goto_programt::const_targett target) const
Definition: full_slicer_class.h:144
slicing_criteriont
Definition: full_slicer.h:32
full_slicert::cfg_nodet::node_required
bool node_required
Definition: full_slicer_class.h:53
properties_criteriont
Definition: full_slicer_class.h:135
full_slicert::queuet
std::stack< cfgt::entryt > queuet
Definition: full_slicer_class.h:63
full_slicert::cfg
cfgt cfg
Definition: full_slicer_class.h:60
assert_criteriont::operator()
virtual bool operator()(goto_programt::const_targett target) const
Definition: full_slicer_class.h:112
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
full_slicert::add_dependencies
void add_dependencies(const cfgt::nodet &node, queuet &queue, const dependence_grapht &dep_graph, const dep_node_to_cfgt &dep_node_to_cfg)
Definition: full_slicer.cpp:20
full_slicert
Definition: full_slicer_class.h:38
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
properties_criteriont::properties_criteriont
properties_criteriont(const std::list< std::string > &properties)
Definition: full_slicer_class.h:138
dependence_grapht::post_dominators_mapt
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
Definition: dependence_graph.h:225
full_slicert::dep_node_to_cfgt
std::vector< cfgt::entryt > dep_node_to_cfgt
Definition: full_slicer_class.h:62
full_slicert::add_decl_dead
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
Definition: full_slicer.cpp:60
full_slicer.h
full_slicert::cfgt
cfg_baset< cfg_nodet > cfgt
Definition: full_slicer_class.h:59
full_slicert::operator()
void operator()(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
Definition: full_slicer.cpp:284
full_slicert::add_jumps
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
Definition: full_slicer.cpp:91
cfg_baset< cfg_nodet >
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
in_function_criteriont::in_function_criteriont
in_function_criteriont(const std::string &function_name)
Definition: full_slicer_class.h:121
in_function_criteriont::operator()
virtual bool operator()(goto_programt::const_targett target) const
Definition: full_slicer_class.h:126
full_slicert::fixedpoint
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
Definition: full_slicer.cpp:215
full_slicert::cfg_nodet::cfg_nodet
cfg_nodet()
Definition: full_slicer_class.h:49
in_function_criteriont::target_function
const irep_idt target_function
Definition: full_slicer_class.h:132
in_function_criteriont
Definition: full_slicer_class.h:118
properties_criteriont::property_ids
const std::list< std::string > & property_ids
Definition: full_slicer_class.h:163
goto_functions.h
cfg_baset< cfg_nodet >::entryt
std::size_t entryt
Definition: cfg.h:65
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
full_slicert::jumpst
std::list< cfgt::entryt > jumpst
Definition: full_slicer_class.h:64
full_slicert::decl_deadt
std::unordered_map< irep_idt, queuet > decl_deadt
Definition: full_slicer_class.h:65
full_slicert::add_function_calls
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
Definition: full_slicer.cpp:36
assert_criteriont
Definition: full_slicer_class.h:109
full_slicert::add_to_queue
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
Definition: full_slicer_class.h:95
full_slicert::cfg_nodet
Definition: full_slicer_class.h:47
dependence_graph.h
grapht< cfg_base_nodet< cfg_nodet, goto_programt::const_targett > >::nodet
cfg_base_nodet< cfg_nodet, goto_programt::const_targett > nodet
Definition: graph.h:170
slice
void slice(symex_target_equationt &equation)
Definition: slice.cpp:208