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

[Zhongxing Xu]

On Sun, Jun 6, 2010 at 11:30 AM, Jordy Rose <jediknil at belkadan.com> wrote:

>
> The design of this patch is such that it /creates/ overflow conditions,
> which are not errors. Consider a condition which reduces to (x-1 >=
> UINT_MAX), where x is unsigned. The new SimpleConstraintManager::EvalBinOp
> essentially rewrites this as (x >= UINT_MAX+1), which of course is an
> overflow for the type. This isn't an error, it's vacuously false, so we
> know that the true branch is infeasible.
>
> Similarly, if the condition comes down to ((x+2)-1 >= UINT_MAX), it's true
> iff (x >= UINT_MAX-1). The constraint manager rewrites this first to ((x+2)
> >= UINT_MAX+1) and then to (x >= UINT_MAX-1). Even though there was an
> intermediate "overflow" of UINT_MAX+1, the final constraint is still
> meaningful.
>

I understand your point. I mean we should also report such tautology
conditions to the user in some checker and re-use that results in the
following evaluation.


>
> I agree that a general overflow checker would be useful, but that's not
> what I was using it for here. None of the test cases are actually about
> true overflows.
>
>
> On Sun, 6 Jun 2010 11:04:09 +0800, Zhongxing Xu <xuzhongxing at gmail.com>
> wrote:
> > Hi Jordy,
> >
> > This patch looks good to me.
> >
> > About overflow, in the future it could be filtered in another specific
> > integer overflow checker. For example, if we have code:
> >
> >   if (x + c1 > c2) ...
> >
> > and c2 - c1 > MAX_INT, it's better to process this case in a overflow
> > checker to say that this condition could never be true and emit a
> warning
> > about it. Then abort the path or proceed as the condition indicates.
> >
> > With this integer overflow checker, the process of overflow in
> constraint
> > manager could be simpler or different. For example, we could emit
> warning
> > once an overflow occurs, and ignore their cancel out effects entirely.
> >
> > On Sun, Jun 6, 2010 at 9:01 AM, Jordy Rose <jediknil at belkadan.com>
> wrote:
> >
> >> *ping*
> >>
> >> Very basic support for handling conditions involving addition and
> >> subtraction, such as this:
> >>
> >>  char* name = malloc(1);
> >>  if (length+1 == 10) {
> >>    free(name);
> >>  }
> >>  if (length+1 == 10) {
> >>    name = malloc(1); // no-warning
> >>  }
> >>  free(name);
> >>
> >> Fixes PR2695; next on the list would be to expand this for the case in
> >> PR4550, which uses shifts. These will be harder, of course, since
> shifts
> >> and the rest of the binary operations (except XOR) destroy information.
> >>
> >> Hoping this is a reasonable way to implement this? In particular, I get
> >> the feeling that there's an easier way to perform APSInt operations and
> >> catch overflow.
> >>
> >> _______________________________________________
> >> cfe-commits mailing list
> >> cfe-commits at cs.uiuc.edu
> >> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
> >>
> >>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20100606/d6dcaa10/attachment.html>