**Motivation**

Our optimizer does a lot of work trying to eliminate branches by condition line `x < y`

basing on some dominating facts from branches/assumes/guards. Currently, a lot of work like this is done through SCEV implication engine. However, it has its downsides, at least:

- It is known to be embarassingly slow. Each branch makes a query that traverses up the dominator tree, and each query may trigger a non-linearly-growing chain of queries required to prove it. It’s hard to evaluate overall complexity, but it’s huge.
- Current implementation mostly focuses on checks against loop induction variables and ignores vast majority of other checks. Details here: Why not eliminate range checks for non-indvars?
- We can only infer facts from one dominating check. However, sometimes the fact we need is implied by a set of dominating conditions. Example is here: [SCEV] Missing implication opportunity: cannot infer inequality from 2 guarding conditions · Issue #58074 · llvm/llvm-project · GitHub

Overall, the motivating example is following: we want to prove that `x < val_n`

from dominating conditions like:

```
x <= val_1
val1 < val_2
val2 <= val_3
...
val_(n-1) <= val_n
```

Note that to prove `<`

, it is enough that one of the known condition is `<`

and all others can be `<=`

. For proving `x <= val_n`

, all of them can be `<=`

.

We also want it to work for any values (not just induction variables) and have a reasonable cost in terms of compile time.

**Proposal**

We can have a pass that does the following:

- Stores a partially ordered set (POS) of values known by the basic block entry*. This set is a graph, where nodes are values and edges between
`x`

and`y`

exists if it’s known that the block entry is guarded by fact`x < y`

or`x <= y`

(edges are marked by exact predicate). - In the entry block, the set is empty
- If a block has one predecessor, and it has terminator like
`x < y`

, then POS of current block is POS of its predecessor united with fact`x < y`

from its terminator - For any other block, POS is a POS of its immediate dominator, or intersection of POSes of its predecessors (which is a bit harder to implement).
- We traverse blocks in RPOT and analyze their conditional branch terminators.

We try to prove it can be eliminated. Imagine the terminator is`x <= y`

. If our graph contains a path from`x`

to`y`

, it can be replaced with`if (true)`

. Alternatively, try to prove`x > y`

by finding a path from`y`

to`x`

that contains at least one`<`

(other can be`<=`

), and if so, replace with`if (false)`

. - If we coudn’t prove either, we continue. The condition from the branch will be added to POS’es of its successors.

- facts may not only become known on entry, but also somewhere in the middle because of
`llvm.experimental.guard`

and`llvm.assume`

, but let’s omit this for simplicity of explanation

**Complexity**

Let `N`

be number of basic blocks. RPOT traversal is `O(N)`

, on each predicate we need to find a path in the graph. The graph has at most `N`

edges (no more than one from each preceding block), so overall complexity is `O(N * N)`

.

Ideologically, it looks similar to GVN but for comparison graphs.

Thoughts?