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

[Gábor Horváth]

Hello there,

My GSoC proposal [1] is slightly related. It does not involve automatic
synthesis of models and in the long run the textual representation of model
files will not be appropriate. But it can be considered as a first step
towards global analysis.

Cheers,
Gábor


[1]:
http://www.google-melange.com/gsoc/proposal/review/student/google/gsoc2014/xazax/5629499534213120


On 28 March 2014 04:27, Hammond, John <john.hammond at intel.com> wrote:

>  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 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
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev
>
>
>
> _______________________________________________
> cfe-dev mailing list
> 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/fae22dd2/attachment.html>