[LLVMdev] GSoC - Range Analysis

[Victor Campos]

> can you please clarify whether the pass only looks at operations with the
> nsw flag (and bails out on others), or just assumes that there is no wrapping
> behaviour anywhere.

It handles operations in the same way regardless of nsw flag.

>
> Another excellent use for range analysis would be to warn about signed operations that will definitely overflow.

Good idea. I'll include your suggestion in my proposal.

> Is this really true?  For example, suppose you know that X is in the range
> [1, +inf], and now you calculate Y = 1 / X, then you get that Y is in the
> range [0, 1].  But there is no guarantee that Y is really in that range:
> since X might have overflowed it might for example be equal to -1, in which
> case Y would be equal to -1 too, outside the range [0, 1].  In short, I doubt
> you can conclude that a variable Y is really in a range [c1, c2] just from the
> information that c1 > -inf and c2 < +inf.  I think you also need to look at the
> history of how you got there.


Duncan, you are right. We thought that we were treating all the
possible cases where we could get an overflow (we handle 18 bitcodes),
but we forgot this bug in division. But I think that after fixing it,
we can still provide an implementation of range analysis that ensures
that [c1, c2], c1, c2 in Z indicate that an overflow did not happen to
arrive in this variable. What do you think? There are only 18
instructions that produce good intervals, so we should be able to
prove that a safe implementation is free of overflows in integer
limits.
  Even if we use a different domain, say, rings (the module domain),
it seems rather tricky to me to handle overflows conservatively. Could
any of you recommend us any papers that deal with the wrapping
semantics of integer arithmetics in the context of range analysis? We
here also agree that we should do something more effective to deal
with integer overflows. So far, we want to ensure that all the integer
limits, e.g., [c1, c2], c1, c2 in Z are free of overflows. We thought
that we were doing it, but there are still some bugs to treat in the
analysis, as Duncan has pointed. One problem is that in order to give
this kinds of guarantees, the analysis becomes more conservative than
we wish it would have to be.