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

[Ted Kremenek]

On Aug 9, 2010, at 1:14 PM, Jordy Rose wrote:

>> As long as the SymbolicRegion 'SR' is live, the symbol representing the
>> extent should be live.  In your example, 'x' binds to a SymbolicRegion. 
>> Since 'x' is live, so is that binding, and thus so is the symbol
>> representing the extent.  If this not working?
> 
> No, it's just that the extent usually isn't the string length.

Ah right.

> For this
> definition the strlen and extent are clearly different.
> 
> char x[5] = "abc"
> 
> In addition, information about string lengths is easily invalidated (hence
> the motivation for ProcessRegionChange), while extents stay constant for
> the entire life of the region. So SymbolExtent would have to be modified to
> be suitable for this.

You are right that the length of a string can change over time, but I think we can still represent them in a way similar to SymbolExtent.  I still don't believe that we need different symbols to represent the string length, but rather that the constraints on that symbol are allowed to change.

>From SymbolManager::isLive()'s perspective, how about allowing a "checker-defined" derived symbol that is either based on a symbol or a MemRegion.  It can then have an associated checker "tag" (like we do for tagging ExplodedNodes).  The tag would be used to distinguish different kinds of derived symbols, but SymbolManager would keep the symbol live as long as the thing it is derived from is live.  Would that work?

Note that this approach also allows us to model SymbolExtents as just a special case, with a reserved "tag" representing extents.