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