Article

Free access

Infinitary control flow analysis: a collecting semantics for closure analysis

Authors:

Flemming Nielson,

Hanne Riis NielsonAuthors Info & Claims

POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 332 - 345

https://doi.org/10.1145/263699.263745

Published: 01 January 1997 Publication History

Abstract

Defining the collecting semantics is usually the first crucial step in adapting the general methodology of abstract interpretation to the semantic framework or programming language at hand. In this paper we show how to define a collecting semantics for control flow analysis: due to the generality of the formulation we need to appeal to coinduction (or greatest fixed points) in order to define the analysis. We then prove the semantic soundness of the collecting semantics and that all totally deterministic instantiations have a least solution; this incorporates k-CFA, polymorphic splitting and a new class of uniform-k-CFA analyses.

References

[1]

A. Aiken, E. L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Proc. POPL'94, pages 163-173, 1994.

Digital Library

[2]

P. Cousot and Ft. Cousot. Abstract Interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in Proc. 4th POPL, pages 238-252. ACM Press, 1977.

Digital Library

[3]

P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. 6th POPL, pages 269-282, 1979.

Digital Library

[4]

P. Cousot and R. Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In Proc. FPCA '95, pages 170-181. ACM Press, 1995.

Digital Library

[5]

A. Deutsch. Interprocedural may-aliasing for pointers: beyond k-limiting. In Proc. PLDI '94, pages 230-241. ACM Press, 1994.

Digital Library

[6]

K.-F. Fax6n. Optimizing lazy functional programs using flow inference. In Proc. SAS '95, pages 136- 153. SLNCS 983, 1995.

Digital Library

[7]

M. Felleisen and D. P. Friedman. Control operators, the SECD-machine, and the A-calculus. In Formal Description of Programming Concepts 111. North-Holland, 1986.

[8]

C. Flanagan and M. Felleisen. The semantics of future and its use in program optimization. In Prvc. POPL '95, pages 209-220. ACM Press, 1995.

Digital Library

[9]

N. Heintze. Set-based analysis of ML programs. In Proc. LFP'94, pages 306-317, 1994.

Digital Library

[10]

S. Jagannathan and S. Weeks. A unified treatment of flow analysis in higher-order languages. In Prvc. POPL '95. ACM Press, 1995.

Digital Library

[11]

S. Jagannathan and A. Wright. Effective flow analysis for avoiding run-time checks, in Proc. SAS '95, pages 207-224. SLNCS 983, 1995.

Digital Library

[12]

N. D. Jones and F. Nielson. Abstract Interpretation: a semantics-based tool for program analysis. In Handbook of Logic in Computer Science vol. 4. Oxford University Press, 1995.

Digital Library

[13]

J. Palsberg. Closure analysis in constraint form. ACM TOPLAS, 17 (1):47-62, 1995.

Digital Library

[14]

G. D. Plotkin. A structural approach to operational semantics. Technical Report FN-19, DAIMI, Aarhus University, Denmark, 1981.

[15]

P. Sestoft. Analysis and e.Oicient implementation of functional programs. Ph.D.-thesis, Department of Computer Science, University of Copenhagen, Denmark, 1991.

[16]

O. Shivers. Control flow analysis in Scheme. In Proc. PLDI'88, pages 164-174. ACM Sigplan Notices 7 (1), 1988.

Digital Library

[17]

O. Shivers. The semantics of Scheme control-flow analysis. In Partial Evaluation and Semantics- Based Program Manipulation. ACM SIGPLAN Notices 26 (9), 1991.

Digital Library

[18]

M. Wand and P. Steckler. Selective and lightweight closure conversion. In Proc. POPL '94, pages 435- 445. ACM Press, 1994.

Digital Library

Cited By

Montagu BJensen TFreund SYahav E(2021)Trace-based control-flow analysisProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454057(482-496)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454057
Pavlinovic ZSu YWies T(2021)Data flow refinement type inferenceProceedings of the ACM on Programming Languages10.1145/34343005:POPL(1-31)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434300
Contractor MFluet M(2020)Type- and Control-Flow Directed DefunctionalizationProceedings of the 32nd Symposium on Implementation and Application of Functional Languages10.1145/3462172.3462193(79-92)Online publication date: 2-Sep-2020
https://dl.acm.org/doi/10.1145/3462172.3462193
Show More Cited By

Index Terms

Infinitary control flow analysis: a collecting semantics for closure analysis
1. Theory of computation

