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
abstract_objectt::internal_equality
virtual bool internal_equality(const abstract_object_pointert &other) const
Definition: abstract_object.h:354
abstract_hashert::operator()
result_typet operator()(argument_typet const &s) const noexcept
Definition: abstract_object.h:465
abstract_objectt::dump_map
static void dump_map(std::ostream out, const shared_mapt &m)
Definition: abstract_object.cpp:244
abstract_objectt::abstract_object_meet_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.
Definition: abstract_object.cpp:101
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
abstract_objectt::is_top
virtual bool is_top() const
Find out if the abstract object is top.
Definition: abstract_object.cpp:150
abstract_objectt::merge
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.
Definition: abstract_object.cpp:189
abstract_objectt::output
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
Definition: abstract_object.cpp:170
sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash >
typet
The type of an expression, extends irept.
Definition: type.h:28
abstract_objectt::should_use_base_merge
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()...
Definition: abstract_object.cpp:211
abstract_objectt::type
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Definition: abstract_object.cpp:53
abstract_objectt::internal_hash
virtual size_t internal_hash() const
Definition: abstract_object.h:349
abstract_objectt::should_use_base_meet
bool should_use_base_meet(const abstract_object_pointert &other) const
Helper function to decide if base meet implementation should be used.
Definition: abstract_object.cpp:231
abstract_objectt::set_top
void set_top()
Definition: abstract_object.h:449
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
sharing_ptrt
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
Definition: abstract_object.h:73
abstract_objectt::clear_top
abstract_object_pointert clear_top() const
Definition: abstract_object.h:310
abstract_hashert::result_typet
std::size_t result_typet
Definition: abstract_object.h:464
abstract_objectt::get_statistics
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
Definition: abstract_object.cpp:284
abstract_objectt::internal_abstract_object_pointert
internal_sharing_ptrt< class abstract_objectt > internal_abstract_object_pointert
Definition: abstract_object.h:401
expr.h
abstract_hashert::argument_typet
abstract_object_pointert argument_typet
Definition: abstract_object.h:463
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
abstract_objectt::has_been_modified
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...
Definition: abstract_object.h:238
abstract_equalert::operator()
bool operator()(argument_typet const &left, argument_typet const &right) const noexcept
Definition: abstract_object.h:475
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
abstract_objectt::~abstract_objectt
virtual ~abstract_objectt()
Definition: abstract_object.h:117
abstract_objectt::shared_mapt
sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > shared_mapt
Definition: abstract_object.h:217
abstract_objectt::locationst
std::set< goto_programt::const_targett > locationst
Definition: abstract_object.h:215
abstract_objectt::to_constant
virtual exprt to_constant() const
Converts to a constant expression if possible.
Definition: abstract_object.cpp:165
abstract_objectt::make_top
abstract_object_pointert make_top() const
Definition: abstract_object.h:300
abstract_objectt::dump_map_diff
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.
Definition: abstract_object.cpp:261
abstract_objectt::set_not_top_internal
virtual void set_not_top_internal()
Definition: abstract_object.h:370
abstract_equalert::result_typet
std::size_t result_typet
Definition: abstract_object.h:474
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:76
abstract_objectt::update_location_context
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...
Definition: abstract_object.cpp:237
abstract_objectt::bottom
bool bottom
Definition: abstract_object.h:362
abstract_objectt::abstract_object_visitort
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
Definition: abstract_object.h:327
goto_program.h
Concrete Goto Program.
abstract_equalert::argument_typet
abstract_object_pointert argument_typet
Definition: abstract_object.h:473
abstract_equalert
Definition: abstract_object.h:472
abstract_objectt::abstract_object_meet
abstract_object_pointert abstract_object_meet(const abstract_object_pointert &other) const
Helper function for base meet.
Definition: abstract_object.cpp:89
abstract_objectt::unwrap_context
virtual abstract_object_pointert unwrap_context() const
Definition: abstract_object.cpp:279
abstract_objectt::abstract_object_merge
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,...
Definition: abstract_object.cpp:64
abstract_hashert
Definition: abstract_object.h:462
abstract_object_statistics.h
Statistics gathering for the variable senstivity domain.
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
abstract_objectt::verify
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
Definition: abstract_object.cpp:160
abstract_objectt::internal_sharing_ptrt
std::shared_ptr< T > internal_sharing_ptrt
Definition: abstract_object.h:398
abstract_objectt::set_not_top
void set_not_top()
Definition: abstract_object.h:454
abstract_objectt::write
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.
Definition: abstract_object.cpp:139
abstract_objectt::set_top_internal
virtual void set_top_internal()
Definition: abstract_object.h:367
abstract_objectt::meet
static abstract_object_pointert meet(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Interface method for the meet operation.
Definition: abstract_object.cpp:217
abstract_objectt::top
bool top
Definition: abstract_object.h:363
abstract_objectt::abstract_object_merge_internal
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...
Definition: abstract_object.cpp:76
abstract_objectt
Definition: abstract_object.h:79
abstract_objectt::is_bottom
virtual bool is_bottom() const
Find out if the abstract object is bottom.
Definition: abstract_object.cpp:155
constant_exprt
A constant literal expression.
Definition: std_expr.h:2668
sharing_map.h
Sharing map.
abstract_objectt::abstract_object_visitort::visit
virtual abstract_object_pointert visit(const abstract_object_pointert element) const =0
abstract_objectt::visit_sub_elements
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.
Definition: abstract_object.h:344
abstract_objectt::mutable_clone
virtual internal_abstract_object_pointert mutable_clone() const
Definition: abstract_object.h:404
abstract_objectt::t
typet t
To enforce copy-on-write these are private and have read-only accessors.
Definition: abstract_object.h:361
abstract_objectt::expression_transform
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.
Definition: abstract_object.cpp:108
abstract_objectt::abstract_objectt
abstract_objectt(const typet &type)
Definition: abstract_object.cpp:25