<br><br><div class="gmail_quote">On Sun, Feb 22, 2009 at 2:43 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;">
<div class="Ih2E3d"><br>
On Feb 21, 2009, at 2:42 AM, 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;">
That's understandable, but I still think its not quite the right design for the broader problem.  I think we want to do is update the type information associated with the symbol, not change the symbol itself.  By conjuring up new symbols like this we are going to:<br>

<br>
I completely agree with that we should update the type information instead of creating a new symbol. But as symbols are immutable, how can we do this? A conjured symbol has three parts of information: Stmt*, QualType, and a Count. Should I take the same Stmt* and Count but with the new QualType to create the new symbol?<br>

<br>
</blockquote>
<br>
<br></div>
Hi Zhongxing,<br>
<br>
We have a variety of options, each one which we should probably discuss in some detail as I think we're going to have to make some important changes.<br>
<br>
1) Use the GDM to track symbol information.<br>
<br>
Pros: Hooks in with our existing mechanism for throwing extra information into the GRState.  It also makes symbol information path-sensitive.<br>
<br>
Cons: We need access to the GRState object to get a symbol's state, so clients would need to be changed/updated.  This is probably okay and consistent with many other kinds of meta-data we need to query.<br>
<br>
2) Use AnonTypedRegions to handle the layering of type information.<br>
<br>
This whole discussion seems to really only concern symbols that represent locations.  When symbols are scalar values, casts will require us reasoning about conversions anyway, so I think the type of those symbols will stay fixed.<br>

<br>
In your example:<div class="Ih2E3d"><br>
<br>
void* myfunc();<br>
<br>
void f13() {<br>
 char** array;<br>
 array = myfunc();<br>
 char *p = array[0];<br>
 char c = *p<br>
}<br>
<br></div>
We can have 'myfunc()' return a loc::SymbolVal with type void* for the symbol.  The cast from void* to char** gets the SymbolRegion for the symbol and then layers on top of it an AnonTypedRegion.  This is what AnonTypedRegion was designed for.  Then 'array[0]' does a lookup on the bindings to the ElementRegions of the AnonTypedRegion.<br>

<br>
A bonus of this approach is that we can nicely catch path-sensitive type errors.  For example:<br>
<br>
 char** array;<br>
 array = myfunc();<br>
 int** array2 = (void*) array;<br>
 array[0] = ...<br>
 int x = array2[0];<br>
<br>
Here the load from array2[0] is suspicious because we had a binding to an ElementRegion of the AnonTypedRegion(char**) and we are treating it as an ElementRegion of the AnonTypedRegion(int**).  This kind of reasoning, while potentially complicated, can only be done in the StoreManager since it understands how it structures regions.<br>

<br>
Pros: Works with our existing infrastructure and APIs.  Provides the flexibility to do a whole-bunch of path-sensitive type checking.<br>
<br>
Cons: We're still reasoning about loc::SymbolVal(sym) and loc::MemoryRegionVal(SymbolicRegion(sym)), two concepts which mean the same thing.  This will complicate the logic in EvalCast, the ConstraintManagers, etc.</blockquote>
<div><br>I prefer the AnonTypedRegion approach. The AnonTypedRegion appears to be the right tool to handle various abuse of the C type system. The first approach is an option when there are more and more information about a symbol to track.<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>
<br>
To address the "con" I suggest we remove loc::SymbolVal and just have loc::MemoryRegionVal(SymbolicRegion(sym)).  This is a cleanup I think we should do anyway, as it consolidates our reasoning about symbolic memory into one place.</blockquote>
<div><br>Yeah, this cleanup should be done first. Then we won't have symbolic locations. We will only have symbolic regions.<br></div></div><br>