[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

CoVaC: Compiler Validation by Program Analysis of the Cross-Product

  • Conference paper
FM 2008: Formal Methods (FM 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5014))

Included in the following conference series:

  • 836 Accesses

Abstract

The paper presents a deductive framework for proving program equivalence and its application to automatic verification of transformations performed by optimizing compilers. To leverage existing program analysis techniques, we reduce the equivalence checking problem to analysis of one system – a cross-product of the two input programs. We show how the approach can be effectively used for checking equivalence of consonant (i.e., structurally similar) programs. Finally, we report on the prototype tool that applies the developed methodology to verify that a compiler optimization run preserves the program semantics. Unlike existing frameworks, CoVaC accommodates absence of compiler annotations and handles most of the classical intraprocedural optimizations such as constant folding, reassociation, common subexpression elimination, code motion, dead code elimination, branch optimizations, and others.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

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

    Chapter  Google Scholar 

  2. Zuck, L., Pnueli, A., Fang, Y., Goldberg, B.: VOC: A methodology for the translation validation of optimizing compilers. Journal of Universal Computer Science 9(3), 223–247 (2003)

    Google Scholar 

  3. Necula, G.C.: Translation validation for an optimizing compiler. In: Programming Language Design and Implementation, pp. 83–95. ACM Press, New York (2000)

    Google Scholar 

  4. Rival, X.: Symbolic transfer function-based approaches to certified compilation. In: POPL, pp. 1–13. ACM Press, New York (2004)

    Google Scholar 

  5. Barthe, G., D’Argenio, P., Rezk, T.: Secure information flow by self-composition. In: Computer Security Foundations Workshop, p. 100. IEEE Computer Society Press, Los Alamitos (2004)

    Google Scholar 

  6. Barthe, G., D’Argenio, P., Rezk, T.: The LLVM Compiler Infrastructure Project, http://llvm.org/ , http://llvm.org/ , http://llvm.org

  7. Zaks, A., Pnueli, A.: CoVaC: Compiler validation by program analysis of the cross-product. Technical report, NYU (2007), http://cs.nyu.edu/acsys/publications.html

  8. Pnueli, A.: Verification of procedural programs. In: We Will Show Them! Essays in Honour of Dov Gabbay, vol. 2, pp. 543–590. College Publications (2005)

    Google Scholar 

  9. Zuck, L., Pnueli, A., Goldberg, B., Barrett, C., Fang, Y., Hu, Y.: Translation and run-time validation of loop tranformations. Formal Methods in System Design 27(3), 335–360 (2005)

    Article  MATH  Google Scholar 

  10. Floyd, R.W.: Assigning meanings to programs. In: Symposia in Applied Mathematics, vol. 19, pp. 19–32 (1967)

    Google Scholar 

  11. Gulwani, S., Necula, G.: Global value numbering using random interpretation. In: POPL, pp. 342–352. ACM Press, New York (2004)

    Google Scholar 

  12. The YICES SMT Solver, http://yices.csl.sri.com , http://yices.csl.sri.com

  13. CVC3: An Automatic Theorem Prover for Satisfiability Modulo Theories (SMT), http://www.cs.nyu.edu/acsys/cvc3/

  14. Simpson, L.T.: Value-Driven Redundancy Elimination. PhD thesis, Rice University (1996)

    Google Scholar 

  15. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  16. Park, D.: Concurrency and automata on infinite sequences. In: 5th GI-Conference on Theoretical Computer Science, pp. 167–183. Springer, Heidelberg (1981)

    Google Scholar 

  17. Fang, Y.: Translation Validation of Optimizing Compilers. PhD thesis, New York University (2005)

    Google Scholar 

  18. Pnueli, A., Zaks, A.: Validation of interprocedural optimizations. In: 7th International Workshop on Compiler Optimization Meets Compiler Verificaiton (2008)

    Google Scholar 

  19. Huang, Y., Childer, B.R., Soffa, M.L.: Catching and identifying bugs in register allocation. In: Static Analysis Symposium, pp. 281–300. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  20. Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes 28(6), 2–2 (2003)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. New York University, New York

    Anna Zaks & Amir Pnueli

Authors
  1. Anna Zaks
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Amir Pnueli
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jorge Cuellar Tom Maibaum Kaisa Sere

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zaks, A., Pnueli, A. (2008). CoVaC: Compiler Validation by Program Analysis of the Cross-Product. In: Cuellar, J., Maibaum, T., Sere, K. (eds) FM 2008: Formal Methods. FM 2008. Lecture Notes in Computer Science, vol 5014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68237-0_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-68237-0_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-68235-6

  • Online ISBN: 978-3-540-68237-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics