[cfe-commits] [patch] cast SymbolVal

[Ted Kremenek]

On Feb 20, 2009, at 1:17 AM, Zhongxing Xu wrote:

> If we are casting a symbolic value, make a new conjured symbol with  
> the cast-to type.
> The patch is short, but it causes a lot of ObjC test cases to fail.
> Ted, could you please help me with this?
>
> <cast.patch>_______________________________________________
> cfe-commits mailing list
> cfe-commits at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits

Hi Zhongxing,

What is the motivation behind this patch?  I'm not certain what  
problem it solves.  When we lose analysis precision we automatically  
generate new conjured symbols at any location where we bind to a  
MemRegion (which ultimately is the only place where tracking a named- 
but-unknown value is useful).  Also, I believe that fundamentally this  
isn't the right approach for capturing improving the analyzer's  
reasoning of basic program semantics.

For symbols that are locations (loc::SymbolVal), I think pointer-to- 
pointer casts should *not* create a new symbol as the location value  
has not changed. This is why the Objective-C tests fail, as it is  
perfectly legal to cast a pointer between a C type and its Objective-C  
equivalent.  More generally pointer-to-pointer casts should pass the  
loc::SymbolVal through because after all the pointer itself has not  
changed, just it's interpretation.  We can flag type system warnings  
if you wish, but conjuring a new symbol just loses information and  
doesn't gain any.

For casts involving integer promotions or truncations (where currently  
the tracked symbol gets "lost") one possibility is to extend SVals  
with a "promotion" value that wraps a symbol.  For example:

void foo(int x) {
   ...
   if (((short) x) < 32) { ... }
   ..l
   if (((short) x) < 32) { ... }
   ...
}

We currently don't handle this well because the conversion to a short  
causes us to evaluate '(short) x' to UnknownVal.  For this I think  
we'll probably need a new SVal that represents an integer conversion.   
Then we'll need to model integer conversions explicitly in the  
ConstraintManagers (those that cannot handle them can treat them as  
UnknownVal).  In the above example, if we take the true branch at the  
first condition we know something very specific about the lower 16  
bits of x (as well as its signedness) and nothing about the upper 16  
bits.  I know this is going to be potentially hard to model, but I  
think it is the only way to handle these cases (conjuring a new symbol  
won't help at all).

Ted