Encode the basic refinement of escaped local blocks

Author: aqjune

ir/memory.cpp

@@ -1855,11 +1855,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> bid_other,
                              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 = (bid_other ? local_block_val : non_local_block_val)[bid];
+  auto &mem2 = bid_other ? other.local_block_val[*bid_other].val : 
+                           other.non_local_block_val[bid].val;
 
   if (mem1.val.eq(mem2))
     return true;
@@ -1890,7 +1891,23 @@ 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() == tgt.isBlockAlive() &&
+         src.blockSize() == tgt.blockSize() &&
+         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;
 
@@ -1905,29 +1922,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>>
@@ -1958,7 +1964,8 @@ Memory::refined(const Memory &other, bool skip_constants,
     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_src == 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> bid_other,
                             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

@@ -486,35 +486,63 @@ 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) 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 (is_const_bid)
+    // Look into the bytes
+    blkrefined = m.blockRefined(*this, other, (unsigned)bid_const,
+                                (unsigned)bid_tgt_const, undefs);
+  else
+    blkrefined = m.blockPropertiesRefined(*this, other);
+
+  return other.isLocal() && 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;
+
+  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 {
   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;
+    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())
+    local = encodeLocalPtrRefinement(other, undef);
 
-  // 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,14 @@ 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;
+  smt::expr encodeLocalPtrRefinement(const Pointer &other,
+                                     std::set<smt::expr> &undefs) const;
+  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);

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

@@ -44,3 +44,5 @@ define i32 @tgt() noinline {
 }
 
 declare void @bar(%struct1* sret(%struct1))
+
+; ERROR: Couldn't prove the correctness of the transformation

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,5 +1,4 @@
 ; TODO: needs refinement of local blocks working
-; XPASS: Transformation seems to be correct
 
 define i8 @f() {
   %a = alloca i8
@@ -9,3 +8,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