Skip to main content
SpringerLink
Log in

Black-Box Equivalence Checking Across Compiler Optimizations

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2017)

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

Included in the following conference series:

Abstract

Equivalence checking is an important building block for program synthesis and verification. For a synthesis tool to compete with modern compilers, its equivalence checker should be able to verify the transformations produced by these compilers. We find that the transformations produced by compilers are much varied and the presence of undefined behaviour allows them to produce even more aggressive optimizations. Previous work on equivalence checking has been done in the context of translation validation, where either a pass-by-pass based approach was employed or a set of handpicked optimizations were proven. These settings are not suitable for a synthesis tool where a black-box approach is required.

This paper presents the design and implementation of an equivalence checker which can perform black-box checking across almost all the composed transformations produced by modern compilers. We evaluate the checker by testing it across unoptimized and optimized binaries of SPEC benchmarks generated by gcc, clang, icc and ccomp. The tool has overall success rates of 76% and 72% for O2 and O3 optimizations respectively, for this first of its kind experiment.

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 EPUB and 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

Notes

  1. 1.

    a-b-c is sequential composition of edges a-b and b-c. a-b-c||a-d-c is parallel composition of edges a-b-c and a-d-c.

  2. 2.

    In the programs we consider, the only method to perform I/O is through function calls (that may internally invoke system calls).

