[ConstraintElimination] A miscompile in presence of shl nuw nsw and llvm.umin

[DaniilSuchkov]

The following commit: 71f56e4
Triggered this miscompile: https://alive2.llvm.org/ce/z/oBg-u8

Now opt -passes=constraint-elimination -S turns

define i1 @test(i32 %arg) {
  %icmp = icmp slt i32 %arg, 0
  %shl = shl nuw nsw i32 %arg, 3
  %call4 = call i32 @llvm.umin.i32(i32 %shl, i32 80)
  ret i1 %icmp
}

declare i32 @llvm.umin.i32(i32, i32) #0

attributes #0 = { nocallback nofree nosync nounwind speculatable willreturn memory(none) }

into

define i1 @test(i32 %arg) {
  %shl = shl nuw nsw i32 %arg, 3
  %call4 = call i32 @llvm.umin.i32(i32 %shl, i32 80)
  ret i1 false
}

declare i32 @llvm.umin.i32(i32, i32) #0

attributes #0 = { nocallback nofree nosync nounwind speculatable willreturn memory(none) }

Given this debug output:

opt -passes=constraint-elimination before-constr-elim-renamed.ll -S -debug-only=constraint-elimination,constraint-system
Processing fact to add to the system: icmp ule i32 %call4, %shl
Adding 'icmp ule i32 %call4, %shl'
  constraint: -8 * %arg + %call4 <= 0

---
-1 * %arg <= 0
-8 * %arg + %call4 <= 0
-1 * %call4 <= 0
8 * %arg <= -1
unsat
Adding 'icmp sge i32 %call4, 0'
  constraint: -1 * %call4 <= 0

Adding 'icmp sle i32 %call4, %shl'
  constraint: -8 * %arg + %call4 <= 0

Processing fact to add to the system: icmp ule i32 %call4, 80
Adding 'icmp ule i32 %call4, 80'
  constraint: %call4 <= 80

Adding 'icmp sge i32 %call4, 0'
  constraint: -1 * %call4 <= 0

Adding 'icmp sle i32 %call4, 80'
  constraint: %call4 <= 80

Top of stack : 0 1
CB: 0 1
Processing condition to simplify:   %icmp = icmp slt i32 %arg, 0
Checking   %icmp = icmp slt i32 %arg, 0
---
-1 * %call4 <= 0
-8 * %arg + %call4 <= 0
-1 * %call4 <= 0
%call4 <= 80
-1 * %arg <= 0
sat
---
-1 * %call4 <= 0
-8 * %arg + %call4 <= 0
-1 * %call4 <= 0
%call4 <= 80
%arg <= -1
unsat
Condition icmp sge i32 %arg, 0 implied by dominating constraints
-1 * %call4 <= 0
-8 * %arg + %call4 <= 0
-1 * %call4 <= 0
%call4 <= 80

I'm not 100% sure if the aforementioned patch causes the miscompile, of if it merely triggers it on this specific reproducer. The fact that something like -1 * %call4 <= 0 is reported as a "dominating constraint" seems suspicious to a person who's not familiar with the logic of ConstraintElimination and it doesn't look directly related to that patch. However, if I replace the shl nuw nsw i32 %arg, 3 with mul nuw nsw i32 %arg, 8, the miscompile doesn't happen: https://alive2.llvm.org/ce/z/EL2bCh.

[nikic]

From the debug log, I suspect that we're using the unsigned constraint system to prove a signed fact for some reason.

cc @fhahn

[nikic]

Okay, this is an interesting case.

We are adding an icmp ule i32 %call4, %shl fact, which get transferred as icmp sge i32 %call4, 0 and icmp sle i32 %call4, %shl to the signed system, because %shl is known non-negative.

Then we are checking whether a solution of these constraints plus %arg <= -1 exists, which it does not.

This is "correct" in the sense that if that umin call returns a non-poison result, then icmp slt i32 %arg, 0 is indeed known to be false. But we obviously can't actually make that assumption.

@dtcxzyw @fhahn This makes me think that the way we are currently adding facts for MinMaxIntrinsic (and I guess abs as well) is pretty fundamentally incorrect, because it effectively imposes a constraint that the umin operation returns a well-defined value. Any thoughts on how to fix this without dropping support for them entirely?

[nikic]

(The difference between shl and mul in the reproducer is because ValueTracking apparently currently doesn't know that mul nuw nsw is non-negative, but knows that shl nuw nsw is.)

[dtcxzyw]

@dtcxzyw @fhahn This makes me think that the way we are currently adding facts for MinMaxIntrinsic (and I guess abs as well) is pretty fundamentally incorrect, because it effectively imposes a constraint that the umin operation returns a well-defined value. Any thoughts on how to fix this without dropping support for them entirely?

Can we conservatively check these intrinsics using isGuaranteedNotToBePoison?

[nikic]

If it's not too complicated, I think a better solution would be to only add the intrinsic constraints when the result variable is added to the constraint system.

[fhahn]

If it's not too complicated, I think a better solution would be to only add the intrinsic constraints when the result variable is added to the constraint system.

One way to do that would be to check the uses of the intrinsic and find all the branches that it feeds, and add it as fact for the successors.

[nikic]

@dtcxzyw Do you plan to submit a PR for this issue?

[dtcxzyw]

@dtcxzyw Do you plan to submit a PR for this issue?

I will post a patch later.

[fhahn]

I've pushed a fix that only adds the facts if the result is guaranteed to not be poison so the mis-compile is fixed. I also added a TODO to improve things if possible.

Reopening so we can pick the fix for the release branch

[nikic]

@fhahn Why does your fix only do this for min/max but not abs? Can't it have the same problem?

[fhahn]

@fhahn Why does your fix only do this for min/max but not abs? Can't it have the same problem?

I wasn't able to come up with a problematic test case so far for abs, but there's a few more things to try.

[DaniilSuchkov]

@fhahn I'm not familiar with how this pass works, so I have a question: will this pass still use min/max/etc. to infer facts about the arguments of those intrinsics? I'm just a bit confused by the terminology: I see that it adds "constraints" based on things like icmp, which on their own don't actually constrain anything unless you branch on the result (or do something similar).

[nikic]

@fhahn I'm not familiar with how this pass works, so I have a question: will this pass still use min/max/etc. to infer facts about the arguments of those intrinsics? I'm just a bit confused by the terminology: I see that it adds "constraints" based on things like icmp, which on their own don't actually constrain anything unless you branch on the result (or do something similar).

Constraints for icmps will only be added in branches that the icmp dominates (or code that an assume with an icmp dominates). The intrinsic handling was a bit special in that constraints are added unconditionally.

[nikic]

/cherry-pick c83180c 3d91d96

[llvmbot]

/pull-request #80260