value_set.h

Go to the documentation of this file.

#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_H
#define CPROVER_POINTER_ANALYSIS_VALUE_SET_H
 
#include <tuple>
#include <map>
#include <pointer-analysis/value_sets.h>
#include <optional>
#include <set>
#include <irep2/irep2.h>
#include <util/arith/mp_arith.h>
#include <util/symtab/namespace.h>
#include <util/base/numbering.h>
#include <util/expr/type_byte_size.h>
#include <util/persistent_map.h>

 
/* Index of, and bytes spanned by, the leading component of a value-set suffix
 * `rest` (with its '.' already dropped) among the member @p names. Member
 * names are not identifiers -- clang spells an anonymous member
 * "S::(anonymous at f.c:4:9)", which contains '.' -- so the component is the
 * longest declared name `rest` continues on a component boundary, never
 * whatever precedes the next '.' or '['. */
std::optional<std::pair<size_t, size_t>> match_leading_component(
  const std::vector<irep_idt> &names,
  const std::string &rest);
 
typedef hash_numbering<expr2tc, irep2_hash> object_numberingt;
typedef hash_numbering<unsigned, std::hash<unsigned>> object_number_numberingt;
 
class value_sett
{
public:
  explicit value_sett(const namespacet &_ns)
    : location_number(0),
      ns(_ns),
      xchg_name("value_sett::__ESBMC_xchg_ptr"),
      xchg_num(0)
  {
  }
 
  /* rec_cache is deliberately not copied: it points into the stack frame of an
   * in-progress query, and a copy can only be taken between queries. */
  value_sett(const value_sett &ref)
    : location_number(ref.location_number),
      values(ref.values),
      ns(ref.ns),
      xchg_name("value_sett::__ESBMC_xchg_ptr"),
      xchg_num(0)
  {
  }
 
  value_sett &operator=(const value_sett &ref)
  {
    location_number = ref.location_number;
    values = ref.values;
    xchg_name = ref.xchg_name;
    xchg_num = ref.xchg_num;
    // No need to copy ns, it should be the same in all contexts.
    return *this;
  }
 
  //*********************************** Types
  //************************************

  typedef std::set<expr2tc> expr_sett;

  class objectt
  {
  public:
    objectt() : offset(0), offset_is_set(true), offset_alignment(0)
    {
    }
 
    objectt(bool offset_set, unsigned int operand)
    {
      if (offset_set)
      {
        offset_is_set = true;
        offset = BigInt(operand);
        offset_alignment = 1;
      }
      else
      {
        offset_is_set = false;
        offset_alignment = operand;
        assert(offset_alignment != 0);
      }
    }
 
    explicit objectt(bool offset_set [[maybe_unused]], const BigInt &_offset)
      : offset(_offset), offset_is_set(true)
    {
      assert(offset_set);
      offset_alignment = 1;
    }

    BigInt offset;
    bool offset_is_set;
    unsigned int offset_alignment;
    bool offset_is_zero() const
    {
      return offset_is_set && offset.is_zero();
    }
    bool operator==(const objectt &o) const
    {
      return offset_is_set == o.offset_is_set &&
             offset_alignment == o.offset_alignment &&
             (!offset_is_set || offset == o.offset);
    }
    bool operator!=(const objectt &o) const
    {
      return !(*this == o);
    }
  };

  typedef std::unordered_map<unsigned, objectt> object_mapt;
  class object_map_dt
  {
    // If you said this class looks pretty map like, it's because it used to be
    // a subclass of std::map, which was far too funky for me, thanks.
  public:
    ~object_map_dt()
    {
      for (auto const &it : themap)
        value_sett::obj_numbering_deref(it.first);
    }
 
    object_map_dt()
    {
    }
 
    object_map_dt &operator=(const object_map_dt &other) = default;
 
