cprover
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:
40 changed(false)
41 {
42 }
43
45
46 virtual void initialize(const namespacet &ns)=0;
47
48 virtual bool transform(
49 const namespacet &ns,
50 const irep_idt &function_from,
51 locationt from,
52 const irep_idt &function_to,
53 locationt to) = 0;
54
56 {
57 }
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
83 exprt get_guard(locationt from, locationt to) const;
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> seen_locations;
97
98 std::map<locationt, unsigned> statistics;
99
100 bool seen(const locationt &l)
101 {
102 return (seen_locations.find(l)!=seen_locations.end());
103 }
104
106 ns(_ns),
107 initialized(false)
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<locationt> working_sett;
159
160 locationt get_next(working_sett &working_set);
161
163 working_sett &working_set,
164 locationt l)
165 {
166 working_set.push(l);
167 }
168
169 // true = found something new
170 bool fixedpoint(
171 const irep_idt &function_id,
172 const goto_programt &goto_program,
173 const goto_functionst &goto_functions);
174
175 void fixedpoint(
176 const goto_functionst &goto_functions);
177
178 // true = found something new
179 bool visit(
180 const irep_idt &function_id,
181 locationt l,
182 working_sett &working_set,
183 const goto_programt &goto_program,
184 const goto_functionst &goto_functions);
185
187 {
188 l++;
189 return l;
190 }
191
192 typedef std::set<irep_idt> functions_donet;
194
195 typedef std::set<irep_idt> recursion_sett;
197
199
200 // function calls
202 const irep_idt &calling_function,
203 locationt l_call,
204 const exprt &function,
205 const exprt::operandst &arguments,
206 statet &new_state,
207 const goto_functionst &goto_functions);
208
209 bool do_function_call(
210 const irep_idt &calling_function,
211 locationt l_call,
212 const goto_functionst &goto_functions,
213 const goto_functionst::function_mapt::const_iterator f_it,
214 const exprt::operandst &arguments,
215 statet &new_state);
216
217 // abstract methods
218
219 virtual statet &get_state()=0;
220 virtual const statet &get_state() const=0;
221
223
224 virtual void get_reference_set(
225 const exprt &expr,
226 expr_sett &expr_set)=0;
227};
228
229
230template<typename T>
232{
233public:
234 // constructor
237 {
238 }
239
241
242 virtual void clear()
243 {
244 state.clear();
246 }
247
248 T &get_data() { return state; }
249 const T &get_data() const { return state; }
250
251protected:
252 T state; // one global state
253
254 virtual statet &get_state() { return state; }
255
256 virtual const statet &get_state() const { return state; }
257
259 const exprt &expr,
260 expr_sett &expr_set)
261 {
262 state.get_reference_set(ns, expr, expr_set);
263 }
264
265private:
266 // to enforce that T is derived from abstract_domain_baset
267 void dummy(const T &s) { const statet &x=dummy1(s); (void)x; }
268};
269
270#endif // CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
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
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
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)
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 &)
std::priority_queue< locationt > working_sett
std::map< locationt, unsigned > statistics
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.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:593
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.