[cfe-commits] [patch] cast SymbolVal

[Zhongxing Xu]

On Sat, Feb 21, 2009 at 2:06 AM, Ted Kremenek <kremenek at apple.com> wrote:

>
> 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.


Hi Ted, consider this code:
void* myfunc();

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

Currently clang crashes on this code. We conjured a symbol for call to
myfunc() with type void*. But when we dereference
*p, clang expects the type of the symbol to be char**. We does nothing when
casting void* to char**.
This patch tries to solve this problem specifically. What I want to do
essentially is to change the symbol's type when doing casting.
But as symbols are immutable, I just created a new symbol with the right
type.



> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20090221/aef9b316/attachment.html>