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

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)

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

@@ -0,0 +1,13 @@
+; EXPECT: 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
+}