CBMC
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 message_handlert &message_handler);
46
47protected:
48 struct cfg_nodet
49 {
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,
75
77 const cfgt::nodet &node,
78 queuet &queue,
81
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,
91
92 void add_jumps(
93 queuet &queue,
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{
113public:
114 virtual bool
116 {
117 return target->is_assert();
118 }
119};
120
122{
123public:
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
135protected:
137};
138
140{
141public:
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
167protected:
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:38
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, 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)
A collection of goto functions.
instructionst::const_iterator const_targett
N nodet
Definition graph.h:169
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:44