change memcpy semantics to allow memcpy(p, p, foo) per latest LLVM changes
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -758,12 +758,13 @@ static expr disjoint(const expr &begin1, const expr &len1, const expr &begin2,
}
// This function assumes that both begin + len don't overflow
-void Pointer::isDisjoint(const expr &len1, const Pointer &ptr2,
+void Pointer::isDisjointOrEqual(const expr &len1, const Pointer &ptr2,
const expr &len2) const {
+ auto off = getOffsetSizet();
+ auto off2 = ptr2.getOffsetSizet();
m.state->addUB(getBid() != ptr2.getBid() ||
- disjoint(getOffsetSizet(),
- len1.zextOrTrunc(bits_size_t),
- ptr2.getOffsetSizet(),
+ off == off2 ||
+ disjoint(off, len1.zextOrTrunc(bits_size_t), off2,
len2.zextOrTrunc(bits_size_t)));
}
@@ -2051,7 +2052,7 @@ void Memory::memcpy(const expr &d, const expr &s, const expr &bytesize,
state->addUB(dst.isDereferenceable(bytesize, align_dst, true));
state->addUB(src.isDereferenceable(bytesize, align_src, false));
if (!is_move)
- src.isDisjoint(bytesize, dst, bytesize);
+ src.isDisjointOrEqual(bytesize, dst, bytesize);
// copy to itself
if ((src == dst).isTrue())

MODIFY
ir/memory.h
ir/memory.h
@@ -163,7 +163,7 @@ public:
bool iswrite = false);
smt::AndExpr isDereferenceable(const smt::expr &bytes, unsigned align,
bool iswrite);
- void isDisjoint(const smt::expr &len1, const Pointer &ptr2,
+ void isDisjointOrEqual(const smt::expr &len1, const Pointer &ptr2,
const smt::expr &len2) const;
smt::expr isBlockAlive() const;
smt::expr isWritable() const;

ADD
tests/alive-tv/memory/memcpy-eq.srctgt.ll
+; ERROR: Value mismatch
+
+declare void @llvm.memcpy.p0i8.p0i8.i32(i8*, i8*, i32, i1)
+
+define i8 @src() {
+ %p1 = alloca i8
+ %p2 = alloca i8
+ store i8 42, i8* %p1
+ call void @llvm.memcpy.p0i8.p0i8.i32(i8* %p1, i8* %p1, i32 1, i1 0)
+ call void @llvm.memcpy.p0i8.p0i8.i32(i8* %p2, i8* %p1, i32 1, i1 0)
+ %v = load i8, i8* %p2
+ ret i8 %v
+}
+
+define i8 @tgt() {
+ ret i8 43
+}

change memcpy semantics to allow memcpy(p, p, foo) per latest LLVM changes