Yingwei Zheng
287294d54d
[ConstraintElim] Do not allow overflows in Decomposition
( #140541 )
...
Consider the following case:
```
define i1 @pr140481(i32 %x) {
%cond = icmp slt i32 %x, 0
call void @llvm.assume(i1 %cond)
%add = add nsw i32 %x, 5001000
%mul1 = mul nsw i32 %add, -5001000
%mul2 = mul nsw i32 %mul1, 5001000
%cmp2 = icmp sgt i32 %mul2, 0
ret i1 %cmp2
}
```
Before this patch, `decompose(%mul2)` returns `-25010001000000 * %x +
4052193514966861312`.
Therefore, `%cmp2` will be simplified into true because `%x s< 0 &&
-25010001000000 * %x + 4052193514966861312 s<= 0` is unsat.
It is incorrect since the offset `-25010001000000 * 5001000 ->
4052193514966861312` signed wraps.
This patch treats a decomposition as invalid if overflows occur when
computing coefficients.
Closes https://github.com/llvm/llvm-project/issues/140481 .
2025-05-22 11:31:04 +08:00
Yingwei Zheng
aa054c6810
[ConstraintElim] Simplify and/or instead of replacing its operand ( #139874 )
...
In `checkOrAndOpImpliedByOther`, replacing an operand of a disjoint or
is unsafe: https://alive2.llvm.org/ce/z/4R4hxN
This patch performs the simplification directly, to avoid miscompilation
and unnecessary canonicalization.
Closes https://github.com/llvm/llvm-project/issues/137937 .
2025-05-14 23:37:41 +08:00
Shan Huang
f49ee00ec4
[DebugInfo][ConstraintElimination] Fix debug value loss in replacing comparisons with the speculated constants ( #136839 )
...
Fix #135736
2025-05-05 21:08:58 +08:00
Iris Shi
b54b3e81f2
Recommit "[ConstraintElim] Simplify cmp after uadd.sat/usub.sat ( #135603 )" ( #136467 )
2025-04-30 21:49:18 +08:00
Iris Shi
349dc34b46
[ConstraintElim] Fix poison check before adding intrinsic facts ( #136291 )
2025-04-30 21:46:07 +08:00
Arthur Eubanks
be9f72cf37
Revert "[ConstraintElim] Simplify cmp after uadd.sat/usub.sat ( #135603 )"
...
This reverts commit fe54d1afcca055f464840654dd2ec3fd83aea688.
Causes miscompiles, see #135603 .
2025-04-18 15:37:37 +00:00
Iris
fe54d1afcc
[ConstraintElim] Simplify cmp after uadd.sat/usub.sat ( #135603 )
...
- Closes #135557
2025-04-14 20:15:55 +08:00
Andreas Jonson
4b29c28564
[ConstraintElim] Preserve analyses when IR is unchanged. ( #128588 )
2025-02-25 14:22:55 +01:00
Andreas Jonson
6aeec5eabf
[ConstraintElim] Test for #128588
2025-02-25 12:35:05 +01:00
Marina Taylor
72768d9bb8
[ConstraintElim] Teach checkAndReplaceCondition about samesign ( #128168 )
...
`samesign upred` is equivalent to `spred`:
https://alive2.llvm.org/ce/z/57iaEC
2025-02-24 13:07:47 +00:00
Stephen Senran Zhang
7fb97bee92
[ConstraintElimination] Add eq/ne facts to signed constraint system ( #121423 )
...
Facts of eq/ne were added to unsigned system only, causing some missing
optimizations. This patch adds eq/ne facts to both signed & unsigned
constraint system.
Fixes #117961 .
2025-01-23 11:00:31 +01:00
Yingwei Zheng
003fb2aeb4
[ConstraintElim] Decompose sub nsw
( #118219 )
...
Closes https://github.com/llvm/llvm-project/issues/118211 .
2024-12-16 16:41:04 +08:00
Ramkumar Ramachandra
a22578d38c
ConstraintElim: teach fact-transfer about samesign ( #115893 )
...
When the samesign flag is present on an icmp, we can transfer all the
facts on the unsigned system to the signed system, and vice-versa: we do
this by specializing transferToOtherSystem when samesign is present.
2024-12-15 17:31:58 +00:00
Yingwei Zheng
5fa59edfa7
[ConstraintElim] Add support for trunc nsw/nuw
( #118745 )
...
Proof for `trunc nsw nneg X -> trunc nuw X`:
https://alive2.llvm.org/ce/z/ooP6Mt
2024-12-06 23:15:31 +08:00
Nikita Popov
a608607fd7
[ConstraintElim] Add support for decomposing gep nuw ( #118639 )
...
ConstraintElimination currently only supports decomposing gep nusw with
non-negative indices (with "non-negative" possibly being enforced via
pre-condition).
Add support for gep nuw, which directly gives us the necessary
guarantees for the decomposition.
2024-12-04 16:27:31 +01:00
Nikita Popov
75af62839b
[ConstraintElim] Add tests for gep nuw (NFC)
2024-12-04 13:17:02 +01:00
Florian Hahn
45ff28746f
[ConstraintSystem] Fix signed overflow in negate.
...
Use AddOverflow for potentially overflowing addition to fixed signed
integer overflow.
Compile-time impact is in the noise
https://llvm-compile-time-tracker.com/compare.php?from=bfb26202e05ee2932b4368b5fca607df01e8247f&to=195b0707148b567c674235e59712458e7ce1bb0e&stat=instructions:u
2024-12-03 21:06:36 +00:00
Nikita Popov
10223c72a9
[ConstraintElim] Use nusw flag for GEP decomposition
...
Check for nusw instead of inbounds when decomposing GEPs.
In this particular case, we can also look through multiple nusw
flags, because we will ultimately be working in the unsigned
constraint system.
2024-12-03 15:56:29 +01:00
Yingwei Zheng
0f0c0c36e3
[ConstraintElim] Extend checkOrAndOpImpliedByOther
to handle and/or expr trees. ( #117123 )
...
This patch extends `checkOrAndOpImpliedByOther` to handle and/or trees.
Limitation: At least one of the operands of root and/or instruction
should be an icmp. That is, this patch doesn't support expressions like
`(cmp1 & cmp2) & (cmp3 & cmp4)`.
Closes https://github.com/llvm/llvm-project/issues/117107 .
Compile-time impact:
http://llvm-compile-time-tracker.com/compare.php?from=69cc3f096ccbdef526bbd5a065a25c95122e87ee&to=919416d2c4c71e3b9fe533af2c168a36c7893be5&stat=instructions%3Au
2024-11-27 09:04:52 +08:00
Paul Walker
56c091ea71
[LLVM][IR] Use splat syntax when printing ConstantExpr based splats. ( #116856 )
...
This brings the printing of scalable vector constant splats inline with
their fixed length counterparts.
2024-11-21 11:21:12 +00:00
Yingwei Zheng
52361d0368
[ConstraintElim] Bail out on non-dedicated exits when adding exiting conditions ( #116627 )
...
This patch bails out non-dedicated exits to avoid adding exiting
conditions to invalid context.
Closes https://github.com/llvm/llvm-project/issues/116553 .
2024-11-18 23:41:04 +08:00
Paul Walker
38fffa630e
[LLVM][IR] Use splat syntax when printing Constant[Data]Vector. ( #112548 )
2024-11-06 11:53:33 +00:00
Florian Hahn
f58312ef56
[ConstraintElim] Add tests with exiting latch.
2024-09-10 14:45:49 +01:00
Florian Hahn
e25eb14331
[ConstraintElim] Add tests for loops with chained header conditions.
2024-09-09 14:04:17 +01:00
Yingwei Zheng
85b6aac7c2
[ConstraintElim] Fix miscompilation caused by PR97974 ( #105790 )
...
Fixes https://github.com/llvm/llvm-project/issues/105785 .
2024-08-23 16:06:00 +08:00
Poseydon42
d18ca43edc
[ConstraintElimination] Add support for UCMP/SCMP intrinsics ( #97974 )
...
This adds checks to fold calls to `ucmp`/`scmp` where a comparative
relationship between the arguments can be established.
2024-07-10 21:59:59 +02:00
Florian Hahn
5b927130b0
[ConstraintElim] Use cond from header as upper bound on IV in exit BB. ( #94610 )
...
For loops, we can use the condition in the loop header as upper bound on
the compared induction in the unique exit block, if it exists. This can
be done even if there are multiple in-loop edges to the unique exit
block, as any other exit may only exit earlier.
More generally, we could add the OR of all exit conditions to the exit,
but that's a possible future extension.
PR: https://github.com/llvm/llvm-project/pull/94610
2024-07-09 19:37:38 +01:00
Florian Hahn
798754f6c6
[ConstraintElim] Add multi-exit tests for #94610 .
...
Additional test coverage with multi-exit loops for
https://github.com/llvm/llvm-project/pull/94610 .
2024-06-28 22:29:17 +01:00
Florian Hahn
3d11b3d750
[ConstraintElim] Add test for mis-compile due to #94610 .
...
Additional test coverage for a miscompile in earlier versions of
https://github.com/llvm/llvm-project/pull/94610 .
2024-06-28 18:43:02 +01:00
Florian Hahn
b7b8d02896
[ConstraintElim] Add induction tests with different start values.
...
Extra tests for https://github.com/llvm/llvm-project/pull/94610 .
2024-06-06 15:33:24 +01:00
Florian Hahn
41d73504c9
[ConstraintElim] Add set of tests where a loop iv is used in exit.
...
Test cases inspired by
https://github.com/llvm/llvm-project/issues/90417 .
2024-06-06 13:43:55 +01:00
Florian Hahn
ba0e871db8
[ConstraintElim] Look through SExt with precond Op sge 0.
...
Look through SExt with a precondition that the operand is signed
positive.
https://alive2.llvm.org/ce/z/zvVVHj
2024-05-22 13:11:04 +01:00
Florian Hahn
8a5d51b039
[ConstraintElim] Use default depth for most calls of isNonNegative.
...
Helps to improve resuls in some cases, while being overall neutral with
respect to compile-time,
https://llvm-compile-time-tracker.com/compare.php?from=2c9b6c1b36b8185299de083c3058e0c1e7760442&to=5984b1649dc12741308089de235647cf036df95f&stat=instructions:u
2024-02-28 13:14:40 +00:00
Florian Hahn
4e9fe860d2
[ConstraintElim] Add additional sext tests with unsigned predicates.
2024-02-27 09:25:23 +00:00
Yingwei Zheng
87b1e735b2
[ConstraintElim] Decompose sext-like insts for signed predicates ( #82344 )
...
Alive2: https://alive2.llvm.org/ce/z/A8dtGp
Fixes #82271 .
2024-02-23 01:16:39 +08:00
Yingwei Zheng
8ca351d394
[ConstraintElim] Add pre-commit tests for PR82271. NFC. ( #82357 )
...
This patch adds some tests for
https://github.com/llvm/llvm-project/pull/82344 .
2024-02-20 23:28:05 +08:00
Alexander Shaposhnikov
4d8e849dfb
[ConstraintElim] Add facts for llvm.abs >= 0 ( #79070 )
...
Add facts for llvm.abs >= 0.
https://alive2.llvm.org/ce/z/GXnMHu
2024-02-06 15:16:41 -08:00
Nikita Popov
2d69827c5c
[Transforms] Convert tests to opaque pointers (NFC)
2024-02-05 11:57:34 +01:00
Yingwei Zheng
bc9c2be357
[ConstraintElim] Simplify MinMaxIntrinsic
( #75306 )
...
This patch replaces min/max intrinsic with one of its operands if
possible.
Alive2: https://alive2.llvm.org/ce/z/LoHfYf
Fixes #75155 .
2024-02-04 21:07:40 +08:00
Alexander Shaposhnikov
eb98b5003c
[ConstraintElim] Add tests for llvm.abs >= 0 ( #79068 )
...
Add tests for llvm.abs >= 0.
This is a preparation for
https://github.com/llvm/llvm-project/pull/79070 .
2024-01-29 10:45:29 -08:00
Florian Hahn
3d91d9613e
[ConstraintElim] Make sure min/max intrinsic results are not poison.
...
The result of umin may be poison and in that case the added constraints
are not be valid in contexts where poison doesn't cause UB. Only queue
facts for min/max intrinsics if the result is guaranteed to not be
poison.
This could be improved in the future, by only adding the fact when
solving conditions using the result value.
Fixes https://github.com/llvm/llvm-project/issues/78621 .
2024-01-24 14:25:55 +00:00
Florian Hahn
c83180c124
[ConstraintElim] Add tests for #78621 .
...
Tests with umin where the result may be poison for
https://github.com/llvm/llvm-project/issues/78621 .
2024-01-24 11:56:03 +00:00
Nikita Popov
ed1632b72e
[ConstraintElim] Support signed induction variables ( #77103 )
...
When adding information for induction variables, add both unsigned and
signed constraints, with corresponding signed and unsigned
preconditions.
I believe the logic here is equally valid for signed/unsigned, we just
need to add preconditions of the same type.
2024-01-08 10:00:23 +01:00
Nikita Popov
65df69619c
[ConstraintElim] Add tests for signed induction variables (NFC)
2024-01-05 15:31:59 +01:00
Nikita Popov
71f56e49ce
[ConstraintElim] Decompose shl nsw for signed predicates ( #76961 )
...
shl nsw x, shift can be interpreted as mul nsw x, (1<<shift), except
when shift is bw-1 (https://alive2.llvm.org/ce/z/vDh2xT ). Use this when
decomposing shl. The equivalent decomposition for the unsigned case
already exists.
2024-01-05 09:53:05 +01:00
Nikita Popov
db34a94710
[ConstraintElim] Add tests for shl nsw decomposition (NFC)
2024-01-04 15:13:10 +01:00
Nikita Popov
f812251875
[ConstraintElim] Use SCEV to check for multiples ( #76925 )
...
When adding constraints for induction variables, if the step is not one,
we need to make sure that (end-start) is a multiple of step, otherwise
we might step over the end value.
Currently this only supports one specific pattern for pointers, where
the end is a gep of the start with an appropriate offset.
Generalize this by using SCEV to check for multiples, which also makes
this work for integer IVs.
2024-01-04 14:04:15 +01:00
Nikita Popov
87f1cf04cd
[ConstraintElim] Add tests for int phi with non-one step (NFC)
2024-01-04 10:04:08 +01:00
Florian Hahn
3c127e83c0
[ConstraintElim] Replace NUWSub decomp with recursive decomp of ops.
...
The current patterns for NUWSub decompositions do not handle negative
constants correctly at the moment (causing #76713 ).
Replace the incorrect pattern by more general code that recursively
decomposes the operands and then combines the results. This is already
done in most other places that handle operators like add/mul.
This means we fall back to the general constant handling code (fixes the
mis-compile) while also being able to support reasoning about
decomposable expressions in the SUB operands.
Fixes https://github.com/llvm/llvm-project/issues/76713 .
2024-01-02 22:05:57 +00:00
Florian Hahn
8c7dfafa0a
[ConstraintElim] Add extra tests with chained subs.
2024-01-02 20:51:22 +00:00