Class Pointer

ir/pointer.h:17–175

class Memory;

class Pointer {
  Memory &m;

  // [0, padding, bid, offset, attributes (1 bit for each)] -- logical pointer
  // [1, padding, address, attributes] -- physical pointer
  // The top bit of bid is 1 if the block is local, 0 otherwise.
  // A local memory block is a memory block that is
  // allocated by an instruction during the current function call. This does
  // not include allocated blocks from a nested function call. A heap-allocated
  // block can also be a local memory block.
  // Otherwise, a pointer is pointing to a non-local block, which can be either
  // of global variable, heap, or a stackframe that is not this function call.
  // The lowest bits represent whether the pointer value came from a nocapture/
  // readonly argument. If block is local, is-readonly or is-nocapture cannot
  // be 1.
  // TODO: missing support for address space
  smt::expr p;

  smt::expr getValue(const char *name, const smt::FunctionExpr &local_fn,
                      const smt::FunctionExpr &nonlocal_fn,
                      const smt::expr &ret_type, bool src_name = false) const;

public:
  Pointer(const Memory &m, const smt::expr &bid, const smt::expr &offset,
          const smt::expr &attr);
  Pointer(const Memory &m, const char *var_name, const ParamAttrs &attr);
  Pointer(const Memory &m, smt::expr p);
  Pointer(const Memory &m, unsigned bid, bool local, smt::expr attr = {});
  Pointer(const Memory &m, const smt::expr &bid, const smt::expr &offset,
          const ParamAttrs &attr = {});

  static Pointer mkPhysical(const Memory &m, const smt::expr &addr);
  static Pointer mkPhysical(const Memory &m, const smt::expr &addr,
                            const smt::expr &attr);

  Pointer(const Pointer &other) noexcept = default;
  Pointer(Pointer &&other) noexcept = default;
  void operator=(Pointer &&rhs) noexcept { p = std::move(rhs.p); }

  // returns (log-ptr, domain of inboundness)
  std::pair<Pointer, smt::expr>
    findLogicalLocalPointer(const smt::expr &addr) const;
  std::pair<Pointer, smt::expr> toLogicalLocal() const;

  static smt::expr mkLongBid(const smt::expr &short_bid, bool local);
  static smt::expr mkUndef(State &s);

  static unsigned totalBits();
  static unsigned bitsShortBid();
  static unsigned bitsShortOffset();
  static unsigned zeroBitsShortOffset();
  static bool hasLocalBit();

  smt::expr isLogical() const;

  smt::expr isLocal(bool simplify = true) const;
  smt::expr isConstGlobal() const;
  smt::expr isWritableGlobal() const;