Encode the basic refinement of escaped local blocks

ir/memory.cpp

@@ -1903,11 +1903,12 @@ expr Memory::int2ptr(const expr &val) const {
   return expr::mkIf(val == 0, null, fn);
 }
 
-expr Memory::blockValRefined(const Memory &other, unsigned bid, bool local,
+expr Memory::blockValRefined(const Memory &other, unsigned bid,
+                             optional<unsigned> another_localbid,
                              const expr &offset, set<expr> &undef) const {
-  assert(!local);
-  auto &mem1 = non_local_block_val[bid];
-  auto &mem2 = other.non_local_block_val[bid].val;
+  auto &mem1 = (another_localbid ? local_block_val : non_local_block_val)[bid];
+  auto &mem2 = another_localbid ? other.local_block_val[*another_localbid].val :
+                                  other.non_local_block_val[bid].val;
 
   if (mem1.val.eq(mem2))
     return true;
@@ -1938,7 +1939,24 @@ expr Memory::blockValRefined(const Memory &other, unsigned bid, bool local,
   return val.refined(val2);
 }
 
+expr Memory::blockPropertiesRefined(const Pointer &src, const Pointer &tgt)
+    const {
+  expr aligned(true);
+  expr src_align = src.blockAlignment();
+  expr tgt_align = tgt.blockAlignment();
+  // if they are both non-const, then the condition holds per the precondition
+  if (src_align.isConst() || tgt_align.isConst())
+    aligned = src_align.ule(tgt_align);
+
+  return src.isBlockAlive().implies(tgt.isBlockAlive()) &&
+         src.blockSize() == tgt.blockSize() &&
+         ((src.isLocal() && tgt.isByval()) ||
+          src.getAllocType() == tgt.getAllocType()) &&
+         aligned;
+}
+
 expr Memory::blockRefined(const Pointer &src, const Pointer &tgt, unsigned bid,
+                          optional<unsigned> bid_other,
                           set<expr> &undef) const {
   unsigned bytes_per_byte = bits_byte / 8;
 
@@ -1953,29 +1971,18 @@ expr Memory::blockRefined(const Pointer &src, const Pointer &tgt, unsigned bid,
       expr off_expr = expr::mkUInt(off, Pointer::bitsShortOffset());
       val_refines
         &= (ptr_offset == off_expr).implies(
-             blockValRefined(tgt.getMemory(), bid, false, off_expr, undef));
+             blockValRefined(tgt.getMemory(), bid, bid_other, off_expr, undef));
     }
   } else {
     val_refines
       = src.getOffsetSizet().ult(src.blockSizeOffsetT()).implies(
-          blockValRefined(tgt.getMemory(), bid, false, ptr_offset, undef));
+          blockValRefined(tgt.getMemory(), bid, bid_other, ptr_offset, undef));
   }
 
   assert(src.isWritable().eq(tgt.isWritable()));
 
-  expr aligned(true);
-  expr src_align = src.blockAlignment();
-  expr tgt_align = tgt.blockAlignment();
-  // if they are both non-const, then the condition holds per the precondition
-  if (src_align.isConst() || tgt_align.isConst())
-    aligned = src_align.ule(tgt_align);
-
   expr alive = src.isBlockAlive();
-  return alive == tgt.isBlockAlive() &&
-         blk_size == tgt.blockSize() &&
-         src.getAllocType() == tgt.getAllocType() &&
-         aligned &&
-         alive.implies(val_refines);
+  return blockPropertiesRefined(src, tgt) && alive.implies(val_refines);
 }
 
 tuple<expr, Pointer, set<expr>>
@@ -2027,7 +2034,8 @@ Memory::refined(const Memory &other, bool fncall,
     Pointer q(other, p());
     if (p.isByval().isTrue() && q.isByval().isTrue())
       continue;
-    ret &= (ptr_bid == bid_expr).implies(blockRefined(p, q, bid, undef_vars));
+    ret &= (ptr_bid == bid_expr)
+        .implies(blockRefined(p, q, bid, nullopt, undef_vars));
   }
 
   // restrict refinement check to set of request blocks

ir/memory.h

@@ -195,11 +195,17 @@ class Memory {
                    const smt::expr &bytes, const smt::expr &val,
                    const std::set<smt::expr> &undef, uint64_t align);
 
