Control-flow analysis of function calls and returns by abstract interpretation

Jan Midtgaard (1) , Thomas Jensen (2)

1 Department of Computer Science [Aarhus]
2 CELTIQUE - Software certification with semantic analysis

Abstract interpretation techniques are used to derive a control-flow analysis for a simple higher-order functional language. The analysis approximates the interprocedural control-flow of both function calls and returns in the presence of first-class functions and tail-call optimization. The analysis is systematically derived by abstract interpretation of a stack-based abstract machine using a series of Galois connections. We prove that the analysis is equivalent to an analysis obtained by first transforming the program into continuation-passing style and then performing control flow analysis of the transfored program. We then show how the analysis induces an equivalent constraint-based formulation, thereby providing a rational reconstruction of a constraint-based CFA from abstract interpretation principles.

Mots clés: Control-flow analysis; Abstract interpretation; CPS TRANSFORMATION; PROGRAMS

Mots clés: LOGIC; SEMANTICS

Domaines: Logique en informatique [cs.LO]

Jan Midtgaard, Thomas Jensen. Control-flow analysis of function calls and returns by abstract interpretation. Information and Computation, 2012, 2012, pp.49-76. ⟨10.1016/j.ic.2011.11.005⟩. ⟨hal-00758152⟩