[cfe-dev] Allowing checkers to mark symbols as live

[Ted Kremenek]

On Aug 9, 2010, at 6:16 PM, Jordy Rose wrote:

> I've started working on this, but I'm a little worried about "constraints
> on that symbol [being] allowed to change". Up till now symbols have been
> immutable. While it wouldn't be too hard to add a
> ClearConstraints(SymbolRef) method to ConstraintManager, I'm concerned that
> it won't be clear when to clear constraints on a symbol and when it's
> better to replace it with a new one.

I was thinking about this, and this is a very valid point.  We've been treating symbols as "immutable" values that we gradually add additional constraints.

> We could restrict constraint-clearing to these region metadata symbols,
> since they don't have a way to be replaced. But it still feels odd.

Yes it does feel odd.  Odd enough that it's probably wrong.

I guess you are right that the length is a location-sensitive symbol (similar to conjured symbols, with the creation points embedded into the symbol), but that doesn't 100% feel like the right solution either.  Whenever the string length may have changed (e.g., by a store), I suppose that would be a new symbol value to track the length.  But even that is overly conservative; the length of the string doesn't change unless you insert a null character.

At any rate, if you decide to model the extent with a new symbol, the best solution to me from the liveness perspective is to use something that is similar to a derived symbol (like SymbolExtent) that is live (at least from the perspective of SymbolManager::isLive) if the MemRegion/Symbol it derives from is live.  It could include a creation point like conjured symbols if you wanted to incorporate that information in as well, but adding that location-context unless we need it seems undesirable to me (since it artificially causes path bifurcation).