Hi Jordy,
Overall this looks like stellar work. 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'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?
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>
_______________________________________________
cfe-commits mailing list
cfe-commits@cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
