Jan Midtgaard
Thomas P. Jensen
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.
Supplemental Material
- J. M. Ashley and R. K. Dybvig. A practical and flexible flow analysis for higher-order languages. ACM Transactions on Programming Languages and Systems, 20(4):845--868, 1998. Google Scholar
Digital Library
- A. E. Ayers. Efficient closure analysis with reachability. In M. Billaud, P. Castéran, M.-M. Corsini, K. Musumbu, and A. Rauzy, editors, Actes WSA'92 Workshop on Static Analysis, Bigre, pages 126--134, Bordeaux, France, Sept. 1992. Atelier Irisa, IRISA, Campus de Beaulieu.Google Scholar
- D. Cachera, T. Jensen, D. Pichardie, and V. Rusu. Extracting a data flow analyser in constructive logic. Theoretical Computer Science, 342(1): 56--78, 2005. Google ScholarDigital Library
- W. D. Clinger. Proper tail recursion and space efficiency. In K. D. Cooper, editor, Proc. of the ACM SIGPLAN 1998 Conference on Programming Languages Design and Implementation, pages 174--185, Montréal, Canada, June 1998. Google ScholarDigital Library
- C. Consel and O. Danvy. For a better support of static data flow. In J. Hughes, editor, Proc. of the Fifth ACM Conference on Functional Programming and Computer Architecture, volume 523 of LNCS, pages 496--519, Cambridge, Massachusetts, Aug. 1991. Springer-Verlag. Google ScholarDigital Library
- P. Cousot. The calculational design of a generic abstract interpreter. In M. Broy and R. Steinbrüggen, editors, Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam, 1999.Google Scholar
- P. Cousot. Semantic foundations of program analysis. In S. S. Muchnick and N. D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303--342. Prentice-Hall, 1981.Google Scholar
- P. Cousot and R. Cousot. Abstract interpretation of algebraic polynomial systems. In M. Johnson, editor, Proc. of the Sixth International Conference on Algebraic Methodology and Software Technology, AMAST'97, volume 1349 of LNCS, pages 138--154, Sydney, Australia, Dec. 1997. Springer-Verlag. Google ScholarDigital Library
- P. Cousot and R. Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), invited paper. In H. Bal, editor, Proc. of the Fifth IEEE International Conference on Computer Languages, pages 95--112, Toulouse, France, May 1994.Google Scholar
- P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511--547, Aug. 1992a.Google ScholarCross Ref
- P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2--3):103--179, 1992b. Google ScholarDigital Library
- P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In B. K. Rosen, editor, Proc. of the Sixth Annual ACM Symposium on Principles of Programming Languages, pages 269--282, San Antonio, Texas, Jan. 1979. Google ScholarDigital Library
- D. Damian and O. Danvy. Syntactic accidents in program analysis: On the impact of the CPS transformation. Journal of Functional Programming, 13(5):867--904, 2003. A preliminary version was presented at the 2000 ACM SIGPLAN International Conference on Functional Programming. Google ScholarDigital Library
- O. Danvy. Three steps for the CPS transformation. Technical Report CIS-92-2, Kansas State University, Manhattan, Kansas, Dec. 1991.Google Scholar
- B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge University Press, Cambridge, England, second edition, 2002.Google Scholar
- S. K. Debray and T. A. Proebsting. Interprocedural control flow analysis of first-order programs with tail-call optimization. ACM Transactions on Programming Languages and Systems, 19(4):568--585, 1997. Google ScholarDigital Library
- C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of compiling with continuations. In D. W. Wall, editor, Proc. of the ACM SIGPLAN 1993 Conference on Programming Languages Design and Implementation, pages 237--247, Albuquerque, New Mexico, June 1993. Google ScholarDigital Library
- K. L. S. Gasser, F. Nielson, and H. R. Nielson. Systematic realisation of control flow analyses for CML. In M. Tofte, editor, Proc. of the Second ACM SIGPLAN International Conference on Functional Programming, pages 38--51, Amsterdam, The Netherlands, June 1997. Google ScholarDigital Library
- R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361--416, 2000. Google ScholarDigital Library
- N. Heintze. Set-based program analysis of ML programs. In C. L. Talcott, editor, Proc. of the 1994 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. VII, No. 3, pages 306--317, Orlando, Florida, June 1994. Google ScholarDigital Library
- N. D. Jones. Flow analysis of lambda expressions (preliminary version). In S. Even and O. Kariv, editors, Automata, Languages and Programming, 8th Colloquium, Acre (Akko), volume 115 of LNCS, pages 114--128, Israel, July 1981. Springer-Verlag. Google ScholarDigital Library
- J. Midtgaard. Control-flow analysis of functional programs. Technical Report BRICS RS-07-18, Dept. of Comp. Sci., University of Aarhus, Aarhus, Denmark, Dec. 2007. Accepted for publication in ACM Computing Surveys.Google ScholarCross Ref
- J. Midtgaard and T. Jensen. A calculational approach to control-flow analysis by abstract interpretation. In M. Alpuente and G. Vidal, editors, Static Analysis, 15th International Symposium, SAS 2008, volume 5079 of LNCS, pages 347--362, Valencia, Spain, July 2008a. Springer-Verlag. Google ScholarDigital Library
- J. Midtgaard and T. P. Jensen. Control-flow analysis of function calls and returns by abstract interpretation. Rapport de Recherche RR-6681, INRIA Rennes -- Bretagne Atlantique, Oct. 2008b.Google Scholar
- M. Might and O. Shivers. Environmental analysis via ΔCFA. In S. Peyton Jones, editor, Proc. of the 33rd Annual ACM Symposium on Principles of Programming Languages, pages 127--140, Charleston, South Carolina, Jan. 2006. Google ScholarDigital Library
- R. Milner and M. Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87(1):209--220, 1991. Google ScholarDigital Library
- F. Nielson and H. R. Nielson. Infinitary control flow analysis: a collecting semantics for closure analysis. In N. D. Jones, editor, Proc. of the 24th Annual ACM Symposium on Principles of Programming Languages, pages 332--345, Paris, France, Jan. 1997. Google ScholarDigital Library
- F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999. Google ScholarDigital Library
- H. R. Nielson and F. Nielson. Flow logic: a multi-paradigmatic approach to static analysis. In T. Æ. Mogensen, D. A. Schmidt, and I. H. Sudborough, editors, The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, volume 2566 of LNCS, pages 223--244. Springer-Verlag, 2002. Google ScholarDigital Library
- J. Palsberg. Closure analysis in constraint form. ACM Transactions on Programming Languages and Systems, 17(1):47--62, 1995. Google ScholarDigital Library
- J. Palsberg and M. I. Schwartzbach. Safety analysis versus type inference. Information and Computation, 118(1):128--141, 1995. Google ScholarDigital Library
- J. Palsberg and M. Wand. CPS transformation of flow information. Journal of Functional Programming, 13(5):905--923, 2003. Google ScholarDigital Library
- D. Pichardie. Interprétation abstraite en logique intuitioniste: extraction d'analyseurs Java certifiés. PhD thesis, Université de Rennes 1, Sept. 2005.Google Scholar
- A. Sabry and M. Felleisen. Is continuation-passing useful for data flow analysis? In V. Sarkar, editor, Proc. of the ACM SIGPLAN 1994 Conference on Programming Languages Design and Implementation, pages 1--12, Orlando, Florida, June 1994. Google ScholarDigital Library
- P. Sestoft. Replacing function parameters by global variables. In J. E. Stoy, editor, Proc. of the Fourth International Conference on Functional Programming and Computer Architecture, pages 39--53, London, England, Sept. 1989. Google ScholarDigital Library
- O. Shivers. Control-flow analysis in Scheme. In M. D. Schwartz, editor, Proc. of the ACM SIGPLAN 1988 Conference on Programming Languages Design and Implementation, pages 164--174, Atlanta, Georgia, June 1988. Google ScholarDigital Library
- F. Spoto and T. P. Jensen. Class analyses as abstract interpretations of trace semantics. ACM Transactions on Programming Languages and Systems, 25(5):578--630, 2003. Google ScholarDigital Library
Index Terms
- Control-flow analysis of function calls and returns by abstract interpretation
Recommendations
Trace-based control-flow analysis
PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and ImplementationWe define a small-step semantics for the untyped λ-calculus, that traces the β-reductions that occur during evaluation. By abstracting the computation traces, we reconstruct k-CFA using abstract interpretation, and justify constraint-based k-CFA in a ...
Control-flow analysis of function calls and returns by abstract interpretation
ICFP '09We 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 ...
Control-flow analysis of function calls and returns by abstract interpretation
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 ...
Comments