On Thu, Jun 10, 2010 at 3:41 PM, Zhongxing Xu <xuzhongx...@gmail.com> wrote:
> > > On Wed, Jun 9, 2010 at 8:38 AM, Jordy Rose <jedik...@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.
_______________________________________________ cfe-commits mailing list cfe-commits@cs.uiuc.edu http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
