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,
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 #endif
103  queue.push(entry);
104  }
105 };
106 
108 {
109 public:
111  {
112  return target->is_assert();
113  }
114 };
115 
117 {
118 public:
120  const std::list<std::string> &properties):
121  property_ids(properties)
122  {
123  }
124 
126  {
127  if(!target->is_assert())
128  return false;
129 
130  const std::string &p_id=
131  id2string(target->source_location.get_property_id());
132 
133  for(std::list<std::string>::const_iterator
134  it=property_ids.begin();
135  it!=property_ids.end();
136  ++it)
137  if(p_id==*it)
138  return true;
139 
140  return false;
141  }
142 
143 protected:
144  const std::list<std::string> &property_ids;
145 };
146 
147 #endif // CPROVER_GOTO_INSTRUMENT_FULL_SLICER_CLASS_H
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:22
void slice(symex_target_equationt &equation)
Definition: slice.cpp:209
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
Control Flow Graph.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
Goto Programs with Functions.
std::unordered_map< irep_idt, queuet > decl_deadt
virtual bool operator()(goto_programt::const_targett target)
properties_criteriont(const std::list< std::string > &properties)
std::size_t entryt
Definition: cfg.h:65
std::stack< cfgt::entryt > queuet
const std::list< std::string > & property_ids
cfg_base_nodet< cfg_nodet, goto_programt::const_targett > nodet
Definition: graph.h:136
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
instructionst::const_iterator const_targett
Definition: goto_program.h:398
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::list< cfgt::entryt > jumpst
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
Definition: full_slicer.cpp:62
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
Definition: full_slicer.cpp:38
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
goto_programt coverage_criteriont criterion
Definition: cover.cpp:63
Slicing.
cfg_baset< cfg_nodet > cfgt
void operator()(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
virtual bool operator()(goto_programt::const_targett target)
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
Definition: full_slicer.cpp:93
std::vector< cfgt::entryt > dep_node_to_cfgt