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

[Jordy Rose]

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

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.