[cfe-dev] Lazy bindings

[Zhongxing Xu]

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/20081216/b5749d8e/attachment.html>