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

[Zhongxing Xu]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20100610/340a89d1/attachment.html>