cprover
ai_domain.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_DOMAIN_H
13 #define CPROVER_ANALYSES_AI_DOMAIN_H
14 
15 #include <util/expr.h>
16 #include <util/json.h>
17 #include <util/make_unique.h>
18 #include <util/xml.h>
19 
21 
22 // forward reference the abstract interpreter interface
23 class ai_baset;
24 
28 {
29 protected:
32  {
33  }
34 
35 public:
36  virtual ~ai_domain_baset()
37  {
38  }
39 
41 
56 
57  virtual void transform(
58  const irep_idt &function_from,
59  locationt from,
60  const irep_idt &function_to,
61  locationt to,
62  ai_baset &ai,
63  const namespacet &ns) = 0;
64 
65  virtual void
66  output(std::ostream &, const ai_baset &, const namespacet &) const
67  {
68  }
69 
70  virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const;
71 
72  virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const;
73 
75  virtual void make_bottom() = 0;
76 
79  virtual void make_top() = 0;
80 
82  virtual void make_entry() = 0;
83 
84  virtual bool is_bottom() const = 0;
85 
86  virtual bool is_top() const = 0;
87 
99 
103 
105  virtual bool ai_simplify(exprt &condition, const namespacet &) const
106  {
107  (void)condition; // unused parameter
108  return true;
109  }
110 
112  virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const;
113 
116  virtual exprt to_predicate(void) const
117  {
118  if(is_bottom())
119  return false_exprt();
120  else
121  return true_exprt();
122  }
123 };
124 
125 #endif
virtual bool is_top() const =0
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
Definition: ai_domain.h:105
virtual void make_bottom()=0
no states
virtual void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns)=0
how function calls are treated: a) there is an edge from each call site to the function head b) there...
Definition: json.h:23
virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const
Definition: ai_domain.cpp:16
virtual bool is_bottom() const =0
Symbol Table + CFG.
The Boolean constant true.
Definition: std_expr.h:4443
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
instructionst::const_iterator const_targett
Definition: goto_program.h:415
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Definition: xml.h:18
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
virtual exprt to_predicate(void) const
Gives a Boolean condition that is true for all values represented by the domain.
Definition: ai_domain.h:116
The Boolean constant false.
Definition: std_expr.h:4452
ai_domain_baset()
The constructor is expected to produce 'false' or 'bottom'.
Definition: ai_domain.h:31
virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const
Simplifies the expression but keeps it as an l-value.
Definition: ai_domain.cpp:42
The basic interface of an abstract interpreter.
Definition: ai.h:32
virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const
Definition: ai_domain.cpp:25
Base class for all expressions.
Definition: expr.h:54
virtual ~ai_domain_baset()
Definition: ai_domain.h:36
goto_programt::const_targett locationt
Definition: ai_domain.h:40
virtual void make_top()=0
all states – the analysis doesn't use this, and domains may refuse to implement it.
virtual void output(std::ostream &, const ai_baset &, const namespacet &) const
Definition: ai_domain.h:66
virtual void make_entry()=0
Make this domain a reasonable entry-point state.