CBMC
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  message_handlert &message_handler);
46 
47 protected:
48  struct cfg_nodet
49  {
51  {
52  }
53 
56 #ifdef DEBUG_FULL_SLICERT
57  std::set<unsigned> required_by;
58 #endif
59  };
60 
63 
64  typedef std::vector<cfgt::entryt> dep_node_to_cfgt;
65  typedef std::stack<cfgt::entryt> queuet;
66  typedef std::list<cfgt::entryt> jumpst;
67  typedef std::unordered_map<irep_idt, queuet> decl_deadt;
68 
69  void fixedpoint(
70  goto_functionst &goto_functions,
71  queuet &queue,
72  jumpst &jumps,
73  decl_deadt &decl_dead,
74  const dependence_grapht &dep_graph);
75 
76  void add_dependencies(
77  const cfgt::nodet &node,
78  queuet &queue,
79  const dependence_grapht &dep_graph,
80  const dep_node_to_cfgt &dep_node_to_cfg);
81 
82  void add_function_calls(
83  const cfgt::nodet &node,
84  queuet &queue,
85  const goto_functionst &goto_functions);
86 
87  void add_decl_dead(
88  const cfgt::nodet &node,
89  queuet &queue,
90  decl_deadt &decl_dead);
91 
92  void add_jumps(
93  queuet &queue,
94  jumpst &jumps,
95  const dependence_grapht::post_dominators_mapt &post_dominators);
96 
98  queuet &queue,
99  const cfgt::entryt &entry,
101  {
102 #ifdef DEBUG_FULL_SLICERT
103  cfg[entry].required_by.insert(reason->location_number);
104 #else
105  (void)reason; // unused parameter
106 #endif
107  queue.push(entry);
108  }
109 };
110 
112 {
113 public:
114  virtual bool
116  {
117  return target->is_assert();
118  }
119 };
120 
122 {
123 public:
124  explicit in_function_criteriont(const std::string &function_name)
125  : target_function(function_name)
126  {
127  }
128 
129  virtual bool
131  {
132  return function_id == target_function;
133  }
134 
135 protected:
137 };
138 
140 {
141 public:
143  const std::list<std::string> &properties):
144  property_ids(properties)
145  {
146  }
147 
148  virtual bool
150  {
151  if(!target->is_assert())
152  return false;
153 
154  const std::string &p_id =
155  id2string(target->source_location().get_property_id());
156 
157  for(std::list<std::string>::const_iterator
158  it=property_ids.begin();
159  it!=property_ids.end();
160  ++it)
161  if(p_id==*it)
162  return true;
163 
164  return false;
165  }
166 
167 protected:
168  const std::list<std::string> &property_ids;
169 };
170 
171 #endif // CPROVER_GOTO_INSTRUMENT_FULL_SLICER_CLASS_H
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:198
Control Flow Graph.
virtual bool operator()(const irep_idt &, goto_programt::const_targett target) const
base_grapht::node_indext entryt
Definition: cfg.h:91
base_grapht::nodet nodet
Definition: cfg.h:92
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
Definition: full_slicer.cpp:36
std::list< cfgt::entryt > jumpst
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
std::unordered_map< irep_idt, queuet > decl_deadt
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
cfg_baset< cfg_nodet > cfgt
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
Definition: full_slicer.cpp:54
void operator()(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion, message_handlert &message_handler)
std::stack< cfgt::entryt > queuet
std::vector< cfgt::entryt > dep_node_to_cfgt
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
Definition: full_slicer.cpp:85
A collection of goto functions.
instructionst::const_iterator const_targett
Definition: goto_program.h:615
virtual bool operator()(const irep_idt &function_id, goto_programt::const_targett) const
const irep_idt target_function
in_function_criteriont(const std::string &function_name)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
properties_criteriont(const std::list< std::string > &properties)
const std::list< std::string > & property_ids
virtual bool operator()(const irep_idt &, goto_programt::const_targett target) const
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40