<br><br><div class="gmail_quote">On Tue, Dec 16, 2008 at 5:22 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 Dec 14, 2008, at 8:52 PM, 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;">
Another much simplified scheme:<br>
<br>
* leave all locations uninitialized<br>
* if a location is assigned Unknown, bind it to Unknown explicitly in the bindings.<br>
<br>
Then Retrieve becomes:<br>
<br>
Retrieve (L)<br>
{<br>
  if L has binding<br>
    return L's binding<br>
  else<br>
    if L is on stack or heap<br>
      return UndefinedVal<br>
    else<br>
      return SymbolicVal<br>
}<br>
<br>
The locations that are assigned unknown should not be too much, so this would not incur too much overhead. The only bindings that would be removed explicitly are those that are dead.<br>
</blockquote>
<br></div></div>
This is a great start.  We could treat recording "UnknownVal" as the same thing as putting something in the killset.</blockquote><div><br>Yeah, then Retrieve becomes:<br><br>Retrieve (L)<br>{<br>  if (L has binding)<br>
    return L's binding<br>  else if (L is in killset)<br>      return unknown<br>  else<br>    if (L is on stack or heap)<br>      return undefined<br>    else<br>      return symbolic<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;">
<br>
<br>
By "heap", I assume you are referring to blocks returned by calls to malloc()?</blockquote><div><br>Yes.<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>
One thing that would be nice to eventually model is default initialization for array elements and struct fields.  For example:<br>
<br>
  int large_buffer[2000] = { 1 }; // the rest of the elements are bound to 0<br>
<br>
Not having to bind the value '0' to elements 1...1999 would be nice, as we know that their default value is 0.  We could put this in a side map in the GDM (i.e. default_element_value: MemRegion* -> SVal).  I actually don't think this would be hard to do at all.  It also means that we scale with the number of elements referenced, not with the number declared.</blockquote>
<div><br>This is cool. <br></div></div><br>