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

[Zhongxing Xu]

On Tue, Aug 10, 2010 at 4:14 PM, Jordy Rose <jediknil at belkadan.com> wrote:
>
> On Tue, 10 Aug 2010 13:05:28 +0800, Zhongxing Xu <xuzhongxing at gmail.com>
> wrote:
>> 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.
>
> Right now if you say "this should be live", the SymbolReaper will save
> that symbol unconditionally. The trouble is what Ted originally brought up:
> that even when the associated region dies the strlen symbol will still be
> kept around. There's no way (yet) to say "this should be live if its
> associated region is live and dead otherwise".

Just as your patch, before RemoveDeadBindings, checkers mark live
symbols, SymbolReaper cache them. When SymbolReaper is queried about
the liveness of those symbols, it first check if its associated region
is alive, if so, it return true. otherwise return false.

>
> Off-the-top-of-my-head ideas to get around this include adding a callback
> for dead region sweeping and making a new symbol that lives if a parent
> region lives /and/ it's been markLive()ed. Neither of these gets rid of
> MarkLiveSymbols, though.
>
> If we wanted crawlable symbol maps, we could probably work something into
> GRStateTrait, much like how SVals allow you to iterate over the symbol refs
> in the expression.
>