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(
99 const irep_idt &function_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
122 virtual void make_entry()
123 {
124 make_top();
125 }
126
127 virtual bool is_bottom() const = 0;
128
129 virtual bool is_top() const = 0;
130
144
148
150 virtual bool ai_simplify(exprt &condition, const namespacet &) const
151 {
152 (void)condition; // unused parameter
153 return true;
154 }
155
157 virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const;
158
161 virtual exprt to_predicate(void) const
162 {
163 if(is_bottom())
164 return false_exprt();
165 else
166 return true_exprt();
167 }
168};
169
170// No virtual interface is complete without a factory!
172{
173public:
177
179 {
180 }
181
182 virtual std::unique_ptr<statet> make(locationt l) const = 0;
183 virtual std::unique_ptr<statet> copy(const statet &s) const = 0;
184
185 // Not domain construction but requires knowing the precise type of statet
186 virtual bool
188 const = 0;
189};
190// Converting make to take a trace_ptr instead of a location would
191// require removing the backwards-compatible
192// location_sensitive_storaget::get_state(locationt l)
193// function which is used by some of the older domains
194
195// It would be great to have a single (templated) default implementation.
196// However, a default constructor is not part of the ai_domain_baset interface
197// and there are some domains which don't have one. So we need to separate the
198// methods.
199template <typename domainT>
201{
202public:
206
207 std::unique_ptr<statet> copy(const statet &s) const override
208 {
209 return util_make_unique<domainT>(static_cast<const domainT &>(s));
210 }
211
212 bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to)
213 const override
214 {
215 // For backwards compatability, use the location version
216 return static_cast<domainT &>(dest).merge(
217 static_cast<const domainT &>(src), from, to);
218 }
219};
220
221template <typename domainT>
223 : public ai_domain_factoryt<domainT>
224{
225public:
229
230 std::unique_ptr<statet> make(locationt l) const override
231 {
232 auto d = util_make_unique<domainT>();
233 CHECK_RETURN(d->is_bottom());
234 return std::unique_ptr<statet>(d.release());
235 }
236};
237
238template <typename domainT>
240 : public ai_domain_factoryt<domainT>
241{
242public:
246
247 std::unique_ptr<statet> make(locationt l) const override
248 {
249 auto d = util_make_unique<domainT>(l);
250 CHECK_RETURN(d->is_bottom());
251 return std::unique_ptr<statet>(d.release());
252 }
253};
254
255#endif
Abstract Interpretation history.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:118
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 void make_entry()
Make this domain a reasonable entry-point state For most domains top is sufficient.
Definition ai_domain.h:122
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:161
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 directly (see make_entry) and domains may refuse to implem...
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 bool is_top() const =0
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
Definition ai_domain.h:150
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:176
virtual ~ai_domain_factory_baset()
Definition ai_domain.h:178
ai_domain_baset::locationt locationt
Definition ai_domain.h:175
virtual std::unique_ptr< statet > make(locationt l) const =0
ai_domain_baset statet
Definition ai_domain.h:174
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:230
ai_domain_factory_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:228
ai_domain_factory_baset::locationt locationt
Definition ai_domain.h:227
ai_domain_factory_baset::statet statet
Definition ai_domain.h:226
ai_domain_factory_baset::locationt locationt
Definition ai_domain.h:244
std::unique_ptr< statet > make(locationt l) const override
Definition ai_domain.h:247
ai_domain_factory_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:245
ai_domain_factory_baset::statet statet
Definition ai_domain.h:243
std::unique_ptr< statet > copy(const statet &s) const override
Definition ai_domain.h:207
ai_domain_factory_baset::statet statet
Definition ai_domain.h:203
ai_domain_factory_baset::locationt locationt
Definition ai_domain.h:204
ai_domain_factory_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:205
bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to) const override
Definition ai_domain.h:212
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:563
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
The Boolean constant false.
Definition std_expr.h:3017
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:3008
Definition xml.h:21
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495