[cfe-dev] Fixed Point Analysis on GRExprEngine

[Ted Kremenek]

On Dec 27, 2010, at 5:02 AM, Nimrod Partush <nimi at cs.technion.ac.il> wrote:

> 1. I've noticed that CLang has 2 different analysis modules: GRExprEngine and DataFlowSolver. The former has advanced abstract domains but does not perform fixed point analysis (but rather bounded checking) like the latter. I want to use GRExprEngine for fixed point analysis (i,e, i want to invoke a Join during the analysis). How can i do that?

This would require some major surgery in the core engine.  It would also require API hooks from the various checkers to perform the join operation.  Probably the place to handle the joins would be when worklist units corresponding to block edges are dequeued from the worklist.

> 
> 2. What are your thoughts on linking the APRON abstract domain library to CLang? This will allow for a much stronger constraint language than the current one.

It depends.  Performance is actually very important in the analysis engine, so depending on another library form such core functionality would put fairly strong requirements on that other library.  Switching over to another abstract domain library as the "default" would be a huge change, and not one taken lightly.

One of the design points of the analysis engine was to try and allow flexible modeling depending on how much analysis sophistication is desired.  For example, the ConstraintManager and StoreManager interfaces are thin and virtual, allowing one to swap in entirely different constraint managers.  While the SVal interface is still fairly immature, the hope is that it would be flexible enough that it could easily map to other abstract domains (or possibly wrap the abstract domains of other libraries).  That way someone could use an external constraint solver while the main analysis engine (and checkers) reason using high-level "intentional" APIs.  I'm not familiar with APRON, but it could possible be incorporated in this way.