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 
32 class ai_baset
33 {
34 public:
37 
39  {
40  }
41 
42  virtual ~ai_baset()
43  {
44  }
45 
47  void operator()(
48  const irep_idt &function_identifier,
49  const goto_programt &goto_program,
50  const namespacet &ns)
51  {
52  goto_functionst goto_functions;
53  initialize(goto_program);
54  entry_state(goto_program);
55  fixedpoint(function_identifier, goto_program, goto_functions, ns);
56  finalize();
57  }
58 
60  void operator()(
61  const goto_functionst &goto_functions,
62  const namespacet &ns)
63  {
64  initialize(goto_functions);
65  entry_state(goto_functions);
66  fixedpoint(goto_functions, ns);
67  finalize();
68  }
69 
71  void operator()(const goto_modelt &goto_model)
72  {
73  const namespacet ns(goto_model.symbol_table);
74  initialize(goto_model.goto_functions);
75  entry_state(goto_model.goto_functions);
76  fixedpoint(goto_model.goto_functions, ns);
77  finalize();
78  }
79 
81  void operator()(
82  const irep_idt &function_identifier,
83  const goto_functionst::goto_functiont &goto_function,
84  const namespacet &ns)
85  {
86  goto_functionst goto_functions;
87  initialize(goto_function);
88  entry_state(goto_function.body);
89  fixedpoint(function_identifier, goto_function.body, goto_functions, ns);
90  finalize();
91  }
92 
103  virtual std::unique_ptr<statet> abstract_state_before(locationt l) const = 0;
104 
114  virtual std::unique_ptr<statet> abstract_state_after(locationt l) const
115  {
118  INVARIANT(!l->is_end_function(), "No state after the last instruction");
119  return abstract_state_before(std::next(l));
120  }
121 
123  virtual void clear()
124  {
125  }
126 
128  virtual void output(
129  const namespacet &ns,
130  const goto_functionst &goto_functions,
131  std::ostream &out) const;
132 
134  void output(
135  const goto_modelt &goto_model,
136  std::ostream &out) const
137  {
138  const namespacet ns(goto_model.symbol_table);
139  output(ns, goto_model.goto_functions, out);
140  }
141 
143  void output(
144  const namespacet &ns,
145  const goto_programt &goto_program,
146  std::ostream &out) const
147  {
148  output(ns, goto_program, "", out);
149  }
150 
152  void output(
153  const namespacet &ns,
154  const goto_functionst::goto_functiont &goto_function,
155  std::ostream &out) const
156  {
157  output(ns, goto_function.body, "", out);
158  }
159 
161  virtual jsont output_json(
162  const namespacet &ns,
163  const goto_functionst &goto_functions) const;
164 
167  const goto_modelt &goto_model) const
168  {
169  const namespacet ns(goto_model.symbol_table);
170  return output_json(ns, goto_model.goto_functions);
171  }
172 
175  const namespacet &ns,
176  const goto_programt &goto_program) const
177  {
178  return output_json(ns, goto_program, "");
179  }
180 
183  const namespacet &ns,
184  const goto_functionst::goto_functiont &goto_function) const
185  {
186  return output_json(ns, goto_function.body, "");
187  }
188 
190  virtual xmlt output_xml(
191  const namespacet &ns,
192  const goto_functionst &goto_functions) const;
193 
196  const goto_modelt &goto_model) const
197  {
198  const namespacet ns(goto_model.symbol_table);
199  return output_xml(ns, goto_model.goto_functions);
200  }
201 
204  const namespacet &ns,
205  const goto_programt &goto_program) const
206  {
207  return output_xml(ns, goto_program, "");
208  }
209 
212  const namespacet &ns,
213  const goto_functionst::goto_functiont &goto_function) const
214  {
215  return output_xml(ns, goto_function.body, "");
216  }
217 
218 protected:
221  virtual void initialize(const goto_programt &goto_program);
222 
224  virtual void initialize(const goto_functionst::goto_functiont &goto_function);
225 
228  virtual void initialize(const goto_functionst &goto_functions);
229 
232  virtual void finalize();
233 
236  void entry_state(const goto_programt &goto_program);
237 
240  void entry_state(const goto_functionst &goto_functions);
241 
248  virtual void output(
249  const namespacet &ns,
250  const goto_programt &goto_program,
251  const irep_idt &identifier,
252  std::ostream &out) const;
253 
260  virtual jsont output_json(
261  const namespacet &ns,
262  const goto_programt &goto_program,
263  const irep_idt &identifier) const;
264 
271  virtual xmlt output_xml(
272  const namespacet &ns,
273  const goto_programt &goto_program,
274  const irep_idt &identifier) const;
275 
277  typedef std::map<unsigned, locationt> working_sett;
278 
280  locationt get_next(working_sett &working_set);
281 
283  working_sett &working_set,
284  locationt l)
285  {
286  working_set.insert(
287  std::pair<unsigned, locationt>(l->location_number, l));
288  }
289 
292  bool fixedpoint(
293  const irep_idt &function_identifier,
294  const goto_programt &goto_program,
295  const goto_functionst &goto_functions,
296  const namespacet &ns);
297 
298  virtual void fixedpoint(
299  const goto_functionst &goto_functions,
300  const namespacet &ns)=0;
301 
303  const goto_functionst &goto_functions,
304  const namespacet &ns);
305 
307  const goto_functionst &goto_functions,
308  const namespacet &ns);
309 
314  bool visit(
315  const irep_idt &function_identifier,
316  locationt l,
317  working_sett &working_set,
318  const goto_programt &goto_program,
319  const goto_functionst &goto_functions,
320  const namespacet &ns);
321 
322  // function calls
324  const irep_idt &calling_function_identifier,
325  locationt l_call,
326  locationt l_return,
327  const exprt &function,
328  const exprt::operandst &arguments,
329  const goto_functionst &goto_functions,
330  const namespacet &ns);
331 
332  bool do_function_call(
333  const irep_idt &calling_function_identifier,
334  locationt l_call,
335  locationt l_return,
336  const goto_functionst &goto_functions,
337  const goto_functionst::function_mapt::const_iterator f_it,
338  const exprt::operandst &arguments,
339  const namespacet &ns);
340 
341  // abstract methods
342 
343  virtual bool merge(const statet &src, locationt from, locationt to)=0;
344  // for concurrent fixedpoint
345  virtual bool merge_shared(
346  const statet &src,
347  locationt from,
348  locationt to,
349  const namespacet &ns)=0;
350 
353  virtual statet &get_state(locationt l)=0;
354 
357  virtual const statet &find_state(locationt l) const=0;
358 
360  virtual std::unique_ptr<statet> make_temporary_state(const statet &s)=0;
361 };
362 
363 // domainT is expected to be derived from ai_domain_baseT
364 template<typename domainT>
365 class ait:public ai_baset
366 {
367 public:
368  // constructor
370  {
371  }
372 
374 
375  domainT &operator[](locationt l)
376  {
377  typename state_mapt::iterator it=state_map.find(l);
378  if(it==state_map.end())
379  throw std::out_of_range("failed to find state");
380 
381  return it->second;
382  }
383 
384  const domainT &operator[](locationt l) const
385  {
386  typename state_mapt::const_iterator it=state_map.find(l);
387  if(it==state_map.end())
388  throw std::out_of_range("failed to find state");
389 
390  return it->second;
391  }
392 
393  std::unique_ptr<statet> abstract_state_before(locationt t) const override
394  {
395  typename state_mapt::const_iterator it = state_map.find(t);
396  if(it == state_map.end())
397  {
398  std::unique_ptr<statet> d = util_make_unique<domainT>();
399  CHECK_RETURN(d->is_bottom());
400  return d;
401  }
402 
403  return util_make_unique<domainT>(it->second);
404  }
405 
406  void clear() override
407  {
408  state_map.clear();
409  ai_baset::clear();
410  }
411 
412 protected:
413  typedef std::
414  unordered_map<locationt, domainT, const_target_hash, pointee_address_equalt>
417 
418  // this one creates states, if need be
419  virtual statet &get_state(locationt l) override
420  {
421  return state_map[l]; // calls default constructor
422  }
423 
424  // this one just finds states
425  const statet &find_state(locationt l) const override
426  {
427  typename state_mapt::const_iterator it=state_map.find(l);
428  if(it==state_map.end())
429  throw std::out_of_range("failed to find state");
430 
431  return it->second;
432  }
433 
434  bool merge(const statet &src, locationt from, locationt to) override
435  {
436  statet &dest=get_state(to);
437  return static_cast<domainT &>(dest).merge(
438  static_cast<const domainT &>(src), from, to);
439  }
440 
441  std::unique_ptr<statet> make_temporary_state(const statet &s) override
442  {
443  return util_make_unique<domainT>(static_cast<const domainT &>(s));
444  }
445 
447  const goto_functionst &goto_functions,
448  const namespacet &ns) override
449  {
450  sequential_fixedpoint(goto_functions, ns);
451  }
452 
453 private:
456  void dummy(const domainT &s) { const statet &x=s; (void)x; }
457 
460  override
461  {
462  throw "not implemented";
463  }
464 };
465 
466 template<typename domainT>
467 class concurrency_aware_ait:public ait<domainT>
468 {
469 public:
470  using statet = typename ait<domainT>::statet;
471  using locationt = typename statet::locationt;
472 
473  // constructor
475  {
476  }
477 
479  const statet &src,
480  locationt from,
481  locationt to,
482  const namespacet &ns) override
483  {
484  statet &dest=this->get_state(to);
485  return static_cast<domainT &>(dest).merge_shared(
486  static_cast<const domainT &>(src), from, to, ns);
487  }
488 
489 protected:
491  const goto_functionst &goto_functions,
492  const namespacet &ns) override
493  {
494  this->concurrent_fixedpoint(goto_functions, ns);
495  }
496 };
497 
498 #endif // CPROVER_ANALYSES_AI_H
ai_baset::output_xml
xmlt output_xml(const namespacet &ns, const goto_programt &goto_program) const
Output the abstract states for a single function as XML.
Definition: ai.h:203
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
ai_baset::output_json
virtual jsont output_json(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as JSON.
Definition: ai.cpp:63
ait::merge_shared
bool merge_shared(const statet &, locationt, locationt, const namespacet &) override
This function should not be implemented in sequential analyses.
Definition: ai.h:459
ai_baset::fixedpoint
bool fixedpoint(const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Run the fixedpoint algorithm until it reaches a fixed point.
Definition: ai.cpp:233
ai_baset::visit
bool visit(const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Perform one step of abstract interpretation from location l Depending on the instruction type it may ...
Definition: ai.cpp:262
ai_baset::make_temporary_state
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)=0
Make a copy of a state.
ai_baset::locationt
goto_programt::const_targett locationt
Definition: ai.h:36
ai_domain.h
ait::operator[]
const domainT & operator[](locationt l) const
Definition: ai.h:384
ait::state_map
state_mapt state_map
Definition: ai.h:416
ait::dummy
void dummy(const domainT &s)
This function exists to enforce that domainT is derived from ai_domain_baset.
Definition: ai.h:456
ait::fixedpoint
void fixedpoint(const goto_functionst &goto_functions, const namespacet &ns) override
Definition: ai.h:446
ait::get_state
virtual statet & get_state(locationt l) override
Get the state for the given location, creating it in a default way if it doesn't exist.
Definition: ai.h:419
ai_baset::sequential_fixedpoint
void sequential_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:445
ai_baset::output_xml
virtual xmlt output_xml(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as XML.
Definition: ai.cpp:119
goto_model.h
exprt
Base class for all expressions.
Definition: expr.h:54
ait
Definition: ai.h:365
goto_modelt
Definition: goto_model.h:24
ai_baset::operator()
void operator()(const goto_modelt &goto_model)
Run abstract interpretation on a whole program.
Definition: ai.h:71
ai_baset::find_state
virtual const statet & find_state(locationt l) const =0
Get the state for the given location if it already exists; throw an exception if it doesn't.
ait::ait
ait()
Definition: ai.h:369
jsont
Definition: json.h:23
xml.h
ai_domain_baset::is_bottom
virtual bool is_bottom() const =0
ai_baset::~ai_baset
virtual ~ai_baset()
Definition: ai.h:42
expr.h
ait::abstract_state_before
std::unique_ptr< statet > abstract_state_before(locationt t) const override
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
Definition: ai.h:393
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
ai_baset::statet
ai_domain_baset statet
Definition: ai.h:35
ai_baset::concurrent_fixedpoint
void concurrent_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:456
make_unique.h
ai_baset::get_state
virtual statet & get_state(locationt l)=0
Get the state for the given location, creating it in a default way if it doesn't exist.
ait::locationt
goto_programt::const_targett locationt
Definition: ai.h:373
ai_baset::merge
virtual bool merge(const statet &src, locationt from, locationt to)=0
ai_baset::get_next
locationt get_next(working_sett &working_set)
Get the next location from the work queue.
Definition: ai.cpp:221
ai_baset::operator()
void operator()(const goto_functionst &goto_functions, const namespacet &ns)
Run abstract interpretation on a whole program.
Definition: ai.h:60
ai_baset::output
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Output the abstract states for a whole program.
Definition: ai.cpp:24
ai_baset::entry_state
void entry_state(const goto_programt &goto_program)
Set the abstract state of the entry location of a single function to the entry state required by the ...
Definition: ai.cpp:191
ai_baset::output_json
jsont output_json(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
Output the abstract states for a single function as JSON.
Definition: ai.h:182
ai_baset::output
void output(const goto_modelt &goto_model, std::ostream &out) const
Output the abstract states for a whole program.
Definition: ai.h:134
ai_baset::put_in_working_set
void put_in_working_set(working_sett &working_set, locationt l)
Definition: ai.h:282
ai_baset::abstract_state_before
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
concurrency_aware_ait::merge_shared
bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns) override
This function should not be implemented in sequential analyses.
Definition: ai.h:478
concurrency_aware_ait::fixedpoint
void fixedpoint(const goto_functionst &goto_functions, const namespacet &ns) override
Definition: ai.h:490
ai_baset::operator()
void operator()(const irep_idt &function_identifier, const goto_programt &goto_program, const namespacet &ns)
Run abstract interpretation on a single function.
Definition: ai.h:47
ai_baset::merge_shared
virtual bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns)=0
ait::merge
bool merge(const statet &src, locationt from, locationt to) override
Definition: ai.h:434
ai_baset::output_json
jsont output_json(const namespacet &ns, const goto_programt &goto_program) const
Output the abstract states for a single function as JSON.
Definition: ai.h:174
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
ai_baset::abstract_state_after
virtual std::unique_ptr< statet > abstract_state_after(locationt l) const
Get a copy of the abstract state after the given instruction, without needing to know what kind of do...
Definition: ai.h:114
ai_baset::finalize
virtual void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
Definition: ai.cpp:216
xmlt
Definition: xml.h:18
ai_baset::do_function_call
bool do_function_call(const irep_idt &calling_function_identifier, 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:325
ai_baset::output
void output(const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a function.
Definition: ai.h:143
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
ait::operator[]
domainT & operator[](locationt l)
Definition: ai.h:375
ai_baset::output
void output(const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
Output the abstract states for a function.
Definition: ai.h:152
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:40
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
ai_baset::do_function_call_rec
bool do_function_call_rec(const irep_idt &calling_function_identifier, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:405
concurrency_aware_ait
Definition: ai.h:467
ai_baset::ai_baset
ai_baset()
Definition: ai.h:38
ai_baset
The basic interface of an abstract interpreter.
Definition: ai.h:32
ai_baset::output_json
jsont output_json(const goto_modelt &goto_model) const
Output the abstract states for a whole program as JSON.
Definition: ai.h:166
json.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
ai_baset::clear
virtual void clear()
Reset the abstract state.
Definition: ai.h:123
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
ait::find_state
const statet & find_state(locationt l) const override
Get the state for the given location if it already exists; throw an exception if it doesn't.
Definition: ai.h:425
ai_baset::initialize
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: ai.cpp:202
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
ait::clear
void clear() override
Reset the abstract state.
Definition: ai.h:406
ai_baset::working_sett
std::map< unsigned, locationt > working_sett
The work queue, sorted by location number.
Definition: ai.h:277
ai_baset::output_xml
xmlt output_xml(const goto_modelt &goto_model) const
Output the abstract states for the whole program as XML.
Definition: ai.h:195
ai_baset::output_xml
xmlt output_xml(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
Output the abstract states for a single function as XML.
Definition: ai.h:211
ait::make_temporary_state
std::unique_ptr< statet > make_temporary_state(const statet &s) override
Make a copy of a state.
Definition: ai.h:441
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
ai_baset::operator()
void operator()(const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Run abstract interpretation on a single function.
Definition: ai.h:81
statet
unsigned int statet
Definition: trace_automaton.h:24
validation_modet::INVARIANT
@ INVARIANT
ait::state_mapt
std::unordered_map< locationt, domainT, const_target_hash, pointee_address_equalt > state_mapt
Definition: ai.h:415
concurrency_aware_ait::concurrency_aware_ait
concurrency_aware_ait()
Definition: ai.h:474
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470