More Web Proxy on the site http://driver.im/

Article

A formally verified SSA-Based middle-end: Static single assignment meets compcert

Authors:

Delphine Demange,

David PichardieAuthors Info & Claims

ESOP'12: Proceedings of the 21st European conference on Programming Languages and Systems

Pages 47 - 66

https://doi.org/10.1007/978-3-642-28869-2_3

Published: 24 March 2012 Publication History

Abstract

CompCert is a formally verified compiler that generates compact and efficient PowerPC, ARM and x86 code for a large and realistic subset of the C language. However, CompCert foregoes using Static Single Assignment (SSA), an intermediate representation that allows for writing simpler and faster optimizers, and is used by many compilers. In fact, it has remained an open problem to verify formally a SSA-based compiler middle-end. We report on a formally verified, SSA-based, middle-end for CompCert. Our middle-end performs conversion from CompCert intermediate form to SSA form, optimization of SSA programs, including Global Value Numbering, and transforming out of SSA to intermediate form. In addition to provide the first formally verified SSA-based middle-end, we address two problems raised by Leroy [13]: giving a simple and intuitive formal semantics to SSA, and leveraging the global properties of SSA to reason locally about program optimizations.

References

[1]

Alpern, B., Wegman, M. N., Zadeck, F. K.: Detecting equality of variables in programs. In: POPL 1988. ACM (1988)

Digital Library

[2]

Appel, A. W.: SSA is functional programming. SIGPLAN Notices 33 (1998)

Digital Library

[3]

Blech, J. O., Glesner, S., Leitner, J., Mülling, S.: Optimizing code generation from SSA form: A comparison between two formal correctness proofs in Isabelle/HOL. In: COCV 2005. ENTCS. Elsevier (2005)

Digital Library

[4]

Briggs, P., Cooper, K. D., Harvey, T. J., Simpson, L. T.: Practical improvements to the construction and destruction of static single assignment form. In: SPE (1998)

Digital Library

[5]

Briggs, P., Cooper, K. D., Simpson, L. T.: Value numbering. In: SPE (1997)

Digital Library

[6]

Companion web page, http://www.irisa.fr/celtique/ext/compcertSSA

[7]

Cytron, R., Ferrante, J., Rosen, B. K., Wegman, M. N., Zadeck, F. K.: Efficiently computing static single assignment form and the control dependence graph. In: ACM TOPLAS (1991)

Digital Library

[8]

Dargaye, Z., Leroy, X.: Mechanized Verification of CPS Transformations. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 211-225. Springer, Heidelberg (2007)

Digital Library

[9]

Hack, S., Grund, D., Goos, G.: Register Allocation for Programs in SSA-Form. In: Mycroft, A., Zeller, A. (eds.) CC 2006. LNCS, vol. 3923, pp. 247-262. Springer, Heidelberg (2006)

Digital Library

[10]

Knoop, J., Koschützki, D., Steffen, B.: Basic-Block Graphs: Living Dinosaurs? In: Koskimies, K. (ed.) CC 1998. LNCS, vol. 1383, pp. 65-79. Springer, Heidelberg (1998)

Digital Library

[11]

Knoop, J., Rüthing, O., Steffen, B.: Lazy code motion. In: PLDI 1992 (1992)

Digital Library

[12]

Lengauer, T., Tarjan, R. E.: A fast algorithm for finding dominators in a flowgraph. In: ACM TOPLAS (1979)

Digital Library

[13]

Leroy, X.: A formally verified compiler back-end. JAR 43(4) (2009)

Digital Library

[14]

The LLVM compiler infrastructure, http://llvm.org/

[15]

Mansky, W., Gunter, E.: A Framework for Formal Verification of Compiler Optimizations. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 371-386. Springer, Heidelberg (2010)

Digital Library

[16]

Matsuno, Y., Ohori, A.: A type system equivalent to static single assignment. In: PPDP 2006. ACM (2006)

Digital Library

[17]

Menon, V., Glew, N., Murphy, B. R., McCreight, A., Shpeisman, T., Adl-Tabatabai, A. R., Petersen, L.: A verifiable SSA program representation for aggressive compiler optimization. In: POPL 2006, ACM (2006)

Digital Library

[18]

Necula, G.: Translation validation for an optimizing compiler. In: PLDI 2000. ACM (2000)

Digital Library

[19]

Pnueli, A., Siegel, M. D., Singerman, E.: Translation Validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151-166. Springer, Heidelberg (1998)

Digital Library

[20]

Rideau, L., Serpette, B. P., Leroy, X.: Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves. In: JAR (2008)

Digital Library

[21]

Stepp, M., Tate, R., Lerner, S.: Equality-Based Translation Validator for LLVM. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 737-742. Springer, Heidelberg (2011)

Digital Library

[22]

Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. In: POPL 2009. ACM (2009)

Digital Library

[23]

Tristan, J. B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: PLDI 2011. ACM (2011)

Digital Library

[24]

Tristan, J. B., Leroy, X.: Verified validation of lazy code motion. In: PLDI 2009. ACM (2009)

Digital Library

[25]

Tristan, J. B., Leroy, X.: A simple, verified validator for software pipelining. In: POPL 2010. ACM (2010)

