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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
ai_domain_baset::make_bottom
virtual void make_bottom()=0
no states
ai_domain_baset::transform
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...
goto_model.h
exprt
Base class for all expressions.
Definition: expr.h:54
ai_domain_baset::output_json
virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const
Definition: ai_domain.cpp:16
jsont
Definition: json.h:23
xml.h
ai_domain_baset::is_bottom
virtual bool is_bottom() const =0
expr.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
make_unique.h
ai_domain_baset::ai_domain_baset
ai_domain_baset()
The constructor is expected to produce 'false' or 'bottom'.
Definition: ai_domain.h:31
ai_domain_baset::ai_simplify_lhs
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
ai_domain_baset::output_xml
virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const
Definition: ai_domain.cpp:25
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
xmlt
Definition: xml.h:18
ai_domain_baset::~ai_domain_baset
virtual ~ai_domain_baset()
Definition: ai_domain.h:36
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:40
ai_domain_baset::to_predicate
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
ai_baset
The basic interface of an abstract interpreter.
Definition: ai.h:32
json.h
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
ai_domain_baset::make_entry
virtual void make_entry()=0
Make this domain a reasonable entry-point state.
ai_domain_baset::is_top
virtual bool is_top() const =0
ai_domain_baset::ai_simplify
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
Definition: ai_domain.h:105
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
ai_domain_baset::output
virtual void output(std::ostream &, const ai_baset &, const namespacet &) const
Definition: ai_domain.h:66
ai_domain_baset::make_top
virtual void make_top()=0
all states – the analysis doesn't use this, and domains may refuse to implement it.