mirror of
https://github.com/RPCS3/llvm-mirror.git
synced 2025-01-31 20:51:52 +01:00
c35a8829f6
When we need to prove implication of expressions of different type width, the default strategy is to widen everything to wider type and prove in this type. This does not interact well with AddRecs with negative steps and unsigned predicates: such AddRec will likely not have a `nuw` flag, and its `zext` to wider type will not be an AddRec. In contraty, `trunc` of an AddRec in some cases can easily be proved to be an `AddRec` too. This patch introduces an alternative way to handling implications of different type widths. If we can prove that wider type values actually fit in the narrow type, we truncate them and prove the implication in narrow type. Differential Revision: https://reviews.llvm.org/D89548 Reviewed By: fhahn