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

[Zhongxing Xu]

On Tue, Aug 10, 2010 at 12:50 PM, Ted Kremenek <kremenek at apple.com> wrote:
> On Aug 9, 2010, at 9:30 PM, Jordy Rose wrote:
>
>> How can you kill such a symbol, though? If we keep immutable symbols
>> around until their associated regions die, and the string length gets
>> invalidated and requested several times, we end up with several dead
>> symbols that are still tied to a live region.
>>
>> (I'm not objecting to finding a better solution than MarkLiveSymbols, just
>> trying to bring up all the requirements. The current scheme has the problem
>> that the checker doesn't know when the symbols /should/ die.)
>
> Thanks Jordy, I think I understand now.   If I understand things correctly, the problem here is that RemoveDeadBindings only crawls the Environment and the Store.  This extra symbol is not referenced in either, but instead only lives in the GDM (which records the symbol currently used to represent the string length).  So the purpose of MarkLiveSymbols is to find symbols that were not covered by either.  Not having MarkLiveSymbols only worked if we only used a single symbol to represent the string length (in which case a side map in the GDM isn't necessary), instead of having different symbols.
>
> In that case, I'd be fine with adding MarkLiveSymbols, as long as the mechanism to determine whether or not a symbol was dead was done by SymbolReaper and SymbolManager, and not logic specific to the Checker.  Basically, MarkLiveSymbols allows GRExprEngine to crawl the set of symbols that could be live/dead, and no more.  As we evolve our APIs, and possibly make the GDM a little less opaque, it would be nice that "symbol maps" in the GDM were just automatically crawled instead of the Checker having to implement boilerplate like this.
>
> @Zhongxing: what do you think?

Exactly.  We want to keep symbols immutable, and this requires the
checker to generate multiple symbols to associated with a region. The
liveness of these symbols are determined by two components: the
checker knows which is the current symbol; the symbol reaper knows
whether the symbol's associated region is still live.

So MarkLiveSymbols only let the checker say 'I think these symbols
should be live', nothing more. It's still the symbol reaper to decide
the symbol liveness.