<div dir="ltr"><div><div><div>Hello there,<br><br></div>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.<br>
<br></div>Cheers,<br></div>Gábor<br><div><div><br><br>[1]: <a href="http://www.google-melange.com/gsoc/proposal/review/student/google/gsoc2014/xazax/5629499534213120">http://www.google-melange.com/gsoc/proposal/review/student/google/gsoc2014/xazax/5629499534213120</a><br>
</div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On 28 March 2014 04:27, Hammond, John <span dir="ltr"><<a href="mailto:john.hammond@intel.com" target="_blank">john.hammond@intel.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div link="blue" vlink="purple" lang="EN-US">
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Howdy,<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">I had the same question. But in each specific case I found that I could:<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p><u></u><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><span>1.<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Divide the analysis in to a data gathering phase and an error reporting phase (so two global make passes).<u></u><u></u></span></p>
<p><u></u><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><span>2.<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">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.<u></u><u></u></span></p>
<p><u></u><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><span>3.<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Write some python or awk that munges the output of the first phase into a single file.<u></u><u></u></span></p>
<p><u></u><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><span>4.<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Have the checker read that file in the second phase and emit appropriate diagnostics.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">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)<u></u><u></u></span></p>
<p class="MsoNormal" style="text-indent:.5in"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">ReturnsNULL FUNCTION<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">or<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> DependentReturn CALLER CALLEE<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">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).<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Step 3 above does the graph theoretic reduction to determine which functions may return NULL and puts this in a single file.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Step 4 reruns make and passes that file as an argument or environmental variable to the checker/AST visitor.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">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.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">It probably sounds worse than it is. All of that said, native support for global analysis would be awesome.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Best,<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">John<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0in 0in 0in 4.0pt">
<div>
<div style="border:none;border-top:solid #b5c4df 1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal"><b><span style="font-size:10.0pt;font-family:"Tahoma","sans-serif"">From:</span></b><span style="font-size:10.0pt;font-family:"Tahoma","sans-serif""> <a href="mailto:cfe-dev-bounces@cs.uiuc.edu" target="_blank">cfe-dev-bounces@cs.uiuc.edu</a> [mailto:<a href="mailto:cfe-dev-bounces@cs.uiuc.edu" target="_blank">cfe-dev-bounces@cs.uiuc.edu</a>]
<b>On Behalf Of </b>Jordan Rose<br>
<b>Sent:</b> Thursday, March 27, 2014 5:20 PM<br>
<b>To:</b> <a href="mailto:larry.1.yang@nokia.com" target="_blank">larry.1.yang@nokia.com</a><br>
<b>Cc:</b> <a href="mailto:cfe-dev@cs.uiuc.edu" target="_blank">cfe-dev@cs.uiuc.edu</a><br>
<b>Subject:</b> Re: [cfe-dev] abstract interpretation work across different source files<u></u><u></u></span></p>
</div>
</div><div><div class="h5">
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<p class="MsoNormal">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).<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">(Who is "we"? Mostly Ted Kremenek, the code owner for the analyzer, along with Anna Zaks and myself.)<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">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. :-)<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Jordan<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal">On Mar 18, 2014, at 21:54 , <a href="mailto:larry.1.yang@nokia.com" target="_blank">
larry.1.yang@nokia.com</a> wrote:<u></u><u></u></p>
</div>
<p class="MsoNormal"><br>
<br>
<u></u><u></u></p>
<div>
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"">Hello there,<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif""> <u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"">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.<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif""> <u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"">Any directions/hints on this will be much appreciated.<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif""> <u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"">Br,<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"">Larry<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif""> <u></u><u></u></span></p>
</div>
<p class="MsoNormal"><span style="font-size:9.0pt;font-family:"Helvetica","sans-serif"">_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@cs.uiuc.edu" target="_blank"><span style="color:purple">cfe-dev@cs.uiuc.edu</span></a><br>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev" target="_blank"><span style="color:purple">http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev</span></a><u></u><u></u></span></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
</div></div></div>
</div>
</div>
<br>_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@cs.uiuc.edu">cfe-dev@cs.uiuc.edu</a><br>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev</a><br>
<br></blockquote></div><br></div>