Patched #1242

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

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<TypedByte>
@@ -1234,7 +1237,10 @@ Memory::load(const Pointer &ptr, unsigned bytes, set<expr> &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(expr::mkUInt(bid, Pointer::bitsShortBid()), 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());

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 = p.isBlockAlive();
+    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)

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

tests/alive-tv/calls/escape2.srctgt.ll

@@ -1,25 +1,32 @@
 @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
   %q2 = call ptr @f(ptr %q) ; cannot be %p
   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
 }

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))

tests/alive-tv/lifetime-load-poison.srctgt.ll

@@ -0,0 +1,13 @@
+; ERROR: Source is more defined than target
+
+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
+}