Abstract Interpretation Framework written in Haskell.
Perform the static numerical analysis on C-like programs using Abstract Interpretation.
- Before building the project, you need to install Apron (an open-source software built by INRIA, France.) and PPL (Parma Polyhedra Library, developed at University of Parma, Italy).
- After that, type make all.
- Prototype language:
- Defined in AbstractSyntax.hs. C-like syntax.
- Front-end (FrontEnd.hs):
- Using Haskell with compiler writing package Parsec.
- Intermediate Representation is an AST encapsuled as a Haskell class.
- Back-end (SemanticsAnalysis.hs):
- Automatically construct the interface of Apron and PPL using Haskell FFL.
- Process the numerical values of program variables in AST, then assign polyhedron domains for them along with the program data flow.
- Print out the source code with numerical values of program variables at each line inside the comment.
- Abstract values of program variables are represented as polyhedra consisting of inequality constraints.
The whole analysis procedure is static, which means you don't need to really execute the program to check the numerical safety in the runtime. Instead, this work is done at the compile time.
INRIA already provides an online analyzer to see the power of abstract interpretation: Interproc. You can try it with the default convext polyhedra domain, or other interesting domains like intervals, octagons, etc.