Skip to main content
SpringerLink
Log in
Book cover

International Static Analysis Symposium

SAS 2008: Static Analysis pp 347–362Cite as

A Calculational Approach to Control-Flow Analysis by Abstract Interpretation

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5079))

Abstract

We present a derivation of a control-flow analysis by abstract interpretation. Our starting point is a transition system semantics defined as an abstract machine for a small functional language in continuation-passing style. We obtain a Galois connection for abstracting the machine states by composing Galois connections, most notable an independent-attribute Galois connection on machine states and a Galois connection induced by a closure operator associated with a constituent-parts relation on environments. We calculate abstract transfer functions by applying the state abstraction to the collecting semantics, resulting in a novel characterization of demand-driven 0-CFA.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Appel, A.W.: Compiling with Continuations. Cambridge University Press, New York (1992)

    Google Scholar 

  2. Ayers, A.E.: Abstract Analysis and Optimization of Scheme. PhD thesis, Massachusetts Institute of Technology, Cambridge, Massachusetts (September 1993)

    Google Scholar 

  3. Biswas, S.K.: A demand-driven set-based analysis. In: Jones (ed.) [17], pp. 372–385.

    Google Scholar 

  4. Bondorf, A.: Automatic autoprojection of higher-order recursive equations. Science of Computer Programming 17(1-3), 3–34 (1991)

    Article  MATH  Google Scholar 

  5. Cousot, P.: Semantic foundations of program analysis. In: Muchnick, Jones (eds.) [24], ch. 10, pp. 303–342.

    Google Scholar 

  6. Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbrüggen, R. (eds.) Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)

    Google Scholar 

  7. Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science 277(1–2), 47–103 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  8. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Sethi, R. (ed.) Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, Los Angeles, California, pp. 238–252 (January 1977)

    Google Scholar 

  9. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Rosen, B.K. (ed.) Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, pp. 269–282 (January 1979)

    Google Scholar 

  10. Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  11. Cousot, P., Cousot, R.: Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), invited paper. In: Bal, H. (ed.) Proceedings of the Fifth IEEE International Conference on Computer Languages, Toulouse, France, pp. 95–112 ( May 1994)

    Google Scholar 

  12. Danvy, O., Dzafic, B., Pfenning, F.: On proving syntactic properties of CPS programs. In: Third International Workshop on Higher-Order Operational Techniques in Semantics, Paris, France. Electronic Notes in Theoretical Computer Science, vol. 26, pp. 19–31 (September 1999)

    Google Scholar 

  13. Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002)

    MATH  Google Scholar 

  14. Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: Wall, D.W. (ed.) Proceedings of the ACM SIGPLAN 1993 Conference on Programming Languages Design and Implementation, Albuquerque, New Mexico, pp. 237–247 (June 1993)

    Google Scholar 

  15. Gasser, K.L.S., Nielson, F., Nielson, H.R.: Systematic realisation of control flow analyses for CML. In: Tofte, M. (ed.) Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming, Amsterdam, The Netherlands, pp. 38–51 (June 1997)

    Google Scholar 

  16. Jones, N.D.: Flow analysis of lambda expressions (preliminary version). In: Proceedings of the 8th Colloquium on Automata, Languages and Programming, London, UK, pp. 114–128 (1981)

    Google Scholar 

  17. Jones, N.D. (ed.): Proceedings of the Twenty-Fourth Annual ACM Symposium on Principles of Programming Languages, Paris, France (January 1997)

    Google Scholar 

  18. Jones, N.D., Muchnick, S.S.: Complexity of flow analysis, inductive assertion synthesis and a language due to Dijkstra. In: Muchnick, Jones (eds.) [24], pp. 380–393.

    Google Scholar 

  19. Jones, N.D., Nielson, F.: Abstract interpretation: a semantics-based tool for program analysis. In: Handbook of logic in computer science, vol. 4, pp. 527–636. Oxford University Press, Oxford (1995)

    Google Scholar 

  20. Landin, P.J.: The mechanical evaluation of expressions. The Computer Journal 6(4), 308–320 (1964)

    MATH  Google Scholar 

  21. Midtgaard, J.: Control-flow analysis of functional programs. Technical Report BRICS RS-07-18, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark (December 2007)

    Google Scholar 

  22. Might, M., Shivers, O.: Improving flow analyses via ΓCFA: abstract garbage collection and counting. In: Lawall, J. (ed.) Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming (ICFP 2006), Portland, Oregon, pp. 13–25 (September 2006)

    Google Scholar 

  23. Milner, R., Tofte, M.: Co-induction in relational semantics. Theoretical Computer Science 87(1), 209–220 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  24. Muchnick, S.S., Jones, N.D. (eds.): Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs (1981)

    MATH  Google Scholar 

  25. Nielson, F., Nielson, H.R.: Infinitary control flow analysis: a collecting semantics for closure analysis. In: Jones (ed.) [17], pp. 332–345

    Google Scholar 

  26. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)

    MATH  Google Scholar 

  27. Palsberg, J.: Closure analysis in constraint form. ACM Transactions on Programming Languages and Systems 17(1), 47–62 (1995)

    Article  Google Scholar 

  28. Sabry, A., Felleisen, M.: Is continuation-passing useful for data flow analysis? In: Sarkar, V. (ed.) Proceedings of the ACM SIGPLAN 1994 Conference on Programming Languages Design and Implementation, Orlando, Florida, pp. 1–12 (June 1994)

    Google Scholar 

  29. Schmidt, D.A.: Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Inc. (1986)

    Google Scholar 

  30. Sestoft, P.: Replacing function parameters by global variables. Master’s thesis, DIKU, Computer Science Department, University of Copenhagen, Copenhagen, Denmark (October 1988)

    Google Scholar 

  31. Shivers, O.: Control-flow analysis in Scheme. In: Schwartz, M.D. (ed.) Proceedings of the ACM SIGPLAN 1988 Conference on Programming Languages Design and Implementation, Atlanta, Georgia, pp. 164–174 (June 1988)

    Google Scholar 

  32. Shivers, O.: Control-Flow Analysis of Higher-Order Languages or Taming Lambda. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Report CMU-CS-91-145 (May 1991)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Rennes - Bretagne Atlantique,  

    Jan Midtgaard

  2. CNRS IRISA, Campus de Beaulieu, 35042, Rennes Cedex, France

    Thomas Jensen

Authors
  1. Jan Midtgaard
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Jensen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

María Alpuente Germán Vidal

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Midtgaard, J., Jensen, T. (2008). A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. In: Alpuente, M., Vidal, G. (eds) Static Analysis. SAS 2008. Lecture Notes in Computer Science, vol 5079. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69166-2_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-69166-2_23

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-69163-1

  • Online ISBN: 978-3-540-69166-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation