[cfe-dev] Some problems about function summary

[Ted Kremenek]

On Jun 10, 2011, at 7:22 PM, Jordy Rose wrote:

> Hi, Ted and Zhenbo. All of this seems very interesting to me too; currently, a function call throws an awful lot of the analyzer's carefully constructed constraints out the window. I just wanted to add that it's probably possible to make a pessimistic function summary mechanism. That is, rather than assuming a function summary models /all/ salient behavior of a function, it can simply make guarantees about certain variables, or add certain constraints, without promising anything else.
> 
> Say, perhaps, that the only "summary" information we have is that if a length parameter is zero, the buffer parameter doesn't need to be invalidated. (I have no idea how we'd represent that.) That means we can go ahead and invalidate any other regions, globals, etc. as usual, but we can still take advantage of the information we /do/ have.


Hi Jordy,

In my own words, I'll generalize a bit what you are suggesting.

One aspect of summaries is that they should model what pieces of memory are modified.  A perfect summary would require no region invalidations, as it would just model the modifications directly.  A less perfect summary would say "I know this part of memory *could* be modified, but I don't know what the value is."  The least perfect summary assumes that all memory can be touched.

Conceptually what we have now is a summary-based analysis where we always use the most conservative summary.  So we already have a summary-based analysis, but it isn't general, and it assumes the most pessimistic results possible.

So what you are suggesting are summaries that don't explicitly model all possible memory modifications that a function could make, but a conservative estimate (but more precise than what we currently have) of how memory could be modified.  To do this, we need to make region invalidation a declarative effect in the summary (just like any other changes the summary models), which ExprEngine then explicitly performs when applying the summary.  As part of this, we would just need to make "region invalidation" in the summary dependent on value constraints, just like any other aspect of a summary.  One way to do this would be to store region invalidation information literally in a GRState (that would be used to construct a summary).  We could (for example) put this in the GRState's GDM, and provide an API for clients to store region invalidation constraints in the GRState.  This would allow checkers with domain-specific knowledge of a function to model these region invalidation constraints (in the absence of more perfect summary information).

Ted
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20110612/9a364fda/attachment.html>