[cfe-dev] Some problems about function summary

[Jordy Rose]

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.

I'm sure there's plenty of caveats to be overcome here, but it seems like any of these six/seven parts of a summary would be an improvement over none. Especially if you/we figure out a way to provide this information across translation units.

Just my two cents!
Jordy


On Jun 8, 2011, at 13:54, Ted Kremenek wrote:

> 
> Hi Zhenbo,
> 
> I was looking through my old emails, and stumbled upon this one.  I'm so sorry for not replying to it sooner.
> 
> Function summaries are a tough nut to crack.  There are a variety of issues to tackle.  Beyond memory updates, I think there are a bunch of other issues that need to be captured in a summary.  Here is a (partial) list:
> 
> 1) Memory updates (changes to the symbolic store)
> 2) Return values
> 3) Return values via out parameters
> 4) Constraints added to symbols, which can add "path constraints" on memory updates, return values, etc.
> 5) Unifying symbols (alpha-renaming) in the symbolic store and path constraints
> 6) Modeling checker state updates
> 7) and possibly many others...
> 
[snip]
> 
> All of this of course is a big project, which is why the *inlining* approach to inter-procedural analysis is more immediately appealing for doing simple inter-procedural analysis.  With the inlining approach, we analyze the caller, and when we see a function call, we just inline the semantics of the caller in situ by literally continuing the analysis of the caller by binding actual parameters to formal parameters, and the callee's analysis is done purely in the context of caller's.  This is easy and highly precise, but won't scale beyond simple cases.
> 
> Hope this helps,
> Ted