These safety-critical sectors are usually governed by software safety standards, e.g., DO-178C (aerospace) requires the developer to verify the executable code, and not just the source code. Current methods to verify executable code are ad hoc --- for example, developers often disable compiler optimizations and undertake laborious manual reviews of the executable code, as required for safety audits.
Based on over eleven years of research at IIT Delhi, we have developed a formal equivalence checker that checks whether the executable code is equivalent to the source code. CompilerAI Labs Pvt. Ltd. is a startup incubated at IIT Delhi that is commercializing this formal equivalence checker. Our equivalence checker can be used by the developers to obtain independently verifiable proofs of correctness of the executable code (with respect to the source code) --- this enables a more systematic validation method for the correctness of a compilation than the current practice. You can test-drive the equivalence checker on your browser by following the steps below.
0.9.0
.
If you choose a verified compilation (e.g., "Compile strlen_src.c
"), the tool first compiles the C source code and then performs an equivalence check between the source code and the generated 32-bit x86 executable. If you choose an equivalence check (e.g., "strlen_src.c
→ strlen_dst.c
"), then an equivalence check is performed between the two C programs, or a C program and an assembly program.
The equivalence checks are performed at function granularity. For two files to be compared for equivalence, they should have functions with the same names (but potentially different implementations) in both files.
If an input file contain multiple functions, a separate eqcheck entry is created for each function, after the initial processing of the input files.
Depending on the complexity of the transformations and the size of the input function, an equivalence check can take anywhere between a few seconds to a few hours. Our research continuously strives to make this faster.
In addition to the product graph, the proof also includes panes that display the two programs (in source, assembly, and IR formats). You can click on an edge of the product graph to view the correlated paths in these programs (in each format). The proof encodes the fact that the correlated paths behave identically and keep the two programs' states related.
This is a formal proof of equivalence: if our tool identifies two programs to be equivalent, then they are (in principle) guaranteed to behave identically for all possible legal inputs to the programs.
If the equivalence checker fails to successfully prove equivalence, the user may inspect the search tree to understand the reasons for the equivalence failure.
You can click on any of the nodes of this search tree to view the (partial) product graph developed incrementally by the algorithm till that stage. Different branches of the tree may represent different product graphs --- it is possible for the search algorithm to backtrack during this search for a proof.
O3
optimization: session name tsvc
.bzip2
compression utility at O1
optimization: session name bzip2
.These examples demonstrate that the equivalence checker is able to compute equivalence for a large category of transformations on a large set of programs. If an equivalence check does not succeed (e.g., it runs for a long time and gets terminated after a timeout), then this may be either because the programs were inequivalent or because our algorithm could not identify an equivalence proof. The latter situation is due to the incompleteness of our equivalence checker. The equivalence checker is always sound --- if a formal equivalence proof is identified by the tool, the two input programs are guaranteed to have equivalent runtime behaviour.
We are continuously improving the completeness of our equivalence checker by minimizing the cases where the equivalence checker is unable to identify an equivalence proof (when the programs were indeed equivalent). If you use the equivalence checker to produce a verified compilation of a C program, you can make the equivalence proof search more tractable by dividing the input C program into smaller individual functions.
Please try the equivalence checker for yourself. Please share your feedback with us at sorav@compiler.ai --- we very much appreciate your critical feedback.