publication . Preprint . 2017

Souper: A Synthesizing Superoptimizer

Sasnauskas, Raimondas; Chen, Yang; Collingbourne, Peter; Ketema, Jeroen; Lup, Gratian; Taneja, Jubi; Regehr, John;
Open Access English
  • Published: 13 Nov 2017
If we can automatically derive compiler optimizations, we might be able to sidestep some of the substantial engineering challenges involved in creating and maintaining a high-quality compiler. We developed Souper, a synthesizing superoptimizer, to see how far these ideas might be pushed in the context of LLVM. Along the way, we discovered that Souper's intermediate representation was sufficiently similar to the one in Microsoft Visual C++ that we applied Souper to that compiler as well. Shipping, or about-to-ship, versions of both compilers contain optimizations suggested by Souper but implemented by hand. Alternately, when Souper is used as a fully automated op...
ACM Computing Classification System: Software_PROGRAMMINGLANGUAGES
free text keywords: Computer Science - Programming Languages
Related Organizations
Download from
25 references, page 1 of 2

[1] A. W. Appel. SSA is functional programming. SIGPLAN Not., 33(4):17-20, Apr. 1998.

[2] S. Bansal and A. Aiken. Automatic generation of peephole superoptimizers. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 394-403, 2006.

[3] C. Barrett, A. Stump, and C. Tinelli. The SMT-LIB Standard: Version 2.0. In A. Gupta and D. Kroening, editors, Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, 2010.

[4] S. Buchwald. Optgen: A Generator for Local Optimizations, pages 171-189. London, UK, Apr. 2015. [OpenAIRE]

[5] C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI'08, pages 209-224, 2008.

[6] R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst., 13(4):451-490, Oct. 1991.

[7] W. Dietz, P. Li, J. Regehr, and V. Adve. Understanding integer overflow in C/C++. ACM Trans. Softw. Eng. Methodol., 25(1): 2:1-2:29, Dec. 2015. [OpenAIRE]

[8] C. W. Fraser. A compact, machine-independent peephole optimizer. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '79, pages 1-6, 1979.

[9] T. Granlund and R. Kenner. Eliminating branches using a superoptimizer and the GNU C Compiler. In Proceedings of the ACM SIGPLAN 1992 Conference on Programming Language Design and Implementation, pages 341-352, 1992. [OpenAIRE]

[10] S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of loop-free programs. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '11, pages 62-73, 2011.

[11] R. R. Kessler. Peep: An architectural description driven peephole optimizer. In Proceedings of the 1984 SIGPLAN Symposium on Compiler Construction, pages 106-110, 1984.

[12] C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In Proceedings of the International Symposium on Code Generation and Optimization: Feedback-directed and Runtime Optimization, pages 75-88, 2004. [OpenAIRE]

[13] X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, July 2009. [OpenAIRE]

[14] N. P. Lopes, D. Menendez, S. Nagarakatte, and J. Regehr. Provably correct peephole optimizations with Alive. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 22-32, 2015.

[15] H. Massalin. Superoptimizer: A look at the smallest program. In Proceedings of the Second International Conference on Architectual Support for Programming Languages and Operating Systems, pages 122-126, 1987. [OpenAIRE]

25 references, page 1 of 2
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue