cprover
Loading...
Searching...
No Matches
ai_domain.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Abstract Interpretation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
39
40#ifndef CPROVER_ANALYSES_AI_DOMAIN_H
41#define CPROVER_ANALYSES_AI_DOMAIN_H
42
43#include <util/json.h>
44#include <util/make_unique.h>
45#include <util/xml.h>
46
47#include "ai_history.h"
48
49// forward reference the abstract interpreter interface
50class ai_baset;
51
55{
56protected:
60 {
61 }
62
65 {
66 }
67
68public:
70 {
71 }
72
75
96 virtual void transform(
98 trace_ptrt from,
99 const irep_idt &function_to,
100 trace_ptrt to,
101 ai_baset &ai,
102 const namespacet &ns) = 0;
103
104 virtual void
105 output(std::ostream &, const ai_baset &, const namespacet &) const
106 {
107 }
108
109 virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const;
110
111 virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const;
112
114 virtual void make_bottom() = 0;
115
118 virtual void make_top() = 0;
119
121 virtual void make_entry() = 0;
122
123 virtual bool is_bottom() const = 0;
124
125 virtual bool is_top() const = 0;
126
140
144
146 virtual bool ai_simplify(exprt &condition, const namespacet &) const
147 {
148 (void)condition; // unused parameter
149 return true;
150 }
151
153 virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const;
154
157 virtual exprt to_predicate(void) const
158 {
159 if(is_bottom())
160 return false_exprt();
161 else
162 return true_exprt();
163 }
164};
165
166// No virtual interface is complete without a factory!
168{
169public:
173
175 {
176 }
177
178 virtual std::unique_ptr<statet> make(locationt l) const = 0;
179 virtual std::unique_ptr<statet> copy(const statet &s) const = 0;
180
181 // Not domain construction but requires knowing the precise type of statet
182 virtual bool
183 merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to)
184 const = 0;
185};
186// Converting make to take a trace_ptr instead of a location would
187// require removing the backwards-compatible
188// location_sensitive_storaget::get_state(locationt l)
189// function which is used by some of the older domains
190
191// It would be great to have a single (templated) default implementation.
192// However, a default constructor is not part of the ai_domain_baset interface
193// and there are some domains which don't have one. So we need to separate the
194// methods.
195template <typename domainT>
197{
198public:
202
203 std::unique_ptr<statet> copy(const statet &s) const override
204 {
205 return util_make_unique<domainT>(static_cast<const domainT &>(s));
206 }
207
208 bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to)
209 const override
210 {
211 // For backwards compatability, use the location version
212 return static_cast<domainT &>(dest).merge(
213 static_cast<const domainT &>(src), from, to);
214 }
215};
216
217template <typename domainT>
219 : public ai_domain_factoryt<domainT>
220{
221public:
225
226 std::unique_ptr<statet> make(locationt l) const override
227 {
228 auto d = util_make_unique<domainT>();
229 CHECK_RETURN(d->is_bottom());
230 return std::unique_ptr<statet>(d.release());
231 }
232};
233
234#endif
Abstract Interpretation history.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:119
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition ai_domain.h:55
virtual bool is_bottom() const =0
virtual void transform(const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt 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...
virtual void make_bottom()=0
no states
ai_domain_baset()
The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the d...
Definition ai_domain.h:59
virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const
Definition ai_domain.cpp:26
virtual exprt to_predicate(void) const
Gives a Boolean condition that is true for all values represented by the domain.
Definition ai_domain.h:157
ai_history_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:74
virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const
Definition ai_domain.cpp:17
virtual void make_top()=0
all states – the analysis doesn't use this, and domains may refuse to implement it.
goto_programt::const_targett locationt
Definition ai_domain.h:73
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:43
virtual void output(std::ostream &, const ai_baset &, const namespacet &) const
Definition ai_domain.h:105
virtual void make_entry()=0
Make this domain a reasonable entry-point state.
virtual bool is_top() const =0
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
Definition ai_domain.h:146
virtual ~ai_domain_baset()
Definition ai_domain.h:69
ai_domain_baset(const ai_domain_baset &old)
A copy constructor is part of the domain interface.
Definition ai_domain.h:64
ai_domain_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:172
virtual ~ai_domain_factory_baset()
Definition ai_domain.h:174
ai_domain_baset::locationt locationt
Definition ai_domain.h:171
virtual std::unique_ptr< statet > make(locationt l) const =0
ai_domain_baset statet
Definition ai_domain.h:170
virtual std::unique_ptr< statet > copy(const statet &s) const =0
virtual bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to) const =0
std::unique_ptr< statet > make(locationt l) const override
Definition ai_domain.h:226
ai_domain_factory_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:224
ai_domain_factory_baset::locationt locationt
Definition ai_domain.h:223
ai_domain_factory_baset::statet statet
Definition ai_domain.h:222
std::unique_ptr< statet > copy(const statet &s) const override
Definition ai_domain.h:203
ai_domain_factory_baset::statet statet
Definition ai_domain.h:199
ai_domain_factory_baset::locationt locationt
Definition ai_domain.h:200
ai_domain_factory_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:201
bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to) const override
Definition ai_domain.h:208
std::shared_ptr< const ai_history_baset > trace_ptrt
History objects are intended to be immutable so they can be shared to reduce memory overhead.
Definition ai_history.h:43
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
The Boolean constant false.
Definition std_expr.h:2865
instructionst::const_iterator const_targett
Definition json.h:27
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The Boolean constant true.
Definition std_expr.h:2856
Definition xml.h:21
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495