[cfe-dev] Proposed: change tracking for RegionStore

Jordy Rose jediknil at belkadan.com
Fri Jul 30 22:42:49 PDT 2010


On Fri, 30 Jul 2010 19:05:35 -0700, Ted Kremenek <kremenek at apple.com>
wrote:
> On Jul 30, 2010, at 3:33 PM, Jordy Rose wrote:
>> 
>> And hm. How can we inject new analysis state at the level of Bind or
>> Invalidate, where only the Store is being changed? Not all
>> store-modifying
>> code goes through GRState.
> 
> 
> I think Bind and Invalidate would still work as expected, but just
return
> the list of regions that "subscribers" had said they cared about.
> 
> Bind and Invalidate, however, are only called at specific places (e.g.,
in
> GRExprEngine), and usually when one is reasoning about a GRState or
> ExplodedNode.  Does it seem plausible to try and do the callbacks after
the
> Bind/Invalidate, possibly generating new ExplodedNodes?  For example, I
can
> see this happening when evaluating a store within GRExprEngine.

I'm thinking of modeling functions, though. The only place where this is
used now is MallocChecker's fill value (admittedly, a patch from me, weeks
ago). But memset() is basically Invalidate-then-BindDefault.
OSAtomicChecker is using EvalStore, but it's not as clean as it should be.
There's no EvalFill or EvalInvalidate. Should there be?

I'm inclined to not allow new ExplodedNodes here, only a one-to-one filter
of GRStates. That is, you can change states when getting a region update,
but not bifurcate the state. This limits us to "places that call
GRState::makeWithStore", which are a manageable set. But still not at the
GRExprEngine level. I'm not thrilled with turning every bind* call into
this:

RegionSet RS = C.getEngine().GetInterestingRegions();
tie(state, RS) = state->bindLoc(L, V, RS);
C.getEngine().NoteRegionsChanged(state, RS);

Or this:

state = state->bindLoc(L, V, C.getEngine());

They both seem like they're mixing levels. But having to move these cover
methods for Bind* and friends (eight methods) up to the engine seems a
little silly. Maybe it shouldn't.



More information about the cfe-dev mailing list