[enhancement][opt] Optimization opportunity: tie overflow conditions e.g. after an add, in to range analysis (overflow detection)

[cdleary]

What's hard to do? (limit 100 words)

Filing to discuss, maybe we already have some semblance of this? cc @meheff @scampanoni

It's a common pattern for people to test whether a value is zero after an add (e.g. with the value 1) has been performed to see if the value has become zero as a way of detecting overflow. Or, they test whether the sign has flipped with respect to the operands signs. We should optimize away these patterns of "overflow tests" if range analysis indicates an overflow is impossible.

(This would be slightly more direct to analyze if we canonicalized to an add-with-carry operation, but I don't think that's strictly necessary, just may make the opportunity a little more directly apparent in the IR.)

As a case study, consider converting an int32 to float as we do in the float32.x library's from_int -- for round-to-nearest even, you may need to bump the fraction based on round/sticky bits. If the fraction overflows, we may need to bump the exponent. If the exponent overflows, we have to produce NaN. However, the maximum exponent we can get based on the most set bit is 127+31=158, which means we can never overflow to inf in practice, even though we may have written that case in the source code for completeness (especially if it were parameterized for different floating point types) -- one way we might have naively detect that overflow would be to compare after the addition if the value has flipped sign -- if we know that was impossible we could optimize away that sel and condition.

Current best alternative workaround (limit 100 words)

Optimization opportunity, so not getting the optimization and relying on the underlying synthesis tool if it's within a single stage.

Your view of the "best case XLS enhancement" (limit 100 words)

We optimize away overflow detections that cannot occur.

[allight]

We already do this in at least some circumstances. EG

%%dslx --top=noover --pipeline_stages=2

fn noover(a: u8) -> (u1, u1) {
  let b = a ++ u1:0;
  let c = u8:0 ++ a;
  (b + u9:1 == u9:0, c+ u16:1 == u16:0)
}

optimizes to

package user_module

top fn __user_module__noover(a: bits[8] id=1) -> (bits[1], bits[1]) {
  ret literal.40: (bits[1], bits[1]) = literal(value=(0, 0), id=40, pos=[(0,5,2)])
}

We admittedly only run range analysis a few times so it is possible we miss this in some cases.