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 <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 {
32 public:
33  domain_baset():seen(false)
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 &ns,
47  locationt l)
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  locationt from,
62  locationt to)=0;
63 
64  virtual void output(
65  const namespacet &ns,
66  std::ostream &out) const
67  {
68  }
69 
70  typedef std::unordered_set<exprt, irep_hash> expr_sett;
71 
72  // will go away
73  virtual void get_reference_set(
74  const namespacet &ns,
75  const exprt &expr,
76  std::list<exprt> &dest)
77  {
78  // dummy, overload me!
79  dest.clear();
80  }
81 
82  // also add
83  //
84  // bool merge(const T &b, locationt to);
85  //
86  // this computes the join between "this" and "b"
87  // return true if "this" has changed
88 
89 protected:
90  bool seen;
91 
92  friend class static_analysis_baset;
93 };
94 
95 // don't use me -- I am just a base class
96 // use static_analysist instead
98 {
99 public:
102 
103  explicit static_analysis_baset(const namespacet &_ns):
104  ns(_ns),
105  initialized(false)
106  {
107  }
108 
109  virtual void initialize(
111  {
112  if(!initialized)
113  {
114  initialized=true;
116  }
117  }
118 
119  virtual void initialize(
120  const goto_functionst &goto_functions)
121  {
122  if(!initialized)
123  {
124  initialized=true;
125  generate_states(goto_functions);
126  }
127  }
128 
129  virtual void update(const goto_programt &goto_program);
130  virtual void update(const goto_functionst &goto_functions);
131 
132  virtual void operator()(
133  const goto_programt &goto_program);
134 
135  virtual void operator()(
136  const goto_functionst &goto_functions);
137 
139  {
140  }
141 
142  virtual void clear()
143  {
144  initialized=false;
145  }
146 
147  virtual void output(
148  const goto_functionst &goto_functions,
149  std::ostream &out) const;
150 
151  void output(
153  std::ostream &out) const
154  {
155  output(goto_program, "", out);
156  }
157 
158  virtual bool has_location(locationt l) const=0;
159 
161  {
162  generate_state(l);
163  }
164 
165  // utilities
166 
167  // get guard of a conditional edge
168  static exprt get_guard(locationt from, locationt to);
169 
170  // get lhs that return value is assigned to
171  // for an edge that returns from a function
172  static exprt get_return_lhs(locationt to);
173 
174 protected:
175  const namespacet &ns;
176 
177  virtual void output(
179  const irep_idt &identifier,
180  std::ostream &out) const;
181 
182  typedef std::map<unsigned, locationt> working_sett;
183 
184  locationt get_next(working_sett &working_set);
185 
187  working_sett &working_set,
188  locationt l)
189  {
190  working_set.insert(
191  std::pair<unsigned, locationt>(l->location_number, l));
192  }
193 
194  // true = found something new
195  bool fixedpoint(
197  const goto_functionst &goto_functions);
198 
199  virtual void fixedpoint(
200  const goto_functionst &goto_functions)=0;
201 
203  const goto_functionst &goto_functions);
205  const goto_functionst &goto_functions);
206 
207  // true = found something new
208  bool visit(
209  locationt l,
210  working_sett &working_set,
212  const goto_functionst &goto_functions);
213 
215  {
216  l++;
217  return l;
218  }
219 
220  virtual bool merge(statet &a, const statet &b, locationt to)=0;
221  // for concurrent fixedpoint
222  virtual bool merge_shared(statet &a, const statet &b, locationt to)=0;
223 
224  typedef std::set<irep_idt> functions_donet;
226 
227  typedef std::set<irep_idt> recursion_sett;
229 
230  void generate_states(
231  const goto_functionst &goto_functions);
232 
233  void generate_states(
234  const goto_programt &goto_program);
235 
237 
238  // function calls
240  locationt l_call, locationt l_return,
241  const exprt &function,
242  const exprt::operandst &arguments,
243  statet &new_state,
244  const goto_functionst &goto_functions);
245 
246  void do_function_call(
247  locationt l_call, locationt l_return,
248  const goto_functionst &goto_functions,
249  const goto_functionst::function_mapt::const_iterator f_it,
250  const exprt::operandst &arguments,
251  statet &new_state);
252 
253  // abstract methods
254 
255  virtual void generate_state(locationt l)=0;
256  virtual statet &get_state(locationt l)=0;
257  virtual const statet &get_state(locationt l) const=0;
258  virtual std::unique_ptr<statet> make_temporary_state(statet &s)=0;
259 
261 
262  virtual void get_reference_set(
263  locationt l,
264  const exprt &expr,
265  std::list<exprt> &dest)=0;
266 };
267 
268 // T is expected to be derived from domain_baset
269 template<typename T>
271 {
272 public:
273  // constructor
274  explicit static_analysist(const namespacet &_ns):
276  {
277  }
278 
280 
282  {
283  typename state_mapt::iterator it=state_map.find(l);
284  if(it==state_map.end())
285  throw "failed to find state";
286 
287  return it->second;
288  }
289 
290  const T &operator[](locationt l) const
291  {
292  typename state_mapt::const_iterator it=state_map.find(l);
293  if(it==state_map.end())
294  throw "failed to find state";
295 
296  return it->second;
297  }
298 
299  virtual void clear()
300  {
301  state_map.clear();
303  }
304 
305  virtual bool has_location(locationt l) const
306  {
307  return state_map.count(l)!=0;
308  }
309 
310 protected:
311  typedef std::map<locationt, T> state_mapt;
313 
315  {
316  typename state_mapt::iterator it=state_map.find(l);
317  if(it==state_map.end())
318  throw "failed to find state";
319 
320  return it->second;
321  }
322 
323  virtual const statet &get_state(locationt l) const
324  {
325  typename state_mapt::const_iterator it=state_map.find(l);
326  if(it==state_map.end())
327  throw "failed to find state";
328 
329  return it->second;
330  }
331 
332  virtual bool merge(statet &a, const statet &b, locationt to)
333  {
334  return static_cast<T &>(a).merge(static_cast<const T &>(b), to);
335  }
336 
337  virtual std::unique_ptr<statet> make_temporary_state(statet &s)
338  {
339  return util_make_unique<T>(static_cast<T &>(s));
340  }
341 
342  virtual void generate_state(locationt l)
343  {
344  state_map[l].initialize(ns, l);
345  }
346 
347  virtual void get_reference_set(
348  locationt l,
349  const exprt &expr,
350  std::list<exprt> &dest)
351  {
352  state_map[l].get_reference_set(ns, expr, dest);
353  }
354 
355  virtual void fixedpoint(const goto_functionst &goto_functions)
356  {
357  sequential_fixedpoint(goto_functions);
358  }
359 
360 private:
361  // to enforce that T is derived from domain_baset
362  void dummy(const T &s) { const statet &x=dummy1(s); (void)x; }
363 
364  // not implemented in sequential analyses
365  virtual bool merge_shared(
366  statet &a,
367  const statet &b,
369  {
370  throw "not implemented";
371  }
372 };
373 
374 template<typename T>
376 {
377 public:
378  // constructor
380  static_analysist<T>(_ns)
381  {
382  }
383 
384  virtual bool merge_shared(
388  {
389  return static_cast<T &>(a).merge_shared(
390  this->ns,
391  static_cast<const T &>(b),
392  to);
393  }
394 
395 protected:
396  virtual void fixedpoint(const goto_functionst &goto_functions)
397  {
398  this->concurrent_fixedpoint(goto_functions);
399  }
400 };
401 
402 #endif // CPROVER_ANALYSES_STATIC_ANALYSIS_H
static exprt get_guard(locationt from, locationt to)
const namespacet & ns
virtual std::unique_ptr< statet > make_temporary_state(statet &s)=0
std::map< unsigned, locationt > working_sett
std::map< locationt, T > state_mapt
virtual statet & get_state(locationt l)=0
recursion_sett recursion_set
void sequential_fixedpoint(const goto_functionst &goto_functions)
virtual void transform(const namespacet &ns, locationt from, locationt to)=0
Goto Programs with Functions.
virtual void output(const goto_functionst &goto_functions, std::ostream &out) const
domain_baset::expr_sett expr_sett
virtual std::unique_ptr< statet > make_temporary_state(statet &s)
virtual bool merge_shared(statet &a, const statet &b, locationt to)=0
static exprt get_return_lhs(locationt to)
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions)
goto_programt::const_targett locationt
virtual bool has_location(locationt l) const =0
static_analysist(const namespacet &_ns)
void insert(locationt l)
virtual const statet & get_state(locationt l) const
virtual void generate_state(locationt l)=0
virtual void clear()
functions_donet functions_done
concurrency_aware_static_analysist(const namespacet &_ns)
void do_function_call_rec(locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
void put_in_working_set(working_sett &working_set, locationt l)
goto_programt::const_targett locationt
virtual bool merge(statet &a, const statet &b, locationt to)=0
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)
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void concurrent_fixedpoint(const goto_functionst &goto_functions)
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
virtual void get_reference_set(locationt l, const exprt &expr, std::list< exprt > &dest)=0
std::set< irep_idt > recursion_sett
const T & operator[](locationt l) const
std::vector< exprt > operandst
Definition: expr.h:45
void generate_states(const goto_functionst &goto_functions)
T & operator[](locationt l)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
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:42
virtual void operator()(const goto_programt &goto_program)
virtual ~static_analysis_baset()
virtual void initialize(const goto_functionst &goto_functions)
virtual void update(const goto_programt &goto_program)
virtual void initialize(const namespacet &ns, locationt l)
state_mapt state_map
goto_programt & goto_program
Definition: cover.cpp:63
virtual void generate_state(locationt l)
locationt get_next(working_sett &working_set)
void do_function_call(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)
virtual statet & get_state(locationt l)
virtual void initialize(const goto_programt &goto_program)
unsigned int statet
virtual bool merge_shared(static_analysis_baset::statet &a, const static_analysis_baset::statet &b, goto_programt::const_targett to)
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
static_analysis_baset(const namespacet &_ns)