References

  1. Bansal, S., Aiken, A.: Automatic generation of peephole superoptimizers. In: Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XII, pp. 394–403. ACM (2006)

    Google Scholar 

  2. Bansal, S., Aiken, A.: Binary translation using peephole superoptimizers. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI 2008, pp. 177–192. USENIX Association (2008)

    Google Scholar 

  3. Churchill, B., Sharma, R., Bastien, J., Aiken, A.: Sound loop superoptimization for Google native client. In: Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2017, pp. 313–326. ACM (2017)

    Google Scholar 

  4. Dahiya, M., Bansal, S.: Modeling undefined behaviour semantics for checking equivalence across compiler optimizations. In: Hardware and Software: Verification and Testing - 13th International Haifa Verification Conference, HVC 2017 (2017)

    Google Scholar 

  5. De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008/ETAPS 2008, pp. 337–340 (2008)

    Google Scholar 

  6. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_49

    Google Scholar 

  7. Felsing, D., Grebing, S., Klebanov, V., Rümmer, P., Ulbrich, M.: Automating regression verification. In: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE 2014, pp. 349–360. ACM (2014)

    Google Scholar 

  8. 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 

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

  10. 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: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013, pp. 191–201. ACM (2013)

    Google Scholar 

  11. ICC developer forums discussion: icc-16.0.3 not respecting fno-strict-overflow flag? https://software.intel.com/en-us/forums/intel-c-compiler/topic/702516

  12. ICC developer forums discussion: icc-16.0.3 not respecting no-ansi-alias flag? https://software.intel.com/en-us/forums/intel-c-compiler/topic/702187

  13. Kanade, A., Sanyal, A., Khedker, U.P.: Validation of GCC optimizers through trace generation. Softw. Pract. Exper. 39(6), 611–639 (2009)

    Article  Google Scholar 

  14. Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, pp. 327–337. ACM (2009)

    Google Scholar 

  15. 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 

  16. 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 

  17. Le, V., Afshari, M., Su, Z.: Compiler validation via equivalence modulo inputs. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 216–226. ACM (2014)

    Google Scholar 

  18. Le, V., Sun, C., Su, Z.: Finding deep compiler bugs via guided stochastic program mutation. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, pp. 386–399. ACM (2015)

    Google Scholar 

  19. Lerner, S., Millstein, T., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, PLDI 2003, pp. 220–231. ACM (2003)

    Google Scholar 

  20. Lerner, S., Millstein, T., Rice, E., Chambers, C.: Automated soundness proofs for dataflow analyses and transformations via local rules. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, pp. 364–377. ACM (2005)

    Google Scholar 

  21. Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd ACM Symposium on Principles of Programming Languages, pp. 42–54. ACM Press (2006)

    Google Scholar 

  22. Leung, A., Bounov, D., Lerner, S.: C-to-verilog translation validation. In: Formal Methods and Models for Codesign (MEMOCODE), pp. 42–47 (2015)

    Google Scholar 

  23. Lopes, N.P., Menendez, D., Nagarakatte, S., Regehr, J.: Provably correct peephole optimizations with alive. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 22–32. ACM (2015)

    Google Scholar 

  24. Lopes, N.P., Monteiro, J.: Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. Int. J. Softw. Tools Technol. Transf. 18(4), 359–374 (2016)

    Article  Google Scholar 

  25. Massalin, H.: Superoptimizer: a look at the smallest program. In: Proceedings of the Second International Conference on Architectual Support for Programming Languages and Operating Systems, ASPLOS II, pp. 122–126. IEEE Computer Society Press (1987)

    Google Scholar 

  26. Necula, G.C.: Translation validation for an optimizing compiler. In: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, PLDI 2000, pp. 83–94. ACM (2000)

    Google Scholar 

  27. Phothilimthana, P.M., Thakur, A., Bodik, R., Dhurjati, D.: Scaling up superoptimization. In: Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2016, pp. 297–310. ACM (2016)

    Google Scholar 

  28. 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 

  29. Poetzsch-Heffter, A., Gawkowski, M.: Towards proof generating compilers. Electron. Notes Theor. Comput. Sci. 132(1), 37–51 (2005)

    Article  Google Scholar 

  30. Samet, H.: Proving the correctness of heuristically optimized code. Commun. ACM 21(7), 570–582 (1978)

    Article  MATH  Google Scholar 

  31. Schkufza, E., Sharma, R., Aiken, A.: Stochastic superoptimization. In: Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2013, pp. 305–316. ACM (2013)

    Google Scholar 

  32. Sharma, R., Schkufza, E., Churchill, B., Aiken, A.: Data-driven equivalence checking. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2013, pp. 391–406. ACM (2013)

    Google Scholar 

  33. Sharma, R., Schkufza, E., Churchill, B., Aiken, A.: Conditionally correct superoptimization. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, pp. 147–162. ACM (2015)

    Google Scholar 

  34. 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 

  35. 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 

  36. Tate, R., Stepp, M., Lerner, S.: Generating compiler optimizations from proofs. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 389–402. ACM (2010)

    Google Scholar 

  37. Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, POPL 2009, pp. 264–276. ACM (2009)

    Google Scholar 

  38. Tristan, J.B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 295–305. ACM (2011)

    Google Scholar 

  39. Wang, X., Zeldovich, N., Kaashoek, M.F., Solar-Lezama, A.: Towards optimization-safe systems: analyzing the impact of undefined behavior. In: Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, SOSP 2013 (2013)

    Google Scholar 

  40. Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 283–294. ACM (2011)

    Google Scholar 

  41. 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 

  42. Zhao, J., Nagarakatte, S., Martin, M.M., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pp. 427–440. ACM (2012)

    Google Scholar 

  43. Zhao, J., Nagarakatte, S., Martin, M.M., Zdancewic, S.: Formal verification of SSA-based optimizations for LLVM. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, pp. 175–186. ACM (2013)

    Google Scholar 

  44. Zuck, L., Pnueli, A., Fang, Y., Goldberg, B.: Voc: a methodology for the translation validation of optimizing compilers. J. Univ. Comput. Sci. 9(3), 223–247 (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. University of Colorado, Boulder, Colorado, USA

    Bor-Yuh Evan Chang

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). Black-Box Equivalence Checking Across Compiler Optimizations. In: Chang, BY. (eds) Programming Languages and Systems. APLAS 2017. Lecture Notes in Computer Science(), vol 10695. Springer, Cham. https://doi.org/10.1007/978-3-319-71237-6_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-71237-6_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-71236-9

  • Online ISBN: 978-3-319-71237-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation