[cfe-dev] Proposed: change tracking for RegionStore

[Ted Kremenek]

On Jul 30, 2010, at 12:56 PM, Jordy Rose wrote:

> It's mainly an API problem as well. A StoreManager may do multiple Add()
> or Remove() calls as part of a single action, and between those actions the
> store isn't exactly in a reasonable state. For example, the old code for
> initializing an array with a string would copy each element of the string
> into the array. All that happens here is that change markers get
> redundantly cleared, but with callbacks the observer might be able to see
> the store with undefined values, or whatever.
> 
> (I haven't looked through RegionStore to see if that's actually true.)
> 
> Moving the callback up to Bind or Invalidate might work,

This is the level I was thinking of.

> but then the
> stores would have to keep track of every region touched during the call --
> annoying, but not impossible.

Not necessarily.  Instead of tracking all regions that modified, we can have a registered list of subscribers (provides as input to Bind/Invalidate) that want to know when *specific* regions (and/or their subregions) have been touched.  If there are no subscribers, then we record nothing.  If there are subscribers, we only record information for regions that they have said they care about. Most subscribers will only care about regions for which they have checker-specific state, and that set should be small.

> This could still show up during a larger
> operation, since the StoreManager doesn't know who's modifying the store.
> (It could be part of modeling a function's behavior, for example.)

That is true, and we want individual subscribers (which are probably Checkers) to have the ability to interject new analysis state (either via new GRState objects or ExplodedNodes).  Not every call to Bind/Invalidate is structured to work that way, but it could probably be done.

One thing I like about this approach is that it could be a natural extension of the Checker callback interface.

> If we can work out the right API for that, I'd be happy to switch over.
> First pass: any call that returns a new Store will call
> 
> void RegionWatcher::RegionChanged(Store NewStore, const MemRegion *MR)
> 
> for each region, and it's up to the RegionWatcher to traverse
> superclasses.

Superclasses?

> This would probably be using the logical view of regions
> rather than the internal view, which I'm still not sure is better.


Subscribers/checkers need to be StoreManager agnostic, and in the common cases they will be reasoning (with checker-specific state) about SymbolicRegions and VarRegions (or other "base" regions).  We really don't want checkers to get into the business of directly reasoning about individual array elements, as that could implicitly require discretizing the representation of the contents of the array instead of reasoning about it symbolically.