Method record_store

ir/memory.cpp:1375–1410

}

void Memory::record_store(const Pointer &p, const smt::expr &bytes) {
  assert(has_initializes_attr);

  auto is_local = p.isLocal();
  if (is_local.isTrue())
    return;

  unsigned bytes_per_byte = bits_byte / 8;
  expr bid = p.getShortBid();
  expr offset = p.getShortOffset();
  uint64_t bytes_i;
  if (bytes.isUInt(bytes_i) && (bytes_i / bytes_per_byte) <= 8) {
    for (uint64_t off = 0; off < (bytes_i / bytes_per_byte); ++off) {
      expr off_expr = expr::mkUInt(off, offset);
      has_stored_arg
        = expr::mkIf(is_local,
                     has_stored_arg,
                     has_stored_arg.store(bid.concat(offset + off_expr), true));
    }
  } else {
    expr var     = expr::mkQVar(0, bid.concat(offset));
    expr var_bid = var.extract(var.bits()-1, offset.bits());
    expr var_off = var.trunc(offset.bits());

    expr bytes_div = bytes.zextOrTrunc(offset.bits())
                          .udiv(expr::mkUInt(bytes_per_byte, bytes));
    has_stored_arg
      = expr::mkIf(is_local,
                   has_stored_arg,
                   expr::mkLambda(var, "#bid_off",
                     (bid == var_bid &&
                      var_off.uge(offset) &&
                      var_off.ult(offset + bytes_div)) ||
                     has_stored_arg.load(var)));
  }
}

static bool memory_unused() {
  return num_locals_src == 0 && num_locals_tgt == 0 && num_nonlocals == 0;