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 
39 
40 #ifndef CPROVER_ANALYSES_AI_DOMAIN_H
41 #define CPROVER_ANALYSES_AI_DOMAIN_H
42 
43 #include <util/expr.h>
44 #include <util/json.h>
45 #include <util/make_unique.h>
46 #include <util/xml.h>
47 
49 
50 #include "ai_history.h"
51 
52 // forward reference the abstract interpreter interface
53 class ai_baset;
54 
58 {
59 protected:
63  {
64  }
65 
68  {
69  }
70 
71 public:
72  virtual ~ai_domain_baset()
73  {
74  }
75 
78 
99  virtual void transform(
100  const irep_idt &function_from,
101  trace_ptrt from,
102  const irep_idt &function_to,
103  trace_ptrt to,
104  ai_baset &ai,
105  const namespacet &ns)
106  {
107  return transform(
108  function_from,
109  from->current_location(),
110  function_to,
111  to->current_location(),
112  ai,
113  ns);
114  }
115 
116  DEPRECATED(SINCE(2019, 08, 01, "use the history signature instead"))
117  virtual void transform(
118  const irep_idt &function_from,
119  locationt from,
120  const irep_idt &function_to,
121  locationt to,
122  ai_baset &ai,
123  const namespacet &ns) = 0;
124 
125  virtual void
126  output(std::ostream &, const ai_baset &, const namespacet &) const
127  {
128  }
129 
130  virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const;
131 
132  virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const;
133 
135  virtual void make_bottom() = 0;
136 
139  virtual void make_top() = 0;
140 
142  virtual void make_entry() = 0;
143 
144  virtual bool is_bottom() const = 0;
145 
146  virtual bool is_top() const = 0;
147 
161 
165 
167  virtual bool ai_simplify(exprt &condition, const namespacet &) const
168  {
169  (void)condition; // unused parameter
170  return true;
171  }
172 
174  virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const;
175 
178  virtual exprt to_predicate(void) const
179  {
180  if(is_bottom())
181  return false_exprt();
182  else
183  return true_exprt();
184  }
185 };
186 
187 // No virtual interface is complete without a factory!
189 {
190 public:
194 
196  {
197  }
198 
199  virtual std::unique_ptr<statet> make(locationt l) const = 0;
200  virtual std::unique_ptr<statet> copy(const statet &s) const = 0;
201 
202  // Not domain construction but requires knowing the precise type of statet
203  virtual bool
204  merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to)
205  const = 0;
206 };
207 // Converting make to take a trace_ptr instead of a location would
208 // require removing the backwards-compatible
209 // location_sensitive_storaget::get_state(locationt l)
210 // function which is used by some of the older domains
211 
212 // It would be great to have a single (templated) default implementation.
213 // However, a default constructor is not part of the ai_domain_baset interface
214 // and there are some domains which don't have one. So we need to separate the
215 // methods.
216 template <typename domainT>
218 {
219 public:
223 
224  std::unique_ptr<statet> copy(const statet &s) const override
225  {
226  return util_make_unique<domainT>(static_cast<const domainT &>(s));
227  }
228 
229  bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to)
230  const override
231  {
232  // For backwards compatability, use the location version
233  return static_cast<domainT &>(dest).merge(
234  static_cast<const domainT &>(src),
235  from->current_location(),
236  to->current_location());
237  }
238 };
239 
240 template <typename domainT>
242  : public ai_domain_factoryt<domainT>
243 {
244 public:
248 
249  std::unique_ptr<statet> make(locationt l) const override
250  {
251  auto d = util_make_unique<domainT>();
252  CHECK_RETURN(d->is_bottom());
253  return std::unique_ptr<statet>(d.release());
254  }
255 };
256 
257 #endif
ai_domain_factory_default_constructort
Definition: ai_domain.h:243
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
ai_domain_factory_baset::merge
virtual bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to) const =0
ai_domain_factoryt::trace_ptrt
ai_domain_factory_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:222
ai_domain_baset::make_bottom
virtual void make_bottom()=0
no states
ai_domain_baset::ai_domain_baset
ai_domain_baset(const ai_domain_baset &old)
A copy constructor is part of the domain interface.
Definition: ai_domain.h:67
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
ai_domain_factory_baset::trace_ptrt
ai_domain_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:193
ai_domain_factory_baset::make
virtual std::unique_ptr< statet > make(locationt l) const =0
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
ai_domain_factory_baset
Definition: ai_domain.h:189
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:27
xml.h
ai_domain_baset::is_bottom
virtual bool is_bottom() const =0
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:77
ai_domain_factory_baset::copy
virtual std::unique_ptr< statet > copy(const statet &s) const =0
ai_domain_factory_baset::statet
ai_domain_baset statet
Definition: ai_domain.h:191
expr.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
ai_domain_baset::transform
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)
how function calls are treated: a) there is an edge from each call site to the function head b) there...
Definition: ai_domain.h:99
make_unique.h
ai_domain_factory_default_constructort::trace_ptrt
ai_domain_factory_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:247
ai_domain_baset::ai_domain_baset
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:62
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:3964
ai_domain_factoryt::locationt
ai_domain_factory_baset::locationt locationt
Definition: ai_domain.h:221
ai_domain_factoryt::merge
bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to) const override
Definition: ai_domain.h:229
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
ai_domain_factory_baset::~ai_domain_factory_baset
virtual ~ai_domain_factory_baset()
Definition: ai_domain.h:195
xmlt
Definition: xml.h:21
ai_history.h
Abstract Interpretation history.
ai_domain_baset::~ai_domain_baset
virtual ~ai_domain_baset()
Definition: ai_domain.h:72
ai_domain_factory_default_constructort::make
std::unique_ptr< statet > make(locationt l) const override
Definition: ai_domain.h:249
ai_domain_factory_default_constructort::locationt
ai_domain_factory_baset::locationt locationt
Definition: ai_domain.h:246
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
ai_domain_factoryt
Definition: ai_domain.h:218
ai_domain_factory_default_constructort::statet
ai_domain_factory_baset::statet statet
Definition: ai_domain.h:245
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
ai_domain_factoryt::statet
ai_domain_factory_baset::statet statet
Definition: ai_domain.h:220
ai_history_baset::trace_ptrt
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
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:178
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
json.h
ai_domain_factory_baset::locationt
ai_domain_baset::locationt locationt
Definition: ai_domain.h:192
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
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:167
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:58
ai_domain_baset::output
virtual void output(std::ostream &, const ai_baset &, const namespacet &) const
Definition: ai_domain.h:126
ai_domain_factoryt::copy
std::unique_ptr< statet > copy(const statet &s) const override
Definition: ai_domain.h:224
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.