Re: Add overflow infinity handling to VRP

[Zdenek Dvorak <rakdver at atrey dot karlin dot mff dot cuni dot cz>]

Hello,

> > > VRP currently uses TYPE_MAX_VALUE and TYPE_MIN_VALUE as infinity.
> > > However, it is somewhat vague about the notion of overflow.  For
> > > example, if a range has a max of TYPE_MAX_VALUE, and VRP subtracts 1,
> > > the max will become TYPE_MAX_VALUE - 1.  That is not appropriate if
> > > the max was set to TYPE_MAX_VALUE due to a signed overflow.  (It is
> > > also possible that this might lead VRP to an incorrect conclusion in
> > > some cases, although I didn't try to prove that.)
> > 
> > What VRP is doing is treating an overflow as a saturtation rather than
> > pegging it to a specific value which is what your patch does.
> > Saturation is actually the normal way of treating signed type overflow
> > rather than wrapping so you are treading a standard way for a non
> > standard way which is worse than the current behavior I think.
> 
> That makes no sense to me.  No common processor saturates on signed
> overflow.  All common processors wrap on signed overflow.
> 
> Moreover, it's not really accurate to imply that VRP currently models
> signed overflow as saturation.  VRP currently does not distinguish
> TYPE_MAX from an overflow value.  That is not the same as saturating,
> because VRP also uses TYPE_MAX to represent values that increase
> steadily during loops.

what exactly is the difference between saturation and the current
behavior?  If I understand things correctly, saturation is exactly
what we do now -- replacing everything larger than MAX by MAX, and
not further treating the value in any special way.

I also do not quite understand what gains do you expect from this
change.  You cannot reasonably expect to get anything useful for issuing
warnings, as a large part of the ranges vrp uses are half-ranges (obtained
from checks like a > 0), and almost any operation on half-ranges will
create such infinities.

Zdenek