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

[Jordy Rose]

(responses inline)

On Mon, 14 Jun 2010 22:33:43 -0700, Ted Kremenek <kremenek at apple.com>
wrote:
> One meta-leval observation I have
> concerns pushing the 'Adjustment' value into RangeConstraintManager and
> BasicConstraintManager respectively.  Before with RangeConstraintManager
> the implementations for AssumeSymEQ, AssumeSymNE, etc., were all
> practically identical.  Looking at the new methods, I can still see the
> commonality, but now it is pushed out it into the individual methods. 
> Similarly in BasicConstraintManager, we see the same theme; 'Adjustment'
is
> used repeatedly in the same way.

I would argue that the implementations of the AssumeSym*() methods in
RangeConstraintManager were not very uniform...it's just that all the
non-uniformity was pushed into RangeSet's Add*() methods. In this
formulation, it's reversed -- the special cases are handled in the
AssumeSym*() methods, but eventually it's the RangeSet Intersect() methods
that perform the real work.

I'll admit it's a little worse for BasicConstraintManager, since it's only
the special cases that /don't/ use the adjustment. ("$sym + constant <=
MAX", for example, which is different from "$sym <= MAX-constant".)


> I'm not certain what the right approach is here, but my gut feeling is
> that by pushing 'Adjustment' down into the specialized
> SimpleConstraintManagers we lose some flexibility to make changes later
> where we add another layer of cleverness.
> 
> The common theme I seem is that the 'Adjustment' value is used to
> "transform" the constraint values associated with a symbol.  Perhaps
> instead of passing an 'Adjustment' value, we can pass a "Transformer"
> object that transforms those constrained values into some transformed
> value.  Basically the Transformer handles the rewriting of the
constraint
> values as if we had them available to use in the SimpleSValuator.  This
way
> if we decide to add additional transformations, we can more easily push
> that logic into RangeConstraintManager/BasicConstraintManager by just
> modifying the Transformer, and not the individual ConstraintManagers
> themselves.  This is just a wild idea off the top of my head, but it
just
> seems to me that adding layer upon layer of clever hacks like this won't
> scale if we have to modify the ConstraintManagers themselves.
> 
> What do you think?

At first, I did indeed try to handle all the adjustment up front, before
hitting the AssumeSym*() methods. Then I tried subsuming the six methods
into one, which almost worked but ended up becoming a nightmare switch
statement. In the end, it seemed the original interface worked the best,
with adding the adjustment parameter.

You're right: it's completely not scalable. It's certainly useful to have
access to the value before "adjustment" or "transformation" -- that's what
allows us to short-circuit the tautological cases. But it's true that past
those cases, it's just a function applied to the value itself
(BasicConstraintManager) or the bounds of the intersection range
(RangeConstraintManager). Although some care does have to be taken for
RangeConstraintManager to handle ranges that wrap around (which is
currently done explicitly by splitting the range in two).

What I'm worried about is that this is going to be overkill for something
that may never grow beyond additive operations. That is,
RangeConstraintManager may not be the best way to handle SymSymExprs, or
even SymIntExprs with other operations in them. (The solution space for
"x%2 == 0" would have O(MAX) ranges. And a naive transformation for "x/2 >=
1" would take the range [1, MAX] and turn it into [2, MAX*2].) I suppose
right now a Transformer would just be a stack object made of a
BinaryOperator::Opcode and an APSInt value, while a later one could compose
operations. Even so, I think it may be a bit of a YAGNI case.

Well. I don't think it would be hard to alter the current code to use a
Transformer -- just change all "X - Adjustment" expressions to
"T.transform(X)". If you think it's worth it, I can go ahead and do that.
(My schedule is currently a little spotty cause I'm on vacation, so I may
not actually have that changed until Sunday.) What it won't do is remove
any complexity in the disparate AssumeSym*() methods (though allowing
wraparound ranges would). But it does allow for more possible expansion in
the future.


> On Jun 14, 2010, at 1:21 PM, Jordy Rose wrote:
> 
>> Finally revised and with better test cases.
>> 
>> Summary of changes:
>> - SimpleSValuator folds additive expressions ("$sym + k1 - k2").
>> 
>> - SimpleSValuator does not make UnknownVals everywhere it could. When
the
>> LHS is a symbol or symbolic expression, it should probably only make a
>> SymExprVal if the constraint manager actually canReasonAbout() it.
>> 
>> - SimpleConstraintManager's subclasses can now handle expressions of
the
>> form "($sym + k1) <> k2", where "<>" is a comparison operator.
>> 
>> - SimpleConstraintManager's AssumeSymREL (pure virtual) methods take an
>> extra "adjustment" parameter. This corresponds to "k1" in the above
>> expression.
>> 
>> - RangeSets (an implementation detail of RangeConstraintManager) are
now
>> narrowed down using "intersections", rather than comparison-based
>> constraints.
>> 
>> - Overflow is modeled for both unsigned and signed types.
>> 
>> - There is no special testing for true tautological expressions (x + k1
<
>> MAX).
>> 
>> - There is now a static version of
>> BinaryOperator::isAdditiveOp().<additive-folding.patch>