return isKnownNonZero(Op, Depth + 1, Q);
}
+
/// Return true if it is known that V1 != V2.
static bool isKnownNonEqual(const Value *V1, const Value *V2, unsigned Depth,
const Query &Q) {
if (Depth >= MaxAnalysisRecursionDepth)
return false;
- // See if we can recurse through (exactly one of) our operands.
+ // See if we can recurse through (exactly one of) our operands. This
+ // requires our operation be 1-to-1 and map every input value to exactly
+ // one output value. Such an operation is invertible.
auto *O1 = dyn_cast<Operator>(V1);
auto *O2 = dyn_cast<Operator>(V2);
if (O1 && O2 && O1->getOpcode() == O2->getOpcode()) {
return isKnownNonEqual(O1->getOperand(0), O2->getOperand(0),
Depth + 1, Q);
break;
+ case Instruction::Mul:
+ // invertible if A * B == (A * B) mod 2^N where A, and B are integers
+ // and N is the bitwdith. The nsw case is non-obvious, but proven by
+ // alive2: https://alive2.llvm.org/ce/z/Z6D5qK
+ if ((!cast<BinaryOperator>(O1)->hasNoUnsignedWrap() ||
+ !cast<BinaryOperator>(O2)->hasNoUnsignedWrap()) &&
+ (!cast<BinaryOperator>(O1)->hasNoSignedWrap() ||
+ !cast<BinaryOperator>(O2)->hasNoSignedWrap()))
+ break;
+
+ // Assume operand order has been canonicalized
+ if (O1->getOperand(1) == O2->getOperand(1) &&
+ isa<ConstantInt>(O1->getOperand(1)) &&
+ !cast<ConstantInt>(O1->getOperand(1))->isZero())
+ return isKnownNonEqual(O1->getOperand(0), O2->getOperand(0),
+ Depth + 1, Q);
+ break;
case Instruction::SExt:
case Instruction::ZExt:
if (O1->getOperand(0)->getType() == O2->getOperand(0)->getType())
ret i1 %cmp
}
+; op could wrap mapping two values to the same output value.
+define i1 @mul1(i8 %B) {
+; CHECK-LABEL: @mul1(
+; CHECK-NEXT: [[A:%.*]] = add i8 [[B:%.*]], 1
+; CHECK-NEXT: [[A_OP:%.*]] = mul i8 [[A]], 27
+; CHECK-NEXT: [[B_OP:%.*]] = mul i8 [[B]], 27
+; CHECK-NEXT: [[CMP:%.*]] = icmp eq i8 [[A_OP]], [[B_OP]]
+; CHECK-NEXT: ret i1 [[CMP]]
+;
+ %A = add i8 %B, 1
+ %A.op = mul i8 %A, 27
+ %B.op = mul i8 %B, 27
+
+ %cmp = icmp eq i8 %A.op, %B.op
+ ret i1 %cmp
+}
+
+define i1 @mul2(i8 %B) {
+; CHECK-LABEL: @mul2(
+; CHECK-NEXT: ret i1 false
+;
+ %A = add i8 %B, 1
+ %A.op = mul nuw i8 %A, 27
+ %B.op = mul nuw i8 %B, 27
+
+ %cmp = icmp eq i8 %A.op, %B.op
+ ret i1 %cmp
+}
+
+define i1 @mul3(i8 %B) {
+; CHECK-LABEL: @mul3(
+; CHECK-NEXT: ret i1 false
+;
+ %A = add i8 %B, 1
+ %A.op = mul nsw i8 %A, 27
+ %B.op = mul nsw i8 %B, 27
+
+ %cmp = icmp eq i8 %A.op, %B.op
+ ret i1 %cmp
+}
+
+; Multiply by zero collapses all values to one
+define i1 @mul4(i8 %B) {
+; CHECK-LABEL: @mul4(
+; CHECK-NEXT: ret i1 true
+;
+ %A = add i8 %B, 1
+ %A.op = mul nuw i8 %A, 0
+ %B.op = mul nuw i8 %B, 0
+
+ %cmp = icmp eq i8 %A.op, %B.op
+ ret i1 %cmp
+}
+
+; C might be zero, we can't tell
+define i1 @mul5(i8 %B, i8 %C) {
+; CHECK-LABEL: @mul5(
+; CHECK-NEXT: [[A:%.*]] = add i8 [[B:%.*]], 1
+; CHECK-NEXT: [[A_OP:%.*]] = mul nuw nsw i8 [[A]], [[C:%.*]]
+; CHECK-NEXT: [[B_OP:%.*]] = mul nuw nsw i8 [[B]], [[C]]
+; CHECK-NEXT: [[CMP:%.*]] = icmp eq i8 [[A_OP]], [[B_OP]]
+; CHECK-NEXT: ret i1 [[CMP]]
+;
+ %A = add i8 %B, 1
+ %A.op = mul nsw nuw i8 %A, %C
+ %B.op = mul nsw nuw i8 %B, %C
+
+ %cmp = icmp eq i8 %A.op, %B.op
+ ret i1 %cmp
+}
+
+
!0 = !{ i8 1, i8 5 }