Superoptimizer, Equivalence Checker, and Related Stuff

About is a research effort at re-imagining the compilation infrastructure. We employ AI algorithms to automatically optimize programs. We employ formal verification techniques to generate confidence in the correctness of the optimizations. As our research matures, we intend to provide links to working demos and downloadable packages on this page.

Counter algorithm for blackbox equivalence checking

Are you an assembly language developer? Or do you want to validate the code generated by a compiler? Our equivalence checker can compute equivalence between a C program and its optimized, usually aggressively vectorized assembly code implementation. The assembly code implementation may be generated by a compiler or hand-written. The algorithm that automatically constructs an equivalence proof is called Counter, and to the best of our knowledge, it is the most robust equivalence checking algorithm till date. You can try it yourself at the following online demo links. Our OOPSLA 2020 paper on the Counter algorithm will be out soon.

Counter Demo and Examples

You can run the Counter equivalence checking algorithm for yourself here. Here are some pre-configured examples that demonstrate the Counter algorithm in action. Each row lists a benchmark name (C code); for each benchmark, we demonstrate equivalence computation against O3-optimized assembly implementations generated by the GCC and Clang/LLVM compilers.
s000 clang gcc
s1112 clang gcc
s112 clang gcc
s121 clang gcc
s1221 clang gcc
s122 clang gcc
s1251 clang gcc
s127 clang gcc
s1281 clang gcc
s1351 clang gcc
s162 clang gcc
s173 clang gcc
s176 clang gcc
s2244 clang gcc
s243 clang gcc
s251 clang gcc
s3251 clang gcc
s351 clang gcc
s452 clang gcc
s453 clang gcc
sum1d clang gcc
vdotr clang gcc
vpv clang gcc
vpvpv clang gcc
vpvts clang gcc
vpvtv clang gcc
vtv clang gcc
vtvtv clang gcc
s1111 clang gcc
s1115 clang gcc
s1119 clang gcc
s111 clang gcc
s113 clang gcc
s114 clang gcc
s1161 clang gcc
s116 clang gcc
s119 clang gcc
s1213 clang gcc
s124 clang gcc
s125 clang gcc
s1279 clang gcc
s128 clang gcc
s131 clang gcc
s132 clang gcc
s1421 clang gcc
s171 clang gcc
s174 clang gcc
s2233 clang gcc
s252 clang gcc
s253 clang gcc
s254 clang gcc
s2710 clang gcc
s2711 clang gcc
s2712 clang gcc
s271 clang gcc
s272 clang gcc
s273 clang gcc
s274 clang gcc
s276 clang gcc
s293 clang gcc
s3111 clang gcc
s311 clang gcc
s317 clang gcc
s319 clang gcc
s331 clang gcc
s352 clang gcc
s4115 clang gcc
s421 clang gcc
s423 clang gcc
s441 clang gcc
s442 clang gcc
s443 clang gcc
s471 clang gcc
va clang gcc
vbor clang gcc
vif clang gcc

Counter Download

Counter source code is available at

OOElala optimizing compiler

Programming languages like C and C++ leave the Order of Evaluation of operands in an expression unspecified. This provides optimization leverage, with resulting speedups as high as 2.6x on real-world code. This optimization opportunity was hitherto not exploited by modern compilers. Our optimizing compiler, OOElala, which is based on Clang/LLVM, includes an algorithm to realize this latent performance opportunity. Please see the PLDI 2020 paper on OOElala for more details.

OOElala Demo and Examples

You can try OOElala for yourself here. Here are some pre-configured examples that demonstrate OOElala in action.

OOElala Download

OOElala source code is available at

Relevant Publications

Brief descriptions of these papers are available at this Github page.

Collaborate with us

We are looking for both young and accomplished researchers and engineers to work and/or collaborate with us. If you are interested in sharing the excitement and joy of participating in our efforts towards the creation of a new type of compilation infrastructure, here are some potential ways we can collaborate.
  • Collaborate with us remotely in our development efforts. If you are interested in such a collaboration, please send us a note. We would love to have a meaningful collaboration that may help all of us achieve our research goals faster. That said, we cannot accept all collaboration requests, as we need to carefully balance the synchronization and starting overheads with the benefits of collaborating. Such a collaboration would perhaps work best if you are already an expert working in this domain and you feel interested in knowing more about our efforts.
  • Join us at IIT Delhi either as visiting faculty, Postdoc, or PhD candidate.
  • Join us at IIT Delhi as a Research Associate for a minimum duration of eighteen months.
Please reach out to Sorav Bansal to take this conversation forward.

Acknowledgements: The online demo links are based on Compiler Explorer.