From 0dadb5b54978a8c6bdb9ebd370133a75db05aa7f Mon Sep 17 00:00:00 2001 From: Yohello1 Date: Thu, 5 Mar 2026 02:55:02 -0500 Subject: [PATCH 1/6] Patched #1242 --- ir/memory.cpp | 10 ++++++++-- ir/pointer.cpp | 2 +- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/ir/memory.cpp b/ir/memory.cpp index 879731074..c030dbfeb 100644 --- a/ir/memory.cpp +++ b/ir/memory.cpp @@ -1207,7 +1207,10 @@ static expr mk_store(expr mem, const expr &offset, const expr &val) { TypedByte Memory::raw_load(bool local, unsigned bid, const expr &offset) const { auto &block = (local ? local_block_val : non_local_block_val)[bid]; - return { Byte(*this, ::raw_load(block.val, offset)), DataType(block.type) }; + expr alive = isBlockAlive(expr::mkUInt(bid, Pointer::bitsShortBid()), local); + return { Byte(*this, mkIf_fold(alive, ::raw_load(block.val, offset), + Byte::mkPoisonByte(*this)())), + DataType(block.type) }; } vector @@ -1234,7 +1237,10 @@ Memory::load(const Pointer &ptr, unsigned bytes, set &undef, assert(idx < blk_size); uint64_t max_idx = blk_size - bytes + idx; expr off = blk_offset + expr::mkUInt(idx, offset); - loaded[i].first.add(::raw_load(blk.val, off, max_idx), cond); + expr is_alive = isBlockAlive(bid, local); + loaded[i].first.add(mkIf_fold(is_alive, ::raw_load(blk.val, off, max_idx), + poison), + cond); loaded[i].second |= blk.type; } undef.insert(blk.undef.begin(), blk.undef.end()); diff --git a/ir/pointer.cpp b/ir/pointer.cpp index 51bd9512f..41ad6a7c2 100644 --- a/ir/pointer.cpp +++ b/ir/pointer.cpp @@ -539,7 +539,7 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align, expr bytes = bytes0.zextOrTrunc(bits_for_offset); auto block_constraints = [&](const Pointer &p) { - expr ret = p.isBlockAlive(); + expr ret = (iswrite || is_asm) ? p.isBlockAlive() : true; if (iswrite) ret &= p.isWritable() && !p.isNoWrite(); else if (!ignore_accessability) From 2d33163389a6bf18c302cc0e150800e9cf768a50 Mon Sep 17 00:00:00 2001 From: Yohello1 Date: Thu, 5 Mar 2026 03:06:23 -0500 Subject: [PATCH 2/6] Added tests for lifetime-load-poision --- tests/alive-tv/lifetime-load-poison.srctgt.ll | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 tests/alive-tv/lifetime-load-poison.srctgt.ll diff --git a/tests/alive-tv/lifetime-load-poison.srctgt.ll b/tests/alive-tv/lifetime-load-poison.srctgt.ll new file mode 100644 index 000000000..82d1dd891 --- /dev/null +++ b/tests/alive-tv/lifetime-load-poison.srctgt.ll @@ -0,0 +1,17 @@ +; TEST-ARGS: -disable-poison-input-allowance +; EXPECT: ERROR: Source is more defined than target + +; Should return posioned value based on LangRef Change https://github.com/llvm/llvm-project/pull/157852 +; Pulled this code from nunoplopes https://github.com/AliveToolkit/alive2/issues/1242 + +define i8 @src() { + %p = alloca i8 + call void @llvm.lifetime.start.p0(ptr %p) + call void @llvm.lifetime.end.p0(ptr %p) + %v = load i8, ptr %p + ret i8 %v +} + +define i8 @tgt() { + unreachable +} From 27be9f11beeb7d0aff0a05131119d2514c3c77e1 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 17 Mar 2026 21:10:04 +0000 Subject: [PATCH 3/6] Update lifetime-load-poison.srctgt.ll --- tests/alive-tv/lifetime-load-poison.srctgt.ll | 4 ---- 1 file changed, 4 deletions(-) diff --git a/tests/alive-tv/lifetime-load-poison.srctgt.ll b/tests/alive-tv/lifetime-load-poison.srctgt.ll index 82d1dd891..6dde17d76 100644 --- a/tests/alive-tv/lifetime-load-poison.srctgt.ll +++ b/tests/alive-tv/lifetime-load-poison.srctgt.ll @@ -1,9 +1,5 @@ -; TEST-ARGS: -disable-poison-input-allowance ; EXPECT: ERROR: Source is more defined than target -; Should return posioned value based on LangRef Change https://github.com/llvm/llvm-project/pull/157852 -; Pulled this code from nunoplopes https://github.com/AliveToolkit/alive2/issues/1242 - define i8 @src() { %p = alloca i8 call void @llvm.lifetime.start.p0(ptr %p) From eee1999c982bedaa25b35f09484617c74cd9c2ca Mon Sep 17 00:00:00 2001 From: Yohello1 Date: Sat, 4 Apr 2026 20:24:08 -0400 Subject: [PATCH 4/6] Updated README to include ninja check command --- README.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index b4840670a..2eca7645b 100644 --- a/README.md +++ b/README.md @@ -76,7 +76,7 @@ Building and Running Translation Validation -------- Alive2's `opt` and `clang` translation validation requires a build of LLVM with -RTTI and exceptions turned on. The latest version of Alive2 is always intended +RTTI and exceptions turned on. The latest version Of Alive2 is always intended to be built against the latest version of LLVM, using the main branch from the LLVM repo on Github. LLVM can be built in the following way. @@ -107,6 +107,12 @@ cmake -GNinja -DCMAKE_PREFIX_PATH=~/llvm/build -DBUILD_TV=1 -DCMAKE_BUILD_TYPE=R ninja ``` +Then to validate, and run all tests you can run: +``` +ninja check +``` + + Translation validation of one or more LLVM passes transforming an IR file: ``` ~/alive/build/alive-tv -passes=instcombine foo.ll From 030b7e4376794f8d77b97dae60bb239d3ebf0284 Mon Sep 17 00:00:00 2001 From: Yohello1 Date: Sat, 25 Apr 2026 23:38:34 -0400 Subject: [PATCH 5/6] Fixed tests --- tests/alive-tv/bugs/pr23599.srctgt.ll | 2 ++ tests/alive-tv/calls/escape2.srctgt.ll | 7 +++++++ tests/alive-tv/calls/ptr-store.srctgt.ll | 5 +++++ tests/alive-tv/lifetime-load-poison.srctgt.ll | 2 +- 4 files changed, 15 insertions(+), 1 deletion(-) diff --git a/tests/alive-tv/bugs/pr23599.srctgt.ll b/tests/alive-tv/bugs/pr23599.srctgt.ll index 1aadf796e..1d1390de7 100644 --- a/tests/alive-tv/bugs/pr23599.srctgt.ll +++ b/tests/alive-tv/bugs/pr23599.srctgt.ll @@ -46,3 +46,5 @@ declare void @llvm.memset.p0i8.i64(ptr captures(none), i8, i64, i32, i1) declare void @llvm.memcpy.p0i8.p0i8.i64(ptr captures(none), ptr captures(none) readonly, i64, i32, i1) declare void @_Z5PrintRK12ether_header(ptr dereferenceable(12)) declare void @llvm.lifetime.end(i64, ptr captures(none)) + +; ERROR: Mismatch in memory diff --git a/tests/alive-tv/calls/escape2.srctgt.ll b/tests/alive-tv/calls/escape2.srctgt.ll index 8939cceb9..670326e16 100644 --- a/tests/alive-tv/calls/escape2.srctgt.ll +++ b/tests/alive-tv/calls/escape2.srctgt.ll @@ -1,8 +1,12 @@ @glb = global ptr null declare ptr @f(ptr %p) +declare void @llvm.lifetime.start(i64, ptr captures(none)) +declare void @llvm.lifetime.end(i64, ptr captures(none)) + define i8 @src() { %p = alloca i8 + call void @llvm.lifetime.start(i64 1, ptr %p) store i8 1, ptr %p %q = load ptr, ptr @glb @@ -10,16 +14,19 @@ define i8 @src() { store i8 2, ptr %q2 %v = load i8, ptr %p + call void @llvm.lifetime.end(i64 1, ptr %p) ret i8 %v } define i8 @tgt() { %p = alloca i8 + call void @llvm.lifetime.start(i64 1, ptr %p) store i8 1, ptr %p %q = load ptr, ptr @glb %q2 = call ptr @f(ptr %q) ; cannot be %p store i8 2, ptr %q2 + call void @llvm.lifetime.end(i64 1, ptr %p) ret i8 1 } diff --git a/tests/alive-tv/calls/ptr-store.srctgt.ll b/tests/alive-tv/calls/ptr-store.srctgt.ll index cc525ce4f..77805cdc9 100644 --- a/tests/alive-tv/calls/ptr-store.srctgt.ll +++ b/tests/alive-tv/calls/ptr-store.srctgt.ll @@ -1,14 +1,17 @@ define void @src(ptr %0, i1 %1) { %3 = alloca i64, align 8 + call void @llvm.lifetime.start(i64 8, ptr %3) store ptr null, ptr %0, align 8 call void @fn() br i1 %1, label %4, label %5 4: + call void @llvm.lifetime.end(i64 8, ptr %3) ret void 5: store i64 0, ptr %3, align 8 + call void @llvm.lifetime.end(i64 8, ptr %3) ret void } @@ -19,3 +22,5 @@ define void @tgt(ptr %0, i1 %1) { } declare void @fn() +declare void @llvm.lifetime.start(i64, ptr captures(none)) +declare void @llvm.lifetime.end(i64, ptr captures(none)) diff --git a/tests/alive-tv/lifetime-load-poison.srctgt.ll b/tests/alive-tv/lifetime-load-poison.srctgt.ll index 6dde17d76..c238352ef 100644 --- a/tests/alive-tv/lifetime-load-poison.srctgt.ll +++ b/tests/alive-tv/lifetime-load-poison.srctgt.ll @@ -1,4 +1,4 @@ -; EXPECT: ERROR: Source is more defined than target +; ERROR: Source is more defined than target define i8 @src() { %p = alloca i8 From 2069c9bc59890403e07689017f6e74ce0ba5263c Mon Sep 17 00:00:00 2001 From: Yohello1 Date: Sat, 25 Apr 2026 23:41:01 -0400 Subject: [PATCH 6/6] Fixed changes in ir files --- ir/memory.cpp | 2 +- ir/pointer.cpp | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/ir/memory.cpp b/ir/memory.cpp index c030dbfeb..f4f69cca3 100644 --- a/ir/memory.cpp +++ b/ir/memory.cpp @@ -1237,7 +1237,7 @@ Memory::load(const Pointer &ptr, unsigned bytes, set &undef, assert(idx < blk_size); uint64_t max_idx = blk_size - bytes + idx; expr off = blk_offset + expr::mkUInt(idx, offset); - expr is_alive = isBlockAlive(bid, local); + expr is_alive = isBlockAlive(expr::mkUInt(bid, Pointer::bitsShortBid()), local); loaded[i].first.add(mkIf_fold(is_alive, ::raw_load(blk.val, off, max_idx), poison), cond); diff --git a/ir/pointer.cpp b/ir/pointer.cpp index 41ad6a7c2..2d5c26cfe 100644 --- a/ir/pointer.cpp +++ b/ir/pointer.cpp @@ -539,7 +539,9 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align, expr bytes = bytes0.zextOrTrunc(bits_for_offset); auto block_constraints = [&](const Pointer &p) { - expr ret = (iswrite || is_asm) ? p.isBlockAlive() : true; + expr ret = expr::mkIf(p.isStackAllocated(), + (iswrite || is_asm) ? p.isBlockAlive() : true, + p.isBlockAlive()); if (iswrite) ret &= p.isWritable() && !p.isNoWrite(); else if (!ignore_accessability)