renaming.h

Go to the documentation of this file.

#ifndef _GOTO_SYMEX_RENAMING_H_
#define _GOTO_SYMEX_RENAMING_H_
 
#include <set>
#include <util/persistent_map.h>
#include <goto-symex/symex_invariant.h>
#include <util/expr/expr_util.h>
#include <irep2/irep2_guard.h>
#include <util/base/i2string.h>
#include <irep2/irep2_expr.h>
#include <util/irep/std_expr.h>
 
class namespacet;
 
namespace renaming
{
struct renaming_levelt
{
public:
  virtual void get_original_name(expr2tc &expr) const = 0;
  virtual void rename(expr2tc &expr) = 0;
  virtual void remove(const expr2tc &symbol) = 0;
 
  virtual void get_ident_name(expr2tc &symbol) const = 0;
 
  virtual ~renaming_levelt() = default;
  //  protected:
  //  XXX: should leave protected enabled, but g++ 5.4 on ubuntu 16.04 does not
  //  appear to honor the following friend directive?
  static void get_original_name(expr2tc &expr, symbol2t::renaming_level lev);
  friend void build_goto_symex_classes();
};
 
// level 1 -- function frames
// this is to preserve locality in case of recursion
 
struct level1t : public renaming_levelt
{
public:
  struct name_rec_hash;
  class name_record
  {
  public:
    name_record() : base_name("")
    {
    }
 
    name_record(const symbol2t &sym) : base_name(sym.thename)
    {
    }
 
    name_record(const irep_idt &name) : base_name(name)
    {
    }
 
    int compare(const name_record &ref) const
    {
      if (base_name.get_no() < ref.base_name.get_no())
        return -1;
      if (base_name.get_no() > ref.base_name.get_no())
        return 1;
 
      return 0;
    }
 
    bool operator<(const name_record &ref) const
    {
      if (compare(ref) == -1)
        return true;
      return false;
    }
 
    bool operator==(const name_record &ref) const
    {
      if (compare(ref) == 0)
        return true;
      return false;
    }
 
    irep_idt base_name;
 
    friend struct renaming::level1t::name_rec_hash;
  };
 
  struct name_rec_hash
  {
    size_t operator()(const name_record &ref) const
    {
      return ref.base_name.get_no();
    }
 
    bool operator()(const name_record &ref, const name_record &ref2) const
    {
      return ref < ref2;
    }
  };
 
  typedef persistent_map<name_record, unsigned, name_rec_hash> current_namest;
  current_namest current_names;
  unsigned int thread_id;
  // Set externally (alongside thread_id) so rename() / get_ident_name()
  // can check is_thread_local on globals and route them per-thread
  // instead of to the shared level1_global bucket (issue #4434, #4433).
  const namespacet *ns = nullptr;
 
  void rename(expr2tc &expr) override;
  void get_ident_name(expr2tc &symbol) const override;
  void remove(const expr2tc &symbol) override
  {
    current_names.erase(name_record(to_symbol2t(symbol)));
  }
 
  void rename(const expr2tc &symbol, unsigned frame)
  {
    // Given that this is level1, use base symbol.
    name_record rec(to_symbol2t(symbol));
    const unsigned *cur = current_names.find(rec);
    // I1 at L1: an activation index only ever grows.
    SYMEX_INVARIANT(
      !cur || *cur <= frame, "L1 activation counter moved backwards");
    current_names.set(rec, frame);
  }
 
  void get_original_name(expr2tc &expr) const override
  {
    renaming_levelt::get_original_name(expr, symbol_renaming_level::level0);
  }
 
  unsigned int current_number(const irep_idt &name) const;
 
  level1t() = default;
  ~level1t() override = default;
 
  virtual void print(std::ostream &out) const;
};
 
// level 2 -- SSA
 
struct level2t : public renaming_levelt
{
protected:
  virtual void
  coveredinbees(expr2tc &lhs_sym, unsigned count, unsigned node_id);
 
public:
  class name_record
  {
  public:
    name_record()
    {
      compute_hash();
    }
 
    name_record(const symbol2t &sym)
      : base_name(sym.thename),
        lev(sym.rlevel),
        l1_num(sym.level1_num),
        t_num(sym.thread_num)
    {
      compute_hash();
    }
 
    int compare(const name_record &ref) const
    {
      if (hash < ref.hash)
        return -1;
      if (hash > ref.hash)
        return 1;
 
      if (base_name < ref.base_name)
        return -1;
      if (ref.base_name < base_name)
        return 1;
 
      if (lev < ref.lev)
        return -1;
      if (lev > ref.lev)
        return 1;
 
      if (l1_num < ref.l1_num)
        return -1;
      if (l1_num > ref.l1_num)
        return 1;
 
      if (t_num < ref.t_num)
        return -1;
      if (t_num > ref.t_num)
        return 1;
 
      return 0;
    }
 