Recommendations

Control flow analysis in scheme
Proceedings of the SIGPLAN '88 conference on Programming language design and implementation

Traditional flow analysis techniques, such as the ones typically employed by optimizing Fortran compilers, do not work for Scheme-like languages. This paper presents a flow analysis technique — control flow analysis — which is applicable to Scheme-like ...
Control flow analysis
Proceedings of a symposium on Compiler optimization

Any static, global analysis of the expression and data relationships in a program requires a knowledge of the control flow of the program. Since one of the primary reasons for doing such a global analysis in a compiler is to produce optimized programs, ...
Bidirectional data flow analysis for type inferencing

Tennenbaum's data flow analysis based formulation of type inferencing is termed bidirectional in the ''Dragon Book''; however, it fails to qualify as a formal data flow framework and is not amenable to complexity analysis. Further, the types discovered ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 1997

497 pages

ISBN:0897918533

DOI:10.1145/263699

Chairmen:
Peter Lee
Carnegie Mellon Univ., Pittsburgh, PA
,
Fritz Henglein
Univ. of Copenhagen, Copenhagen, Denmark
,
Neil D. Jones
Univ. of Copenhagen, Copenhagen, Denmark

Copyright © 1997 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
Ctr Natl de la Recherche Sci
L'Ecole des Mines de Paris: L'Ecole des Mines de Paris
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1997

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL97

Sponsor:

SIGPLAN
Ctr Natl de la Recherche Sci
L'Ecole des Mines de Paris
SIGACT

POPL97: 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 15 - 17, 1997

Paris, France

Acceptance Rates

POPL '97 Paper Acceptance Rate 36 of 225 submissions, 16%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

80
Total Citations
View Citations
161
Total Downloads

Downloads (Last 12 months)56
Downloads (Last 6 weeks)6

Reflects downloads up to 22 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Montagu BJensen TFreund SYahav E(2021)Trace-based control-flow analysisProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454057(482-496)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454057
Pavlinovic ZSu YWies T(2021)Data flow refinement type inferenceProceedings of the ACM on Programming Languages10.1145/34343005:POPL(1-31)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434300
Contractor MFluet M(2020)Type- and Control-Flow Directed DefunctionalizationProceedings of the 32nd Symposium on Implementation and Application of Functional Languages10.1145/3462172.3462193(79-92)Online publication date: 2-Sep-2020
https://dl.acm.org/doi/10.1145/3462172.3462193
Germane KMcCarthy JAdams MMight M(2019)Demand Control-Flow AnalysisVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-11245-5_11(226-246)Online publication date: 11-Jan-2019
https://doi.org/10.1007/978-3-030-11245-5_11
Darais DMight MVan Horn D(2015)Galois transformers and modular abstract interpreters: reusable metatheory for program analysisACM SIGPLAN Notices10.1145/2858965.281430850:10(552-571)Online publication date: 23-Oct-2015
https://dl.acm.org/doi/10.1145/2858965.2814308
Darais DMight MVan Horn DAldrich JEugster P(2015)Galois transformers and modular abstract interpreters: reusable metatheory for program analysisProceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications10.1145/2814270.2814308(552-571)Online publication date: 23-Oct-2015
https://dl.acm.org/doi/10.1145/2814270.2814308
Pierro AWiklicky H(2015)Probabilistic Abstract InterpretationEssays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays on Semantics, Logics, and Calculi - Volume 956010.1007/978-3-319-27810-0_6(111-139)Online publication date: 1-Oct-2015
https://dl.acm.org/doi/10.1007/978-3-319-27810-0_6
Adsit CFluet M(2014)An Efficient Type- and Control-Flow Analysis for System FProceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages10.1145/2746325.2746327(1-14)Online publication date: 1-Oct-2014
https://dl.acm.org/doi/10.1145/2746325.2746327
Glaze DLabich NMight MVan Horn D(2013)Optimizing abstract abstract machinesACM SIGPLAN Notices10.1145/2544174.250060448:9(443-454)Online publication date: 25-Sep-2013
https://dl.acm.org/doi/10.1145/2544174.2500604
Glaze DLabich NMight MVan Horn DMorrisett GUustalu T(2013)Optimizing abstract abstract machinesProceedings of the 18th ACM SIGPLAN international conference on Functional programming10.1145/2500365.2500604(443-454)Online publication date: 25-Sep-2013
https://dl.acm.org/doi/10.1145/2500365.2500604
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents