[cfe-commits] [PATCH] A tentative implementation of RegionStoreManager

[Ted Kremenek]

On Oct 5, 2008, at 7:27 AM, Zhongxing Xu wrote:

> A modified patch. Fixed a minor bug. Please discard the former one.
>
> On Sun, Oct 5, 2008 at 9:58 PM, Zhongxing Xu <xuzhongxing at gmail.com>  
> wrote:
> This patch implements part of RegionStoreManager. Only SetRVal() and  
> getInitialStore() method is implemented.
> The store model is implemented as a map from Region* to RVal.
> Global and parameter pointers are assumed to point to an  
> AnonTypedRegion initially, which resides in a new Unknown  
> MemSpaceRegion. Is this reasonable?
> A new field 'PointedBy' is added to AnonTypedRegion, which  
> represents the pointer variable that points to this region. Can we  
> have a better name for it? Later we have to have more information to  
> differentiate AnonTypedRegion. For example, how to differentiate  
> heap objects created at the same program point along different paths?

Hi Zhongxing,

A bunch of comments.

First, I think  my idea was to have MemRegions be immutable to keep  
with GRState being immutable.  This invokes a lot of interesting  
design issues.

First, it means that all the fields in a MemRegion stay fixed.  This  
means that the super region stays fixed (which may not be what we want  
to do).  One reason I didn't have back pointers from a super region to  
its subregions is that subregions can be added at any time, and we  
want to differentiate between one GRState having X number of  
subregions for region R and another GRState having Y number of  
subregions for a region R.

My either idea was to have regions encode minimal information that  
could be shared amongst different implementations of StoreManager.   
I'm not really certain why you wish to add a VarDecl* "pointedBy"  
field into AnonTypedRegion?  I didn't get around to commenting this  
class, but AnonTypedRegion is meant to represent a typed chunk of  
memory; it doesn't have to be pointed by a VarDecl.   It also seems to  
me that you are using AnonTypedRegion exactly the way BasicStore uses  
VarRegion.  Isn't it the same thing?  The "Anon" means anonymous; it  
means there is no name associated with this region.

There are different ways to differentiate heap objects created along  
different paths.  One is to do the same thing we do with "conjured  
symbols" and use the current block counter (i.e., look at the counter  
of how many times the current basic block has been visited along a  
given path).  Note that regions don't always need to be unique along  
different paths; all we want is that different objects along the same  
path are unique.  We actually want similar objects along different  
paths to have the same region (when possible) so that the analysis  
caches out when possible.

Another thing to consider is whether or not we need a counter in  
"VarRegion".  For example, when a variable goes out of scope, it's  
region is now invalid, but another region for the same VarDecl could  
come into existence (think about loops).  This would allow us to model  
more cases where objects point to memory that is no longer valid.

Further, there is no reason we cannot allow subclasses of VarRegion or  
AnonTypedRegion.  We would need to some tricks to get the classof()  
stuff working with subclasses of these types, but it seems doable if  
there is a need.

Looking at the design of MemRegion, we probably want:

1) Some kind of counter or other identifier we can embed in  
AnonTypedRegion.  We don't want this to be overzealous with uniquing  
AnonTypedRegions so that we still get the benefits of caching.

2) The RegionManager should probably be owned by the StoreManager, and  
all creation of regions should go through the StoreManager (which uses  
the RegionManager).  This way StoreManagers are free to manage the  
policy of the creation and use of regions.

3) Enforce a strictly functional design on MemRegions.  This  
potentially means storing more information about regions in the store  
(which can potentially be re-factored into a "RegionContext" object  
that is embedded in the store).

I have to go, but I'll try and come back with some additional comments  
later.  Overall, the ideas in your patch look very promising!

Ted
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20081005/b643a907/attachment.html>