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

[Zhongxing Xu]

I'm inclined to Jordy's original proposal that Checkers should be able
to control some symbols that only they know what the symbol means,
when the symbol dies.

The benefit is that symbols still remains what it is: a representation
of a value generated somewhere, and immutable. The checker could
generate a symbol to represent what it thinks representing the length
of the string, and next time when it change its mind, it can generate
a new symbol, and mark the old one dead. This seems very natural to
me. And it won't pollute the state with unnecessary symbols, because
it knows exactly when the symbol is live and dead.

On Tue, Aug 10, 2010 at 1:15 AM, Ted Kremenek <kremenek at apple.com> wrote:
> Hi Jordy,
>
> I have mixed feelings about adding this, and I think this needs strong justification.  Why is it needed?  What symbols do we need to keep around that aren't related to live regions, or the values bound to live regions?  Right now symbols can indicate that they are derived from other symbols (or are related to regions), and their liveness is extended if they thing they derive from is also live.  If a symbol is no longer live, why do we need to continue tracking state?
>
> My concern about adding this is that it artificially will extend the lifetime of symbols, causing the GRState to accumulate extra state that defeats state caching.  The current set of checkers already do a bad job of removing stale data from the GDM for dead symbols.

Why? Checkers get informed by callback EvalDeadSymbols().

>
> Also, from the way you've implemented the callback, the checkers will be called before the state is crawled by RemoveDeadBindings.  This means that a Checker basically gets to unconditionally mark a symbol as live regardless of whether or not the rest of the analysis would mark the symbol live.  That seems too unconditional to me.  It also extends the lifetime of other derived symbols that would otherwise get pruned from the state.
>
> On Aug 8, 2010, at 1:20 PM, Jordy Rose wrote:
>
>> The last bit of infrastructure I'd like to add for CStringChecker: the
>> ability for checkers to mark symbols live. This lets checkers use conjured
>> symbols for data that lives in the GDM, rather than in the store. This
>> doesn't affect EvalDeadSymbols.
>>
>> I think it's pretty straightforward, but since it's another new callback I
>> figured it was worth waiting for comments before committing. (When we work
>> out a general mechanism for checker caching we can make this a cached
>> callback.)<MarkLiveSymbols.patch>_______________________________________________
>> cfe-dev mailing list
>> cfe-dev at cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev
>
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev
>