[cfe-dev] Extend Static Analyzer with Abstract Interpretation

[Ted Kremenek]

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

> 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".
> 
> (ii) Specify "abstract domain" which to my knowledge is similar to symbolic
> value and constraints.
> 
> (iii) Define state and transfer function based on the domain.
> 
> (iv) Other things I didn't consider, e.g. Someone has already done this for
> me, and I should use his.

While elements of the symbolic execution employ concepts from abstract interpretation, the analyzer engine itself does not do a fix point computation to compute the set of possible abstract states at a given program point.  Building that kind of solver is completely doable, but a very different approach than the one we tool.  If you are interested in just local analysis on a single CFG, the elements of the CFG can serve as program points, and a worklist algorithm can be used to do the fix point analysis.  Of course you will need to define widening operations and the like, but that depends completely on the domain that you want to define.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20121210/ddc435bc/attachment.html>