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

[Jordy Rose]

On Mon, 9 Aug 2010 13:31:51 -0700, Ted Kremenek <kremenek at apple.com>
wrote:
> 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.


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.

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.

I'll keep going in this direction for now.