skip to main content
10.1145/1926385.1926397acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Static analysis of multi-staged programs via unstaging translation

Published: 26 January 2011 Publication History

Abstract

Static analysis of multi-staged programs is challenging because the basic assumption of conventional static analysis no longer holds: the program text itself is no longer a fixed static entity, but rather a dynamically constructed value. This article presents a semantic-preserving translation of multi-staged call-by-value programs into unstaged programs and a static analysis framework based on this translation. The translation is semantic-preserving in that every small-step reduction of a multi-staged program is simulated by the evaluation of its unstaged version. Thanks to this translation we can analyze multi-staged programs with existing static analysis techniques that have been developed for conventional unstaged programs: we first apply the unstaging translation, then we apply conventional static analysis to the unstaged version, and finally we cast the analysis results back in terms of the original staged program. Our translation handles staging constructs that have been evolved to be useful in practice (typified in Lisp's quasi-quotation): open code as values, unrestricted operations on references and intentional variable-capturing substitutions. This article omits references for which we refer the reader to our companion technical report.

Supplementary Material

MP4 File (9-mpeg-4.mp4)

References

[1]
Baris Aktemur. Improving Efficiency and Safety of Program Generation. PhD thesis, University of Illinois at Urbana-Champaign, 2009.
[2]
Martin Berger and Laurence Tratt. Program logics for homogeneous meta-programming. In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, to appear, 2010.
[3]
Cristiano Calcagno, Eugenio Moggi, and Walid Taha. Closed types as a simple approach to safe imperative multi-stage programming. In ICALP '00: Proceedings of the 27th International Colloquium on Automata, Languages and Programming, pages 25--36, London, UK, 2000. Springer-Verlag.
[4]
Chiyan Chen and Hongwei Xi. Meta-programming through typeful code representation. In ACM International Conference on Functional Programming, pages 275--286. ACM, August 2003.
[5]
Tae-Hyoung Choi, Oukseh Lee, Hyunha Kim, and Kyung-Goo Doh. A practical string analyzer by the widening approach. In Proceedings of the Asian Symposium on Programming Languages and Systems, volume 4729 of Lecture Notes in Computer Science, pages 374--388, Sydney, Austrailia, November 2006. Springer-Verlag.
[6]
Wontae Choi, Baris Aktemur, and Kwangkeun Yi. Semantics preservation proof of an unstaging translation of lisp-like multi-staged languages. Technical Report ROSAEC-2010-009, ROSAEC Center, Seoul National University, 2010. http://rosaec.snu.ac.kr/publish/2010/techmemo/ROSAEC-2010-009.pdf.
[7]
Aske Simon Christensen, Anders Muller, and Michael I. Schwartzbach. Precise analysis of string expressions. In Proceedings of the Static Analysis Symposium, pages 1--18. Springer-Verlag, 2003.
[8]
Hubert Comon, Max Dauchet, Remi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree automata techniques and applications, April 1999.
[9]
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238--252, Los Angeles, California, 1977. ACM Press, New York, NY.
[10]
P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511--547, 1992.
[11]
Patrick Cousot and Radhia Cousot. Systematic design of program transformation frameworks by abstract interpretation. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages pp.178--190, January 2002.
[12]
Olivier Danvy. Type-directed partial evaluation. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 242--257. ACM, Jan 1996.
[13]
Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 258--270. ACM, 1996.
[14]
Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Journal of the ACM, 48(3):555--604, 2001.
[15]
Kyung-Goo Doh, Hyunha Kim, and David Schmidt. Abstract parsing: static analysis of dynamically generated string output using LR-parsing technology. In Proceeeding of the International Static Analysis Symposium, 2009.
[16]
Dawson R. Engler. VCODE:A retargetable, extensible, very fast dynamic code generation system. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation, pages 160--170, New York, 1996. ACM.
[17]
Ferenc Gécseg and Magnus Steinby. Tree Automata. Akadémiai Kiadó, 1984.
[18]
Paul Graham. On Lisp: an advanced techniques for Common Lisp. Prentice Hall, 1994.
[19]
Nevin Heintze. Set Based Program Analysis. PhD thesis, Carnegie Mellon University, October 1992.
[20]
Nevin Heintze. Set based analysis of ML programs. In Proceedings of the SIGPLAN Conference on Lisp and Functional Programming, pages 306--317, 1994.
[21]
Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial evaluation and automatic program generation. Prentice-Hall, 1993.
[22]
Pierre Jouvelot and David K. Gifford. Algebraic reconstruction of types and effects. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 303--310, 1991.
[23]
Yukiyoshi Kameyama, Oleg Kiselyov, and Chung chieh Shan. Closing the stage: from staged code to typed closure. In Proceedings of The ACM Symposium on Partial Evaluation and Program Manipulations, pages 147--157, 2008.
[24]
Sam Kamin, Baris Aktemur, and Michael Katelman. Staging static analyses for program generation. In GPCE '06: Proceedings of the 5th international conference on Generative programming and component engineering, pages 1--10, New York, NY, USA, 2006. ACM.
[25]
Ik-Soon Kim, Kwangkeun Yi, and Cristiano Calcagno. A polymorphic modal type system for lisp-like multi-staged languages. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 257--269, 2006.
[26]
M. Leone and Peter Lee. Optimizing ML with run-time code generation. In Proceedings of the ACM SIGPLAN'96 Conference on Programming Language Design and Implementation, pages 137--148. ACM Press, June 1996.
[27]
John M. Lucassen and David K. Gifford. Polymorphic effect systems. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 47--57, 1988.
[28]
H. Massalim. An Efficient Implementation of Functional Operating System Services. PhD thesis, Columbia University, 1992.
[29]
Yasuhiko Minamide. Static approximation of dynamically generated web pages. In Proceedings of the International Conference on World Wide Web, pages 432--441, New York, NY, USA, 2005. ACM.
[30]
Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 271--283. ACM, 1996.
[31]
Aleksandar Nanevski and Frank Pfenning. Staged computation with names and necessity. Journal of Functional Programming, 15(6):893--939, 2005.
[32]
Massimilian Poletto, Wilson C. Hsieh, Dawson R. Engler, and M. Frans Kasshoek. C and tcc:a language and compiler for dynamic code generation. ACM Transactions on Programming Languages and Systems, 21:324--369, March 1999.
[33]
Tim Sheard and Simon Peyton Jones. Template meta-programming for Haskell. In Proceedings of The Haskell Workshop, October 2002. http:/www.haskell.org/haskellwiki/Template_Haskell
[34]
Frederick Smith, Dan Grossman, Greg Morrisett, Luke Hornof, and Trevor Jim. Compiling for template-based run-time code generation. Journal of Functional Programming, 13(3):677--708, 2003.
[35]
Guy L. Steele. Common Lisp the Language, 2nd edition. Digital Press, 1990.
[36]
Walid Taha, Cristiano Calcagno, Xavier Leroy, and Ed Pizzi. MetaOCaml. http:/www.metaocaml.org/
[37]
Walid Taha and Michael Florentin Nielsen. Environment classifiers. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 2003.
[38]
Makoto Tatsuta. Translation of multi-staged language. Technical Report NII-2010-003E, National Institute of Informatics, Tokyo, 2010. http://research.nii.ac.jp/TechReports.
[39]
Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λ-calculus using a stack of regions. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 188--201, January 1994.
[40]
Edwin Westbrook, Mathias Ricken, Jun Inoue, Yilong Yao, Tamer Abdelatif, and Walid Taha. Mint: Java multi-stage programming using weak separability. In Proceedings of The ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010.

Cited By

View all
  • (2024)Closure-Free Functional Programming in a Two-Level Type TheoryProceedings of the ACM on Programming Languages10.1145/36746488:ICFP(659-692)Online publication date: 15-Aug-2024
  • (2019)Analysis of MiniJava programs via translation to MLProceedings of the 21st Workshop on Formal Techniques for Java-like Programs10.1145/3340672.3341119(1-3)Online publication date: 15-Jul-2019
  • (2017)Verification of code generators via higher-order model checkingProceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation10.1145/3018882.3018886(59-70)Online publication date: 2-Jan-2017
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2011
652 pages
ISBN:9781450304900
DOI:10.1145/1926385
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 46, Issue 1
    POPL '11
    January 2011
    624 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/1925844
    Issue’s Table of Contents
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

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 January 2011

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. abstract interpretation
  2. multi-staged language
  3. projection
  4. semantics perservation
  5. static analysis
  6. unstaging translation

Qualifiers

  • Research-article

Conference

POPL '11
Sponsor:

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)9
  • Downloads (Last 6 weeks)2
