Method mkLocalDisjAddrAxioms

ir/memory.cpp:2095–2136

}

void Memory::mkLocalDisjAddrAxioms(const expr &allocated, const expr &short_bid,
                                   const expr &size, const expr &align,
                                   unsigned align_bits) {
  if (!observesAddresses())
    return;

  unsigned var_bw = bits_ptr_address - align_bits - Pointer::hasLocalBit();
  auto addr_var = expr::mkFreshVar("local_addr", expr::mkUInt(0, var_bw));
  state->addQuantVar(addr_var);

  if (!Pointer::hasLocalBit())
    state->addPre(addr_var != 0);

  expr blk_addr = addr_var.concat_zeros(align_bits);
  expr full_addr = Pointer::hasLocalBit()
                     ? expr::mkUInt(1, 1).concat(blk_addr) : blk_addr;

  if (align_bits == 0) {
    auto shift = expr::mkUInt(bits_ptr_address, full_addr) -
                   align.zextOrTrunc(bits_ptr_address);
    state->addPre((full_addr << shift) == 0);
  }

  // addr + size only overflows for one case when obj is aligned
  expr no_ovfl;
  if (size.ule(align.zextOrTrunc(bits_size_t)).isTrue())
    no_ovfl = addr_var != expr::mkInt(-1, addr_var);
  else
    no_ovfl
      = blk_addr.add_no_uoverflow(
          size.zextOrTrunc(bits_ptr_address - Pointer::hasLocalBit()));
  state->addPre(allocated.implies(no_ovfl));

  // Disjointness of block's address range with other local blocks
  state->addPre(
    allocated.implies(
      disjoint_local_blocks(*this, full_addr,
                            size.zextOrTrunc(bits_ptr_address),
                            align, local_blk_addr)));

  local_blk_addr.add(short_bid, std::move(blk_addr));
}

pair<expr, expr>
Memory::alloc(const expr *size, uint64_t align, BlockKind blockKind,