    bool operator<(const name_record &ref) const
    {
      if (compare(ref) == -1)
        return true;
      return false;
    }
 
    bool operator==(const name_record &ref) const
    {
      if (compare(ref) == 0)
        return true;
      return false;
    }
 
    irep_idt base_name;
    symbol2t::renaming_level lev = symbol2t::renaming_level::level0;
    unsigned int l1_num = 0;
    unsigned int t_num = 0;
 
    // Derived from the fields above; used as the fast-path primary key in
    // compare() and by name_rec_hash. compare() short-circuits on it, so it
    // must stay a pure function of them — compute_hash() is the only writer.
    size_t hash = 0;
 
  private:
    void compute_hash()
    {
      size_t seed = 0;
      esbmct::hash_combine(seed, base_name.get_no());
      esbmct::hash_combine(seed, (uint8_t)lev);
      esbmct::hash_combine(seed, l1_num);
      esbmct::hash_combine(seed, t_num);
      hash = seed;
    }
  };
 
  struct name_rec_hash
  {
    size_t operator()(const name_record &ref) const
    {
      return ref.hash;
    }
 
    bool operator()(const name_record &ref, const name_record &ref2) const
    {
      return ref < ref2;
    }
  };
 
public:
  struct valuet
  {
    unsigned count;
    expr2tc constant;
    unsigned node_id;
    valuet() : count(0), node_id(0)
    {
    }
    // Value equality so the persistent map can be structurally diffed
    // (phi_function). Only invoked on the divergent leaves.
    bool operator==(const valuet &v) const
    {
      return count == v.count && node_id == v.node_id && constant == v.constant;
    }
    bool operator!=(const valuet &v) const
    {
      return !(*this == v);
    }
  };
 
  virtual void make_assignment(
    expr2tc &lhs_symbol,
    const expr2tc &constant_value,
    const expr2tc &assigned_value);
 
  void rename(expr2tc &expr) override;
  virtual void rename(expr2tc &expr, unsigned count) = 0;
 
  void get_ident_name(expr2tc &symbol) const override;
 
  void remove(const expr2tc &symbol) override
  {
    current_names.erase(name_record(to_symbol2t(symbol)));
  }

  valuet current_value(const name_record &rec) const
  {
    const valuet *p = current_names.find(rec);
    return p ? *p : valuet();
  }

  void retire(const name_record &rec)
  {
    current_names.update(rec, [](valuet entry) {
      ++entry.count;
      entry.constant = expr2tc();
      return entry;
    });
  }

  void declare(const name_record &rec)
  {
    if (current_names.find(rec) == nullptr)
      current_names.set(rec, valuet());
  }
 
  void get_original_name(expr2tc &expr) const override
  {
    renaming_levelt::get_original_name(expr, symbol_renaming_level::level1);
  }

  void set_constant(const name_record &rec, const expr2tc &value)
  {
    const valuet *entry = current_names.find(rec);
    SYMEX_INVARIANT(
      entry != nullptr && is_nil_expr(entry->constant),
      "a propagated value may only complete the assignment that minted it");
    // `entry` dangles once the map is written; do not read it below.
    current_names.update(rec, [&value](valuet v) {
      v.constant = value;
      return v;
    });
  }
 
  unsigned current_number(const expr2tc &sym) const;
  unsigned current_number(const name_record &rec) const;
 
  // static method to rename a (l0) variable to the l1 number record specified
  // in the given name_record. The use case for this is phi_function, where
  // we have a handle on name_record's identifying the storage variable that
  // we want to assign to, but lack the ability to address it as a symbol.
  // In that case (or any similar) we need a facility independent of a
  // specific level2t object.
  static void rename_to_record(expr2tc &sym, const name_record &rec);
 
  level2t() = default;
  ~level2t() override = default;
  virtual std::shared_ptr<level2t> clone() const = 0;
 
  virtual void print(std::ostream &out) const;
  virtual void dump() const;
 
  friend void build_goto_symex_classes();
  // Repeat of the above ignored friend directive.
  //
  // Persistent (structurally shared) like level1's map. clone() snapshots
  // this map at every branch for the later merge; a std::unordered_map would
  // deep-copy there, O(tracked names) per branch and so symex quadratic on
  // branch-heavy inputs. The immer HAMT makes the snapshot O(1) and lets
  // phi_function diff two states in O(divergence).
  typedef persistent_map<name_record, valuet, name_rec_hash> current_namest;
 
  current_namest current_names;
};
 
} // namespace renaming
 
#endif /* _GOTO_SYMEX_RENAMING_H_ */