Digital Library

[26]

Zhao, J., Zdancewic, S., Nagarakatte, S., Martin, M.: Formalizing the LLVM intermediate representation for verified program transformation. In: POPL 2012. ACM (2012)

Digital Library

Cited By

Engel DVerbeek FRavindran B(2023)BIRD: A Binary Intermediate Representation for Formally Verified Decompilation of X86-64 BinariesTests and Proofs10.1007/978-3-031-38828-6_1(3-20)Online publication date: 18-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-38828-6_1
Rosemann JSchneider SHack S(2017)Verified Spilling and Translation Validation with RepairInteractive Theorem Proving10.1007/978-3-319-66107-0_27(427-443)Online publication date: 26-Sep-2017
https://dl.acm.org/doi/10.1007/978-3-319-66107-0_27
Blazy SMaroneze APichardie DLeroy XTiu A(2015)Verified Validation of Program SlicingProceedings of the 2015 Conference on Certified Programs and Proofs10.1145/2676724.2693169(109-117)Online publication date: 13-Jan-2015
https://dl.acm.org/doi/10.1145/2676724.2693169
Show More Cited By

A formally verified SSA-Based middle-end: Static single assignment meets compcert
1. Software and its engineering
  1. Software notations and tools
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Recommendations

Formal Verification of an SSA-Based Middle-End for CompCert

CompCert is a formally verified compiler that generates compact and efficient code for a large subset of the C language. However, CompCert foregoes using SSA, an intermediate representation employed by many compilers that enables writing simpler, faster ...
A formally-verified alias analysis
CPP'12: Proceedings of the Second international conference on Certified Programs and Proofs

This paper reports on the formalization and proof of soundness, using the Coq proof assistant, of an alias analysis: a static analysis that approximates the flow of pointer values. The alias analysis considered is of the points-to kind and is ...
A Fast Verified Liveness Analysis in SSA Form
Automated Reasoning
Abstract
Liveness analysis is a standard compiler analysis, enabling several optimizations such as deadcode elimination. The SSA form is a popular compiler intermediate language allowing for simple and fast optimizations. Boissinot et al. [7] designed a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ESOP'12: Proceedings of the 21st European conference on Programming Languages and Systems

March 2012

599 pages

ISBN:9783642288685

Editor:
Helmut Seidl
Technische Universität München, Boltzmannstrasse 3, Garching, Germany

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 24 March 2012

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Engel DVerbeek FRavindran B(2023)BIRD: A Binary Intermediate Representation for Formally Verified Decompilation of X86-64 BinariesTests and Proofs10.1007/978-3-031-38828-6_1(3-20)Online publication date: 18-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-38828-6_1
Rosemann JSchneider SHack S(2017)Verified Spilling and Translation Validation with RepairInteractive Theorem Proving10.1007/978-3-319-66107-0_27(427-443)Online publication date: 26-Sep-2017
https://dl.acm.org/doi/10.1007/978-3-319-66107-0_27
Blazy SMaroneze APichardie DLeroy XTiu A(2015)Verified Validation of Program SlicingProceedings of the 2015 Conference on Certified Programs and Proofs10.1145/2676724.2693169(109-117)Online publication date: 13-Jan-2015
https://dl.acm.org/doi/10.1145/2676724.2693169
Barthe GDemange DPichardie D(2014)Formal Verification of an SSA-Based Middle-End for CompCertACM Transactions on Programming Languages and Systems10.1145/257908036:1(1-35)Online publication date: 1-Mar-2014
https://dl.acm.org/doi/10.1145/2579080
Carbin MMisailovic SRinard M(2013)Verifying quantitative reliability for programs that execute on unreliable hardwareACM SIGPLAN Notices10.1145/2544173.250954648:10(33-52)Online publication date: 29-Oct-2013
https://dl.acm.org/doi/10.1145/2544173.2509546
Carbin MMisailovic SRinard MHosking AEugster PLopes C(2013)Verifying quantitative reliability for programs that execute on unreliable hardwareProceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications10.1145/2509136.2509546(33-52)Online publication date: 29-Oct-2013
https://dl.acm.org/doi/10.1145/2509136.2509546
Zhao JNagarakatte SMartin MZdancewic S(2013)Formal verification of SSA-based optimizations for LLVMACM SIGPLAN Notices10.1145/2499370.246216448:6(175-186)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2462164
Zhao JNagarakatte SMartin MZdancewic SBoehm HFlanagan C(2013)Formal verification of SSA-based optimizations for LLVMProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2491956.2462164(175-186)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2491956.2462164
Blazy SMaroneze APichardie D(2013)Formal Verification of Loop Bound Estimation for WCET AnalysisRevised Selected Papers of the 5th International Conference on Verified Software: Theories, Tools, Experiments - Volume 816410.1007/978-3-642-54108-7_15(281-303)Online publication date: 17-May-2013
https://dl.acm.org/doi/10.1007/978-3-642-54108-7_15
Myreen MOwens S(2012)Proof-producing synthesis of ML from higher-order logicACM SIGPLAN Notices10.1145/2398856.236454547:9(115-126)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2398856.2364545
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents