[cfe-dev] Extend Static Analyzer with Abstract Interpretation

[Anna Zaks]

On Dec 10, 2012, at 6:43 AM, Bridge <bridge at iis.sinica.edu.tw> wrote:

> Hi Team,
> 
>    I'm a research assistant in IIS, AS, Taiwan. Our lab is working on
> topics in abstract interpretation,
> 
> and we are looking for a framework to implement and test our ideas. Then, I
> noticed this project.
> 
> I've read the developer's manual on website, the slides in 2008, and the
> discussion thread below. 
> 
> http://lists.cs.uiuc.edu/pipermail/cfe-dev/2009-January/003996.html
> 
> Also I found this paper, "A Memory Model for Static Analysis of C Programs". 

We've recently gave another talk on the static analyzer. See "Building a checker in 24 hours" at http://llvm.org/devmtg/2012-11/ 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.

> 
> The Front-end and the memory model are quite attractive, so I want to build
> our work based on them.
> 
> The website says the engine do symbolic execution. I think it can be
> modified for abstract interpretation.
> 
> Hence, I need some advice on where should I hack to achieve followings.
> 
> (i)  Apply another algorithm to traverse CFG for finding "fixed-point".

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. 

Take a look at AnalysesConsumer.cpp, which initiates the traversal.

> 
> (ii) Specify "abstract domain" which to my knowledge is similar to symbolic
> value and constraints.

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.)

> (iii) Define state and transfer function based on the domain.
> 

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.

> (iv) Other things I didn't consider, e.g. Someone has already done this for
> me, and I should use his.
> 
> Thank you.
> 
> 
> Hsieh, Chiao
> bridge at iis.sinica.edu.tw
> 
> 
> 
> 
> --
> View this message in context: http://clang-developers.42468.n3.nabble.com/Extend-Static-Analyzer-with-Abstract-Interpretation-tp4028829.html
> Sent from the Clang Developers mailing list archive at Nabble.com.
> _______________________________________________
> 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/20121210/915ae246/attachment.html>