value_set.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Value Set
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_H
#define CPROVER_POINTER_ANALYSIS_VALUE_SET_H
 
#include <unordered_set>
 
#include <util/mp_arith.h>
#include <util/reference_counting.h>
#include <util/sharing_map.h>
 
#include "object_numbering.h"
#include "value_sets.h"
 
class namespacet;
class xmlt;
 
class value_sett
{
public:
  value_sett():location_number(0)
  {
  }
 
  value_sett(value_sett &&other)
    : location_number(other.location_number), values(std::move(other.values))
  {
  }
 
  virtual ~value_sett() = default;
 
  value_sett(const value_sett &other) = default;
 
  value_sett &operator=(const value_sett &other) = delete;
 
  value_sett &operator=(value_sett &&other)
  {
    values = std::move(other.values);
    return *this;
  }
 
  virtual bool field_sensitive(const irep_idt &id, const typet &type);
 
  unsigned location_number;
 
  static object_numberingt object_numbering;
 
  typedef std::optional<mp_integer> offsett;
 
  using object_map_dt = std::map<object_numberingt::number_type, offsett>;
 
  static const object_map_dt empty_object_map;
 
  exprt to_expr(const object_map_dt::value_type &it) const;
 
  using object_mapt = reference_counting<object_map_dt, empty_object_map>;
 
  void set(object_mapt &dest, const object_map_dt::value_type &it) const
  {
    dest.write()[it.first]=it.second;
  }
 
  bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
  {
    return insert(dest, it.first, it.second);
  }
 
  bool insert(object_mapt &dest, const exprt &src) const
  {
    return insert(dest, object_numbering.number(src), offsett());
  }
 
  bool insert(
    object_mapt &dest,
    const exprt &src,
    const mp_integer &offset_value) const
  {
    return insert(dest, object_numbering.number(src), offsett(offset_value));
  }
 
  bool insert(
    object_mapt &dest,
    object_numberingt::number_type n,
    const offsett &offset) const;
 
  enum class insert_actiont
  {
    INSERT,
    RESET_OFFSET,
    NONE
  };
 
  insert_actiont get_insert_action(
    const object_mapt &dest,
    object_numberingt::number_type n,
    const offsett &offset) const;
 
  bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
  {
    return insert(dest, object_numbering.number(expr), offset);
  }
 
  struct entryt
  {
    object_mapt object_map;
    irep_idt identifier;
    std::string suffix;
 
    entryt()
    {
    }
 
    entryt(const irep_idt &_identifier, const std::string &_suffix)
      : identifier(_identifier), suffix(_suffix)
    {
    }
 
    bool operator==(const entryt &other) const
    {
      // Note that the object_map comparison below is duplicating the code of
      // operator== defined in reference_counting.h because old versions of
      // clang (3.7 and 3.8) do not resolve the template instantiation correctly
      return identifier == other.identifier && suffix == other.suffix &&
             (object_map.get_d() == other.object_map.get_d() ||
              object_map.read() == other.object_map.read());
    }
    bool operator!=(const entryt &other) const
    {
      return !(*this==other);
    }
  };
 
  typedef sharing_mapt<irep_idt, entryt> valuest;
 
  std::vector<exprt> get_value_set(exprt expr, const namespacet &ns) const;
 
  void clear()
  {
    values.clear();
  }
 
  const entryt *find_entry(const irep_idt &id) const;
 
  void update_entry(
    const entryt &e,
    const typet &type,
    const object_mapt &new_values,
    bool add_to_sets);
 
  void output(std::ostream &out, const std::string &indent = "") const;
 
  xmlt output_xml(void) const;
 
  valuest values;
 
  bool make_union(object_mapt &dest, const object_mapt &src) const;
 
  bool make_union_would_change(const object_mapt &dest, const object_mapt &src)
    const;
 
  bool make_union(const valuest &new_values);
 
  bool make_union(const value_sett &new_values)
  {
    return make_union(new_values.values);
  }
 
  void guard(
    const exprt &expr,
    const namespacet &ns);
 
  void apply_code(
    const codet &code,
    const namespacet &ns)
  {
    apply_code_rec(code, ns);
  }
 
  void assign(
    const exprt &lhs,
    const exprt &rhs,
    const namespacet &ns,
    bool is_simplified,
    bool add_to_sets);
 
  void do_function_call(
    const irep_idt &function,
    const exprt::operandst &arguments,
    const namespacet &ns);
 
  void do_end_function(
    const exprt &lhs,
    const namespacet &ns);
 
  void get_reference_set(
    const exprt &expr,
    value_setst::valuest &dest,
    const namespacet &ns) const;
 
  bool eval_pointer_offset(
    exprt &expr,
    const namespacet &ns) const;
 
  std::optional<irep_idt> get_index_of_symbol(
    irep_idt identifier,
    const typet &type,
    const std::string &suffix,
    const namespacet &ns) const;
 
  void erase_values_from_entry(
    const irep_idt &index,
    const std::unordered_set<exprt, irep_hash> &values_to_erase);
 
  void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns);
 
protected:
  object_mapt
  get_value_set(exprt expr, const namespacet &ns, bool is_simplified) const;
 
  void get_reference_set(
    const exprt &expr,
    object_mapt &dest,
    const namespacet &ns) const
  {
    get_reference_set_rec(expr, dest, ns);
  }
 
  void get_reference_set_rec(
    const exprt &expr,
    object_mapt &dest,
    const namespacet &ns) const;
 
  void dereference_rec(
    const exprt &src,
    exprt &dest) const;
 
  void erase_symbol_rec(
    const typet &type,
    const std::string &erase_prefix,
    const namespacet &ns);
 
  void erase_struct_union_symbol(
    const struct_union_typet &struct_union_type,
    const std::string &erase_prefix,
    const namespacet &ns);
 
protected:
  // Subclass customisation points:
 
  virtual void get_value_set_rec(
    const exprt &expr,
    object_mapt &dest,
    bool &includes_nondet_pointer,
    const std::string &suffix,
    const typet &original_type,
    const namespacet &ns) const;
 
  virtual void assign_rec(
    const exprt &lhs,
    const object_mapt &values_rhs,
    const std::string &suffix,
    const namespacet &ns,
    bool add_to_sets);
 
  virtual void apply_code_rec(
    const codet &code,
    const namespacet &ns);
 
private:
  virtual void adjust_assign_rhs_values(
    const exprt &rhs,
    const namespacet &,
    object_mapt &rhs_values) const
  {
    // unused parameters
    (void)rhs;
    (void)rhs_values;
  }
 
  virtual void apply_assign_side_effects(
    const exprt &lhs,
    const exprt &rhs,
    const namespacet &)
  {
    // unused parameters
    (void)lhs;
    (void)rhs;
  }
};
 
#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H