higher_equal and the widen bits

[John Rose]

On Aug 26, 2010, at 12:45 PM, Tom Rodriguez wrote:

> I was using higher_equal(TypeInt::POS) to identify positive values and came across a weird bug.  I have a type which is int:>=0:www but t->higher_equal(TypeInt::POS) returns false because they have differing widen bits.  Shouldn't the widen bits be ignored in the higher_equal tests or could that create monotonicity problems?  I've written it in a more explicit fashion but it makes me suspicious of our other uses of this idiom.

The global constant TypeInt::POS is already a very wide type, in the general sense of "wide".

(FTR, "wide" here means "tends to absorb other, "narrower" types in Type::meet.  And that terminology FTR is backwards with respect to much of the literature, a fact which confuses even veteran C2-ers.  It helps if you think concretely in terms of assertion sets, which are dual to value sets.  The more assertions, the fewer values, and vice versa.  Joining a pair of types unions a pair of assertion sets, which narrows the resulting value set to the intersection of the original two value sets.)

I doubt whether it is worthwhile allowing it to be less than WidenMax.  If it is always being used as a lower/wider bound (as in the case you mention) there is no value to allowing the global constant to be less than WidenMax.

This is probably true of POS, POS1, and SYMINT also.  If they are only used as higher_equal bounds and operands to join, perhaps they should all have WidenMax instead of WidenMin bits.

(FTR, the purpose of the widen bits is to detect data flow loops in CCP which tend to create slowly sequences of slowly widening type values of the form [0..1], [0..2], [0..3], ..., [0..maxint], [minint..maxint].  This is typical with loop iteration variables, as the dataflow solver works around the loop.  The intermediate steps are probably not interesting, and the widen bits help us decide to skip most of the steps after the first few.  See TypeInt::widen.)

-- John