cprover
Loading...
Searching...
No Matches
full_slicer_class.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Program Slicing
4
5Author: 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
28useful for debugging (remove NOLINT)
29goto-instrument --full-slice a.out c.out
30goto-instrument --show-goto-functions c.out > c.goto
31echo '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{
40public:
41 void operator()(
42 goto_functionst &goto_functions,
43 const namespacet &ns,
45
46protected:
47 struct cfg_nodet
48 {
52
55#ifdef DEBUG_FULL_SLICERT
56 std::set<unsigned> required_by;
57#endif
58 };
59
62
63 typedef std::vector<cfgt::entryt> dep_node_to_cfgt;
64 typedef std::stack<cfgt::entryt> queuet;
65 typedef std::list<cfgt::entryt> jumpst;
66 typedef std::unordered_map<irep_idt, queuet> decl_deadt;
67
68 void fixedpoint(
69 goto_functionst &goto_functions,
70 queuet &queue,
74
76 const cfgt::nodet &node,
77 queuet &queue,
80
82 const cfgt::nodet &node,
83 queuet &queue,
84 const goto_functionst &goto_functions);
85
86 void add_decl_dead(
87 const cfgt::nodet &node,
88 queuet &queue,
90
91 void add_jumps(
92 queuet &queue,
94 const dependence_grapht::post_dominators_mapt &post_dominators);
95
97 queuet &queue,
98 const cfgt::entryt &entry,
100 {
101#ifdef DEBUG_FULL_SLICERT
102 cfg[entry].required_by.insert(reason->location_number);
103#else
104 (void)reason; // unused parameter
105#endif
106 queue.push(entry);
107 }
108};
109
111{
112public:
113 virtual bool
115 {
116 return target->is_assert();
117 }
118};
119
121{
122public:
123 explicit in_function_criteriont(const std::string &function_name)
124 : target_function(function_name)
125 {
126 }
127
128 virtual bool
130 {
131 return function_id == target_function;
132 }
133
134protected:
136};
137
139{
140public:
142 const std::list<std::string> &properties):
143 property_ids(properties)
144 {
145 }
146
147 virtual bool
149 {
150 if(!target->is_assert())
151 return false;
152
153 const std::string &p_id =
154 id2string(target->source_location().get_property_id());
155
156 for(std::list<std::string>::const_iterator
157 it=property_ids.begin();
158 it!=property_ids.end();
159 ++it)
160 if(p_id==*it)
161 return true;
162
163 return false;
164 }
165
166protected:
167 const std::list<std::string> &property_ids;
168};
169
170#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:199
Control Flow Graph.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
virtual bool operator()(const irep_idt &, goto_programt::const_targett target) const
base_grapht::node_indext entryt
Definition cfg.h:91
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:39
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
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)
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)
void operator()(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
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)
A collection of goto functions.
instructionst::const_iterator const_targett
virtual bool operator()(const irep_idt &function_id, goto_programt::const_targett) const
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:91
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:47