CBMC
Loading...
Searching...
No Matches
flow_insensitive_analysis.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Flow Insensitive Static Analysis
4
5Author: Daniel Kroening, kroening@kroening.com
6 CM Wintersteiger
7
8\*******************************************************************/
9
23
24#ifndef CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
25#define CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
26
27#include <queue>
28#include <map>
29#include <iosfwd>
30#include <unordered_set>
31
33
34// don't use me -- I am just a base class
35// please derive from me
37{
38public:
43
45
46 virtual void initialize(const namespacet &ns)=0;
47
48 virtual bool transform(
49 const namespacet &ns,
52 const irep_idt &function_to,
53 locationt to) = 0;
54
58
59 virtual void output(
60 const namespacet &,
61 std::ostream &) const
62 {
63 }
64
65 typedef std::unordered_set<exprt, irep_hash> expr_sett;
66
67 virtual void get_reference_set(
68 const namespacet &,
69 const exprt &,
70 expr_sett &expr_set)
71 {
72 // dummy, overload me!
73 expr_set.clear();
74 }
75
76 virtual void clear(void)=0;
77
78protected:
79 bool changed;
80 // utilities
81
82 // get guard of a conditional edge
84
85 // get lhs that return value is assigned to
86 // for an edge that returns from a function
88};
89
91{
92public:
95
96 std::set<locationt, goto_programt::target_less_than> seen_locations;
97
98 std::map<locationt, unsigned, goto_programt::target_less_than> statistics;
99
100 bool seen(const locationt &l)
101 {
102 return (seen_locations.find(l)!=seen_locations.end());
103 }
104
106 ns(_ns),
108 {
109 }
110
111 virtual void initialize(const goto_programt &)
112 {
113 if(!initialized)
114 {
115 initialized=true;
116 }
117 }
118
119 virtual void initialize(const goto_functionst &)
120 {
121 if(!initialized)
122 {
123 initialized=true;
124 }
125 }
126
127 virtual void update(const goto_programt &goto_program);
128
129 virtual void update(const goto_functionst &goto_functions);
130
131 virtual void
132 operator()(const irep_idt &function_id, const goto_programt &goto_program);
133
134 virtual void operator()(
135 const goto_functionst &goto_functions);
136
138 {
139 }
140
141 virtual void clear()
142 {
143 initialized=false;
144 }
145
146 virtual void output(
147 const goto_functionst &goto_functions,
148 std::ostream &out);
149
150 virtual void output(
151 const irep_idt &function_id,
152 const goto_programt &goto_program,
153 std::ostream &out);
154
155protected:
157
158 typedef std::priority_queue<
159 locationt,
160 std::vector<locationt>,
163
165
168 locationt l)
169 {
170 working_set.push(l);
171 }
172
173 // true = found something new
174 bool fixedpoint(
175 const irep_idt &function_id,
176 const goto_programt &goto_program,
177 const goto_functionst &goto_functions);
178
179 void fixedpoint(
180 const goto_functionst &goto_functions);
181
182 // true = found something new
183 bool visit(
184 const irep_idt &function_id,
185 locationt l,
187 const goto_programt &goto_program,
188 const goto_functionst &goto_functions);
189
191 {
192 l++;
193 return l;
194 }
195
196 typedef std::set<irep_idt> functions_donet;
198
199 typedef std::set<irep_idt> recursion_sett;
201
203
204 // function calls
206 const irep_idt &calling_function,
208 const exprt &function,
209 const exprt::operandst &arguments,
211 const goto_functionst &goto_functions);
212
213 bool do_function_call(
214 const irep_idt &calling_function,
216 const goto_functionst &goto_functions,
217 const goto_functionst::function_mapt::const_iterator f_it,
218 const exprt::operandst &arguments,
220
221 // abstract methods
222
223 virtual statet &get_state()=0;
224 virtual const statet &get_state() const=0;
225
227
228 virtual void get_reference_set(
229 const exprt &expr,
230 expr_sett &expr_set)=0;
231};
232
233
234template<typename T>
236{
237public:
238 // constructor
243
245
246 virtual void clear()
247 {
248 state.clear();
250 }
251
252 T &get_data() { return state; }
253 const T &get_data() const { return state; }
254
255protected:
256 T state; // one global state
257
258 virtual statet &get_state() { return state; }
259
260 virtual const statet &get_state() const { return state; }
261
263 const exprt &expr,
264 expr_sett &expr_set)
265 {
266 state.get_reference_set(ns, expr, expr_set);
267 }
268
269private:
270 // to enforce that T is derived from abstract_domain_baset
271 void dummy(const T &s) { const statet &x=dummy1(s); (void)x; }
272};
273
274#endif // CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
std::unordered_set< exprt, irep_hash > expr_sett
exprt get_guard(locationt from, locationt to) const
virtual void output(const namespacet &, std::ostream &) const
virtual void initialize(const namespacet &ns)=0
virtual void get_reference_set(const namespacet &, const exprt &, expr_sett &expr_set)
virtual bool transform(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to)=0
std::map< locationt, unsigned, goto_programt::target_less_than > statistics
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
std::priority_queue< locationt, std::vector< locationt >, goto_programt::target_less_than > working_sett
virtual void operator()(const irep_idt &function_id, const goto_programt &goto_program)
virtual void get_reference_set(const exprt &expr, expr_sett &expr_set)=0
locationt get_next(working_sett &working_set)
flow_insensitive_analysis_baset(const namespacet &_ns)
std::set< locationt, goto_programt::target_less_than > seen_locations
bool fixedpoint(const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions)
bool visit(const irep_idt &function_id, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
static locationt successor(locationt l)
virtual void update(const goto_programt &goto_program)
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
bool do_function_call_rec(const irep_idt &calling_function, locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
goto_programt::const_targett locationt
virtual void initialize(const goto_programt &)
virtual void initialize(const goto_functionst &)
void put_in_working_set(working_sett &working_set, locationt l)
virtual const statet & get_state() const =0
bool do_function_call(const irep_idt &calling_function, locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
flow_insensitive_abstract_domain_baset statet
virtual statet & get_state()=0
void get_reference_set(const exprt &expr, expr_sett &expr_set)
goto_programt::const_targett locationt
flow_insensitive_analysist(const namespacet &_ns)
virtual const statet & get_state() const
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Goto Programs with Functions.
A total order over targett and const_targett.