Now we use a GDM to map a symbol to its concretized region. We no longer need the base struct pointer to be an lvalue. It only need to be a symbolic value.<br><br>Known problem: we need a way to iterate over live symbols, otherwise the values of AnonPointeeRegions will be swept.<br>
<br><div class="gmail_quote">On Thu, Dec 11, 2008 at 2:14 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><div></div><div class="Wj3C7c"><br><br><div class="gmail_quote">On Thu, Dec 11, 2008 at 1:54 PM, Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com" target="_blank">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;">
<div><br>
On Dec 10, 2008, at 8:06 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;">
Thanks for your comments. They were helpful. Now the interfaces get simplified a lot. Variables and functions are commented well.<br>
<br>
Here I explain the main idea.<br>
<br>
Some struct base is not mutable, e.g., struct s a; a.f = 3; Here the struct base 'a' is not mutable. But some can, e.g.,<br>
<br>
void foo(struct s* p) {<br>
  p->f = 3<br>
}<br>
<br>
When we getInitialStore(), p is initialized to have value loc::SymbolVal, which I call a symbolic pointer. (Note: here no symbolic region is involved).<br>
<br>
In this patch we try to concretize the struct pointer p. We have several preconditions for this concretization:<br>
 - the struct base is a pointer<br>
 - the pointer is symbolic<br>
 - the pointer is an lvalue, so that it can be modified.<br>
<br>
When concretizing the struct base pointer, we pass the pointer's location to StoreManager. Therefore the pointer should be an lvalue and has a location. We get this location by calling<br>
GRExprEngine::getBasePtrLoc(). This method only handles a few cases. In other cases, BasePtrLoc is left Undefined intentionally.<br>
</blockquote>
<br></div>
Hi Zhongxing,<br>
<br>
The patch is looking great, but I still have some concerns about the overall approach.  Consider your example with one modification:<div><br>
<br>
void foo(struct s* p) {<br></div>
  struct s* q = p;<br>
  p->f = 3<br>
}<br>
<br>
After evaluating 'p->f' p will bind to an AnonPointeeRegion, but 'q' will bind to the original symbol.  They are aliases.  It gets arbitrarily worse if the value of 'p' is stored in other places, passed to functions, etc.<br>


<br>
This overall approach feels a little "destructive."  We're losing information here.  After evaluating 'p->f' we've lost the fact that 'p' *still* binds to the value at the entry to the function.<br>


<br>
I see this as being fundamental problematic for four reasons:<br>
<br>
(1) Different analyses may attach information (perhaps using the GDM) to a symbolic value.  Actually replacing a symbolic value with something "concrete" loses that information.<br>
<br>
(2) Consider function summaries.  We don't have them yet, but  basically we would build up a set of constraints and effects in terms of the input to the function.  That input is the symbolic values.  Even if we "concretize" them we need to keep them around.<br>


<br>
(3) Aliasing (i.e., the example I gave).  Concretization via replacing loses this critical information.<br>
<br>
(4) The BugReporter "module" needs to reconstruct information from the ExplodedGraph, including when aliasing relationships come into effect, etc.  Blowing away the original value of 'p' makes this difficult at best.<br>


<br>
The only way to replace a symbolic value with a concrete value is to alpha-rename it throughout the entire state.  This isn't trivial, especially when one considers the GDM.<br>
<br>
I honestly think we need to take a "layered" approach.  Keep a map on the side from "symbols" to concrete values.  That's basically what we do in ConstraintManager when it comes to equality relationships with integers.  Equality relationships with integers is a form of concretizations; that's all were basically doing here, except we're reasoning about the concretization of the heap.<br>


<br>
What do you think?  I have specific comments about your patch (which is looking great!) but I will defer them until we iterate more on this design point.<br><font color="#888888">
<br>
Ted<br>
</font></blockquote></div><br></div></div>Thanks for bringing up these issues. I agree that we should keep the original symbolic value around, and do the conretization with a side mapping. I'll try to implement the idea and see what problems would come up.<br>

</blockquote></div><br>