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

Abstract : 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.
Document type :
Journal articles
Information and Computation, Elsevier, 2012, 2012, pp.49-76. <10.1016/j.ic.2011.11.005>


https://hal.inria.fr/hal-00758152
Contributor : Thomas Jensen <>
Submitted on : Thursday, November 29, 2012 - 1:22:59 PM
Last modification on : Thursday, November 29, 2012 - 2:22:03 PM

File

artikel.pdf
fileSource_public_author

Identifiers

Collections

Citation

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

Export

Share

Metrics

Consultation de
la notice

211

Téléchargement du document

33