/*******************************************************************\

 Module: analyses variable-sensitivity

 Author: Thomas Kiley, thomas.kiley@diffblue.com

\*******************************************************************/

/// \file
/// An abstraction of a pointer that tracks a single pointer
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_POINTER_ABSTRACT_OBJECT_H
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_POINTER_ABSTRACT_OBJECT_H

#include <iosfwd>

#include <analyses/variable-sensitivity/pointer_abstract_object.h>
#include <analyses/variable-sensitivity/write_stack.h>

class constant_pointer_abstract_objectt : public pointer_abstract_objectt
{
private:
  typedef sharing_ptrt<constant_pointer_abstract_objectt>
    constant_pointer_abstract_pointert;

public:
  /// \param type: the type the abstract_object is representing
  explicit constant_pointer_abstract_objectt(const typet &type);

  /// \param type: the type the abstract_object is representing
  /// \param top: is the abstract_object starting as top
  /// \param bottom: is the abstract_object starting as bottom
  ///
  /// Start the abstract object at either top or bottom or neither
  /// Asserts if both top and bottom are true
  constant_pointer_abstract_objectt(const typet &type, bool top, bool bottom);

  /// \param old: the abstract object to copy from
  constant_pointer_abstract_objectt(
    const constant_pointer_abstract_objectt &old);

  /// \param expr: the expression to use as the starting pointer for
  ///              an abstract object
  /// \param environment: the environment in which we evaluate expr
  /// \param ns: the current namespace
  constant_pointer_abstract_objectt(
    const exprt &expr,
    const abstract_environmentt &environment,
    const namespacet &ns);

  /// To try and find a constant expression for this abstract object
  ///
  /// \return Returns an expression representing the value if it can.
  ///          Returns a nil expression if it can be more than one value.
  ///          Returns null_pointer expression if it must be null
  ///          Returns an address_of_exprt with the value set to the
  ///          result of to_constant called on whatever abstract object this
  ///          pointer is pointing to.
  ///
  exprt to_constant() const override;

  /// Print the value of the pointer. Either NULL if nullpointer or
  /// ptr -> ( output of what the pointer is pointing to).
  ///
  /// \param out: the stream to write to
  /// \param ai: the domain in which this object appears
  ///            given as ai_baset so that the interface is the same
  ///            across all domains
  /// \param ns: the current namespace
  void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
    const override;

  /// A helper function to dereference a value from a pointer. Providing
  /// the pointer can only be pointing at one thing, returns an abstract
  /// object representing that thing. If null or top will return top.
  ///
  /// \param env: the environment
  /// \param ns: the namespace
  ///
  /// \return An abstract object representing the value this pointer is pointing
  ///         to
  abstract_object_pointert read_dereference(
    const abstract_environmentt &env,
    const namespacet &ns) const override;

  /// A helper function to evaluate writing to a pointers value.
  /// If the pointer can only be pointing to one element that it overwrites
  /// that element (or merges if merging_write) with the new value.
  /// If don't know what we are pointing to, we delegate to the parent.
  ///
  /// \param environment: the environment
  /// \param ns: the namespace
  /// \param stack: the remaining stack
  /// \param value: the value to write to the dereferenced pointer
  /// \param merging_write: is it a merging write (i.e. we aren't certain
  ///                       we are writing to this particular pointer therefore
  ///                       the value should be merged with whatever is already
  ///                       there or we are certain we are writing to this
  ///                       pointer so therefore the value can be replaced
  ///
  /// \return A modified abstract object representing this pointer after it
  ///         has been written to.
  abstract_object_pointert write_dereference(
    abstract_environmentt &environment,
    const namespacet &ns,
    const std::stack<exprt> &stack,
    const abstract_object_pointert &value,
    bool merging_write) const override;

  void get_statistics(
    abstract_object_statisticst &statistics,
    abstract_object_visitedt &visited,
    const abstract_environmentt &env,
    const namespacet &ns) const override;

protected:
  /// Set this abstract object to be the result of merging this
  /// abstract object. This calls the merge_constant_pointers if
  /// we are trying to merge a constant pointer we use the constant pointer
  /// constant pointer merge
  ///
  /// \param op1: the pointer being merged
  ///
  /// \return Returns the result of the merge.
  abstract_object_pointert merge(abstract_object_pointert op1) const override;

  CLONE

private:
  /// Merges two constant pointers. If they are pointing at the same
  /// value, we merge, otherwise we set to top.
  ///
  /// \param other: the pointer being merged
  ///
  /// \return Returns a new abstract object that is the result of the merge
  ///         unless the merge is the same as this abstract object, in which
  ///         case it returns this.
  abstract_object_pointert
  merge_constant_pointers(const constant_pointer_abstract_pointert other) const;

  write_stackt value_stack;
};

#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONSTANT_POINTER_ABSTRACT_OBJECT_H // NOLINT(*)