    object_map_dt(const object_map_dt &ref)
    {
      *this = ref;
      for (auto const &it : themap)
        value_sett::obj_numbering_ref(it.first);
    }
    typedef object_mapt::const_iterator const_iterator;
    typedef object_mapt::iterator iterator;
 
    objectt &operator[](unsigned i)
    {
      if (themap.find(i) == themap.end())
        value_sett::obj_numbering_ref(i);
      return themap[i];
    }
 
    const_iterator find(unsigned i) const
    {
      return themap.find(i);
    }
 
    iterator find(unsigned i)
    {
      return themap.find(i);
    }
 
    const_iterator begin() const
    {
      return themap.begin();
    }
 
    const_iterator end() const
    {
      return themap.end();
    }
 
    std::size_t size(void) const
    {
      return themap.size();
    }
 
    object_mapt themap;
  };

  struct entryt
  {
    object_mapt object_map;
    std::string identifier;
    std::string suffix;
 
    entryt() = default;
 
    entryt(std::string _identifier, const std::string &_suffix)
      : identifier(std::move(_identifier)), suffix(_suffix)
    {
    }
 
    /* Value equality so the persistent map can be structurally diffed
     * (immer::diff). Only invoked on entries the diff cannot skip by
     * pointer identity, i.e. the divergent leaves. */
    bool operator==(const entryt &e) const
    {
      return identifier == e.identifier && suffix == e.suffix &&
             object_map == e.object_map;
    }
    bool operator!=(const entryt &e) const
    {
      return !(*this == e);
    }
  };

  typedef persistent_map<irep_idt, entryt, irep_id_hash> valuest;

  inline unsigned int get_natural_alignment(const expr2tc &e) const
  {
    const type2tc &t = e->type;
 
    // Null objects are allowed to have symbol types. What alignment to give?
    // Pick 8 bytes, as that's a) word aligned, b) double/uint64_t aligned.
    if (is_null_object2t(e))
      return 8;
 
    assert(!is_symbol_type(t));
    if (is_array_type(t))
    {
      const array_type2t &arr = to_array_type(t);
      return type_byte_size_default(arr.subtype, 8).to_uint64();
    }
 
    return 8;
  }
 
  inline unsigned int offset2align(const expr2tc &e, const BigInt &m) const
  {
    unsigned int nat_align = get_natural_alignment(e);
    if (m == 0)
    {
      return nat_align;
    }
    if ((m % nat_align) == 0)
    {
      return nat_align;
    }
 
    // What's the least alignment available?
    unsigned int max_align = 8;
    do
    {
      // Repeatedly decrease the word size by powers of two, and test to see
      // whether the offset meets that alignment. This will always succeed
      // and exit the loop when the alignment reaches 1.
      if ((m % max_align) == 0)
        return max_align;
      max_align /= 2;
    } while (true);
  }

  expr2tc to_expr(object_mapt::const_iterator it) const;

  void set(object_mapt &dest, object_mapt::const_iterator it) const
  {
    // Fetch/insert iterator
    std::pair<object_mapt::iterator, bool> res =
      dest.insert(object_mapt::value_type(it->first, it->second));
 
    // An entry already present for this object number is left untouched:
    // the assignment below runs only for freshly inserted elements, where
    // it is a no-op.
    if (res.second)
      res.first->second = it->second;
  }
 
  bool insert(object_mapt &dest, object_mapt::const_iterator it) const
  {
    return insert(dest, it->first, it->second);
  }
 
  bool insert(object_mapt &dest, const expr2tc &src, const BigInt &offset) const
  {
    return insert(dest, object_numbering.number(src), objectt(true, offset));
  }

