| 2499 | } |
| 2500 | |
| 2501 | void Memory::copy(const Pointer &src, const Pointer &dst) { |
| 2502 | auto local = dst.isLocal(); |
| 2503 | if (!local.isValid()) { |
| 2504 | local_block_val.clear(); |
| 2505 | non_local_block_val.clear(); |
| 2506 | local_block_val.resize(numLocals()); |
| 2507 | non_local_block_val.resize(numNonlocals()); |
| 2508 | return; |
| 2509 | } |
| 2510 | |
| 2511 | assert(local.isConst()); |
| 2512 | bool dst_local = local.isTrue(); |
| 2513 | uint64_t dst_bid; |
| 2514 | expr dst_bid_expr = dst.getShortBid(); |
| 2515 | ENSURE(dst_bid_expr.isUInt(dst_bid)); |
| 2516 | auto &dst_blk = (dst_local ? local_block_val : non_local_block_val)[dst_bid]; |
| 2517 | dst_blk.undef.clear(); |
| 2518 | dst_blk.type = DATA_NONE; |
| 2519 | |
| 2520 | unsigned has_bv_val = 0; |
| 2521 | auto offset = expr::mkUInt(0, Pointer::bitsShortOffset()); |
| 2522 | DisjointExpr val(Byte::mkPoisonByte(*this)()); |
| 2523 | |
| 2524 | if (!dst_local) |
| 2525 | record_stored_pointer(dst_bid, offset); |
| 2526 | |
| 2527 | auto fn = [&](MemBlock &blk, const Pointer &ptr, unsigned src_bid, |
| 2528 | bool src_local, expr &&cond) { |
| 2529 | // we assume src != dst |
| 2530 | if (src_local == dst_local && src_bid == dst_bid) |
| 2531 | return; |
| 2532 | val.add(blk.val, std::move(cond)); |
| 2533 | dst_blk.undef.insert(blk.undef.begin(), blk.undef.end()); |
| 2534 | dst_blk.type |= blk.type; |
| 2535 | has_bv_val |= 1u << blk.val.isBV(); |
| 2536 | }; |
| 2537 | access(src, expr::mkUInt(bits_byte/8, bits_size_t), bits_byte/8, false, fn); |
| 2538 | |
| 2539 | // if we have mixed array/non-array blocks, switch them all to array |
| 2540 | if (has_bv_val == 3) { |
| 2541 | DisjointExpr<expr> newval; |
| 2542 | for (auto &[v, cond] : val) { |
| 2543 | newval.add(v.isBV() ? expr::mkConstArray(offset, v) : v, cond); |
| 2544 | } |
| 2545 | val = std::move(newval); |
| 2546 | } |
| 2547 | dst_blk.val = *std::move(val)(); |
| 2548 | } |
| 2549 | |
| 2550 | void Memory::fillPoison(const expr &bid) { |
| 2551 | Pointer p(*this, bid, expr::mkUInt(0, bits_for_offset)); |