<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On Dec 10, 2012, at 6:43 AM, Bridge <<a href="mailto:bridge@iis.sinica.edu.tw">bridge@iis.sinica.edu.tw</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">Hi Team,<br><br> I'm a research assistant in IIS, AS, Taiwan. Our lab is working on<br>topics in abstract interpretation,<br><br>and we are looking for a framework to implement and test our ideas. Then, I<br>noticed this project.<br><br>I've read the developer's manual on website, the slides in 2008, and the<br>discussion thread below. <br><br><a href="http://lists.cs.uiuc.edu/pipermail/cfe-dev/2009-January/003996.html">http://lists.cs.uiuc.edu/pipermail/cfe-dev/2009-January/003996.html</a><br><br>Also I found this paper, "A Memory Model for Static Analysis of C Programs". <br></blockquote><div><br></div>We've recently gave another talk on the static analyzer. See "Building a checker in 24 hours" at <a href="http://llvm.org/devmtg/2012-11/">http://llvm.org/devmtg/2012-11/</a> The talk is targeted at someone writing a new check extension to the analyzer so it only has a very high level description of the internals; but I am sure you will find it useful.</div><div><br><blockquote type="cite"><br>The Front-end and the memory model are quite attractive, so I want to build<br>our work based on them.<br><br>The website says the engine do symbolic execution. I think it can be<br>modified for abstract interpretation.<br><br>Hence, I need some advice on where should I hack to achieve followings.<br><br>(i) Apply another algorithm to traverse CFG for finding "fixed-point".<br></blockquote><div><br></div>The ExprEngine/CoreEngine are responsible for walking the CFG. We unroll loops several times by default, but that is configurable. We stop when reaching the fixed point, by caching out on a previously seen state. </div><div><br></div><div>Take a look at AnalysesConsumer.cpp, which initiates the traversal.</div><div><br></div><div><blockquote type="cite"><br>(ii) Specify "abstract domain" which to my knowledge is similar to symbolic<br>value and constraints.<br></blockquote><div><br></div>ConstraintManager/SimpleConstraintManager/RangeConstraintManager is the module responsible for keeping track of constraints on the symbolic values. I would suggest taking a look at it to see if you could implement an abstract domain by replacing/creating your own the ConstraintManager. (It's hard to say if that would be enough/relevant without the details about the abstract domain.)<br><br><blockquote type="cite">(iii) Define state and transfer function based on the domain.<br><br></blockquote><div><br></div><div>If you are only interested in domain specific transfer functions, you should be able to implement them by writing a "checker". (See the talk, which I've referenced above.) That would be the least intrusive way of using/interacting with the analyzer. I'd recommend writing a checker to get a feeling of how the analyzer works as well.</div><br><blockquote type="cite">(iv) Other things I didn't consider, e.g. Someone has already done this for<br>me, and I should use his.<br><br>Thank you.<br><br><br>Hsieh, Chiao<br><a href="mailto:bridge@iis.sinica.edu.tw">bridge@iis.sinica.edu.tw</a><br><br><br><br><br>--<br>View this message in context: http://clang-developers.42468.n3.nabble.com/Extend-Static-Analyzer-with-Abstract-Interpretation-tp4028829.html<br>Sent from the Clang Developers mailing list archive at Nabble.com.<br>_______________________________________________<br>cfe-dev mailing list<br>cfe-dev@cs.uiuc.edu<br>http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev<br></blockquote></div><br></body></html>