Add support for samesign flag

ir/instr.cpp

@@ -2635,8 +2635,11 @@ InlineAsm::InlineAsm(Type &type, string &&name, const string &asm_str,
            std::move(attrs)) {}
 
 
-ICmp::ICmp(Type &type, string &&name, Cond cond, Value &a, Value &b)
-  : Instr(type, std::move(name)), a(&a), b(&b), cond(cond), defined(cond != Any) {
+ICmp::ICmp(Type &type, string &&name, Cond cond, Value &a, Value &b,
+           unsigned flags)
+    : Instr(type, std::move(name)), a(&a), b(&b), cond(cond), flags(flags),
+      defined(cond != Any) {
+  assert((flags & SameSign) == flags);
   if (!defined)
     cond_name = getName() + "_cond";
 }
@@ -2684,7 +2687,10 @@ void ICmp::print(ostream &os) const {
   case UGT: condtxt = "ugt "; break;
   case Any: condtxt = ""; break;
   }
-  os << getName() << " = icmp " << condtxt << *a << ", " << b->getName();
+  os << getName() << " = icmp ";
+  if (flags & SameSign)
+    os << "samesign ";
+  os << condtxt << *a << ", " << b->getName();
   switch (pcmode) {
   case INTEGRAL: break;
   case PROVENANCE: os << ", use_provenance"; break;
@@ -2729,6 +2735,13 @@ StateValue ICmp::toSMT(State &s) const {
     UNREACHABLE();
   };
 
+  fn = [this, fn](const expr &av, const expr &bv, Cond cond) {
+    return fn(av, bv, cond)
+        .toBVBool()
+        .concat(flags & SameSign ? (av.sign() == bv.sign()).toBVBool()
+                                 : expr::mkUInt(1, 1));
+  };
+
   if (isPtrCmp()) {
     fn = [this, &s, fn](const expr &av, const expr &bv, Cond cond) {
       auto &m = s.getMemory();
@@ -2742,7 +2755,9 @@ StateValue ICmp::toSMT(State &s) const {
         return fn(lhs.getAddress(), rhs.getAddress(), cond);
       case PROVENANCE:
         assert(cond == EQ || cond == NE);
-        return cond == EQ ? lhs == rhs : lhs != rhs;
+        return (cond == EQ ? lhs == rhs : lhs != rhs)
+            .toBVBool()
+            .concat(expr::mkUInt(1, 1));
       case OFFSETONLY:
         return fn(lhs.getOffset(), rhs.getOffset(), cond);
       }
@@ -2753,7 +2768,8 @@ 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);
-    return { v.toBVBool(), a.non_poison && b.non_poison };
+    return {v.extract(1, 1),
+            a.non_poison && b.non_poison && v.extract(0, 0).isOne()};
   };
 
   auto &elem_ty = a->getType();
@@ -2777,7 +2793,7 @@ expr ICmp::getTypeConstraints(const Function &f) const {
 }
 
 unique_ptr<Instr> ICmp::dup(Function &f, const string &suffix) const {
-  return make_unique<ICmp>(getType(), getName() + suffix, cond, *a, *b);
+  return make_unique<ICmp>(getType(), getName() + suffix, cond, *a, *b, flags);
 }
 
 

ir/instr.h

@@ -418,17 +418,20 @@ class ICmp final : public Instr {
     PROVENANCE, // compare pointer provenance & offsets
     OFFSETONLY // cmp ofs only. meaningful only when ptrs are based on same obj
   };
+  enum Flags { None = 0, SameSign = 1 << 0 };
 
 private:
   Value *a, *b;
   std::string cond_name;
   Cond cond;
+  unsigned flags;
   bool defined;
   PtrCmpMode pcmode = INTEGRAL;
   smt::expr cond_var() const;
 
 public:
-  ICmp(Type &type, std::string &&name, Cond cond, Value &a, Value &b);
+  ICmp(Type &type, std::string &&name, Cond cond, Value &a, Value &b,
+       unsigned flags = None);
 
   bool isPtrCmp() const;
   PtrCmpMode getPtrCmpMode() const { return pcmode; }

llvm_util/llvm2alive.cpp

@@ -507,7 +507,8 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
     default:
       UNREACHABLE();
     }
-    return make_unique<ICmp>(*ty, value_name(i), cond, *a, *b);
+    return make_unique<ICmp>(*ty, value_name(i), cond, *a, *b,
+                             i.hasSameSign() ? ICmp::SameSign : ICmp::None);
   }
 
   RetTy visitFCmpInst(llvm::FCmpInst &i) {

tests/alive-tv/samesign.srctgt.ll

@@ -0,0 +1,9 @@
+define i1 @src(i8 %x, i8 %y) {
+  %cmp = icmp samesign slt i8 %x, %y
+  ret i1 %cmp
+}
+
+define i1 @tgt(i8 %x, i8 %y) {
+  %cmp = icmp samesign ult i8 %x, %y
+  ret i1 %cmp
+}