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 #include "ai_domain.h"
27 
30 // don't use me -- I am just a base class
31 // use ait instead
32 class ai_baset
33 {
34 public:
37 
39  {
40  }
41 
42  virtual ~ai_baset()
43  {
44  }
45 
47  void operator()(
49  const namespacet &ns)
50  {
51  goto_functionst goto_functions;
54  fixedpoint(goto_program, goto_functions, ns);
55  finalize();
56  }
57 
58  void operator()(
59  const goto_functionst &goto_functions,
60  const namespacet &ns)
61  {
62  initialize(goto_functions);
63  entry_state(goto_functions);
64  fixedpoint(goto_functions, ns);
65  finalize();
66  }
67 
68  void operator()(const goto_modelt &goto_model)
69  {
70  const namespacet ns(goto_model.symbol_table);
71  initialize(goto_model.goto_functions);
72  entry_state(goto_model.goto_functions);
73  fixedpoint(goto_model.goto_functions, ns);
74  finalize();
75  }
76 
77  void operator()(
78  const goto_functionst::goto_functiont &goto_function,
79  const namespacet &ns)
80  {
81  goto_functionst goto_functions;
82  initialize(goto_function);
83  entry_state(goto_function.body);
84  fixedpoint(goto_function.body, goto_functions, ns);
85  finalize();
86  }
87 
93 
96  virtual std::unique_ptr<statet> abstract_state_before(locationt l) const = 0;
97 
99  virtual std::unique_ptr<statet> abstract_state_after(locationt l) const
100  {
103  INVARIANT(!l->is_end_function(), "No state after the last instruction");
104  return abstract_state_before(std::next(l));
105  }
106 
108  virtual void clear()
109  {
110  }
111 
112  virtual void output(
113  const namespacet &ns,
114  const goto_functionst &goto_functions,
115  std::ostream &out) const;
116 
117  void output(
118  const goto_modelt &goto_model,
119  std::ostream &out) const
120  {
121  const namespacet ns(goto_model.symbol_table);
122  output(ns, goto_model.goto_functions, out);
123  }
124 
125  void output(
126  const namespacet &ns,
128  std::ostream &out) const
129  {
130  output(ns, goto_program, "", out);
131  }
132 
133  void output(
134  const namespacet &ns,
135  const goto_functionst::goto_functiont &goto_function,
136  std::ostream &out) const
137  {
138  output(ns, goto_function.body, "", out);
139  }
140 
141 
142  virtual jsont output_json(
143  const namespacet &ns,
144  const goto_functionst &goto_functions) const;
145 
147  const goto_modelt &goto_model) const
148  {
149  const namespacet ns(goto_model.symbol_table);
150  return output_json(ns, goto_model.goto_functions);
151  }
152 
154  const namespacet &ns,
155  const goto_programt &goto_program) const
156  {
157  return output_json(ns, goto_program, "");
158  }
159 
161  const namespacet &ns,
162  const goto_functionst::goto_functiont &goto_function) const
163  {
164  return output_json(ns, goto_function.body, "");
165  }
166 
167 
168  virtual xmlt output_xml(
169  const namespacet &ns,
170  const goto_functionst &goto_functions) const;
171 
173  const goto_modelt &goto_model) const
174  {
175  const namespacet ns(goto_model.symbol_table);
176  return output_xml(ns, goto_model.goto_functions);
177  }
178 
180  const namespacet &ns,
181  const goto_programt &goto_program) const
182  {
183  return output_xml(ns, goto_program, "");
184  }
185 
187  const namespacet &ns,
188  const goto_functionst::goto_functiont &goto_function) const
189  {
190  return output_xml(ns, goto_function.body, "");
191  }
192 
193 protected:
194  // overload to add a factory
195  virtual void initialize(const goto_programt &);
196  virtual void initialize(const goto_functionst::goto_functiont &);
197  virtual void initialize(const goto_functionst &);
198 
199  // override to add a cleanup step after fixedpoint has run
200  virtual void finalize();
201 
202  void entry_state(const goto_programt &);
203  void entry_state(const goto_functionst &);
204 
205  virtual void output(
206  const namespacet &ns,
208  const irep_idt &identifier,
209  std::ostream &out) const;
210 
211  virtual jsont output_json(
212  const namespacet &ns,
214  const irep_idt &identifier) const;
215 
216  virtual xmlt output_xml(
217  const namespacet &ns,
219  const irep_idt &identifier) const;
220 
221 
222  // the work-queue is sorted by location number
223  typedef std::map<unsigned, locationt> working_sett;
224 
225  locationt get_next(working_sett &working_set);
226 
228  working_sett &working_set,
229  locationt l)
230  {
231  working_set.insert(
232  std::pair<unsigned, locationt>(l->location_number, l));
233  }
234 
235  // true = found something new
236  bool fixedpoint(
238  const goto_functionst &goto_functions,
239  const namespacet &ns);
240 
241  virtual void fixedpoint(
242  const goto_functionst &goto_functions,
243  const namespacet &ns)=0;
244 
246  const goto_functionst &goto_functions,
247  const namespacet &ns);
249  const goto_functionst &goto_functions,
250  const namespacet &ns);
251 
252  // Visit performs one step of abstract interpretation from location l
253  // Depending on the instruction type it may compute a number of "edges"
254  // or applications of the abstract transformer
255  // true = found something new
256  bool visit(
257  locationt l,
258  working_sett &working_set,
260  const goto_functionst &goto_functions,
261  const namespacet &ns);
262 
263  // function calls
265  locationt l_call, locationt l_return,
266  const exprt &function,
267  const exprt::operandst &arguments,
268  const goto_functionst &goto_functions,
269  const namespacet &ns);
270 
271  bool do_function_call(
272  locationt l_call, locationt l_return,
273  const goto_functionst &goto_functions,
274  const goto_functionst::function_mapt::const_iterator f_it,
275  const exprt::operandst &arguments,
276  const namespacet &ns);
277 
278  // abstract methods
279 
280  virtual bool merge(const statet &src, locationt from, locationt to)=0;
281  // for concurrent fixedpoint
282  virtual bool merge_shared(
283  const statet &src,
284  locationt from,
285  locationt to,
286  const namespacet &ns)=0;
287  virtual statet &get_state(locationt l)=0;
288  virtual const statet &find_state(locationt l) const=0;
289  virtual std::unique_ptr<statet> make_temporary_state(const statet &s)=0;
290 };
291 
292 // domainT is expected to be derived from ai_domain_baseT
293 template<typename domainT>
294 class ait:public ai_baset
295 {
296 public:
297  // constructor
299  {
300  }
301 
303 
304  domainT &operator[](locationt l)
305  {
306  typename state_mapt::iterator it=state_map.find(l);
307  if(it==state_map.end())
308  throw "failed to find state";
309 
310  return it->second;
311  }
312 
313  const domainT &operator[](locationt l) const
314  {
315  typename state_mapt::const_iterator it=state_map.find(l);
316  if(it==state_map.end())
317  throw "failed to find state";
318 
319  return it->second;
320  }
321 
322  std::unique_ptr<statet> abstract_state_before(locationt t) const override
323  {
324  typename state_mapt::const_iterator it = state_map.find(t);
325  if(it == state_map.end())
326  {
327  std::unique_ptr<statet> d = util_make_unique<domainT>();
328  CHECK_RETURN(d->is_bottom());
329  return d;
330  }
331 
332  return util_make_unique<domainT>(it->second);
333  }
334 
335  void clear() override
336  {
337  state_map.clear();
338  ai_baset::clear();
339  }
340 
341 protected:
342  typedef std::
343  unordered_map<locationt, domainT, const_target_hash, pointee_address_equalt>
346 
347  // this one creates states, if need be
348  virtual statet &get_state(locationt l) override
349  {
350  return state_map[l]; // calls default constructor
351  }
352 
353  // this one just finds states
354  const statet &find_state(locationt l) const override
355  {
356  typename state_mapt::const_iterator it=state_map.find(l);
357  if(it==state_map.end())
358  throw "failed to find state";
359 
360  return it->second;
361  }
362 
363  bool merge(const statet &src, locationt from, locationt to) override
364  {
365  statet &dest=get_state(to);
366  return static_cast<domainT &>(dest).merge(
367  static_cast<const domainT &>(src), from, to);
368  }
369 
370  std::unique_ptr<statet> make_temporary_state(const statet &s) override
371  {
372  return util_make_unique<domainT>(static_cast<const domainT &>(s));
373  }
374 
376  const goto_functionst &goto_functions,
377  const namespacet &ns) override
378  {
379  sequential_fixedpoint(goto_functions, ns);
380  }
381 
382 private:
383  // to enforce that domainT is derived from ai_domain_baset
384  void dummy(const domainT &s) { const statet &x=s; (void)x; }
385 
386  // not implemented in sequential analyses
388  const statet &,
391  const namespacet &) override
392  {
393  throw "not implemented";
394  }
395 };
396 
397 template<typename domainT>
398 class concurrency_aware_ait:public ait<domainT>
399 {
400 public:
401  typedef typename ait<domainT>::statet statet;
402 
403  // constructor
405  {
406  }
407 
409  const statet &src,
412  const namespacet &ns) override
413  {
414  statet &dest=this->get_state(to);
415  return static_cast<domainT &>(dest).merge_shared(
416  static_cast<const domainT &>(src), from, to, ns);
417  }
418 
419 protected:
421  const goto_functionst &goto_functions,
422  const namespacet &ns) override
423  {
424  this->concurrent_fixedpoint(goto_functions, ns);
425  }
426 };
427 
428 #endif // CPROVER_ANALYSES_AI_H
const domainT & operator[](locationt l) const
Definition: ai.h:313
virtual statet & get_state(locationt l)=0
void dummy(const domainT &s)
Definition: ai.h:384
void fixedpoint(const goto_functionst &goto_functions, const namespacet &ns) override
Definition: ai.h:375
virtual statet & get_state(locationt l) override
Definition: ai.h:348
std::unique_ptr< statet > abstract_state_before(locationt t) const override
Accessing individual domains at particular locations (without needing to know what kind of domain or ...
Definition: ai.h:322
void put_in_working_set(working_sett &working_set, locationt l)
Definition: ai.h:227
goto_programt::const_targett locationt
Definition: ai.h:36
goto_programt::const_targett locationt
Definition: ai.h:302
concurrency_aware_ait()
Definition: ai.h:404
Definition: json.h:23
ait()
Definition: ai.h:298
Definition: ai.h:294
virtual bool merge(const statet &src, locationt from, locationt to)=0
std::unique_ptr< statet > make_temporary_state(const statet &s) override
Definition: ai.h:370
void output(const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
Definition: ai.h:133
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Accessing individual domains at particular locations (without needing to know what kind of domain or ...
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:66
virtual bool is_bottom() const =0
virtual void clear()
Resets the domain.
Definition: ai.h:108
std::unordered_map< locationt, domainT, const_target_hash, pointee_address_equalt > state_mapt
Definition: ai.h:344
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
std::map< unsigned, locationt > working_sett
Definition: ai.h:223
ai_baset()
Definition: ai.h:38
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Definition: ai.cpp:24
bool merge_shared(const statet &src, goto_programt::const_targett from, goto_programt::const_targett to, const namespacet &ns) override
Definition: ai.h:408
Symbol Table + CFG.
domainT & operator[](locationt l)
Definition: ai.h:304
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
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:388
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:318
void operator()(const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Definition: ai.h:77
xmlt output_xml(const namespacet &ns, const goto_programt &goto_program) const
Definition: ai.h:179
ait< domainT >::statet statet
Definition: ai.h:401
Abstract Interpretation Domain.
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:191
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:420
void operator()(const goto_modelt &goto_model)
Definition: ai.h:68
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
virtual void finalize()
Definition: ai.cpp:216
bool merge_shared(const statet &, goto_programt::const_targett, goto_programt::const_targett, const namespacet &) override
Definition: ai.h:387
void sequential_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:420
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:233
bool merge(const statet &src, locationt from, locationt to) override
Definition: ai.h:363
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:260
ai_domain_baset statet
Definition: ai.h:35
void operator()(const goto_programt &goto_program, const namespacet &ns)
Running the interpreter.
Definition: ai.h:47
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:160
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:42
virtual ~ai_baset()
Definition: ai.h:42
locationt get_next(working_sett &working_set)
Definition: ai.cpp:221
const statet & find_state(locationt l) const override
Definition: ai.h:354
void clear() override
Resets the domain.
Definition: ai.h:335
void output(const goto_modelt &goto_model, std::ostream &out) const
Definition: ai.h:117
virtual void initialize(const goto_programt &)
Definition: ai.cpp:202
state_mapt state_map
Definition: ai.h:345
goto_programt & goto_program
Definition: cover.cpp:63
void output(const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const
Definition: ai.h:125
void concurrent_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:431
virtual std::unique_ptr< statet > abstract_state_after(locationt l) const
Returns the abstract state after the given instruction.
Definition: ai.h:99
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:122
xmlt output_xml(const goto_modelt &goto_model) const
Definition: ai.h:172
void operator()(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.h:58
xmlt output_xml(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
Definition: ai.h:186
jsont output_json(const goto_modelt &goto_model) const
Definition: ai.h:146
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:153