<div class="gmail_quote">On Sat, Feb 21, 2009 at 2:06 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><div></div><div class="Wj3C7c"><br>
On Feb 20, 2009, at 1:17 AM, Zhongxing Xu wrote:<br>
<br>
</div></div><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">
If we are casting a symbolic value, make a new conjured symbol with the cast-to type.<br>
The patch is short, but it causes a lot of ObjC test cases to fail.<br>
Ted, could you please help me with this?<br>
<br></div></div>
<cast.patch>_______________________________________________<br>
cfe-commits mailing list<br>
<a href="mailto:cfe-commits@cs.uiuc.edu" target="_blank">cfe-commits@cs.uiuc.edu</a><br>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits</a><br>
</blockquote>
<br>
Hi Zhongxing,<br>
<br>
What is the motivation behind this patch?  I'm not certain what problem it solves.  </blockquote><div><br>Hi Ted, consider this code:<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>Currently clang crashes on this code. We conjured a symbol for call to myfunc() with type void*. But when we dereference<br>*p, clang expects the type of the symbol to be char**. We does nothing when casting void* to char**.<br>
This patch tries to solve this problem specifically. What I want to do essentially is to change the symbol's type when doing casting.<br>But as symbols are immutable, I just created a new symbol with the right type.<br>
<br> </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">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.<br>

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

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

<br>
void foo(int x) {<br>
  ...<br>
  if (((short) x) < 32) { ... }<br>
  ..l<br>
  if (((short) x) < 32) { ... }<br>
  ...<br>
}<br>
<br>
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).<font color="#888888"></font> </blockquote>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><font color="#888888"><br>
Ted<br>
<br>
</font></blockquote></div><br>