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

Jan Midtgaard, Thomas P. Jensen

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


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.
Original languageEnglish
Title of host publicationProceeding of the 14th ACM SIGPLAN international conference on Functional Programming : ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009.
PublisherAssociation for Computing Machinery
Publication date2009
ISBN (Print)978-1-60558-332-7
Publication statusPublished - 2009
EventThe 14th ACM SIGPLAN international conference on Functional Programming, ICFP 2009 - Edinburgh, United Kingdom
Duration: 31 Aug 20092 Sep 2009


ConferenceThe 14th ACM SIGPLAN international conference on Functional Programming, ICFP 2009
Country/TerritoryUnited Kingdom


  • Languages
  • Theory
  • Verification
  • Control flow analysis
  • abstract interpretation
  • tail-call optimization
  • continuation-passing style
  • direct style
  • constraint-based analysis

Cite this