Method refined

ir/pointer.cpp:798–831

}

expr Pointer::refined(const Pointer &other) const {
  bool is_asm = other.m.isAsmMode();
  auto [p1l, d1] = toLogicalLocal();
  auto [p2l, d2] = other.toLogicalLocal();

  // This refers to a block that was malloc'ed within the function
  expr local = d2 && p2l.isLocal();
  local &= p1l.getAllocType() == p2l.getAllocType();
  if (is_asm) {
    local &= at_least_same_offseting(p1l, p2l, true);
  } else {
    local &= p1l.blockSize() == p2l.blockSize();
    local &= p1l.getOffset() == p2l.getOffset();
  }
  local &= p1l.isBlockAlive().implies(p2l.isBlockAlive());
  // Attributes are ignored at refinement.

  if (!is_asm)
    local &= isLogical() == other.isLogical();

  // TODO: this induces an infinite loop
  //local &= block_refined(other);

  expr nonlocal = is_asm ? getAddress() == other.getAddress() : *this == other;
  expr is_local = d1 && p1l.isLocal();

  // short-circuit to avoid the constraint below:
  // addr == 0 ? addr' == 0 : addr == addr'
  if (is_asm && is_local.isFalse())
    return nonlocal;

  return expr::mkIf(isNull(), other.isNull(),
                    expr::mkIf(is_local, local, nonlocal));
}

expr Pointer::fninputRefined(const Pointer &other, set<expr> &undef,
                             const expr &byval_bytes) const {