Define memcmp(p,q,0) as zero, fix the last iteration condition
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2498,12 +2498,12 @@ StateValue Memcmp::toSMT(State &s) const {
auto val_eq = val1.value == val2.value;
return { expr::mkIf(val_eq, zero, result_neq),
move(ub_and),
- val_eq && expr::mkUInt(i, vn.bits()).ult(vn) };
+ val_eq && expr::mkUInt(i + 1, vn.bits()).ult(vn) };
};
auto [val, ub]
= LoopLikeFunctionApproximator(ith_exec).encode(s, memcmp_unroll_cnt);
- s.addUB(move(ub));
- return { move(val), true };
+ s.addUB(vnum.ugt(0).implies(move(ub)));
+ return { expr::mkIf(vnum == zero, zero, move(val)), true };
}
expr Memcmp::getTypeConstraints(const Function &f) const {

ADD
tests/alive-tv/memory/memcmp-zero.srctgt.ll
+target datalayout = "e-p:64:64:64"
+
+define i32 @src(i8* %p, i8* %q) {
+ ret i32 0
+}
+
+define i32 @tgt(i8* %p, i8* %q) {
+ %res = call i32 @memcmp(i8* %p, i8* %q, i64 0)
+ ret i32 %res
+}
+
+declare i32 @memcmp(i8* nocapture, i8* nocapture, i64)

Define memcmp(p,q,0) as zero, fix the last iteration condition (#371)