New patch.<br> - A new method CheckStructBase is taking care of the creation of AnonPointeeRegion.<br> - A lightweight lvalue evaluation method is used to get the location of the base expr <br> whose store may be changed.<br>
- AnonPointeeRegion is now identified the the memregion of the pointer pointing to it.<br><br><br><div class="gmail_quote">On Wed, Dec 10, 2008 at 9:12 AM, Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com">kremenek@apple.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;">Hi Zhongxing,<br>
<br>
I like the main ideas about the patch, but I'm a little concerned about placing this logic in StoreManager::getLValueField.<br>
<br>
Do you feel that StoreManager::getLValueField should do the work for both 'x.f' and 'x->f'. That is, the latter can be rewritten as: (*x).f. It seems to me that the (*x) portion is what should lazily create the AnonPointeeRegion, and at that point do the null check. Then, getLValueField just reasons (and only reasons) about "SOMETHING.f", where SOMETHING is an SVal.<br>
<br>
The nice thing about decoupling things in this way is that:<br>
<br>
1) StoreManager::getLValueField and GRStateManager::getLValueField stay simple; they only need to reason about dot-accesses.<br>
<br>
2) GRExprEngine can do the heavy lifting of reasoning about the syntax. As I said, x->f is the same as (*x).f. There is no reason that StoreManager or GRStateManager should be reasoning about syntax in this way. Let's keep the complexity of reasoning about syntax in one place (i.e, GRExprEngine), and have the other components just reason about pure semantic operations (if possible).<br>
<br>
3) Having GRExprEngine handle the syntax allows different StoreManagers to automatically "get it right" with regards to both (*x).f and x->f if they decide to reason about fields. If we need an interface to conjure up new regions (AnonPointeeRegion), then we should add it to StoreManager.<br>
<br>
I also found the following FIXME interesting:<br>
<br>
+ // FIXME: Should also update the value of the base expr. It's no longer a<br>
+ // symbolic pointer.<br>
<br>
In what ways is it no longer symbolic? What does it mean for a region to be symbolic? A symbol is just an abstract name. If we rename the region, what would its new name be?<br>
</blockquote><div><br>This fixme is no longer relevant. GRStateManager::CheckStructBase takes care of updating the base expr value.<br><br>By 'symbolic pointer' I simply means loc::SymbolVal. If we create an AnonPointeeRegion, we should replace it with the loc::MemRegionVal of the AnonPointeeRegion.<br>
<br>I think SymbolicRegion is not involved in this problem. All regions we deal with here are concrete. Only their bindings may be loc::SymbolVal.<br> </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>
We should probably put some more effort into defining the concept of a symbolic region. Also, if we were to alpha-rename a region, we would need to do it throughout the entire state (environment, store, and gdm). Renaming/replacing regions in a GRState once we start using them is something that will be challenging to do, and we should think about whether or not it is necessary.<div>
<div></div><div class="Wj3C7c"><br>
<br>
On Dec 9, 2008, at 5:14 AM, Zhongxing Xu wrote:<br>
<br>
</div></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div><div></div><div class="Wj3C7c">
Conditionally expand a symbolic pointer into a pointer to a real struct. In the following code,<br>
<br>
struct x {<br>
int partno;<br>
};<br>
int foo(struct x *pt)<br>
{<br>
int found;<br>
if(pt->partno != 1) {<br>
found = 0;<br>
}<br>
if(pt->partno == 1 || !found) {<br>
return 1;<br>
}<br>
return 0;<br>
}<br>
<br>
when we visit pt->partno, an AnonPointeeRegion is created lazily for pt. Moreover, only when pt is feasible not null, the region is created. This fixes PR2304.<br></div></div>
<expand.patch>_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@cs.uiuc.edu" target="_blank">cfe-dev@cs.uiuc.edu</a><br>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev</a><br>
</blockquote>
<br>
</blockquote></div><br>