[cfe-dev] Some problems about function summary

[Xu Zhongxing]

Shall I rephrase your ideas more formally:


Suppose under constaint C, the precise summary is S. But we could hardly get S usually. We could generate 3 kinds of summary:


S1: what must happens, i.e., S1 is contained by S.


S2: what could happen, but I know that nothing more can happen, i.e. S2 contains S.


S3: what could happen, but I don't know if other can happen, i.e., the intersection of S3 and S is not empty, but no one contains another.


The current invalidation approximates S2. It reduces false positive.


I don't know the influence of adopting different kinds of summary on the quality of bug reports. I guess for different bug types we need different kind of summary.
 
------------------ Original ------------------
From:  "kremenek"<kremenek at apple.com>;
Date:  Mon, Jun 13, 2011 08:33 AM
To:  "Jordy Rose"<jediknil at belkadan.com>; 
Cc:  "Zhenbo Xu"<xuzb at ios.ac.cn>; "cfe-dev"<cfe-dev at cs.uiuc.edu>; 
Subject:  Re: [cfe-dev] Some problems about function summary

 
 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/20110613/2b1cabee/attachment.html>