Reflects downloads up to 15 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Closure-Free Functional Programming in a Two-Level Type TheoryProceedings of the ACM on Programming Languages10.1145/36746488:ICFP(659-692)Online publication date: 15-Aug-2024
  • (2019)Analysis of MiniJava programs via translation to MLProceedings of the 21st Workshop on Formal Techniques for Java-like Programs10.1145/3340672.3341119(1-3)Online publication date: 15-Jul-2019
  • (2017)Verification of code generators via higher-order model checkingProceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation10.1145/3018882.3018886(59-70)Online publication date: 2-Jan-2017
  • (2016)Information flow analysis for a dynamically typed language with staged metaprogrammingJournal of Computer Security10.3233/JCS-16055724:5(541-582)Online publication date: 8-Nov-2016
  • (2016)Reasoning about multi-stage programsJournal of Functional Programming10.1017/S095679681600025326Online publication date: 7-Nov-2016
  • (2015)Control Flow Analysis for SF Combinator CalculusElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.199.4199(51-67)Online publication date: 7-Dec-2015
  • (2014)Optimization by runtime specialization for sparse matrix-vector multiplicationACM SIGPLAN Notices10.1145/2775053.265877350:3(93-102)Online publication date: 15-Sep-2014
  • (2014)Optimization by runtime specialization for sparse matrix-vector multiplicationProceedings of the 2014 International Conference on Generative Programming: Concepts and Experiences10.1145/2658761.2658773(93-102)Online publication date: 15-Sep-2014
  • (2014)Building call graphs for embedded client-side code in dynamic web applicationsProceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2635868.2635928(518-529)Online publication date: 11-Nov-2014
  • (2014)Effective quotationProceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation10.1145/2543728.2543738(15-26)Online publication date: 11-Jan-2014
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media