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.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Partially funded by Spanish project TIN2009-14599 DESAFIOS 10, and Madrid Regional project S2009TIC-1465 PROMETIDOS, and French project ANR Verasco, FNRAE ASCERT and Bretagne Regional project CertLogS.
Download to read the full chapter text
Chapter PDF
References
Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: POPL 1988. ACM (1988)
Appel, A.W.: SSA is functional programming. SIGPLAN Notices 33 (1998)
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)
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)
Briggs, P., Cooper, K.D., Simpson, L.T.: Value numbering. In: SPE (1997)
Companion web page, http://www.irisa.fr/celtique/ext/compcertSSA
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)
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)
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)
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)
Knoop, J., Rüthing, O., Steffen, B.: Lazy code motion. In: PLDI 1992 (1992)
Lengauer, T., Tarjan, R.E.: A fast algorithm for finding dominators in a flowgraph. In: ACM TOPLAS (1979)
Leroy, X.: A formally verified compiler back-end. JAR 43(4) (2009)
The LLVM compiler infrastructure, http://llvm.org/
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)
Matsuno, Y., Ohori, A.: A type system equivalent to static single assignment. In: PPDP 2006. ACM (2006)
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)
Necula, G.: Translation validation for an optimizing compiler. In: PLDI 2000. ACM (2000)
Pnueli, A., Siegel, M.D., Singerman, E.: Translation Validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998)
Rideau, L., Serpette, B.P., Leroy, X.: Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves. In: JAR (2008)
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)
Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. In: POPL 2009. ACM (2009)
Tristan, J.B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: PLDI 2011. ACM (2011)
Tristan, J.B., Leroy, X.: Verified validation of lazy code motion. In: PLDI 2009. ACM (2009)
Tristan, J.B., Leroy, X.: A simple, verified validator for software pipelining. In: POPL 2010. ACM (2010)
Zhao, J., Zdancewic, S., Nagarakatte, S., Martin, M.: Formalizing the LLVM intermediate representation for verified program transformation. In: POPL 2012. ACM (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barthe, G., Demange, D., Pichardie, D. (2012). A Formally Verified SSA-Based Middle-End. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)