[cfe-dev] Lazy bindings

[Zhongxing Xu]

Hi Ted,

This is the patch for lazy binding.

* failed C test cases are due to bugs in RemoveDeadBindings(),
which removes constraints that is still alive. I plan to fix this
in a later patch. This patch is already messy enough.

* I wish you could help fix failed ObjC test cases, since I have
no access to the Mac development platform. It'll take some time for me
to learn basic things.

* default value of array and struct regions are not implemented
yet, because the GDM of the same type of ImmutableMap<const
Region*, SVal> is already used for region extents.

* Now Bind() methods take and return GRState* because binding could
  also alter GDM.

* No variables are initialized except those declared with initial
  values.

On Tue, Dec 16, 2008 at 9:49 AM, Zhongxing Xu <xuzhongxing at gmail.com> wrote:

>
>
> On Tue, Dec 16, 2008 at 5:22 AM, Ted Kremenek <kremenek at apple.com> wrote:
>
>>
>> On Dec 14, 2008, at 8:52 PM, Zhongxing Xu wrote:
>>
>>  Another much simplified scheme:
>>>
>>> * leave all locations uninitialized
>>> * if a location is assigned Unknown, bind it to Unknown explicitly in the
>>> bindings.
>>>
>>> Then Retrieve becomes:
>>>
>>> Retrieve (L)
>>> {
>>>  if L has binding
>>>    return L's binding
>>>  else
>>>    if L is on stack or heap
>>>      return UndefinedVal
>>>    else
>>>      return SymbolicVal
>>> }
>>>
>>> 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.
>>>
>>
>> This is a great start.  We could treat recording "UnknownVal" as the same
>> thing as putting something in the killset.
>
>
> Yeah, then Retrieve becomes:
>
> Retrieve (L)
> {
>   if (L has binding)
>     return L's binding
>   else if (L is in killset)
>       return unknown
>   else
>     if (L is on stack or heap)
>       return undefined
>     else
>       return symbolic
> }
>
>
>>
>>
>> By "heap", I assume you are referring to blocks returned by calls to
>> malloc()?
>
>
> Yes.
>
>
>>
>>
>> One thing that would be nice to eventually model is default initialization
>> for array elements and struct fields.  For example:
>>
>>  int large_buffer[2000] = { 1 }; // the rest of the elements are bound to
>> 0
>>
>> 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.
>
>
> This is cool.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20081217/a66679d9/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: lazybinding.patch
Type: application/octet-stream
Size: 50839 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20081217/a66679d9/attachment.obj>