nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Relatively Complete Pushdown Analysis of Escape Continuations

verfasst von : Kimball Germane, Matthew Might

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Escape continuations are weaker than full, first-class continuations but nevertheless can express many common control operators. Although language and compiler designs profitably leverage escape continuations, all previous approaches to analyze them statically in a higher-order setting have been ad hoc or imprecise. We present \(\mathrm {MCCFA}2\), a generalization of \(\mathrm {CFA}2\) that analyzes them with pushdown precision in their most-general form. In particular, the summarization algorithm of \(\mathrm {MCCFA}2\) is both sound and complete with respect to a conservative extension of \(\mathrm {CFA}2\)’s abstract semantics. We also present an continuation age analysis as a client of \(\mathrm {MCCFA}2\) that reveals critical function call optimizations.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs

Nächstes Kapitel Demand Control-Flow Analysis

Of course, even return calls the current continuation, but we consider such uses essentially trivial.

Deviating from \(\mathrm {CFA}2\), we omit environments from stack frames as well. This is only to simplify the presentation; they can be reintroduced without difficulty.

Adams, N., Kranz, D., Kelsey, R., Rees, J., Hudak, P., Philbin, J.: ORBIT: an optimizing compiler for scheme. In: SIGPLAN 1986. ACM, New York (1986)

Appel, A.W.: Compiling with Continuations. Cambridge University Press, Cambridge (2007)

Earl, C., Might, M., Van Horn, D.: Pushdown control-flow analysis of higher-order programs. In: Workshop on Scheme and Functional Programming (2010)

Felleisen, M.: On the expressive power of programming languages. Sci. Comput. Program. 17(1), 35–75 (1991)MathSciNetCrossRef

Germane, K., Might, M.: Multi-continuation pushdown analysis. Technical report, January 2019. http://kimball.germane.net/germane-mccfa2-techreport.pdf

Gilray, T., Lyde, S., Adams, M.D., Might, M., Van Horn, D.: Pushdown control-flow analysis for free. In: Proceedings of the 43rd Annual ACM Symposium on Principles of Programming Languages. POPL 2016, pp. 691–704. ACM, New York (2016)

Hieb, R., Dybvig, R.K., Bruggeman, C.: Representing control in the presence of first-class continuations. In: Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation. PLDI 1990, pp. 66–77. ACM, New York (1990)

Johnson, J.I., Van Horn, D.: Abstracting abstract control. In: Proceedings of the 10th ACM Symposium on Dynamic languages, pp. 11–22. ACM (2014)

Kennedy, A.: Compiling with continuations, continued. In: Proceedings of the 12th ACM International Conference on Functional Programming. ICFP 2007, pp. 177–190. ACM, New York (2007)

10.

Kim, J., Yi, K., Danvy, O.: Assessing the overhead of ML exceptions by selective CPS transformation, vol. 5, January 1998

11.

Ley-Wild, R., Fluet, M., Acar, U.A.: Compiling self-adjusting programs with continuations. In: Proceedings of the 13th ACM International Conference on Functional Programming. ICFP 2008, pp. 321–334. ACM, New York (2008)

12.

Liang, S., Sun, W., Might, M., Keep, A., Horn, D.V.: Pruning, pushdown exception-flow analysis. In: Proceedings of the 2014 IEEE 14th International Working Conference on Source Code Analysis and Manipulation, pp. 265–274. IEEE Computer Society (2014)

13.

Might, M.: Environment analysis of higher-order languages (2007)

14.

Might, M., Shivers, O.: Environment analysis via \(\Delta \)CFA. In: Conference Record of the 33rd ACM Symposium on Principles of Programming Languages. POPL 2006, pp. 127–140. ACM, New York (2006)

15.

Shivers, O.: Control-flow analysis of higher-order languages. Ph.D. thesis. Carnegie Mellon University (1991)

16.

Shivers, O., Fisher, D.: Multi-return function call. J. Funct. Program. 16(4), 547–582 (2006)MathSciNetCrossRef

17.

Thielecke, H.: Comparing control constructs by double-barrelled CPS. Higher-Order Symb. Comput. 15(2), 141–160 (2002)CrossRef

18.

Van Horn, D., Might, M.: Abstracting abstract machines. In: Proceedings of the 15th ACM International Conference on Functional Programming. ICFP 2010, pp. 51–62. ACM, New York (2010)

19.

Vardoulakis, D., Shivers, O.: CFA2: a context-free approach to control-flow analysis. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 570–589. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11957-6_30CrossRef

20.

Vardoulakis, D., Shivers, O.: Ordering multiple continuations on the stack. In: Proceedings of the 20th ACM Workshop on Partial Evaluation and Program Manipulation. PEPM 2011, pp. 13–22. ACM, New York (2011)

21.

Vardoulakis, D., Shivers, O.: Pushdown flow analysis of first-class control. In: Proceedings of the 16th ACM International Conference on Functional Programming. ICFP 2011, pp. 69–80. ACM, New York (2011)

Titel: Relatively Complete Pushdown Analysis of Escape Continuations
verfasst von: Kimball Germane
Matthew Might
Verlag: Springer International Publishing
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-11244-8

Electronic ISBN: 978-3-030-11245-5

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-11245-5_10

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"