Galois transformers and modular abstract interpreters: reusable metatheory for program analysis
- 23 October 2015
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
- p. 552-571
- https://doi.org/10.1145/2814270.2814308
Abstract
The design and implementation of static analyzers has become increasingly systematic. Yet for a given language or analysis feature, it often requires tedious and error prone work to implement an analyzer and prove it sound. In short, static analysis features and their proofs of soundness do not compose well, causing a dearth of reuse in both implementation and metatheory. We solve the problem of systematically constructing static analyzers by introducing Galois transformers: monad transformers that transport Galois connection properties. In concert with a monadic interpreter, we define a library of monad transformers that implement building blocks for classic analysis parameters like context, path, and heap (in)sensitivity. Moreover, these can be composed together independent of the language being analyzed. Significantly, a Galois transformer can be proved sound once and for all, making it a reusable analysis component. As new analysis features and abstractions are developed and mixed in, soundness proofs need not be reconstructed, as the composition of a monad transformer stack is sound by virtue of its constituents. Galois transformers provide a viable foundation for reusable and composable metatheory for program analysis. Finally, these Galois transformers shift the level of abstraction in analysis design and implementation to a level where non-specialists have the ability to synthesize sound analyzers over a number of parameters.Keywords
Other Versions
Funding Information
- National Science Foundation (CAREER 1350344)
- DARPA (FA8750-15-2- 0092, FA8750-12-2-0106)
This publication has 18 references indexed in Scilit:
- Widening for Control-FlowLecture Notes in Computer Science, 2014
- Hybrid context-sensitivity for points-to analysisPublished by Association for Computing Machinery (ACM) ,2013
- Control-flow analysis of functional programsACM Computing Surveys, 2012
- Just do itPublished by Association for Computing Machinery (ACM) ,2011
- Parameterized object sensitivity for points-to analysis for JavaACM Transactions on Software Engineering and Methodology, 2005
- ESPPublished by Association for Computing Machinery (ACM) ,2002
- Monad transformers and modular interpretersPublished by Association for Computing Machinery (ACM) ,1995
- Analysis of pointers and structuresPublished by Association for Computing Machinery (ACM) ,1990
- Systematic design of program analysis frameworksPublished by Association for Computing Machinery (ACM) ,1979
- Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpointsPublished by Association for Computing Machinery (ACM) ,1977