<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On Oct 5, 2008, at 7:27 AM, Zhongxing Xu wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">A modified patch. Fixed a minor bug. Please discard the former one.<br><br><div class="gmail_quote">On Sun, Oct 5, 2008 at 9:58 PM, Zhongxing Xu <span dir="ltr"><<a href="mailto:xuzhongxing@gmail.com">xuzhongxing@gmail.com</a>></span> wrote:<br> <blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div dir="ltr">This patch implements part of RegionStoreManager. Only SetRVal() and getInitialStore() method is implemented.<br> The store model is implemented as a map from Region* to RVal.<br>Global and parameter pointers are assumed to point to an AnonTypedRegion initially, which resides in a new Unknown MemSpaceRegion. Is this reasonable?<br> 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?<br> </div> </blockquote></div></div></blockquote></div><br><div>Hi Zhongxing,</div><div><br></div><div>A bunch of comments.</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div><div>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.</div><div><br></div><div>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.</div></div><div><br></div><div>Looking at the design of MemRegion, we probably want:</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>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).</div><div><br></div><div>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!</div><div><br></div><div>Ted</div></body></html>