[cfe-commits] [patch] cast SymbolVal

[Ted Kremenek]

On Feb 21, 2009, at 2:42 AM, Zhongxing Xu wrote:

> 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:
>
> 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?
>


Hi Zhongxing,

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.

1) Use the GDM to track symbol information.

Pros: Hooks in with our existing mechanism for throwing extra  
information into the GRState.  It also makes symbol information path- 
sensitive.

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.

2) Use AnonTypedRegions to handle the layering of type information.

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.

In your example:

void* myfunc();

void f13() {
  char** array;
  array = myfunc();
  char *p = array[0];
  char c = *p
}

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.

A bonus of this approach is that we can nicely catch path-sensitive  
type errors.  For example:

  char** array;
  array = myfunc();
  int** array2 = (void*) array;
  array[0] = ...
  int x = array2[0];

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.

Pros: Works with our existing infrastructure and APIs.  Provides the  
flexibility to do a whole-bunch of path-sensitive type checking.

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.

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.