Discontinuation notice: As of June 1st, 2007, PAG is no longer available as a stand-alone product. For further information, contact support@absint.com.
Static program analysis made easy.
Producing high quality code means that compilers have to perform efficiency-enhancing program transformations. These transformations usually depend on preceding program analyses known as data flow analyses or abstract interpretations. They may range from “simple” intraprocedural bit vector frameworks to highly complex interprocedural alias analyses. Their implementation is usually difficult and expensive.
The program analyzer generator PAG supports the
implementation of static program analyzers. PAG automatically
generates efficient data flow analyzers from concise specifications.
The generative approach frees the PAG user from having to
implement the domain functionality, the traversal of the control flow
graph, and suitable fixpoint algorithms. Thus, saving valuable
development time.
The underlying theory of abstract interpretation provides the relation to the programming language semantics, thus enabling the systematic derivation of provably correct and terminating analyses.
Features
- The high-level input language improves maintainability
- PAG-generated analyzers are highly efficient thanks to sophisticated data structures and iteration algorithms
- PAG-generated interprocedural analyzers can be easily integrated into existing compilers thanks to a well-defined interface
Applications
PAG has been used in several projects by numerous companies and universities to implement:
- Cache behavior prediction
- Stack usage analysis
- Memory error detection (dereferencing null pointers)
- Post pass code optimizations
- Conditional constant propagation
- Addressing mode optimization
- Data dependency analysis on pointer structures
- Optimizations for a video accelerator multiprocessor
- Pipeline analysis
- Escape analysis on Java
- Value analysis on executables
- Shape analysis
- Strongly live variables analyses
- Interval analysis
- Classical bit-vector analyses