-  smt::expr blockValRefined(const Memory &other, unsigned bid, bool local,
+  // If bid_other == nullopt, it encodes the non-local block refinement
+  // Otherwise, it encodes the local block refinement between bid and *bid_other
+  smt::expr blockValRefined(const Memory &other, unsigned bid,
+                            std::optional<unsigned> another_local_bid,
                             const smt::expr &offset,
                             std::set<smt::expr> &undef) const;
   smt::expr blockRefined(const Pointer &src, const Pointer &tgt, unsigned bid,
+                         std::optional<unsigned> bid_other,
                          std::set<smt::expr> &undef) const;
+  smt::expr blockPropertiesRefined(const Pointer &src, const Pointer &tgt)
+                                   const;
 
   void mkLocalDisjAddrAxioms(const smt::expr &allocated,
                              const smt::expr &short_bid,

ir/pointer.cpp

@@ -485,35 +485,73 @@ expr Pointer::refined(const Pointer &other) const {
                       isBlockAlive().implies(other.isBlockAlive()));
 }
 
+expr Pointer::encodeLoadedByteRefined(
+    const Pointer &other, set<expr> &undef_vars) const {
+  // TODO: can we remove these const casts?
+  auto b1 = const_cast<Memory *>(&m)->raw_load(*this, undef_vars);
+  auto b2 = const_cast<Memory *>(&other.m)->raw_load(other, undef_vars);
+  return b1.refined(b2);
+}
+
+expr Pointer::encodeLocalPtrRefinement(
+    const Pointer &other, set<expr> &undefs, bool readsbytes) const {
+  expr tgt_bid = other.getShortBid();
+  expr ofs = expr::mkFreshVar("localblk_ofs", expr::mkUInt(0, bits_for_offset));
+  Pointer this_ofs = *this + ofs;
+  Pointer other_ofs = other + ofs;
+
+  uint64_t bid_const, bid_tgt_const;
+  bool is_const_bid = this_ofs.getShortBid().isUInt(bid_const) &&
+                      tgt_bid.isUInt(bid_tgt_const);
+  expr blkrefined;
+  if (readsbytes && is_const_bid && this->isByval().isFalse() &&
+      other.isByval().isFalse()) {
+    // Look into the bytes.
+    // If this or other pointer is byval, blockRefined cannot be used because
+    // it requires both bids to be local or nonlocal
+    // In the byval case, return the approximated result by simply checking
+    // the block properties in the else clause below
+    blkrefined = m.blockRefined(*this, other, (unsigned)bid_const,
+                                (unsigned)bid_tgt_const, undefs);
+  } else
+    blkrefined = m.blockPropertiesRefined(*this, other);
+
+  return (other.isLocal() || other.isByval()) &&
+      getOffset() == other.getOffset() && move(blkrefined);
+}
+
+expr Pointer::encodeByValArgRefinement(
+    const Pointer &other, set<expr> &undefs, unsigned size) const {
+  expr ofs = expr::mkFreshVar("localblk_ofs", expr::mkUInt(0, bits_for_offset));
+  Pointer this_ofs = *this + ofs;
+  Pointer other_ofs = other + ofs;
+
+  // Dereferenceability of this and other ptr is already encoded by
+  // ParamAttrs::encode.
+  return ofs.ugt(expr::mkUInt(size, ofs))
+      .implies(this_ofs.encodeLoadedByteRefined(other_ofs, undefs));
+}
+
 expr Pointer::fninputRefined(const Pointer &other, set<expr> &undef,
-                             unsigned byval_bytes) const {
+                             unsigned byval_bytes, bool readsbytes) const {
   expr size = blockSizeOffsetT();
   expr off = getOffsetSizet();
   expr size2 = other.blockSizeOffsetT();
   expr off2 = other.getOffsetSizet();
 
-  // TODO: check block value for byval_bytes
-  if (byval_bytes)
-    return true;
+  if (byval_bytes) {
+    // If a value is passed as byval, it must be read.
+    assert(readsbytes);
+    return encodeByValArgRefinement(other, undef, byval_bytes);
+  }
 
-  expr local
-    = expr::mkIf(isHeapAllocated(),
-                 getAllocType() == other.getAllocType() &&
-                   off == off2 && size == size2,
-
-                 expr::mkIf(off.sge(0),
-                            off2.sge(0) &&
-                              expr::mkIf(off.ule(size),
-                                         off2.ule(size2) && off2.uge(off) &&
-                                           (size2 - off2).uge(size - off),
-                                         off2.ugt(size2) && off == off2 &&
-                                           size2.uge(size)),
-                            // maintains same dereferenceability before/after
-                            off == off2 && size2.uge(size)));
-  local = (other.isLocal() || other.isByval()) && local;
+  expr islocal = isLocal();
+  expr local = false;
+  if (!islocal.isFalse() &&
+      (!other.isLocal().isFalse() || !other.isByval().isFalse()))
+    local = encodeLocalPtrRefinement(other, undef, readsbytes);
 
-  // TODO: this induces an infinite loop
-  // block_refined(other);
+  local = (other.isLocal() || other.isByval()) && local;
 
   return expr::mkIf(isNull(), other.isNull(),
                     expr::mkIf(isLocal(), local, *this == other) &&

ir/pointer.h

@@ -35,6 +35,18 @@ class Pointer {
                       const smt::FunctionExpr &nonlocal_fn,
                       const smt::expr &ret_type, bool src_name = false) const;
 
+  smt::expr encodeLoadedByteRefined(const Pointer &other,
+                                    std::set<smt::expr> &undefs) const;
+  // Encode the refinement between
+  // (src ptr, tgt ptr) = (local, local) or (local, byval ptr)
+  smt::expr encodeLocalPtrRefinement(const Pointer &other,
+                                     std::set<smt::expr> &undefs,
+                                     bool readsbytes) const;
+  // Encode the refinement when two ptrs are given as byval args
+  smt::expr encodeByValArgRefinement(const Pointer &otherByval,
+                                     std::set<smt::expr> &undefs,
+                                     unsigned byval_size) const;
+
 public:
   Pointer(const Memory &m, const smt::expr &bid, const smt::expr &offset,
           const smt::expr &attr);
@@ -111,7 +123,7 @@ class Pointer {
 
   smt::expr refined(const Pointer &other) const;
   smt::expr fninputRefined(const Pointer &other, std::set<smt::expr> &undef,
-                           unsigned byval_bytes) const;
+                           unsigned byval_bytes, bool readsbytes) const;
 
   const Memory& getMemory() const { return m; }
 

ir/state.cpp

@@ -716,16 +716,14 @@ expr State::FnCallInput::refinedBy(
   if (!inaccessiblememonly) {
     assert(args_ptr.size() == args_ptr2.size());
     for (unsigned i = 0, e = args_ptr.size(); i != e; ++i) {
-      // TODO: needs to take read/read2 as input to control if mem blocks
-      // need to be compared
       auto &[ptr_in, byval, is_nocapture] = args_ptr[i];
       auto &[ptr_in2, byval2, is_nocapture2] = args_ptr2[i];
       if (byval != byval2 || is_nocapture != is_nocapture2)
         return false;
 
       expr eq_val = Pointer(m, ptr_in.value)
                       .fninputRefined(Pointer(m2, ptr_in2.value),
-                                      undef_vars, byval2);
+                                      undef_vars, byval2, readsmem);
       refines.add(ptr_in.non_poison.implies(eq_val && ptr_in2.non_poison));
 
       if (!refines)

tests/alive-tv/bugs/pr10067.srctgt.ll

@@ -1,6 +1,3 @@
-; To support this test, escaped local blocks should have bytes updated after
-; unkown fn calls.
-
 target datalayout = "e-p:32:32:32-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:32:64-f32:32:32-f64:32:64-v64:64:64-v128:128:128-a0:0:64-f80:128:128-n8:16:32"
 target triple = "i386-apple-darwin10"
 
@@ -10,7 +7,7 @@ target triple = "i386-apple-darwin10"
 define i32 @src() noinline {
   %x = alloca %struct1, align 8
   %y = alloca %struct2, align 8
-  call void @bar(%struct1* sret(%struct1) %x)
+  call void @bar(%struct1* %x)
 
   %gepn1 = getelementptr inbounds %struct2, %struct2* %y, i32 0, i32 0, i32 0
   store i32 0, i32* %gepn1, align 8
@@ -31,7 +28,7 @@ define i32 @tgt() noinline {
   %x = alloca %struct1, align 8
   %y = alloca %struct2, align 8
   %y1 = bitcast %struct2* %y to %struct1*
-  call void @bar(%struct1* sret(%struct1) %y1)
+  call void @bar(%struct1* %y1)
   %gepn1 = getelementptr inbounds %struct2, %struct2* %y, i32 0, i32 0, i32 0
   store i32 0, i32* %gepn1, align 8
   %gepn2 = getelementptr inbounds %struct2, %struct2* %y, i32 0, i32 0, i32 1
@@ -43,4 +40,6 @@ define i32 @tgt() noinline {
   ret i32 %ret
 }
 
-declare void @bar(%struct1* sret(%struct1))
+declare void @bar(%struct1*)
+
+; ERROR: Source is more defined than target

tests/alive-tv/bugs/pr41949-2.srctgt.ll

@@ -1,5 +1,4 @@
 ; https://bugs.llvm.org/show_bug.cgi?id=41949
-; To detect a bug from this, bytes of escaped local blocks should be checked
 
 ;source_filename = "41949.ll"
 target datalayout = "E"
@@ -23,3 +22,5 @@ define void @tgt(i32* %p) {
 }
 
 declare void @test1(i32*)
+
+; ERROR: Source is more defined than target

tests/alive-tv/calls/call-movestr2.src.ll

@@ -1,6 +1,3 @@
-; TODO: needs refinement of local blocks working
-; XPASS: Transformation seems to be correct
-
 define i8 @f() {
   %a = alloca i8
   store i8 3, i8* %a
@@ -9,3 +6,5 @@ define i8 @f() {
 }
 
 declare i8 @g(i8*)
+
+; ERROR: Source is more defined than target

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

@@ -0,0 +1,27 @@
+target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-unknown-linux-gnu"
+
+define void @src(i64 %i) {
+entry:
+  %storage = alloca [16 x i8], align 16
+  %0 = getelementptr inbounds [16 x i8], [16 x i8]* %storage, i64 0, i64 0
+  call void @llvm.memset.p0i8.i64(i8* noundef nonnull align 16 dereferenceable(16) %0, i8 0, i64 16, i1 false)
+  %arrayidx = getelementptr inbounds [16 x i8], [16 x i8]* %storage, i64 0, i64 %i
+  call void @use(i8* nonnull align 1 dereferenceable(1) %arrayidx)
+  ret void
+}
+
+declare void @llvm.memset.p0i8.i64(i8*, i8, i64, i1)
+
+declare void @use(i8* nonnull align 1 dereferenceable(1))
+
+define void @tgt(i64 %i) {
+entry:
+  %storage = alloca [16 x i8], align 16
+  %0 = getelementptr inbounds [16 x i8], [16 x i8]* %storage, i64 0, i64 0
+  %arrayidx = getelementptr inbounds [16 x i8], [16 x i8]* %storage, i64 0, i64 %i
+  call void @use(i8* nonnull align 1 dereferenceable(1) %arrayidx)
+  ret void
+}
+
+; ERROR: Source is more defined than target

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

@@ -0,0 +1,20 @@
+define void @src() {
+  %text = alloca i8, align 1
+
+  call void @llvm.lifetime.start.p0i8(i64 1, i8* %text)
+  call void @llvm.lifetime.end.p0i8(i64 1, i8* %text)
+
+  call void @foo(i8* %text)
+  ret void
+}
+
+define void @tgt() {
+  %text = alloca i8, align 1
+
+  call void @foo(i8* %text)
+  ret void
+}
+
+declare void @foo(i8*)
+declare void @llvm.lifetime.start.p0i8(i64, i8*)
+declare void @llvm.lifetime.end.p0i8(i64, i8*)

tests/alive-tv/calls/writeonly-local.srctgt.ll

@@ -0,0 +1,19 @@
+; This is a valid transformation, but alive-tv reports it as incorrect due to issue 650.
+; SKIP-IDENTITY
+
+define void @src() {
+  %p = alloca i32
+  store i32 0, i32* %p
+  call void @writeonly(i32* %p)
+  ret void
+}
+
+define void @tgt() {
+  %p = alloca i32
+  call void @writeonly(i32* %p)
+  ret void
+}
+
+declare void @writeonly(i32*) writeonly
+
+; ERROR: Source is more defined than target