cprover
ai.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Abstract Interpretation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_AI_H
13 #define CPROVER_ANALYSES_AI_H
14 
15 #include <iosfwd>
16 #include <map>
17 #include <memory>
18 
19 #include <util/json.h>
20 #include <util/xml.h>
21 #include <util/expr.h>
22 #include <util/make_unique.h>
23 
25 
26 // forward reference
27 class ai_baset;
28 
29 // don't use me -- I am just a base class
30 // please derive from me
32 {
33 public:
34  // The constructor is expected to produce 'false'
35  // or 'bottom'
37  {
38  }
39 
40  virtual ~ai_domain_baset()
41  {
42  }
43 
45 
46  // how function calls are treated:
47  // a) there is an edge from each call site to the function head
48  // b) there is an edge from the last instruction (END_FUNCTION)
49  // of the function to the instruction _following_ the call site
50  // (this also needs to set the LHS, if applicable)
51  //
52  // "this" is the domain before the instruction "from"
53  // "from" is the instruction to be interpretted
54  // "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
55  //
56  // PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
57  // PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
58  // PRECONDITION(are_comparable(from,to) ||
59  // (from->is_function_call() || from->is_end_function())
60 
61  virtual void transform(
62  locationt from,
63  locationt to,
64  ai_baset &ai,
65  const namespacet &ns) = 0;
66 
67  virtual void output(
68  std::ostream &out,
69  const ai_baset &ai,
70  const namespacet &ns) const
71  {
72  }
73 
74  virtual jsont output_json(
75  const ai_baset &ai,
76  const namespacet &ns) const;
77 
78  virtual xmlt output_xml(
79  const ai_baset &ai,
80  const namespacet &ns) const;
81 
82  // no states
83  virtual void make_bottom()=0;
84 
85  // all states -- the analysis doesn't use this,
86  // and domains may refuse to implement it.
87  virtual void make_top()=0;
88 
89  // a reasonable entry-point state
90  virtual void make_entry()=0;
91 
92  virtual bool is_bottom() const=0;
93 
94  virtual bool is_top() const=0;
95 
96  // also add
97  //
98  // bool merge(const T &b, locationt from, locationt to);
99  //
100  // This computes the join between "this" and "b".
101  // Return true if "this" has changed.
102  // In the usual case, "b" is the updated state after "from"
103  // and "this" is the state before "to".
104  //
105  // PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
106  // PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
107 
108  // This method allows an expression to be simplified / evaluated using the
109  // current state. It is used to evaluate assertions and in program
110  // simplification
111 
112  // return true if unchanged
113  virtual bool ai_simplify(
114  exprt &condition,
115  const namespacet &ns) const
116  {
117  return true;
118  }
119 
120  // Simplifies the expression but keeps it as an l-value
121  virtual bool ai_simplify_lhs(
122  exprt &condition,
123  const namespacet &ns) const;
124 };
125 
126 // don't use me -- I am just a base class
127 // use ait instead
128 class ai_baset
129 {
130 public:
133 
135  {
136  }
137 
138  virtual ~ai_baset()
139  {
140  }
141 
144  const namespacet &ns)
145  {
146  goto_functionst goto_functions;
149  fixedpoint(goto_program, goto_functions, ns);
150  finalize();
151  }
152 
154  const goto_functionst &goto_functions,
155  const namespacet &ns)
156  {
157  initialize(goto_functions);
158  entry_state(goto_functions);
159  fixedpoint(goto_functions, ns);
160  finalize();
161  }
162 
163  void operator()(const goto_modelt &goto_model)
164  {
165  const namespacet ns(goto_model.symbol_table);
166  initialize(goto_model.goto_functions);
167  entry_state(goto_model.goto_functions);
168  fixedpoint(goto_model.goto_functions, ns);
169  finalize();
170  }
171 
173  const goto_functionst::goto_functiont &goto_function,
174  const namespacet &ns)
175  {
176  goto_functionst goto_functions;
177  initialize(goto_function);
178  entry_state(goto_function.body);
179  fixedpoint(goto_function.body, goto_functions, ns);
180  finalize();
181  }
182 
184  virtual const ai_domain_baset & abstract_state_before(
185  goto_programt::const_targett t) const = 0;
186 
190  {
191  return abstract_state_before(std::next(t));
192  }
193 
194  virtual void clear()
195  {
196  }
197 
198  virtual void output(
199  const namespacet &ns,
200  const goto_functionst &goto_functions,
201  std::ostream &out) const;
202 
203  void output(
204  const goto_modelt &goto_model,
205  std::ostream &out) const
206  {
207  const namespacet ns(goto_model.symbol_table);
208  output(ns, goto_model.goto_functions, out);
209  }
210 
211  void output(
212  const namespacet &ns,
214  std::ostream &out) const
215  {
216  output(ns, goto_program, "", out);
217  }
218 
219  void output(
220  const namespacet &ns,
221  const goto_functionst::goto_functiont &goto_function,
222  std::ostream &out) const
223  {
224  output(ns, goto_function.body, "", out);
225  }
226 
227 
228  virtual jsont output_json(
229  const namespacet &ns,
230  const goto_functionst &goto_functions) const;
231 
233  const goto_modelt &goto_model) const
234  {
235  const namespacet ns(goto_model.symbol_table);
236  return output_json(ns, goto_model.goto_functions);
237  }
238 
240  const namespacet &ns,
241  const goto_programt &goto_program) const
242  {
243  return output_json(ns, goto_program, "");
244  }
245 
247  const namespacet &ns,
248  const goto_functionst::goto_functiont &goto_function) const
249  {
250  return output_json(ns, goto_function.body, "");
251  }
252 
253 
254  virtual xmlt output_xml(
255  const namespacet &ns,
256  const goto_functionst &goto_functions) const;
257 
259  const goto_modelt &goto_model) const
260  {
261  const namespacet ns(goto_model.symbol_table);
262  return output_xml(ns, goto_model.goto_functions);
263  }
264 
266  const namespacet &ns,
267  const goto_programt &goto_program) const
268  {
269  return output_xml(ns, goto_program, "");
270  }
271 
273  const namespacet &ns,
274  const goto_functionst::goto_functiont &goto_function) const
275  {
276  return output_xml(ns, goto_function.body, "");
277  }
278 
279 protected:
280  // overload to add a factory
281  virtual void initialize(const goto_programt &);
282  virtual void initialize(const goto_functionst::goto_functiont &);
283  virtual void initialize(const goto_functionst &);
284 
285  // override to add a cleanup step after fixedpoint has run
286  virtual void finalize();
287 
288  void entry_state(const goto_programt &);
289  void entry_state(const goto_functionst &);
290 
291  virtual void output(
292  const namespacet &ns,
294  const irep_idt &identifier,
295  std::ostream &out) const;
296 
297  virtual jsont output_json(
298  const namespacet &ns,
300  const irep_idt &identifier) const;
301 
302  virtual xmlt output_xml(
303  const namespacet &ns,
305  const irep_idt &identifier) const;
306 
307 
308  // the work-queue is sorted by location number
309  typedef std::map<unsigned, locationt> working_sett;
310 
311  locationt get_next(working_sett &working_set);
312 
314  working_sett &working_set,
315  locationt l)
316  {
317  working_set.insert(
318  std::pair<unsigned, locationt>(l->location_number, l));
319  }
320 
321  // true = found something new
322  bool fixedpoint(
324  const goto_functionst &goto_functions,
325  const namespacet &ns);
326 
327  virtual void fixedpoint(
328  const goto_functionst &goto_functions,
329  const namespacet &ns)=0;
330 
332  const goto_functionst &goto_functions,
333  const namespacet &ns);
335  const goto_functionst &goto_functions,
336  const namespacet &ns);
337 
338  // true = found something new
339  bool visit(
340  locationt l,
341  working_sett &working_set,
343  const goto_functionst &goto_functions,
344  const namespacet &ns);
345 
346  // function calls
348  locationt l_call, locationt l_return,
349  const exprt &function,
350  const exprt::operandst &arguments,
351  const goto_functionst &goto_functions,
352  const namespacet &ns);
353 
354  bool do_function_call(
355  locationt l_call, locationt l_return,
356  const goto_functionst &goto_functions,
357  const goto_functionst::function_mapt::const_iterator f_it,
358  const exprt::operandst &arguments,
359  const namespacet &ns);
360 
361  // abstract methods
362 
363  virtual bool merge(const statet &src, locationt from, locationt to)=0;
364  // for concurrent fixedpoint
365  virtual bool merge_shared(
366  const statet &src,
367  locationt from,
368  locationt to,
369  const namespacet &ns)=0;
370  virtual statet &get_state(locationt l)=0;
371  virtual const statet &find_state(locationt l) const=0;
372  virtual std::unique_ptr<statet> make_temporary_state(const statet &s)=0;
373 };
374 
375 // domainT is expected to be derived from ai_domain_baseT
376 template<typename domainT>
377 class ait:public ai_baset
378 {
379 public:
380  // constructor
382  {
383  }
384 
386 
387  domainT &operator[](locationt l)
388  {
389  typename state_mapt::iterator it=state_map.find(l);
390  if(it==state_map.end())
391  throw "failed to find state";
392 
393  return it->second;
394  }
395 
396  const domainT &operator[](locationt l) const
397  {
398  typename state_mapt::const_iterator it=state_map.find(l);
399  if(it==state_map.end())
400  throw "failed to find state";
401 
402  return it->second;
403  }
404 
406  goto_programt::const_targett t) const override
407  {
408  return (*this)[t];
409  }
410 
411  void clear() override
412  {
413  state_map.clear();
414  ai_baset::clear();
415  }
416 
417 protected:
418  typedef std::
419  unordered_map<locationt, domainT, const_target_hash, pointee_address_equalt>
422 
423  // this one creates states, if need be
424  virtual statet &get_state(locationt l) override
425  {
426  return state_map[l]; // calls default constructor
427  }
428 
429  // this one just finds states
430  const statet &find_state(locationt l) const override
431  {
432  typename state_mapt::const_iterator it=state_map.find(l);
433  if(it==state_map.end())
434  throw "failed to find state";
435 
436  return it->second;
437  }
438 
439  bool merge(const statet &src, locationt from, locationt to) override
440  {
441  statet &dest=get_state(to);
442  return static_cast<domainT &>(dest).merge(
443  static_cast<const domainT &>(src), from, to);
444  }
445 
446  std::unique_ptr<statet> make_temporary_state(const statet &s) override
447  {
448  return util_make_unique<domainT>(static_cast<const domainT &>(s));
449  }
450 
452  const goto_functionst &goto_functions,
453  const namespacet &ns) override
454  {
455  sequential_fixedpoint(goto_functions, ns);
456  }
457 
458 private:
459  // to enforce that domainT is derived from ai_domain_baset
460  void dummy(const domainT &s) { const statet &x=s; (void)x; }
461 
462  // not implemented in sequential analyses
464  const statet &src,
467  const namespacet &ns) override
468  {
469  throw "not implemented";
470  }
471 };
472 
473 template<typename domainT>
474 class concurrency_aware_ait:public ait<domainT>
475 {
476 public:
477  typedef typename ait<domainT>::statet statet;
478 
479  // constructor
481  {
482  }
483 
485  const statet &src,
488  const namespacet &ns) override
489  {
490  statet &dest=this->get_state(to);
491  return static_cast<domainT &>(dest).merge_shared(
492  static_cast<const domainT &>(src), from, to, ns);
493  }
494 
495 protected:
497  const goto_functionst &goto_functions,
498  const namespacet &ns) override
499  {
500  this->concurrent_fixedpoint(goto_functions, ns);
501  }
502 };
503 
504 #endif // CPROVER_ANALYSES_AI_H
const domainT & operator[](locationt l) const
Definition: ai.h:396
virtual statet & get_state(locationt l)=0
virtual bool is_top() const =0
void dummy(const domainT &s)
Definition: ai.h:460
void fixedpoint(const goto_functionst &goto_functions, const namespacet &ns) override
Definition: ai.h:451
virtual statet & get_state(locationt l) override
Definition: ai.h:424
virtual void make_bottom()=0
void put_in_working_set(working_sett &working_set, locationt l)
Definition: ai.h:313
goto_programt::const_targett locationt
Definition: ai.h:132
goto_programt::const_targett locationt
Definition: ai.h:385
concurrency_aware_ait()
Definition: ai.h:480
Definition: json.h:23
ait()
Definition: ai.h:381
Definition: ai.h:377
virtual bool merge(const statet &src, locationt from, locationt to)=0
virtual const ai_domain_baset & abstract_state_after(goto_programt::const_targett t) const
Returns the abstract state after the given instruction.
Definition: ai.h:188
virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const
Definition: ai.cpp:24
std::unique_ptr< statet > make_temporary_state(const statet &s) override
Definition: ai.h:446
void output(const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
Definition: ai.h:219
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
virtual jsont output_json(const namespacet &ns, const goto_functionst &goto_functions) const
Output the domains for the whole program as JSON.
Definition: ai.cpp:134
virtual bool is_bottom() const =0
virtual void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
virtual void clear()
Definition: ai.h:194
std::unordered_map< locationt, domainT, const_target_hash, pointee_address_equalt > state_mapt
Definition: ai.h:420
std::map< unsigned, locationt > working_sett
Definition: ai.h:309
ai_baset()
Definition: ai.h:134
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Definition: ai.cpp:92
bool merge_shared(const statet &src, goto_programt::const_targett from, goto_programt::const_targett to, const namespacet &ns) override
Definition: ai.h:484
Symbol Table + CFG.
domainT & operator[](locationt l)
Definition: ai.h:387
bool do_function_call_rec(locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:452
bool 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, const namespacet &ns)
Definition: ai.cpp:384
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const
Definition: ai.h:113
void operator()(const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Definition: ai.h:172
xmlt output_xml(const namespacet &ns, const goto_programt &goto_program) const
Definition: ai.h:265
ait< domainT >::statet statet
Definition: ai.h:477
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
void entry_state(const goto_programt &)
Definition: ai.cpp:258
Definition: xml.h:18
virtual const statet & find_state(locationt l) const =0
virtual bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns)=0
void fixedpoint(const goto_functionst &goto_functions, const namespacet &ns) override
Definition: ai.h:496
void operator()(const goto_modelt &goto_model)
Definition: ai.h:163
virtual void finalize()
Definition: ai.cpp:283
void sequential_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:526
std::vector< exprt > operandst
Definition: expr.h:45
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:300
ai_domain_baset()
Definition: ai.h:36
bool merge_shared(const statet &src, goto_programt::const_targett from, goto_programt::const_targett to, const namespacet &ns) override
Definition: ai.h:463
bool merge(const statet &src, locationt from, locationt to) override
Definition: ai.h:439
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:326
ai_domain_baset statet
Definition: ai.h:131
void operator()(const goto_programt &goto_program, const namespacet &ns)
Definition: ai.h:142
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)=0
jsont output_json(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
Definition: ai.h:246
virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const
Use the information in the domain to simplify the expression on the LHS of an assignment.
Definition: ai.cpp:53
Definition: ai.h:128
virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const
Definition: ai.cpp:34
Base class for all expressions.
Definition: expr.h:42
virtual void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
Definition: ai.h:67
virtual ~ai_baset()
Definition: ai.h:138
locationt get_next(working_sett &working_set)
Definition: ai.cpp:288
const statet & find_state(locationt l) const override
Definition: ai.h:430
const ai_domain_baset & abstract_state_before(goto_programt::const_targett t) const override
Returns the abstract state before the given instruction.
Definition: ai.h:405
void clear() override
Definition: ai.h:411
void output(const goto_modelt &goto_model, std::ostream &out) const
Definition: ai.h:203
virtual void initialize(const goto_programt &)
Definition: ai.cpp:269
state_mapt state_map
Definition: ai.h:421
goto_programt & goto_program
Definition: cover.cpp:63
virtual ~ai_domain_baset()
Definition: ai.h:40
void output(const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const
Definition: ai.h:211
void concurrent_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:537
goto_programt::const_targett locationt
Definition: ai.h:44
virtual const ai_domain_baset & abstract_state_before(goto_programt::const_targett t) const =0
Returns the abstract state before the given instruction.
virtual xmlt output_xml(const namespacet &ns, const goto_functionst &goto_functions) const
Output the domains for the whole program as XML.
Definition: ai.cpp:189
xmlt output_xml(const goto_modelt &goto_model) const
Definition: ai.h:258
void operator()(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.h:153
virtual void make_top()=0
xmlt output_xml(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
Definition: ai.h:272
jsont output_json(const goto_modelt &goto_model) const
Definition: ai.h:232
unsigned int statet
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
jsont output_json(const namespacet &ns, const goto_programt &goto_program) const
Definition: ai.h:239
virtual void make_entry()=0