memcpy: require input ptrs to be well defined when alignment is specified
Let's see if it doesn't break any LLVM optimization.. But some change is required as otherwise applying checks
to a non-well-defined value is meaningless
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -3667,17 +3667,23 @@ StateValue Memcpy::toSMT(State &s) const {
uint64_t n;
expr vsrc, vdst;
- if (vbytes.isUInt(n) && n > 0) {
+ if (align_dst || (vbytes.isUInt(n) && n > 0)) {
vdst = s.getAndAddPoisonUB(*dst, true).value;
- vsrc = s.getAndAddPoisonUB(*src, true).value;
} else {
auto &sv_dst = s[*dst];
auto &sv_dst2 = s[*dst];
+ s.addUB((vbytes != 0).implies(
+ sv_dst.non_poison && sv_dst.value == sv_dst2.value));
+ vdst = sv_dst.value;
+ }
+
+ if (align_src || (vbytes.isUInt(n) && n > 0)) {
+ vsrc = s.getAndAddPoisonUB(*src, true).value;
+ } else {
auto &sv_src = s[*src];
auto &sv_src2 = s[*src];
- s.addUB((vbytes != 0).implies(sv_dst.non_poison && sv_src.non_poison &&
- (sv_dst.value == sv_dst2.value && sv_src.value == sv_src2.value)));
- vdst = sv_dst.value;
+ s.addUB((vbytes != 0).implies(
+ sv_src.non_poison && sv_src.value == sv_src2.value));
vsrc = sv_src.value;
}

ADD
tests/alive-tv/memory/memcpy-align.srctgt.ll
+define void @src(ptr %0) {
+ %2 = load ptr, ptr %0, align 8
+ %3 = getelementptr inbounds i64, ptr %2, i32 1
+ %4 = getelementptr inbounds i64, ptr %3, i64 0
+ call void @llvm.memcpy.p0.p0.i64(ptr align 4 %4, ptr null, i64 0, i1 false)
+ ret void
+}
+
+define void @tgt(ptr %0) {
+ %2 = load ptr, ptr %0, align 8
+ %3 = getelementptr inbounds i64, ptr %2, i32 1
+ call void @llvm.memcpy.p0.p0.i64(ptr align 4 %3, ptr null, i64 0, i1 false)
+ ret void
+}
+
+declare void @llvm.memcpy.p0.p0.i64(ptr, ptr, i64, i1)

memcpy: require input ptrs to be well defined when alignment is specified
Let's see if it doesn't break any LLVM optimization.. But some change is required as otherwise applying checks
to a non-well-defined value is meaningless