abstract_object.h

Go to the documentation of this file.

/*******************************************************************\
 
 Module: analyses variable-sensitivity
 
 Author: Thomas Kiley, thomas.kiley@diffblue.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_H
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_H
 
#include <memory>
#include <set>
#include <stack>
 
#include <goto-programs/goto_program.h>
#include <util/sharing_map.h>
 
class abstract_environmentt;
class namespacet;
struct abstract_object_statisticst;
enum class widen_modet;
 
#define CLONE                                                                  \
  internal_abstract_object_pointert mutable_clone() const override             \
  {                                                                            \
    typedef std::remove_const<                                                 \
      std::remove_reference<decltype(*this)>::type>::type current_typet;       \
    return internal_abstract_object_pointert(new current_typet(*this));        \
  }
#define CLONE                                                                  \ …
 
 
template <class T>
using sharing_ptrt = std::shared_ptr<const T>; // NOLINT(*)
 
typedef sharing_ptrt<class abstract_objectt> abstract_object_pointert;
using abstract_object_visitedt = std::set<abstract_object_pointert>;
 
class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
{
public:
  abstract_objectt(const typet &type, bool top, bool bottom);
 
  abstract_objectt(
    const exprt &expr,
    const abstract_environmentt &environment,
    const namespacet &ns);
 
  virtual ~abstract_objectt()
  {
  }
  virtual ~abstract_objectt() {…}
 
  virtual const typet &type() const;
 
  virtual bool is_top() const;
 
  virtual bool is_bottom() const;
 
  virtual bool verify() const;
 
  virtual void get_statistics(
    abstract_object_statisticst &statistics,
    abstract_object_visitedt &visited,
    const abstract_environmentt &env,
    const namespacet &ns) 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;
 
  virtual exprt to_constant() const;
 
  exprt to_predicate(const exprt &name) const;
 
  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;
 
  virtual void output(
    std::ostream &out,
    const class ai_baset &ai,
    const namespacet &ns) const;
 
  typedef goto_programt::const_targett locationt;
  typedef sharing_mapt<irep_idt, abstract_object_pointert, false, irep_id_hash>
    shared_mapt;
 
  static void dump_map(std::ostream out, const shared_mapt &m);
  static void
  dump_map_diff(std::ostream out, const shared_mapt &m1, const shared_mapt &m2);
 
  virtual bool has_been_modified(const abstract_object_pointert &before) const
  {
    return this != before.get();
  };
  virtual bool has_been_modified(const abstract_object_pointert &before) const {…}
 
  struct combine_result
  {
    abstract_object_pointert object;
    bool modified;
  };
  struct combine_result {…};
  static combine_result merge(
    const abstract_object_pointert &op1,
    const abstract_object_pointert &op2,
    const locationt &merge_location,
    const widen_modet &widen_mode);
  static combine_result merge(
    const abstract_object_pointert &op1,
    const abstract_object_pointert &op2,
    const widen_modet &widen_mode);
 
  static combine_result meet(
    const abstract_object_pointert &op1,
    const abstract_object_pointert &op2);
 
  virtual abstract_object_pointert
  meet(const abstract_object_pointert &other) const;
 
  virtual abstract_object_pointert
  write_location_context(const locationt &location) const;
 
  virtual abstract_object_pointert
  merge_location_context(const locationt &location) const;
 
  // Const versions must perform copy-on-write
  abstract_object_pointert make_top() const
  {
    if(is_top())
      return shared_from_this();
 
    internal_abstract_object_pointert clone = mutable_clone();
    clone->set_top();
    return clone;
  }
  abstract_object_pointert make_top() const {…}
 
  abstract_object_pointert clear_top() const
  {
    if(!is_top())
      return shared_from_this();
 
    internal_abstract_object_pointert clone = mutable_clone();
    clone->set_not_top();
    return clone;
  }
  abstract_object_pointert clear_top() const {…}
 
  virtual abstract_object_pointert unwrap_context() const;
 
  struct abstract_object_visitort
  {
    virtual abstract_object_pointert
    visit(const abstract_object_pointert &element) const = 0;
  };
  struct abstract_object_visitort {…};
 
  virtual abstract_object_pointert
  visit_sub_elements(const abstract_object_visitort &visitor) const
  {
    return shared_from_this();
  }
  visit_sub_elements(const abstract_object_visitort &visitor) const {…}
 
  virtual size_t internal_hash() const
  {
    return std::hash<abstract_object_pointert>{}(shared_from_this());
  }
  virtual size_t internal_hash() const {…}
 
  virtual bool internal_equality(const abstract_object_pointert &other) const
  {
    return shared_from_this() == other;
  }
  virtual bool internal_equality(const abstract_object_pointert &other) const {…}
 
  virtual exprt to_predicate_internal(const exprt &name) const;
 
private:
  typet t;
  bool bottom;
  bool top;
 
  // Hooks to allow a sub-class to perform its own operations on
  // setting/clearing top
  virtual void set_top_internal()
  {
  }
  virtual void set_top_internal() {…}
  virtual void set_not_top_internal()
  {
  }
  virtual void set_not_top_internal() {…}
 
  virtual abstract_object_pointert
  abstract_object_merge_internal(const abstract_object_pointert &other) const;
 
  virtual abstract_object_pointert
  abstract_object_meet_internal(const abstract_object_pointert &other) const;
 
protected:
  template <class T>
  using internal_sharing_ptrt = std::shared_ptr<T>;
 
  typedef internal_sharing_ptrt<class abstract_objectt>
    internal_abstract_object_pointert;
 
  // Macro is not used as this does not override
  virtual internal_abstract_object_pointert mutable_clone() const
  {
    return internal_abstract_object_pointert(new abstract_objectt(*this));
  }
  virtual internal_abstract_object_pointert mutable_clone() const {…}
 
  abstract_object_pointert
  abstract_object_merge(const abstract_object_pointert &other) const;
 
  bool should_use_base_merge(const abstract_object_pointert &other) const;
 
  virtual abstract_object_pointert merge(
    const abstract_object_pointert &other,
    const widen_modet &widen_mode) const;
 
  abstract_object_pointert
  abstract_object_meet(const abstract_object_pointert &other) const;
 
  bool should_use_base_meet(const abstract_object_pointert &other) const;
 
  // The one exception is merge in descendant classes, which needs this
  void set_top()
  {
    top = true;
    this->set_top_internal();
  }
  void set_top() {…}
  void set_not_top()
  {
    top = false;
    this->set_not_top_internal();
  }
  void set_not_top() {…}
  void set_not_bottom()
  {
    bottom = false;
  }
  void set_not_bottom() {…}
};
class abstract_objectt : public std::enable_shared_from_this<abstract_objectt> {…};
 
struct abstract_hashert
{
  typedef abstract_object_pointert argument_typet;
  typedef std::size_t result_typet;
  result_typet operator()(argument_typet const &s) const noexcept
  {
    return s->internal_hash();
  }
  result_typet operator()(argument_typet const &s) const noexcept {…}
};
struct abstract_hashert {…};
 
struct abstract_equalert
{
  typedef abstract_object_pointert argument_typet;
  typedef std::size_t result_typet;
  bool operator()(argument_typet const &left, argument_typet const &right) const
    noexcept
  {
    return left->internal_equality(right);
  }
  bool operator()(argument_typet const &left, argument_typet const &right) const {…}
};
struct abstract_equalert {…};
 
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_H