Hi Ted,<br><br>This is the patch for lazy binding.<br><br>* failed C test cases are due to bugs in RemoveDeadBindings(),<br>which removes constraints that is still alive. I plan to fix this<br>in a later patch. This patch is already messy enough.<br>
<br>* I wish you could help fix failed ObjC test cases, since I have<br>no access to the Mac development platform. It'll take some time for me<br>to learn basic things.<br><br>* default value of array and struct regions are not implemented<br>
yet, because the GDM of the same type of ImmutableMap<const<br>Region*, SVal> is already used for region extents.<br><br>* Now Bind() methods take and return GRState* because binding could<br>  also alter GDM.<br><br>
* No variables are initialized except those declared with initial<br>  values.<br><br><div class="gmail_quote">On Tue, Dec 16, 2008 at 9:49 AM, Zhongxing Xu <span dir="ltr"><<a href="mailto:xuzhongxing@gmail.com">xuzhongxing@gmail.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;"><br><br><div class="gmail_quote"><div class="Ih2E3d">On Tue, Dec 16, 2008 at 5:22 AM, Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com" target="_blank">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><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><div><br>Yeah, then Retrieve becomes:<div class="Ih2E3d"><br><br>Retrieve (L)<br>
{<br>  if (L has binding)<br>
    return L's binding<br></div>  else if (L is in killset)<br>      return unknown<div class="Ih2E3d"><br>  else<br>    if (L is on stack or heap)<br></div>      return undefined<br>    else<br>      return symbolic<br>
}<br> </div><div class="Ih2E3d"><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><div><br>Yes.<br> </div><div class="Ih2E3d"><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><div><br>This is cool. <br></div></div><br>
</blockquote></div><br>