[cfe-commits] [patch] Tracking simple arithmetic constraints (PR2695)

[Zhongxing Xu]

On Thu, Jun 10, 2010 at 3:59 PM, Jordy Rose <jediknil at belkadan.com> wrote:

>
> On Thu, 10 Jun 2010 15:49:45 +0800, Zhongxing Xu <xuzhongxing at gmail.com>
> wrote:
> > On Thu, Jun 10, 2010 at 3:41 PM, Zhongxing Xu <xuzhongxing at gmail.com>
> > wrote:
> >
> >>
> >>
> >> On Wed, Jun 9, 2010 at 8:38 AM, Jordy Rose <jediknil at belkadan.com>
> wrote:
> >>
> >>> Here's the latest version of the patch, in which the overflow logic
> has
> >>> been moved into SimpleConstraintManager and SValuator is a little more
> >>> discerning about when it should just return UnknownVal.
> >>>
> >>> I considered moving the simplification into SValuator, but haven't
> done
> >>> it
> >>> yet because of this overflow thing. Here's a (roundabout) explanation
> >>> why:
> >>>
> >>> The whole reduction currently relies on this manipulation:
> >>>  $sym + k1 == k2  <--> $sym == k2 - k1
> >>> This is always true logically, but breaks down for other operators
> with
> >>> modular arithmetic. Admittedly, ordering comparisons are less
> meaningful
> >>> in
> >>> a modular-arithmetic context, but...
> >>>
> >>> x+1 > 0 is the same as x > -1, logically -- any nonnegative integer.
> >>> However, in a modular unsigned context, this becomes x > UINT_MAX,
> which
> >>> has no solutions. This is what originally motivated the
> >>> overflow-checking
> >>> code, and just supporting disjoint ranges doesn't eliminate the need
> to
> >>> track overflow.
> >>>
> >>
> >> This example gives me this idea: handling such constraints in the
> current
> >> Simple/Range constraint manager and SValuator framework perhaps is a
> >> mistake. To correctly handle overflow, we should have a new constraint
> >> manager, which have the full ability inside to handle various overflow
> >> conditions.
> >>
> >> I suggest we complete ignore overflow cases in current constraint
> >> managers.
> >>
> >>
> >> For the x+1>0 example, the new constraint manager should solve it
> >> according
> >> to signedness of x. If x is signed, the solution should be x \in (-1,
> >> MAX_INT], if x is unsigned, the soluction is [0, MAX_UINT]
> >>
> >
> > What I mean is for constaints like x + 1 > 0, we can't use simple
> algebraic
> > equality to solve it. And that complexity should be put into a new
> > constraint manager.
>
>
> The basic logic I've been using is this:
>
> Given: (x+a) < b
> Let y = x+a
> Find the range for y>b: [MIN, b-1]
> *Shift* the range by a: [MIN-a, b-a-1].
>
> If a >= b:
>  the entire range has wrapped around to [MAX-a+1, MAX-a+b]
> else:
>  there are two ranges: [MAX-a+1, MAX] and [MIN, b-a-1].
>

Yeah, this logic is right. With this, we can get a precise range for x after
assuming such constraints. This can eliminate the usage of NetOverflow.


>
> This, while long and not particularly friendly or derivable (I had several
> false starts), is not too hard to code, and seems to be working! And more
> importantly, it's correctly modeling C behavior. I'll get it done soon.
>
> The downside, as you point out, is that it can't actually do much with:
>
> if (x+1 < length) {
>  // do something relying on x being small
> }
>
> ...since x could be (U)INT_MAX here.
>

Do you mean 'x' and 'length' are both symbolic here? We can give up for such
cases for now.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20100610/564c9828/attachment.html>