diff --git a/ir/memory.cpp b/ir/memory.cpp index c924b8481..4502f7b5c 100644 --- a/ir/memory.cpp +++ b/ir/memory.cpp @@ -1230,7 +1230,13 @@ void Memory::mkNonPoisonAxioms(bool local) { } } -static expr mk_sub_byte_zext_store_cond(const Byte &val, const Byte &val2) { +expr Memory::mkSubByteZExtStoreCond(const Byte &val, const Byte &val2) const { + bool mk_axiom = &val == &val2; + + // optimization: the initial block is assumed to follow the ABI already. + if (!mk_axiom && isInitialMemBlock(val.p, true)) + return true; + bool always_1_byte = bits_byte >= (1u << num_sub_byte_bits); auto stored_bits = val.numStoredBits(); auto num_bytes @@ -1243,6 +1249,7 @@ static expr mk_sub_byte_zext_store_cond(const Byte &val, const Byte &val2) { ).zextOrTrunc(bits_byte); return val.isPtr() || + (mk_axiom ? expr(false) : !val.boolNonptrNonpoison()) || stored_bits == 0 || val.byteNumber() != num_bytes || val2.nonptrValue().lshr(leftover_bits) == 0; @@ -1271,7 +1278,7 @@ void Memory::mkNonlocalValAxioms(bool skip_consts) { // per the ABI. if (num_sub_byte_bits && isAsmMode()) { state->addAxiom( - expr::mkForAll({ offset }, mk_sub_byte_zext_store_cond(byte, byte))); + expr::mkForAll({ offset }, mkSubByteZExtStoreCond(byte, byte))); } if (!does_ptr_mem_access) @@ -2385,7 +2392,7 @@ expr Memory::blockValRefined(const Memory &other, unsigned bid, bool local, // The ABI requires that sub-byte stores zero extend the stored value if (num_sub_byte_bits && other.isAsmMode()) - r &= mk_sub_byte_zext_store_cond(val, val2); + r &= mkSubByteZExtStoreCond(val, val2); return r; } diff --git a/ir/memory.h b/ir/memory.h index b2d2b154c..ce1a1f0c7 100644 --- a/ir/memory.h +++ b/ir/memory.h @@ -95,6 +95,7 @@ class Byte { static unsigned bitsByte(); friend std::ostream& operator<<(std::ostream &os, const Byte &byte); + friend class Memory; }; @@ -181,6 +182,7 @@ class Memory { smt::expr isBlockAlive(const smt::expr &bid, bool local) const; void mkNonPoisonAxioms(bool local); + smt::expr mkSubByteZExtStoreCond(const Byte &val, const Byte &val2) const; void mkNonlocalValAxioms(bool skip_consts); bool mayalias(bool local, unsigned bid, const smt::expr &offset, diff --git a/tests/alive-tv/asm/delete-store.srctgt.ll b/tests/alive-tv/asm/delete-store.srctgt.ll new file mode 100644 index 000000000..b4318d730 --- /dev/null +++ b/tests/alive-tv/asm/delete-store.srctgt.ll @@ -0,0 +1,12 @@ +; TEST-ARGS: -tgt-is-asm +; SKIP-IDENTITY + +define void @src(ptr %0) { + %2 = load i1, ptr %0, align 1 + store i1 %2, ptr %0, align 1 + ret void +} + +define void @tgt(ptr %0) { + ret void +}