diff --git a/ir/memory.cpp b/ir/memory.cpp index 355d5e6ef..f6c3482f4 100644 --- a/ir/memory.cpp +++ b/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 another_localbid, const expr &offset, set &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 bid_other, set &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> @@ -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 diff --git a/ir/memory.h b/ir/memory.h index a0cc34390..d0f97fd55 100644 --- a/ir/memory.h +++ b/ir/memory.h @@ -195,11 +195,17 @@ class Memory { const smt::expr &bytes, const smt::expr &val, const std::set &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 another_local_bid, const smt::expr &offset, std::set &undef) const; smt::expr blockRefined(const Pointer &src, const Pointer &tgt, unsigned bid, + std::optional bid_other, std::set &undef) const; + smt::expr blockPropertiesRefined(const Pointer &src, const Pointer &tgt) + const; void mkLocalDisjAddrAxioms(const smt::expr &allocated, const smt::expr &short_bid, diff --git a/ir/pointer.cpp b/ir/pointer.cpp index 71909297d..04aab47ea 100644 --- a/ir/pointer.cpp +++ b/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 &undef_vars) const { + // TODO: can we remove these const casts? + auto b1 = const_cast(&m)->raw_load(*this, undef_vars); + auto b2 = const_cast(&other.m)->raw_load(other, undef_vars); + return b1.refined(b2); +} + +expr Pointer::encodeLocalPtrRefinement( + const Pointer &other, set &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 &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 &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) && diff --git a/ir/pointer.h b/ir/pointer.h index a8c369a33..47c787265 100644 --- a/ir/pointer.h +++ b/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 &undefs) const; + // Encode the refinement between + // (src ptr, tgt ptr) = (local, local) or (local, byval ptr) + smt::expr encodeLocalPtrRefinement(const Pointer &other, + std::set &undefs, + bool readsbytes) const; + // Encode the refinement when two ptrs are given as byval args + smt::expr encodeByValArgRefinement(const Pointer &otherByval, + std::set &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 &undef, - unsigned byval_bytes) const; + unsigned byval_bytes, bool readsbytes) const; const Memory& getMemory() const { return m; } diff --git a/ir/state.cpp b/ir/state.cpp index 38051a3c6..7e791989e 100644 --- a/ir/state.cpp +++ b/ir/state.cpp @@ -716,8 +716,6 @@ 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) @@ -725,7 +723,7 @@ expr State::FnCallInput::refinedBy( 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) diff --git a/tests/alive-tv/bugs/pr10067.srctgt.ll b/tests/alive-tv/bugs/pr10067.srctgt.ll index 0139eade2..9541b71af 100644 --- a/tests/alive-tv/bugs/pr10067.srctgt.ll +++ b/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 diff --git a/tests/alive-tv/bugs/pr41949-2.srctgt.ll b/tests/alive-tv/bugs/pr41949-2.srctgt.ll index 5b6ee0d1f..e812c2217 100644 --- a/tests/alive-tv/bugs/pr41949-2.srctgt.ll +++ b/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 diff --git a/tests/alive-tv/calls/call-movestr2.src.ll b/tests/alive-tv/calls/call-movestr2.src.ll index 934a99d08..1401e5bcd 100644 --- a/tests/alive-tv/calls/call-movestr2.src.ll +++ b/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 diff --git a/tests/alive-tv/calls/issue435.srctgt.ll b/tests/alive-tv/calls/issue435.srctgt.ll new file mode 100644 index 000000000..b120dad7d --- /dev/null +++ b/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 diff --git a/tests/alive-tv/calls/lifetime.srctgt.ll b/tests/alive-tv/calls/lifetime.srctgt.ll new file mode 100644 index 000000000..b6a972138 --- /dev/null +++ b/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*) diff --git a/tests/alive-tv/calls/writeonly-local.srctgt.ll b/tests/alive-tv/calls/writeonly-local.srctgt.ll new file mode 100644 index 000000000..34bec327b --- /dev/null +++ b/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