Fix false positive on icmp ptr with samesign flag

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 };
   };
 

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
+}