<div dir="ltr"><br><br><div class="gmail_quote">On Wed, Oct 8, 2008 at 2:00 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;">
<br>
On Oct 6, 2008, at 11:49 PM, Zhongxing Xu wrote:<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Could you show me an example where the same VarDecl should bind to different region during one analysis path?<br>
</blockquote>
<br>
Hopefully here is a better example to illustrate the point I was trying to make.<br>
<br>
Consider:<br>
<br>
int *p = 0;<br>
<br>
for (...) {<br>
  if(some_condition) {<br>
   int j = foo();<br>
   if (p) (*p)++;<br>
   p = &j;<br>
 }<br>
}<br>
<br>
This is a very contrived example, but the point is that the variable 'j' goes out of scope at the end of the true block for if(some_condition), but 'p' still refers to the VarRegion for 'j'  (which at that point is invalid).<br>

<br>
Upon entry to if(some_condition) on a subsequent iteration of the loop, what should we do?  If we have one VarRegion for 'j', then the expression '(*p)++' will appear valid, even though it really refers to the 'j' on a previous loop iteration.  </blockquote>
<div><br>I think there is no such "j on a previous loop iteration". 'j' just represents a fixed memory block on the stack, except this block is reclaimed (shrink the stack) when we exit the true  branch. Whenever we enter the true branch, 'j' will represent the same memory block.<br>
 </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">By coincidence, the value of &j may be the same across loop iterations, but that isn't guaranteed to be the case. </blockquote>
<div><br>I think this is guaranteed to be the case by the C semantics.<br><br>The thing we should do is: when we exit the true branch (or more generally a scope), we mark all local regions as invalid. Next time we enter the scope, we reget them and mark as valid. This validity property is associated with MemRegions only, has nothing to do with VarDecl and mappings. <br>
<br>Once the VarRegion of 'j' is marked as invalid, any dereference of 'p' can be recognized as illegal automatically if 'p' still points to that region. Next time when we enter the scope and meet DeclStmt of 'j', the region is marked as valid again, then '*p' is legal again.<br>
<br>The point here is that 'j' really represents the same memory block whenever we have 'j' in scope. <br> <br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
 This is also poor programming, since 'p' refers to garbage as soon as the compound statement for if(some_condition) finishes.<br>
<br>
There are potentially other solution than having multiple VarRegions.   </blockquote><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">We could potentially fix up all the old bindings to &j after j goes out of scope to point to an invalid region.</blockquote>
<div><br>I don't think we need to fix up all bindings explicitly. We just mark the VarRegion of 'j' as invalid, and do some check when evaluate '*p'.<br> </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
  This seems a little cumbersome, and it also causes us to lose some information that can be cumbersome to recover. (i.e., the region 'p' points to is now invalid, but what region did it point to originally?)<br>
<br>
The only reason I'm bringing this up now is not that we have to implement flexible bindings for VarDecl* -> VarRegions right now (if that indeed is what we decide to do), but that the interface for getLVal(VarDecl*) and getRegion(VarDecl*) that is exposed in GRStateManager and StoreManager probably should take some extra parameters (e.g., const GRState*) to provide some context in case the StoreManager/RegionManager wishes to allow flexible bindings.<br>

</blockquote></div><br></div>