Skip to main content
SpringerLink
Log in

Modeling Undefined Behaviour Semantics for Checking Equivalence Across Compiler Optimizations

  • Conference paper
  • First Online:
Hardware and Software: Verification and Testing (HVC 2017)

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

Included in the following conference series:

Abstract

Previous work on equivalence checking for synthesis and translation validation has usually verified programs across selected optimizations, disabling the ones that exploit undefined behaviour. On the other hand, modern compilers extensively exploit language level undefined behaviour for optimization. Previous work on equivalence checking for translation validation and synthesis yields poor results, when such optimizations relying on undefined behaviour are enabled.

We extend previous work on simulation-based equivalence checking, by adding a framework for reasoning about language level undefined behaviour. We implement our ideas in a tool to compare equivalence across compiler optimizations produced by GCC and LLVM. Testing these compiler optimizations on programs taken from the SPEC integer benchmark suite, we find that modeling undefined behaviour semantics improves success rates for equivalence checking by 31 percentage points (from 50% to 81%) on average, almost uniformly across the two compilers. This significant difference in success rates confirms the widespread impact of undefined behaviour on compiler optimization, something that has been ignored by previous work on equivalence checking. Further, our work brings insight into the relative significance of the different types of C undefined behaviour on compiler optimization.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Bodik, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: FMCAD (2013)

    Google Scholar 

  2. Bansal, S., Aiken, A.: Automatic generation of peephole superoptimizers. In: ASPLOS XII (2006)

    Google Scholar 

  3. Dahiya, M., Bansal, S.: Black-box equivalence checking across compiler optimizations. In: APLAS 2017 (2017)

    Google Scholar 

  4. Debray, S., Muth, R., Weippert, M.: Alias analysis of executable code. In: POPL 1998 (1998)

    Google Scholar 

  5. Felsing, D., Grebing, S., Klebanov, V., Rümmer, P., Ulbrich, M.: Automating regression verification. In: ASE 2014 (2014)

    Google Scholar 

  6. Fernández, M., Espasa, R.: Speculative alias analysis for executable code. In: PACT 2002 (2002)

    Google Scholar 

  7. Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45251-6_29

    Chapter  Google Scholar 

  8. GCC Bugzilla - Bug 68480. https://gcc.gnu.org/bugzilla/show_bug.cgi?id=68480

  9. Hawblitzel, C., Lahiri, S.K., Pawar, K., Hashmi, H., Gokbulut, S., Fernando, L., Detlefs, D., Wadsworth, S.: Will you still compile me tomorrow? static cross-version compiler validation. In: ESEC/FSE 2013 (2013)

    Google Scholar 

  10. Kanade, A., Sanyal, A., Khedker, U.P.: Validation of gcc optimizers through trace generation. Softw. Pract. Exper. (2009)

    Google Scholar 

  11. Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: PLDI 2009 (2009)

    Google Scholar 

  12. Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Rebêlo, H.: Symdiff: a language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 712–717. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_54

    Chapter  Google Scholar 

  13. Lahiri, S.K., Sinha, R., Hawblitzel, C.: Automatic rootcausing for program equivalence failures in binaries. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 362–379. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_21

    Chapter  Google Scholar 

  14. Lee, J., Kim, Y., Song, Y., Hur, C.K., Das, S., Majnemer, D., Regehr, J., Lopes, N.P.: Taming undefined behavior in llvm. In: PLDI 2017 (2017)

    Google Scholar 

  15. Leung, A., Bounov, D., Lerner, S.: C-to-verilog translation validation. In: MEMOCODE (2015)

    Google Scholar 

  16. Lopes, N.P., Menendez, D., Nagarakatte, S., Regehr, J.: Provably correct peephole optimizations with alive. In: PLDI 2015 (2015)

    Google Scholar 

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

    Google Scholar 

  18. Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0054170

    Chapter  Google Scholar 

  19. Poetzsch-Heffter, A., Gawkowski, M.: Towards proof generating compilers. Electron. Notes Theor. Comput. Sci. (2005)

    Google Scholar 

  20. Sharma, R., Schkufza, E., Churchill, B., Aiken, A.: Data-driven equivalence checking. In: OOPSLA 2013 (2013)

    Google Scholar 

  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). https://doi.org/10.1007/978-3-642-22110-1_59

    Chapter  Google Scholar 

  22. Strichman, O., Godlin, B.: Regression verification - a practical way to verify programs. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 496–501. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-69149-5_54

    Chapter  Google Scholar 

  23. Torvalds, L.: https://lkml.org/lkml/2007/5/7/213

  24. Torvalds, L.: https://gcc.gnu.org/ml/gcc/2002-01/msg00395.html

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

    Google Scholar 

  26. Wang, X., Zeldovich, N., Kaashoek, M.F., Solar-Lezama, A.: Towards optimization-safe systems. In: SOSP 2013 (2013)

    Google Scholar 

  27. Zaks, A., Pnueli, A.: CoVaC: compiler validation by program analysis of the cross-product. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 35–51. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0_5

    Chapter  Google Scholar 

  28. Zuck, L., Pnueli, A., Fang, Y., Goldberg, B.: Voc: A methodology for the translation validation of optimizing compilers 9(3) (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Indian Institute of Technology Delhi, New Delhi, India

    Manjeet Dahiya & Sorav Bansal

Authors
  1. Manjeet Dahiya
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sorav Bansal
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Manjeet Dahiya .

Editor information

Editors and Affiliations

  1. Technion - Israel Institute of Technology, Haifa, Israel

    Ofer Strichman

  2. IBM Research Lab, Haifa, Israel

    Rachel Tzoref-Brill

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Dahiya, M., Bansal, S. (2017). Modeling Undefined Behaviour Semantics for Checking Equivalence Across Compiler Optimizations. In: Strichman, O., Tzoref-Brill, R. (eds) Hardware and Software: Verification and Testing. HVC 2017. Lecture Notes in Computer Science(), vol 10629. Springer, Cham. https://doi.org/10.1007/978-3-319-70389-3_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-70389-3_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-70388-6

  • Online ISBN: 978-3-319-70389-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation