diff --git a/ir/instr.cpp b/ir/instr.cpp index ed47eeb23..623f822f2 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -2788,7 +2788,19 @@ StateValue ICmp::toSMT(State &s) const { auto scalar = [&](const StateValue &a, const StateValue &b) -> StateValue { auto fn2 = [&](Cond c) { return fn(a.value, b.value, c); }; auto v = cond != Any ? fn2(cond) : build_icmp_chain(cond_var(), fn2); - auto np = flags & SameSign ? a.value.sign() == b.value.sign() : true; + expr np = true; + if (flags & SameSign) { + if (isPtrCmp()) { + auto &m = s.getMemory(); + Pointer lhs(m, a.value); + Pointer rhs(m, b.value); + m.observesAddr(lhs); + m.observesAddr(rhs); + np = lhs.getAddress().sign() == rhs.getAddress().sign(); + } else { + np = a.value.sign() == b.value.sign(); + } + } return { v.toBVBool(), a.non_poison && b.non_poison && np }; }; diff --git a/tests/alive-tv/samesign-ptr.srctgt.ll b/tests/alive-tv/samesign-ptr.srctgt.ll new file mode 100644 index 000000000..7c8004736 --- /dev/null +++ b/tests/alive-tv/samesign-ptr.srctgt.ll @@ -0,0 +1,34 @@ +target datalayout = "p:8:8:8" + +define i1 @src(ptr %a, ptr %b) { + %pa = ptrtoint ptr %a to i8 + %pb = ptrtoint ptr %b to i8 + %sub = sub i8 %pb, %pa + %gep = getelementptr i8, ptr %a, i8 %sub + %cmp = icmp samesign eq ptr %gep, null + ret i1 %cmp +} + +define i1 @tgt(ptr %a, ptr %b) { + %cmp = icmp samesign eq ptr %b, null + ret i1 %cmp +} + +define i1 @src_offsetonly() { + %cmp = icmp samesign eq ptr null, null + ret i1 %cmp +} + +define i1 @tgt_offsetonly() { + ret i1 true +} + +define i1 @src_provenance(ptr %base) { + %gep = getelementptr inbounds i8, ptr %base, i64 1 + %cnd = icmp samesign eq ptr %gep, null + ret i1 %cnd +} + +define i1 @tgt_provenance(ptr %base) { + ret i1 false +}