cprover
Loading...
Searching...
No Matches
static_analysis.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Static Analysis
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_ANALYSES_STATIC_ANALYSIS_H
13#define CPROVER_ANALYSES_STATIC_ANALYSIS_H
14
15#ifndef USE_DEPRECATED_STATIC_ANALYSIS_H
16#error Deprecated, use ai.h instead
17#endif
18
19#include <iosfwd>
20#include <map>
21#include <memory>
22#include <unordered_set>
23
24#include <util/make_unique.h>
25
27
28// don't use me -- I am just a base class
29// please derive from me
31{
32public:
34 {
35 }
36
37 virtual ~domain_baset()
38 {
39 }
40
42
43 // will go away,
44 // to be replaced by a factory class option to static_analysist
45 virtual void initialize(
46 const namespacet &,
48 {
49 }
50
51 // how function calls are treated:
52 // a) there is an edge from each call site to the function head
53 // b) there is an edge from each return to the last instruction (END_FUNCTION)
54 // of each function
55 // c) there is an edge from the last instruction of the function
56 // to the instruction following the call site
57 // (for setting the LHS)
58
59 virtual void transform(
60 const namespacet &ns,
61 const irep_idt &function_from,
62 locationt from,
63 const irep_idt &function_to,
64 locationt to) = 0;
65
66 virtual void output(
67 const namespacet &,
68 std::ostream &) const
69 {
70 }
71
72 typedef std::unordered_set<exprt, irep_hash> expr_sett;
73
74 // will go away
75 virtual void get_reference_set(
76 const namespacet &,
77 const exprt &,
78 std::list<exprt> &dest)
79 {
80 // dummy, overload me!
81 dest.clear();
82 }
83
84 // also add
85 //
86 // bool merge(const T &b, locationt to);
87 //
88 // this computes the join between "this" and "b"
89 // return true if "this" has changed
90
91protected:
92 bool seen;
93
95};
96
97// don't use me -- I am just a base class
98// use static_analysist instead
100{
101public:
104
105 explicit static_analysis_baset(const namespacet &_ns):
106 ns(_ns),
107 initialized(false)
108 {
109 }
110
111 virtual void initialize(
112 const goto_programt &goto_program)
113 {
114 if(!initialized)
115 {
116 initialized=true;
117 generate_states(goto_program);
118 }
119 }
120
121 virtual void initialize(
122 const goto_functionst &goto_functions)
123 {
124 if(!initialized)
125 {
126 initialized=true;
127 generate_states(goto_functions);
128 }
129 }
130
131 virtual void update(const goto_programt &goto_program);
132 virtual void update(const goto_functionst &goto_functions);
133
134 virtual void operator()(
135 const irep_idt &function_identifier,
136 const goto_programt &goto_program);
137
138 virtual void operator()(
139 const goto_functionst &goto_functions);
140
142 {
143 }
144
145 virtual void clear()
146 {
147 initialized=false;
148 }
149
150 virtual void output(
151 const goto_functionst &goto_functions,
152 std::ostream &out) const;
153
154 void output(
155 const goto_programt &goto_program,
156 std::ostream &out) const
157 {
158 output(goto_program, irep_idt(), out);
159 }
160
161 virtual bool has_location(locationt l) const=0;
162
164 {
166 }
167
168 // utilities
169
170 // get guard of a conditional edge
171 static exprt get_guard(locationt from, locationt to);
172
173 // get lhs that return value is assigned to
174 // for an edge that returns from a function
175 static exprt get_return_lhs(locationt to);
176
177protected:
179
180 virtual void output(
181 const goto_programt &goto_program,
182 const irep_idt &identifier,
183 std::ostream &out) const;
184
185 typedef std::map<unsigned, locationt> working_sett;
186
187 locationt get_next(working_sett &working_set);
188
190 working_sett &working_set,
191 locationt l)
192 {
193 working_set.insert(
194 std::pair<unsigned, locationt>(l->location_number, l));
195 }
196
197 // true = found something new
198 bool fixedpoint(
199 const irep_idt &function_identifier,
200 const goto_programt &goto_program,
201 const goto_functionst &goto_functions);
202
203 virtual void fixedpoint(
204 const goto_functionst &goto_functions)=0;
205
207 const goto_functionst &goto_functions);
209 const goto_functionst &goto_functions);
210
211 // true = found something new
212 bool visit(
213 const irep_idt &function_identifier,
214 locationt l,
215 working_sett &working_set,
216 const goto_programt &goto_program,
217 const goto_functionst &goto_functions);
218
220 {
221 l++;
222 return l;
223 }
224
225 virtual bool merge(statet &a, const statet &b, locationt to)=0;
226 // for concurrent fixedpoint
227 virtual bool merge_shared(statet &a, const statet &b, locationt to)=0;
228
229 typedef std::set<irep_idt> functions_donet;
231
232 typedef std::set<irep_idt> recursion_sett;
234
235 void generate_states(
236 const goto_functionst &goto_functions);
237
238 void generate_states(
239 const goto_programt &goto_program);
240
242
243 // function calls
245 const irep_idt &calling_function,
246 locationt l_call,
247 locationt l_return,
248 const exprt &function,
249 const exprt::operandst &arguments,
250 statet &new_state,
251 const goto_functionst &goto_functions);
252
253 void do_function_call(
254 const irep_idt &calling_function,
255 locationt l_call,
256 locationt l_return,
257 const goto_functionst &goto_functions,
258 const goto_functionst::function_mapt::const_iterator f_it,
259 const exprt::operandst &arguments,
260 statet &new_state);
261
262 // abstract methods
263
264 virtual void generate_state(locationt l)=0;
266 virtual const statet &get_state(locationt l) const=0;
267 virtual std::unique_ptr<statet> make_temporary_state(statet &s)=0;
268
270
271 virtual void get_reference_set(
272 locationt l,
273 const exprt &expr,
274 std::list<exprt> &dest)=0;
275};
276
277// T is expected to be derived from domain_baset
278template<typename T>
280{
281public:
282 // constructor
283 explicit static_analysist(const namespacet &_ns):
285 {
286 }
287
289
291 {
292 typename state_mapt::iterator it=state_map.find(l);
293 if(it==state_map.end())
294 throw std::out_of_range("failed to find state");
295
296 return it->second;
297 }
298
299 const T &operator[](locationt l) const
300 {
301 typename state_mapt::const_iterator it=state_map.find(l);
302 if(it==state_map.end())
303 throw std::out_of_range("failed to find state");
304
305 return it->second;
306 }
307
308 virtual void clear()
309 {
310 state_map.clear();
312 }
313
314 virtual bool has_location(locationt l) const
315 {
316 return state_map.count(l)!=0;
317 }
318
319protected:
320 typedef std::map<locationt, T> state_mapt;
322
324 {
325 typename state_mapt::iterator it=state_map.find(l);
326 if(it==state_map.end())
327 throw std::out_of_range("failed to find state");
328
329 return it->second;
330 }
331
332 virtual const statet &get_state(locationt l) const
333 {
334 typename state_mapt::const_iterator it=state_map.find(l);
335 if(it==state_map.end())
336 throw std::out_of_range("failed to find state");
337
338 return it->second;
339 }
340
341 virtual bool merge(statet &a, const statet &b, locationt to)
342 {
343 return static_cast<T &>(a).merge(static_cast<const T &>(b), to);
344 }
345
346 virtual std::unique_ptr<statet> make_temporary_state(statet &s)
347 {
348 return util_make_unique<T>(static_cast<T &>(s));
349 }
350
351 virtual void generate_state(locationt l)
352 {
353 state_map[l].initialize(ns, l);
354 }
355
356 virtual void get_reference_set(
357 locationt l,
358 const exprt &expr,
359 std::list<exprt> &dest)
360 {
361 state_map[l].get_reference_set(ns, expr, dest);
362 }
363
364 virtual void fixedpoint(const goto_functionst &goto_functions)
365 {
366 sequential_fixedpoint(goto_functions);
367 }
368
369private:
370 // to enforce that T is derived from domain_baset
371 void dummy(const T &s) { const statet &x=dummy1(s); (void)x; }
372
373 // not implemented in sequential analyses
374 virtual bool merge_shared(
375 statet &,
376 const statet &,
378 {
379 throw "not implemented";
380 }
381};
382
383template<typename T>
385{
386public:
387 // constructor
389 static_analysist<T>(_ns)
390 {
391 }
392
393 virtual bool merge_shared(
397 {
398 return static_cast<T &>(a).merge_shared(
399 this->ns,
400 static_cast<const T &>(b),
401 to);
402 }
403
404protected:
405 virtual void fixedpoint(const goto_functionst &goto_functions)
406 {
407 this->concurrent_fixedpoint(goto_functions);
408 }
409};
410
411#endif // CPROVER_ANALYSES_STATIC_ANALYSIS_H
virtual bool merge_shared(static_analysis_baset::statet &a, const static_analysis_baset::statet &b, goto_programt::const_targett to)
virtual void fixedpoint(const goto_functionst &goto_functions)
concurrency_aware_static_analysist(const namespacet &_ns)
virtual void initialize(const namespacet &, locationt)
std::unordered_set< exprt, irep_hash > expr_sett
virtual void output(const namespacet &, std::ostream &) const
goto_programt::const_targett locationt
virtual void get_reference_set(const namespacet &, const exprt &, std::list< exprt > &dest)
virtual void transform(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to)=0
virtual ~domain_baset()
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
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
const namespacet & ns
virtual std::unique_ptr< statet > make_temporary_state(statet &s)=0
virtual void fixedpoint(const goto_functionst &goto_functions)=0
void generate_states(const goto_functionst &goto_functions)
void insert(locationt l)
void output(const goto_programt &goto_program, std::ostream &out) const
void do_function_call(const irep_idt &calling_function, locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
locationt get_next(working_sett &working_set)
virtual bool has_location(locationt l) const =0
bool visit(const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
bool fixedpoint(const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void get_reference_set(locationt l, const exprt &expr, std::list< exprt > &dest)=0
void put_in_working_set(working_sett &working_set, locationt l)
void sequential_fixedpoint(const goto_functionst &goto_functions)
std::set< irep_idt > functions_donet
void concurrent_fixedpoint(const goto_functionst &goto_functions)
virtual void operator()(const irep_idt &function_identifier, const goto_programt &goto_program)
static exprt get_return_lhs(locationt to)
std::set< irep_idt > recursion_sett
virtual void generate_state(locationt l)=0
domain_baset::expr_sett expr_sett
virtual void update(const goto_programt &goto_program)
void do_function_call_rec(const irep_idt &calling_function, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
static locationt successor(locationt l)
static exprt get_guard(locationt from, locationt to)
functions_donet functions_done
virtual statet & get_state(locationt l)=0
virtual void initialize(const goto_programt &goto_program)
std::map< unsigned, locationt > working_sett
virtual const statet & get_state(locationt l) const =0
static_analysis_baset(const namespacet &_ns)
virtual void initialize(const goto_functionst &goto_functions)
goto_programt::const_targett locationt
virtual bool merge_shared(statet &a, const statet &b, locationt to)=0
virtual ~static_analysis_baset()
virtual bool merge(statet &a, const statet &b, locationt to)=0
virtual void output(const goto_functionst &goto_functions, std::ostream &out) const
recursion_sett recursion_set
static_analysist(const namespacet &_ns)
T & operator[](locationt l)
virtual void generate_state(locationt l)
std::map< locationt, T > state_mapt
virtual void get_reference_set(locationt l, const exprt &expr, std::list< exprt > &dest)
virtual bool has_location(locationt l) const
virtual const statet & get_state(locationt l) const
state_mapt state_map
goto_programt::const_targett locationt
const T & operator[](locationt l) const
virtual void clear()
virtual std::unique_ptr< statet > make_temporary_state(statet &s)
virtual void fixedpoint(const goto_functionst &goto_functions)
virtual statet & get_state(locationt l)
virtual bool merge_shared(statet &, const statet &, goto_programt::const_targett)
virtual bool merge(statet &a, const statet &b, locationt to)
void dummy(const T &s)
Goto Programs with Functions.
dstringt irep_idt
Definition: irep.h:37