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