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

Jan Midtgaard, Thomas P. Jensen

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

Resumé

We derive a control-flow analysis that approximates the interprocedural control-flow of both function calls and returns in the presence of first-class functions and tail-call optimization. In addition to an abstract environment, our analysis computes for each expression an abstract control stack, effectively approximating where function calls return across optimized tail calls. The analysis is systematically calculated by abstract interpretation of the stack-based CaEK abstract machine of Flanagan et al. using a series of Galois connections. Abstract interpretation provides a unifying setting in which we 1) prove the analysis equivalent to the composition of a continuation-passing style (CPS) transformation followed by an abstract interpretation of a stack-less CPS machine, and 2) extract an equivalent constraint-based formulation, thereby providing a rational reconstruction of a constraint-based control-flow analysis from abstract interpretation principles.
OriginalsprogEngelsk
TitelProceeding of the 14th ACM SIGPLAN international conference on Functional Programming : ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009.
ForlagAssociation for Computing Machinery
Publikationsdato2009
Sider287-298
ISBN (Trykt)978-1-60558-332-7
StatusUdgivet - 2009
BegivenhedThe 14th ACM SIGPLAN international conference on Functional Programming, ICFP 2009 - Edinburgh, Storbritannien
Varighed: 31 aug. 20092 sep. 2009

Konference

KonferenceThe 14th ACM SIGPLAN international conference on Functional Programming, ICFP 2009
LandStorbritannien
ByEdinburgh
Periode31/08/200902/09/2009

Citer dette

Midtgaard, J., & Jensen, T. P. (2009). Control-flow analysis of function calls and returns by abstract interpretation. I Proceeding of the 14th ACM SIGPLAN international conference on Functional Programming: ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009. (s. 287-298). Association for Computing Machinery.
Midtgaard, Jan ; Jensen, Thomas P. / Control-flow analysis of function calls and returns by abstract interpretation. Proceeding of the 14th ACM SIGPLAN international conference on Functional Programming: ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009.. Association for Computing Machinery, 2009. s. 287-298
@inproceedings{2c35eac0d2b811dea6c9000ea68e967b,
title = "Control-flow analysis of function calls and returns by abstract interpretation",
abstract = "We derive a control-flow analysis that approximates the interprocedural control-flow of both function calls and returns in the presence of first-class functions and tail-call optimization. In addition to an abstract environment, our analysis computes for each expression an abstract control stack, effectively approximating where function calls return across optimized tail calls. The analysis is systematically calculated by abstract interpretation of the stack-based CaEK abstract machine of Flanagan et al. using a series of Galois connections. Abstract interpretation provides a unifying setting in which we 1) prove the analysis equivalent to the composition of a continuation-passing style (CPS) transformation followed by an abstract interpretation of a stack-less CPS machine, and 2) extract an equivalent constraint-based formulation, thereby providing a rational reconstruction of a constraint-based control-flow analysis from abstract interpretation principles.",
keywords = "Languages, Theory, Verification, Control flow analysis, abstract interpretation, tail-call optimization, continuation-passing style, direct style, constraint-based analysis",
author = "Jan Midtgaard and Jensen, {Thomas P.}",
year = "2009",
language = "English",
isbn = "978-1-60558-332-7",
pages = "287--298",
booktitle = "Proceeding of the 14th ACM SIGPLAN international conference on Functional Programming",
publisher = "Association for Computing Machinery",

}

Midtgaard, J & Jensen, TP 2009, Control-flow analysis of function calls and returns by abstract interpretation. i Proceeding of the 14th ACM SIGPLAN international conference on Functional Programming: ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009.. Association for Computing Machinery, s. 287-298, The 14th ACM SIGPLAN international conference on Functional Programming, ICFP 2009, Edinburgh, Storbritannien, 31/08/2009.

Control-flow analysis of function calls and returns by abstract interpretation. / Midtgaard, Jan; Jensen, Thomas P.

Proceeding of the 14th ACM SIGPLAN international conference on Functional Programming: ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009.. Association for Computing Machinery, 2009. s. 287-298.

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

TY - GEN

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

AU - Midtgaard, Jan

AU - Jensen, Thomas P.

PY - 2009

Y1 - 2009

N2 - We derive a control-flow analysis that approximates the interprocedural control-flow of both function calls and returns in the presence of first-class functions and tail-call optimization. In addition to an abstract environment, our analysis computes for each expression an abstract control stack, effectively approximating where function calls return across optimized tail calls. The analysis is systematically calculated by abstract interpretation of the stack-based CaEK abstract machine of Flanagan et al. using a series of Galois connections. Abstract interpretation provides a unifying setting in which we 1) prove the analysis equivalent to the composition of a continuation-passing style (CPS) transformation followed by an abstract interpretation of a stack-less CPS machine, and 2) extract an equivalent constraint-based formulation, thereby providing a rational reconstruction of a constraint-based control-flow analysis from abstract interpretation principles.

AB - We derive a control-flow analysis that approximates the interprocedural control-flow of both function calls and returns in the presence of first-class functions and tail-call optimization. In addition to an abstract environment, our analysis computes for each expression an abstract control stack, effectively approximating where function calls return across optimized tail calls. The analysis is systematically calculated by abstract interpretation of the stack-based CaEK abstract machine of Flanagan et al. using a series of Galois connections. Abstract interpretation provides a unifying setting in which we 1) prove the analysis equivalent to the composition of a continuation-passing style (CPS) transformation followed by an abstract interpretation of a stack-less CPS machine, and 2) extract an equivalent constraint-based formulation, thereby providing a rational reconstruction of a constraint-based control-flow analysis from abstract interpretation principles.

KW - Languages

KW - Theory

KW - Verification

KW - Control flow analysis

KW - abstract interpretation

KW - tail-call optimization

KW - continuation-passing style

KW - direct style

KW - constraint-based analysis

M3 - Article in proceedings

SN - 978-1-60558-332-7

SP - 287

EP - 298

BT - Proceeding of the 14th ACM SIGPLAN international conference on Functional Programming

PB - Association for Computing Machinery

ER -

Midtgaard J, Jensen TP. Control-flow analysis of function calls and returns by abstract interpretation. I Proceeding of the 14th ACM SIGPLAN international conference on Functional Programming: ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009.. Association for Computing Machinery. 2009. s. 287-298