ConstraintAnalysis: Use spans to prove things - #9025
Conversation
| if (x <= uint64_t(maxSigned)) { | ||
| // This is in the range of both signed and unsigned values, so there is | ||
| // no ambiguity. That is, we cannot convert the bit pattern | ||
| // 0xffffffff into a Span, as it might be either uint32_t(-1) | ||
| // or actually negative (but a bit pattern like 0x00000001 is | ||
| // always fine as it can only ever be "1"). | ||
| return Span<IU64>{x, x}; | ||
| } |
There was a problem hiding this comment.
It seems we could be more general here if we separately handled "signed spans" and "unsigned spans" (and disallowed mixing them in any way) rather than trying to smush them both into a single kind of span that handles both signed and unsigned numbers. The ambiguity comes from trying to handle both kinds interchangeably.
Another unambiguous approach would be to do everything in terms of unsigned spans. A signed x < 10 , for instance, could be represented as a pair of unsigned spans: [0, 9], [1 << 31, (1 << 32) - 1].
There was a problem hiding this comment.
Yes, those are other options, but I think the common case is handled well by the current code. Most constant upper bounds are within the shared range anyhow (i.e. most fixed-size arrays and such are not of length 2^31+). And, in the unambiguous range, we can support all operations, even mixed (though I admit mixing signed/unsigned might be rare).
| // is impossible after the ++). This is not possible for signed operations, | ||
| // since x++ does not prove x > 0 there (0 is not the only value that is | ||
| // <= 0). |
There was a problem hiding this comment.
But we could add x > INT_MIN if the upper bound is signed and proves there is no overflow.
There was a problem hiding this comment.
Correct, and if it comes up we could add that I guess. For unsigned, this comes up in every natural loop 0..N (while very few signed loops begin with INT_MIN).
Signed loops also include a lower bound in many cases. Like if a loop begins with an unknown initial value (from a parameter), then an unsigned bounds check is just x < len but a signed one must be x >= 0 && x < len (in unsigned the x >= 0 is "free")
| // since x++ does not prove x > 0 there (0 is not the only value that is | ||
| // <= 0). | ||
| bool hasUnsignedUpperBound = false; | ||
| bool hasUnsignedLowerBound = false; |
There was a problem hiding this comment.
We never set hasUnsignedLowerBound after this. Is it a bug, or is hasUnsignedLowerBound unnecessary? I guess it's not necessary because if there is an existing lower bound, it will subsume the new x > 0 bound.
There was a problem hiding this comment.
Good catch, I had thought to optimize compile time a bit here, but it was incomplete 😄
Yes, it works either way, as the bounds subsume.
I just removed this, as the speedup is probably not worth the code, better to be simple.
2 participants
When two constraints can be expressed as spans, see if one shows the
other is true or not.
Landing this requires improving something else, otherwise tests would
regress: we "got lucky" before and did not notice that
x >= 0wasalways true when unsigned, so we carried that around, and after
x++it turned into
x >= 1which is no longer trivial. We do need that latterconstraint, so add the following rule: when
x++andxdoes notoverflow during that addition (as proven by some bound like
x < 10)then we can add
x > 0(since it can no longer be 0 due to thex++).