[llvm-branch-commits] [llvm] [DA] Add option to run only SIV routines (PR #157084)

[Ryotaro Kasuga via llvm-branch-commits]

kasuga-fj wrote:

Backgrounds:

DA uses SCEV to represent and solve mathematical inequalities, such as:

$$a x + b y < c x + d  y$$

To solve this, equation transformations (e.g., transposition) are applied, resulting in:

$$(a - c) x + (b - d) y < 0$$

However, the terms $(a - c)$ and/or $(b - d)$ can overflow, potentially leading to incorrect results (to clarify, DA uses `ScalarEvolution::isKnownPredicate` to compare both sides of the inequality). In general, I believe it's quite difficult to prove that such overflows won't occur.

Given this, I'm starting to think that ScalarEvolution may not be an appropriate framework for handling these inequalities. To address them correctly, I believe we need to implement at least some kind of wrapper around SCEV and stop relying on `ScalarEvolution::isKnownPredicate`, which would require non-trivial effort.

https://github.com/llvm/llvm-project/pull/157084