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

[Ted Kremenek]

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>