  bool insert(object_mapt &dest, unsigned n, const objectt &object) const
  {
    object_mapt::const_iterator it = dest.find(n);
    if (it == dest.end())
    {
      // new
      dest.insert(object_mapt::value_type(n, object));
      return true;
    }
 
    object_mapt::iterator it2 = dest.find(n);
    objectt &old = it2->second;
    const expr2tc &expr_obj = object_numbering[n];
 
    if (old.offset_is_set && object.offset_is_set)
    {
      if (old.offset == object.offset)
        return false;
 
      // Merge the tracking for two offsets; take the minimum alignment
      // guaranteed by them.
      unsigned long old_align = offset2align(expr_obj, old.offset);
      unsigned long new_align = offset2align(expr_obj, object.offset);
      old.offset_is_set = false;
      old.offset_alignment = std::min(old_align, new_align);
      return true;
    }
 
    if (!old.offset_is_set)
    {
      unsigned int oldalign = old.offset_alignment;
      if (!object.offset_is_set)
      {
        // Both object offsets not set; update alignment to minimum of the two
        old.offset_alignment =
          std::min(old.offset_alignment, object.offset_alignment);
        return !(old.offset_alignment == oldalign);
      }
 
      // Old offset unset; new offset set. Compute the alignment of the
      // new object's offset, and take the minimum of that and the old
      // alignment.
      unsigned int new_alignment = offset2align(expr_obj, object.offset);
      old.offset_alignment = std::min(old.offset_alignment, new_alignment);
      return !(old.offset_alignment == oldalign);
    }
 
    // Old offset alignment is set; new isn't.
    unsigned int old_align = offset2align(expr_obj, old.offset);
    old.offset_alignment = std::min(old_align, object.offset_alignment);
    old.offset_is_set = false;
    return true;
  }
 
  bool
  insert(object_mapt &dest, const expr2tc &expr, const objectt &object) const
  {
    return insert(dest, object_numbering.number(expr), object);
  }

  bool erase(const std::string &name)
  {
    return values.erase(name);
  }

  void erase_object(
    const std::string &id,
    const type2tc &type,
    const std::string &suffix = "");

  void get_value_set(const expr2tc &expr, value_setst::valuest &dest) const;

  void clear()
  {
    values.clear();
  }

  void add_var(const std::string &id, const std::string &suffix)
  {
    touch_entry(entryt(id, suffix));
  }
 
  void add_var(const entryt &e)
  {
    touch_entry(e);
  }

  void del_var(const std::string &id, const std::string &suffix)
  {
    if (suffix.empty())
    {
      values.erase(id);
      return;
    }
    values.erase(concat_key(id, suffix));
  }

  static irep_idt entry_key(const entryt &e)
  {
    if (e.suffix.empty())
      return e.identifier;
    return concat_key(e.identifier, e.suffix);
  }

  void touch_entry(const entryt &e)
  {
    irep_idt key = entry_key(e);
    if (values.find(key) == nullptr)
      values.set(key, e);
  }

  bool update_object_map(const entryt &e, const object_mapt &om, bool merge)
  {
    irep_idt key = entry_key(e);
    const entryt *cur = values.find(key);
    if (cur == nullptr)
    {
      entryt fresh(e.identifier, e.suffix);
      fresh.object_map = om;
      values.set(key, std::move(fresh));
      return true;
    }
    // Rebuild the record from its keys only — the old object_map is either
    // superseded (overwrite) or unioned into a fresh copy (merge), so copying
    // it off `cur` would be wasted.
    entryt upd(cur->identifier, cur->suffix);
    if (merge)
    {
      upd.object_map = cur->object_map;
      if (!make_union(upd.object_map, om))
        return false;
    }
    else
    {
      if (cur->object_map == om)
        return false;
      upd.object_map = om;
    }
    values.set(key, std::move(upd));
    return true;
  }

  static std::string
  concat_key(const std::string &id, const std::string &suffix)
  {
    std::string key;
    key.reserve(id.size() + suffix.size());
    key = id;
    key += suffix;
    return key;
  }

  void add_vars(const std::list<entryt> &vars)
  {
    for (const auto &var : vars)
      add_var(var);
  }

  void output(std::ostream &out) const;

  void dump() const;

  bool make_union(object_mapt &dest, const object_mapt &src) const;

  bool make_union(const valuest &new_values, bool keepnew = false);
 
