<br><br><div class="gmail_quote">On Thu, Jun 10, 2010 at 3:59 PM, Jordy Rose <span dir="ltr"><<a href="mailto:jediknil@belkadan.com">jediknil@belkadan.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<br>
On Thu, 10 Jun 2010 15:49:45 +0800, Zhongxing Xu <<a href="mailto:xuzhongxing@gmail.com">xuzhongxing@gmail.com</a>><br>
<div><div></div><div class="h5">wrote:<br>
> On Thu, Jun 10, 2010 at 3:41 PM, Zhongxing Xu <<a href="mailto:xuzhongxing@gmail.com">xuzhongxing@gmail.com</a>><br>
> wrote:<br>
><br>
>><br>
>><br>
>> On Wed, Jun 9, 2010 at 8:38 AM, Jordy Rose <<a href="mailto:jediknil@belkadan.com">jediknil@belkadan.com</a>><br>
wrote:<br>
>><br>
>>> Here's the latest version of the patch, in which the overflow logic<br>
has<br>
>>> been moved into SimpleConstraintManager and SValuator is a little more<br>
>>> discerning about when it should just return UnknownVal.<br>
>>><br>
>>> I considered moving the simplification into SValuator, but haven't<br>
done<br>
>>> it<br>
>>> yet because of this overflow thing. Here's a (roundabout) explanation<br>
>>> why:<br>
>>><br>
>>> The whole reduction currently relies on this manipulation:<br>
>>>  $sym + k1 == k2  <--> $sym == k2 - k1<br>
>>> This is always true logically, but breaks down for other operators<br>
with<br>
>>> modular arithmetic. Admittedly, ordering comparisons are less<br>
meaningful<br>
>>> in<br>
>>> a modular-arithmetic context, but...<br>
>>><br>
>>> x+1 > 0 is the same as x > -1, logically -- any nonnegative integer.<br>
>>> However, in a modular unsigned context, this becomes x > UINT_MAX,<br>
which<br>
>>> has no solutions. This is what originally motivated the<br>
>>> overflow-checking<br>
>>> code, and just supporting disjoint ranges doesn't eliminate the need<br>
to<br>
>>> track overflow.<br>
>>><br>
>><br>
>> This example gives me this idea: handling such constraints in the<br>
current<br>
>> Simple/Range constraint manager and SValuator framework perhaps is a<br>
>> mistake. To correctly handle overflow, we should have a new constraint<br>
>> manager, which have the full ability inside to handle various overflow<br>
>> conditions.<br>
>><br>
>> I suggest we complete ignore overflow cases in current constraint<br>
>> managers.<br>
>><br>
>><br>
>> For the x+1>0 example, the new constraint manager should solve it<br>
>> according<br>
>> to signedness of x. If x is signed, the solution should be x \in (-1,<br>
>> MAX_INT], if x is unsigned, the soluction is [0, MAX_UINT]<br>
>><br>
><br>
> What I mean is for constaints like x + 1 > 0, we can't use simple<br>
algebraic<br>
> equality to solve it. And that complexity should be put into a new<br>
> constraint manager.<br>
<br>
<br>
</div></div>The basic logic I've been using is this:<br>
<br>
Given: (x+a) < b<br>
Let y = x+a<br>
Find the range for y>b: [MIN, b-1]<br>
*Shift* the range by a: [MIN-a, b-a-1].<br>
<br>
If a >= b:<br>
  the entire range has wrapped around to [MAX-a+1, MAX-a+b]<br>
else:<br>
  there are two ranges: [MAX-a+1, MAX] and [MIN, b-a-1].<br></blockquote><div><br>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.<br>
 </div><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<br>
This, while long and not particularly friendly or derivable (I had several<br>
false starts), is not too hard to code, and seems to be working! And more<br>
importantly, it's correctly modeling C behavior. I'll get it done soon.<br>
<br>
The downside, as you point out, is that it can't actually do much with:<br>
<br>
if (x+1 < length) {<br>
  // do something relying on x being small<br>
}<br>
<br>
...since x could be (U)INT_MAX here.<br></blockquote><div><br>Do you mean 'x' and 'length' are both symbolic here? We can give up for such cases for now. <br></div></div><br>