[cfe-dev] Lazy bindings

[Ted Kremenek]

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.

By "heap", I assume you are referring to blocks returned by calls to  
malloc()?

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.