[cfe-dev] [static analyzer] Sval evaluation to LazyCompoundVal

[Ted Kremenek]

It’s an optimization in the analyzer.  A CompoundVal is the value of a struct type, and it has bindings for all the fields of that struct.  For example, you get a CompoundVal if you track assigning a struct-by-value.

  struct S { … } v1, v2;
  …
  v1 = v2;

In the symbolic analysis, evaluating the expression ‘v2’ should produce a value representing all the bindings of the struct, and then you can track that in the assignment to ‘v1’.  Naively, we can model that as just copying all the bindings for v2 to v1, but this gets extremely expensive to track in the analyzer.  This copying is necessary, however, because ‘v2’ could have its fields modified after the assignment, and the real semantics are that v1 gets a copy after the assignment.

LazyCompoundVal is a hack to make this copying more lazy.  Instead of getting a copy of all the bindings of v2 at the point of assignment, v1 gets a “LazyCompoundVal”, which says “I’m the CompoundVal for the MemRegion for ‘v2’ when a specific symbolic Store was used’.   Then lookups to the fields of v1 just route through that lazy binding, which works effectively as if an actual copy was made.  The StoreManager is suppose to handle all of this lazy lookup to field values for you.

Ted

> On May 16, 2015, at 9:12 AM, Francisco Chiotta <franchiotta at gmail.com> wrote:
> 
> Hello there,
> 
> When a Sval evaluates to a LazyCompoundVal object? What does it mean?
> 
> Thanks!
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev