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

[Ted Kremenek]

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?