Method store

ir/memory.cpp:1227–1292

}

void Memory::store(const Pointer &ptr,
                   const vector<pair<unsigned, expr>> &data,
                   const set<expr> &undef, uint64_t align) {
  if (data.empty())
    return;

  for (auto &[offset, val] : data) {
    Byte byte(*this, expr(val));
    escapeLocalPtr(byte.ptrValue(), byte.isPtr() && byte.ptrNonpoison());
  }

  unsigned bytes = data.size() * (bits_byte/8);

  auto stored_ty = data_type(data, false);
  auto stored_ty_full = data_type(data, true);

  auto fn = [&](MemBlock &blk, const Pointer &ptr, unsigned bid, bool local,
                expr &&cond) {
    auto mem = blk.val;

    uint64_t blk_size;
    bool full_write
      = ptr.blockSizeAligned().isUInt(blk_size) && blk_size == bytes;

    // optimization: if fully rewriting the block, don't bother with the old
    // contents. Pick a value as the default one.
    // If we are initializing const globals, the size may be larger than the
    // init because the size is rounded up to the alignment.
    // The remaining bytes are poison.
    if (full_write || state->isInitializationPhase()) {
      // optimization: if the access size == byte size, then we don't store
      // data as arrays, but simply as a BV
      if (data.size() == 1) {
        mem = data[0].second;
      } else {
        mem = full_write ? data[0].second : Byte::mkPoisonByte(*this)();
      }
      if (cond.isTrue()) {
        blk.undef.clear();
        blk.type = stored_ty_full;
      } else {
        blk.type |= stored_ty_full;
      }
    } else {
      blk.type |= stored_ty;
    }

    expr offset = ptr.getShortOffset();

    for (auto &[idx, val] : data) {
      expr off
        = offset + expr::mkUInt(idx >> Pointer::zeroBitsShortOffset(), offset);
      if (!local)
        record_stored_pointer(bid, off);

      if (full_write && val.eq(data[0].second))
        continue;
      mem = mk_store(std::move(mem), off, val);