| 2584 | } |
| 2585 | |
| 2586 | expr Memory::blockValRefined(const Pointer &src, const Memory &tgt, |
| 2587 | unsigned bid, set<expr> &undef, |
| 2588 | bool full_check) const { |
| 2589 | auto &mem1 = non_local_block_val[bid]; |
| 2590 | auto &mem2 = tgt.non_local_block_val[bid].val; |
| 2591 | |
| 2592 | if (mem1.val.eq(mem2)) |
| 2593 | return true; |
| 2594 | |
| 2595 | // must have had called the exact same function before |
| 2596 | if (is_fncall_mem(bid)) |
| 2597 | return mem1.val == mem2; |
| 2598 | |
| 2599 | auto refined = [&](const expr &offset) -> expr { |
| 2600 | int is_fn1 = isInitialMemBlock(mem1.val, true); |
| 2601 | int is_fn2 = isInitialMemBlock(mem2, true); |
| 2602 | if (is_fn1 && is_fn2) { |
| 2603 | // if both memories are the result of a function call, then refinement |
| 2604 | // holds iff they are equal, otherwise we can always force a behavior |
| 2605 | // of the function such that it will store a different value to memory |
| 2606 | if (is_fn1 == 2 && is_fn2 == 2) |
| 2607 | return mem1.val == mem2; |
| 2608 | |
| 2609 | // an initial memory (m0) vs a function call is always false, as a function |
| 2610 | // may always store something to memory |
| 2611 | assert((is_fn1 == 1 && is_fn2 == 2) || (is_fn1 == 2 && is_fn2 == 1)); |
| 2612 | return false; |
| 2613 | } |
| 2614 | |
| 2615 | Byte val = raw_load(false, bid, offset); |
| 2616 | Byte val2 = tgt.raw_load(false, bid, offset); |
| 2617 | |
| 2618 | if (val.eq(val2)) |
| 2619 | return true; |
| 2620 | |
| 2621 | undef.insert(mem1.undef.begin(), mem1.undef.end()); |
| 2622 | |
| 2623 | expr r = val.refined(val2); |
| 2624 | |
| 2625 | // The ABI requires that sub-byte stores zero extend the stored value |
| 2626 | if (num_sub_byte_bits && tgt.isAsmMode()) |
| 2627 | r &= mkSubByteZExtStoreCond(val, val2); |
| 2628 | |
| 2629 | return r; |
| 2630 | }; |
| 2631 | |
| 2632 | unsigned bytes_per_byte = bits_byte / 8; |
| 2633 | expr ptr_offset = src.getShortOffset(); |
| 2634 | uint64_t bytes; |
| 2635 | if (full_check && |
| 2636 | src.blockSize().isUInt(bytes) && (bytes / bytes_per_byte) <= 8) { |
| 2637 | expr val_refines = true; |
| 2638 | for (unsigned off = 0; off < (bytes / bytes_per_byte); ++off) { |
| 2639 | expr off_expr = expr::mkUInt(off, ptr_offset); |
| 2640 | val_refines &= (ptr_offset == off_expr).implies(refined(off_expr)); |
| 2641 | } |
| 2642 | return val_refines; |
| 2643 | } else { |
nothing calls this directly
no test coverage detected