  bool make_union(const value_sett &new_values, bool keepnew = false)
  {
    return make_union(new_values.values, keepnew);
  }

  void apply_code(const expr2tc &code);

  void assign(const expr2tc &lhs, const expr2tc &rhs, bool add_to_sets = false);
  void assign_struct_union(
    const expr2tc &lhs,
    const expr2tc &rhs,
    const type2tc &lhs_type,
    bool add_to_sets);

  void do_function_call(
    const symbolt &symbol,
    const std::vector<expr2tc> &arguments);

  void do_end_function(const expr2tc &lhs);

  void get_reference_set(const expr2tc &expr, value_setst::valuest &dest) const;

  void get_value_set(const expr2tc &expr, object_mapt &dest) const;

  void retire_objectless_operand(
    object_mapt &op0_set,
    object_mapt &op1_set,
    object_mapt &dest) const;

  void get_value_set_rec_cached(
    const expr2tc &expr,
    object_mapt &dest,
    const std::string &suffix,
    const type2tc &original_type,
    bool under_deref = true) const;
 
private:
  using rec_cache_keyt =
    std::tuple<const expr2t *, std::string, const type2t *, bool>;
  using rec_cachet =
    std::map<rec_cache_keyt, std::tuple<expr2tc, type2tc, object_mapt>>;

  mutable rec_cachet *rec_cache = nullptr;

  void get_value_set_rec(
    const expr2tc &expr,
    object_mapt &dest,
    const std::string &suffix,
    const type2tc &original_type,
    bool under_deref) const;
 
protected:
  std::optional<BigInt> constant_pointer_arith_offset(
    const expr2tc &non_ptr_op,
    const type2tc &subtype,
    bool subtracting) const;

  void offset_pointer_arith_objects(
    const object_mapt &pointer_expr_set,
    const expr2tc &ptr_op,
    const std::optional<BigInt> &total_offs,
    object_mapt &dest) const;

  bool get_symbol_value_set(
    const symbol2t &sym,
    const expr2tc &expr,
    const std::string &suffix,
    const type2tc &original_type,
    object_mapt &dest) const;

  void get_constant_value_set(
    const expr2tc &expr,
    object_mapt &dest,
    const std::string &suffix,
    const type2tc &original_type,
    bool under_deref) const;

  void get_constant_struct_value_set(
    const expr2tc &expr,
    object_mapt &dest,
    const std::string &suffix,
    const type2tc &original_type,
    bool under_deref) const;
 
  void get_constant_union_value_set(
    const expr2tc &expr,
    object_mapt &dest,
    const std::string &suffix,
    const type2tc &original_type) const;
 
  // Like get_value_set_rec, but dedicated to walking through the ireps that
  // are produced by pointer deref byte stitching
  void get_byte_stitching_value_set(
    const expr2tc &expr,
    object_mapt &dest,
    const std::string &suffix,
    const type2tc &original_type) const;

  void get_reference_set(const expr2tc &expr, object_mapt &dest) const
  {
    get_reference_set_rec(expr, dest);
  }

  void get_reference_set_rec(const expr2tc &expr, object_mapt &dest) const;

  void assign_rec(
    const expr2tc &lhs,
    const object_mapt &values_rhs,
    const std::string &suffix,
    bool add_to_sets);

  void do_free(const expr2tc &op);

  expr2tc make_member(const expr2tc &src, const irep_idt &component_name);
 
  static void obj_numbering_ref(unsigned int num);
  static void obj_numbering_deref(unsigned int num);
 
public:
  //********************************** Members
  //***********************************
  unsigned location_number;
  static thread_local object_numberingt object_numbering;
  static thread_local object_number_numberingt obj_numbering_refset;

  valuest values;

  const namespacet &ns;
 
  irep_idt xchg_name;
  unsigned long xchg_num;
};
 
// Exceptions
 
class vsa_not_implemented_exception
{
};
 
#endif