Add support for disjoint

ir/instr.cpp

@@ -122,6 +122,9 @@ BinOp::BinOp(Type &type, string &&name, Value &lhs, Value &rhs, Op op,
   case LShr:
     assert((flags & Exact) == flags);
     break;
+  case Or:
+    assert((flags & Disjoint) == flags);
+    break;
   default:
     assert(flags == 0);
     break;
@@ -190,6 +193,8 @@ void BinOp::print(ostream &os) const {
     os << "nuw ";
   if (flags & Exact)
     os << "exact ";
+  if (flags & Disjoint)
+    os << "disjoint ";
   os << *lhs << ", " << rhs->getName();
 }
 
@@ -349,8 +354,8 @@ StateValue BinOp::toSMT(State &s) const {
     break;
 
   case Or:
-    fn = [](auto &a, auto &ap, auto &b, auto &bp) -> StateValue {
-      return { a | b, true };
+    fn = [&](auto &a, auto &ap, auto &b, auto &bp) -> StateValue {
+      return { a | b, (flags & Disjoint) ? (a & b) == 0 : true };
     };
     break;
 

ir/instr.h

@@ -35,7 +35,7 @@ class BinOp final : public Instr {
             SAdd_Overflow, UAdd_Overflow, SSub_Overflow, USub_Overflow,
             SMul_Overflow, UMul_Overflow,
             And, Or, Xor, Cttz, Ctlz, UMin, UMax, SMin, SMax, Abs };
-  enum Flags { None = 0, NSW = 1 << 0, NUW = 1 << 1, Exact = 1 << 2 };
+  enum Flags { None = 0, NSW = 1 << 0, NUW = 1 << 1, Exact = 1 << 2, Disjoint = 1 << 3 };
 
 private:
   Value *lhs, *rhs;

llvm_util/llvm2alive.cpp

@@ -255,6 +255,10 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
       flags |= BinOp::NUW;
     if (isa<llvm::PossiblyExactOperator>(i) && i.isExact())
       flags = BinOp::Exact;
+    if (const auto *PDI = dyn_cast<llvm::PossiblyDisjointInst>(&i)) {
+      if (PDI->isDisjoint())
+        flags |= BinOp::Disjoint;
+    }
     RETURN_IDENTIFIER(make_unique<BinOp>(*ty, value_name(i), *a, *b, alive_op,
                                          flags));
   }

tests/alive-tv/disjoint.srctgt.ll

@@ -0,0 +1,9 @@
+define i8 @src(i8 %x, i8 %y) {
+  %r = or disjoint i8 %x, %y
+  ret i8 %r
+}
+
+define i8 @tgt(i8 %x, i8 %y) {
+  %r = add nuw i8 %x, %y
+  ret i8 %r
+}