Optimizations can be used to eliminate unecessary overflow checks. This patch introduces some test cases where the checks can be safely removed
Reviewed By: fhahn, fcloutier
Differential Revision: https://reviews.llvm.org/D134038
f213128b29 didn't account for the possibility that the result of
decompose may be empty. Fix that by explicitly checking. Use a newly
introduced helper to also reduce some duplication.
Thanks @bjope for finding the issue!
Keep track if variables are known positive during constraint
decomposition, aggregate the information when building the constraint
object and encode the extra information as constraints to be used during
reasoning.
This patch adds a new transferToOtherSystem helper that tries to
transfer information from signed predicates to the unsigned system and
vice versa.
The initial version adds A >=u B for A >=s B && B >=s 0
https://alive2.llvm.org/ce/z/8b6F9i
Remove the early exit if both constraints contain no variables. This
restriction is unnecessayr for correctness and removing it simplifies
handling of trivial constant conditions in follow-up changes.
A first patch to use the reasoning in ConstraintElimination to simplify
sub with overflow to a regular sub, if the operation is guaranteed to
not overflow.
Reviewed By: spatel
Differential Revision: https://reviews.llvm.org/D125264
After moving the CanAdd check in c60cdb44f7 and using it for
the assume cases as well, the passed in block may not have a branch
instruction as terminator. This can trigger the assertion. Given the new
use case, it doesn't add value any longer and can be removed.
Fixes https://github.com/llvm/llvm-project/issues/54281
When decomposing constraints for unsigned conditions, we can use
negative values by zero-extending them, as long as they are less than
the maximum constraint value.
Fixes https://github.com/llvm/llvm-project/issues/54224
Add missing CanAdd check before adding a condition from an assume
to the successor blocks. When adding information from assume to
successor blocks we need to perform the same CanAdd as we do for adding
a condition from a branch.
Fixes https://github.com/llvm/llvm-project/issues/54217
This patch extends ConstraintElimination to also remove dead variables
when removing a constraint. When a constraint is removed because it is
out of scope, all new variables added for this constraint can also be
removed.
This keeps the total size of the systems much smaller, because it
reduces the number of variables drastically.
It also fixes a bug where variables where removed incorrectly.
Fixes https://github.com/llvm/llvm-project/issues/54228
This patch adds initial support for signed conditions. To do so,
ConstraintElimination maintains two separate systems, one with facts
from signed and one for unsigned conditions.
To start with this means information from signed and unsigned conditions
is kept completely separate. When it is safe to do so, information from
signed conditions may be also transferred to the unsigned system and
vice versa. That's left for follow-ups.
In the initial version, de-composition of signed values just handles
constants and otherwise just uses the value, without trying to
decompose the operation. Again this can be extended in follow-up
changes.
The main benefit of this limited signed support is proving >=s 0
pre-conditions added in D118799. But even this initial version also
fixes PR53273.
Depends on D118799.
Reviewed By: reames
Differential Revision: https://reviews.llvm.org/D118806
With this patch pre-conditions can be added to a list of constraints.
Constraints with pre-conditions can only be used if all pre-conditions
are satisfied when the constraint is used.
The pre-conditions at the moment are specified as a list of
(Predicate, Value *,Value *) tuples. This allow easily checking them
like any other condition, using the existing infrastructure.
This then is used to limit GEP decomposition to cases where we can
prove that offsets are signed positive.
This fixes a couple of incorrect transforms where GEP offsets where
assumed to be signed positive, but they were not.
Note that this effectively disables GEP decomposition, as there's no
support for reasoning about signed predicates. D118806 adds initial
signed support.
Fixes PR49624.
Reviewed By: reames
Differential Revision: https://reviews.llvm.org/D118799
Florian Hahn