full_array_abstract_object.h

Go to the documentation of this file.

/*******************************************************************\
 
 Module: Variable Sensitivity
 
 Author: Thomas Kiley, thomas.kiley@diffblue.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H
 
#include <iosfwd>
 
#include <analyses/variable-sensitivity/abstract_aggregate_object.h>
 
class ai_baset;
 
class full_array_abstract_objectt : public abstract_aggregate_objectt<
                                      full_array_abstract_objectt,
                                      array_aggregate_typet>
{
public:
  typedef sharing_ptrt<full_array_abstract_objectt> const full_array_pointert;
  typedef abstract_aggregate_objectt<
    full_array_abstract_objectt,
    array_aggregate_typet>
    abstract_aggregate_baset;
 
  full_array_abstract_objectt(typet type, bool top, bool bottom);
 
  full_array_abstract_objectt(
    const exprt &expr,
    const abstract_environmentt &environment,
    const namespacet &ns);
 
  void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
    const override;
 
  abstract_object_pointert
  write_location_context(const locationt &location) const override;
  abstract_object_pointert
  merge_location_context(const locationt &location) const override;
 
  abstract_object_pointert
  visit_sub_elements(const abstract_object_visitort &visitor) const override;
 
protected:
  CLONE
 
  abstract_object_pointert read_component(
    const abstract_environmentt &env,
    const exprt &expr,
    const namespacet &ns) const override;
 
  abstract_object_pointert write_component(
    abstract_environmentt &environment,
    const namespacet &ns,
    const std::stack<exprt> &stack,
    const exprt &expr,
    const abstract_object_pointert &value,
    bool merging_write) const override;
 
  void statistics(
    abstract_object_statisticst &statistics,
    abstract_object_visitedt &visited,
    const abstract_environmentt &env,
    const namespacet &ns) const override;
 
  abstract_object_pointert merge(
    const abstract_object_pointert &other,
    const widen_modet &widen_mode) const override;
 
  bool verify() const override;
 
  void set_top_internal() override;
 
private:
  abstract_object_pointert read_element(
    const abstract_environmentt &env,
    const exprt &expr,
    const namespacet &ns) const;
 
  abstract_object_pointert write_element(
    abstract_environmentt &environment,
    const namespacet &ns,
    const std::stack<exprt> &stack,
    const exprt &expr,
    const abstract_object_pointert &value,
    bool merging_write) const;
 
  abstract_object_pointert write_sub_element(
    abstract_environmentt &environment,
    const namespacet &ns,
    const std::stack<exprt> &stack,
    const exprt &expr,
    const abstract_object_pointert &value,
    bool merging_write) const;
 
  abstract_object_pointert write_leaf_element(
    abstract_environmentt &environment,
    const namespacet &ns,
    const exprt &expr,
    const abstract_object_pointert &value,
    bool merging_write) const;
 
  // Since we don't store for any index where the value is top
  // we don't use a regular array but instead a map of array indices
  // to the value at that index
  struct mp_integer_hasht
  {
    size_t operator()(const mp_integer &i) const
    {
      return std::hash<BigInt::ullong_t>{}(i.to_ulong());
    }
  };
 
  typedef sharing_mapt<
    mp_integer,
    abstract_object_pointert,
    false,
    mp_integer_hasht>
    shared_array_mapt;
 
  shared_array_mapt map;
 
  void map_put(
    mp_integer index,
    const abstract_object_pointert &value,
    bool overrun);
  abstract_object_pointert map_find_or_top(
    mp_integer index,
    const abstract_environmentt &env,
    const namespacet &ns) const;
 
  abstract_object_pointert
  get_top_entry(const abstract_environmentt &env, const namespacet &ns) const;
 
  abstract_object_pointert full_array_merge(
    const full_array_pointert &other,
    const widen_modet &widen_mode) const;
 
  exprt to_predicate_internal(const exprt &name) const override;
};
 
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H