Add support for samesign flag (#1098)

AliveToolkit · Oct 16, 2024 · faf59b5 · faf59b5
1 parent 3127683
commit faf59b5
Show file tree

Hide file tree

Showing 4 changed files with 43 additions and 16 deletions.
diff --git a/ir/instr.cpp b/ir/instr.cpp
@@ -8,6 +8,7 @@
 #include "smt/expr.h"
 #include "smt/exprs.h"
 #include "smt/solver.h"
+#include "state_value.h"
 #include "util/compiler.h"
 #include "util/config.h"
 #include <algorithm>
@@ -2635,8 +2636,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,34 +2688,36 @@ 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;
   case OFFSETONLY: os << ", offsetonly"; break;
   }
 }
 
-static expr build_icmp_chain(const expr &var,
-                             const function<expr(ICmp::Cond)> &fn,
-                             ICmp::Cond cond = ICmp::Any,
-                             expr last = expr()) {
+static StateValue build_icmp_chain(const expr &var,
+                                   const function<StateValue(ICmp::Cond)> &fn,
+                                   ICmp::Cond cond = ICmp::Any,
+                                   StateValue last = StateValue()) {
   auto old_cond = cond;
   cond = ICmp::Cond(cond - 1);
 
   if (old_cond == ICmp::Any)
     return build_icmp_chain(var, fn, cond, fn(cond));
 
-  auto e = expr::mkIf(var == cond, fn(cond), last);
+  auto e = StateValue::mkIf(var == cond, fn(cond), last);
   return cond == 0 ? e : build_icmp_chain(var, fn, cond, std::move(e));
 }
 
 StateValue ICmp::toSMT(State &s) const {
   auto &a_eval = s[*a];
   auto &b_eval = s[*b];
 
-  function<expr(const expr&, const expr&, Cond)> fn =
-      [&](auto &av, auto &bv, Cond cond) {
+  auto cmp = [](const expr &av, const expr &bv, Cond cond) {
     switch (cond) {
     case EQ:  return av == bv;
     case NE:  return av != bv;
@@ -2729,8 +2735,15 @@ StateValue ICmp::toSMT(State &s) const {
     UNREACHABLE();
   };
 
+  function<StateValue(const expr &, const expr &, Cond)> fn =
+      [&](auto &av, auto &bv, Cond cond) -> StateValue {
+    return {cmp(av, bv, cond),
+            flags & SameSign ? av.sign() == bv.sign() : expr(true)};
+  };
+
   if (isPtrCmp()) {
-    fn = [this, &s, fn](const expr &av, const expr &bv, Cond cond) {
+    fn = [this, &s, fn](const expr &av, const expr &bv,
+                        Cond cond) -> StateValue {
       auto &m = s.getMemory();
       Pointer lhs(m, av);
       Pointer rhs(m, bv);
@@ -2742,7 +2755,7 @@ 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, true};
       case OFFSETONLY:
         return fn(lhs.getOffset(), rhs.getOffset(), cond);
       }
@@ -2753,7 +2766,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.value.toBVBool(),
+            a.non_poison && b.non_poison && std::move(v.non_poison)};
   };
 
   auto &elem_ty = a->getType();
@@ -2777,7 +2791,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);
 }
 
 

diff --git a/ir/instr.h b/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; }

diff --git a/llvm_util/llvm2alive.cpp b/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) {

diff --git a/tests/alive-tv/samesign.srctgt.ll b/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
+}