cprover
abstract_object.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Thomas Kiley, thomas.kiley@diffblue.com
6 
7 \*******************************************************************/
8 
25 
26 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_H
27 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_H
28 
29 #include <algorithm>
30 #include <iosfwd>
31 #include <iterator>
32 #include <map>
33 #include <memory>
34 #include <set>
35 #include <stack>
36 
39 #include <util/expr.h>
40 #include <util/sharing_map.h>
41 
42 class typet;
43 class constant_exprt;
45 class namespacet;
46 
47 #define CLONE \
48  internal_abstract_object_pointert mutable_clone() const override \
49  { \
50  typedef std::remove_const< \
51  std::remove_reference<decltype(*this)>::type>::type current_typet; \
52  return internal_abstract_object_pointert(new current_typet(*this)); \
53  }
54 
71 
72 template <class T>
73 using sharing_ptrt = std::shared_ptr<const T>; // NOLINT(*)
74 
76 using abstract_object_visitedt = std::set<abstract_object_pointert>;
77 
78 class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
79 {
80 public:
82  explicit abstract_objectt(const typet &type);
83 
90  abstract_objectt(const typet &type, bool top, bool bottom);
91 
100  const exprt &expr,
101  const abstract_environmentt &environment,
102  const namespacet &ns);
103 
112  const typet &type,
113  const exprt &expr,
114  const abstract_environmentt &environment,
115  const namespacet &ns);
116 
118  {
119  }
120 
124  virtual const typet &type() const;
125 
130  virtual bool is_top() const;
131 
135  virtual bool is_bottom() const;
136 
140  virtual bool verify() const;
141 
142  virtual void get_statistics(
143  abstract_object_statisticst &statistics,
144  abstract_object_visitedt &visited,
145  const abstract_environmentt &env,
146  const namespacet &ns) const;
147 
164  const exprt &expr,
165  const std::vector<abstract_object_pointert> &operands,
166  const abstract_environmentt &environment,
167  const namespacet &ns) const;
168 
178  virtual exprt to_constant() const;
179 
197  abstract_environmentt &environment,
198  const namespacet &ns,
199  const std::stack<exprt> &stack,
200  const exprt &specifier,
201  const abstract_object_pointert &value,
202  bool merging_write) const;
203 
210  virtual void output(
211  std::ostream &out,
212  const class ai_baset &ai,
213  const namespacet &ns) const;
214 
215  typedef std::set<goto_programt::const_targett> locationst;
218 
219  static void dump_map(std::ostream out, const shared_mapt &m);
227  static void
228  dump_map_diff(std::ostream out, const shared_mapt &m1, const shared_mapt &m2);
229 
238  virtual bool has_been_modified(const abstract_object_pointert before) const
239  {
243  return this != before.get();
244  };
245 
260  bool &out_modifications);
263 
274  bool &out_modifications);
275 
282  meet(const abstract_object_pointert &other) const;
283 
296  const locationst &locations,
297  const bool update_sub_elements) const;
298 
299  // Const versions must perform copy-on-write
301  {
302  if(is_top())
303  return shared_from_this();
304 
306  clone->set_top();
307  return clone;
308  }
309 
311  {
312  if(!is_top())
313  return shared_from_this();
314 
316  clone->set_not_top();
317  return clone;
318  }
319 
321 
327  {
329  visit(const abstract_object_pointert element) const = 0;
330  };
331 
345  {
346  return shared_from_this();
347  }
348 
349  virtual size_t internal_hash() const
350  {
351  return std::hash<abstract_object_pointert>{}(shared_from_this());
352  }
353 
354  virtual bool internal_equality(const abstract_object_pointert &other) const
355  {
356  return shared_from_this() == other;
357  }
358 
359 private:
362  bool bottom;
363  bool top;
364 
365  // Hooks to allow a sub-class to perform its own operations on
366  // setting/clearing top
367  virtual void set_top_internal()
368  {
369  }
370  virtual void set_not_top_internal()
371  {
372  }
373 
388 
395 
396 protected:
397  template <class T>
398  using internal_sharing_ptrt = std::shared_ptr<T>;
399 
402 
403  // Macro is not used as this does not override
405  {
407  }
408 
417 
425  bool should_use_base_merge(const abstract_object_pointert other) const;
426 
434 
441 
446  bool should_use_base_meet(const abstract_object_pointert &other) const;
447 
448  // The one exception is merge in descendant classes, which needs this
449  void set_top()
450  {
451  top = true;
452  this->set_top_internal();
453  }
454  void set_not_top()
455  {
456  top = false;
457  this->set_not_top_internal();
458  }
459 };
460 
462 {
464  typedef std::size_t result_typet;
465  result_typet operator()(argument_typet const &s) const noexcept
466  {
467  return s->internal_hash();
468  }
469 };
470 
472 {
474  typedef std::size_t result_typet;
475  bool operator()(argument_typet const &left, argument_typet const &right) const
476  noexcept
477  {
478  return left->internal_equality(right);
479  }
480 };
481 
482 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_H
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Statistics gathering for the variable senstivity domain.
virtual bool internal_equality(const abstract_object_pointert &other) const
virtual exprt to_constant() const
Converts to a constant expression if possible.
static abstract_object_pointert meet(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Interface method for the meet operation.
abstract_objectt(const typet &type)
virtual bool has_been_modified(const abstract_object_pointert before) const
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state...
virtual bool is_top() const
Find out if the abstract object is top.
static void dump_map(std::ostream out, const shared_mapt &m)
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
virtual abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const
A helper function to evaluate writing to a component of an abstract object.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual internal_abstract_object_pointert mutable_clone() const
virtual abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const
Interface for transforms.
virtual void set_not_top_internal()
bool should_use_base_meet(const abstract_object_pointert &other) const
Helper function to decide if base meet implementation should be used.
virtual void set_top_internal()
virtual abstract_object_pointert abstract_object_meet_internal(const abstract_object_pointert &other) const
Helper function for base meet, in case additional work was needed.
static void dump_map_diff(std::ostream out, const shared_mapt &m1, const shared_mapt &m2)
Dump all elements in m1 that are different or missing in m2.
std::shared_ptr< T > internal_sharing_ptrt
abstract_object_pointert make_top() const
virtual size_t internal_hash() const
abstract_object_pointert abstract_object_merge(const abstract_object_pointert other) const
Create a new abstract object that is the result of the merge, unless the object would be unchanged,...
virtual abstract_object_pointert update_location_context(const locationst &locations, const bool update_sub_elements) const
Update the location context for an abstract object, potentially propogating the update to any childre...
virtual abstract_object_pointert visit_sub_elements(const abstract_object_visitort &visitor) const
Apply a visitor operation to all sub elements of this abstract_object.
bool should_use_base_merge(const abstract_object_pointert other) const
To detect the cases where the base merge is sufficient to do a merge We can't do if this->is_bottom()...
abstract_object_pointert abstract_object_meet(const abstract_object_pointert &other) const
Helper function for base meet.
abstract_object_pointert clear_top() const
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
virtual abstract_object_pointert abstract_object_merge_internal(const abstract_object_pointert other) const
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after t...
internal_sharing_ptrt< class abstract_objectt > internal_abstract_object_pointert
sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > shared_mapt
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
virtual abstract_object_pointert unwrap_context() const
std::set< goto_programt::const_targett > locationst
typet t
To enforce copy-on-write these are private and have read-only accessors.
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
virtual ~abstract_objectt()
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
A constant literal expression.
Definition: std_expr.h:2668
Base class for all expressions.
Definition: expr.h:54
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The type of an expression, extends irept.
Definition: type.h:28
Concrete Goto Program.
Sharing map.
abstract_object_pointert argument_typet
std::size_t result_typet
bool operator()(argument_typet const &left, argument_typet const &right) const noexcept
abstract_object_pointert argument_typet
std::size_t result_typet
result_typet operator()(argument_typet const &s) const noexcept
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
virtual abstract_object_pointert visit(const abstract_object_pointert element) const =0