[cfe-dev] abstract interpretation work across different source files

[Hammond, John]

Howdy,

I had the same question. But in each specific case I found that I could:


1.      Divide the analysis in to a data gathering phase and an error reporting phase (so two global make passes).

2.      Write a single bi-modal AST visitor or path sensitive checker that emits a flat text file which abstracts the results of the first phase.

3.      Write some python or awk that munges the output of the first phase into a single file.

4.      Have the checker read that file in the second phase and emit appropriate diagnostics.

So for example, say we would like to analyze NULL pointer dereferences. In phase 1, for each TU, for function definition emit (in structured flat text)
ReturnsNULL FUNCTION
or
               DependentReturn CALLER CALLEE

Where FUNCTION, CALLER, and CALLEE uniquely identify a function (I use PATH:LINE:COL:NAME of the canonical declaration and emit errors when functions may not be canonically declared).

Step 3 above does the graph theoretic reduction to determine which functions may return NULL and puts this in a single file.

Step 4 reruns make and passes that file as an argument or environmental variable to the checker/AST visitor.

Usually I modify ccc-analyzer by adding some environmental variables to decide which files to write in phase 1 and which to read in phase 2. Then I write a bash script that wraps make and sets everything up.

It probably sounds worse than it is. All of that said, native support for global analysis would be awesome.
Best,

John

From: cfe-dev-bounces at cs.uiuc.edu [mailto:cfe-dev-bounces at cs.uiuc.edu] On Behalf Of Jordan Rose
Sent: Thursday, March 27, 2014 5:20 PM
To: larry.1.yang at nokia.com
Cc: cfe-dev at cs.uiuc.edu
Subject: Re: [cfe-dev] abstract interpretation work across different source files

Hi, Larry. This is something we've wanted to do for a long time, but it's not a project to undertake lightly. Currently, the static analyzer uses the same logic as the compiler to parse a source file (and its headers) into an AST, and then run that. When you start talking about multiple source files, what we have isn't immediately reusable-Clang's just not set up to handle multiple translation units that also interact, with the exception of some of the indexing work. So the challenge is to come up with some way to share information across translation units (or, less plausibly, to rewire Clang to handle multiple translation units in a common context).

In some of our discussions on this, we've come up with the ideas of either "marshalling" data from one ASTContext to another (which turned out to be quite difficult to get right), or of recording "summaries" of each function that describe how to evaluate it from another context. I think the summary-based approach is a better avenue to go down, but then you have to decide how to get these summaries in and out of the analyzer and what information to include in them. And they have to be better than the default behavior we have now for opaque function calls...but then this has the possibility to be really, really useful.

(Who is "we"? Mostly Ted Kremenek, the code owner for the analyzer, along with Anna Zaks and myself.)

I hope that shines a light on some of the difficulties in implementing this well-it's a project of weeks, if not months. If you're still interested in looking at this, let's come up with a plan to tackle some of these problems. Alternately, I'd be happy to see you contributing to the analyzer, but starting out with something possibly less daunting. :-)

Jordan


On Mar 18, 2014, at 21:54 , larry.1.yang at nokia.com<mailto:larry.1.yang at nokia.com> wrote:


Hello there,

I am looking at clang static analyzer recently, and thinking whether I could make it's abstract interpretation work across different source files, so that the constraints from source file a.c could be applied to other source files like b.c and c.c.

Any directions/hints on this will be much appreciated.

Br,
Larry

_______________________________________________
cfe-dev mailing list
cfe-dev at cs.uiuc.edu<mailto:cfe-dev at cs.uiuc.edu>
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20140328/c96ffa85/attachment.html>