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

[Jordy Rose]

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 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
>>
>>