New Abstract Interpretation Engine

This module defines a set of classes to perform abstract interpretation. More...

Classes
class	otawa::ai::Graph
	Graph concept for ai module. More...
class	otawa::ai::Domain
	Domain concept for ai module. More...
class	otawa::ai::InputIter
	Iterator on input of a vertex. More...
class	otawa::ai::OutputIter
	Iterator to set output values. More...
class	otawa::ai::WorkListDriver< D, G, S >
	Driver of abstract interpretation with a simple to-do list. More...
class	otawa::ai::CFGGraph
	BiDiGraph implementation for CFG. More...
class	otawa::ai::ArrayStore< D, G >
	Stockage of output values as an array. More...
class	otawa::ai::EdgeStore< D, G >
	State storage on the edges. More...

Detailed Description

This module defines a set of classes to perform abstract interpretation.

It is most versatile as the previous module, HalfAbsInt, and should be used to perform now in OTAWA to perform analyzes.

Principles

The support for abstract interpretation is made of different classes that are able to interact together according the needs of the developer. Basically, there are three types of classes:

• drivers – implement the Iterator model, they implement the policy of calculation order (WorkListDriver),
• stores – store and retrieve efficiently results of abstract interpretation (ArrayStore, EdgeStore),
• adapters – provide interface between program representation (as graphs) and other classes (CFGGraph).

Finally, the domains are given by the user and details the abstract interpretation to perform.

Method

First, according to the program representation, developer has to choose a graph adapter. There is only one now (CFGGraph) for a lonely CFG but more will be proposed in the near future.

Second, the abstract interpretation domain has to be designed. It is class providing the following resources:

• empty constructor (for extend freedom in implementation of stage),
• t – type of values in the abstract domain,
• init() – return the initial state (at entry node of the graph),
• join() – join of two values of the abstract domain.

Update functions are not included in this list because they depend only on the way driver is used.

Then the storage and the driver must be chosen and tied together as below. This approach allows to customize the way the computation is performed. In the example below, we just apply the same method whatever the node or the edge.

MyDomain dom;
       CFGGraph graph(cfg);
       ArrayStore<MyDomain, CFGraph> store;
WorkListDriver<MyDomain, CFGGraph, ArrayStore<MyDomain, CFGraph> > driver(dom, graph store);
while(driver)
       driver.check(dom.update(*driver, driver.input()));