<br><br><div class="gmail_quote">On Wed, Jun 9, 2010 at 8:38 AM, 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;">
Here's the latest version of the patch, in which the overflow logic 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 done it<br>
yet because of this overflow thing. Here's a (roundabout) explanation 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 with<br>
modular arithmetic. Admittedly, ordering comparisons are less meaningful 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, which<br>
has no solutions. This is what originally motivated the overflow-checking<br>
code, and just supporting disjoint ranges doesn't eliminate the need to<br>
track overflow.<br></blockquote><div><br>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. <br>
<br>I suggest we complete ignore overflow cases in current constraint managers. <br><br>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]<br>
</div></div>