Equivalence checking and Verified compilation

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.

• Install the equivalence checker on the browser as a vscode.dev extension
• Authenticate using your email address
• Start an equivalence check
• View an equivalence proof and the search tree of a proof
• Save and load a session
• Examples of successful equivalence checks with proofs

Install the equivalence checker on the browser

1. Go to https://vscode.dev
   
   
2. Click on the sixth icon from the top on the left pane, labeled "Extensions" (Ctrl+Shift+X).
   
3. Search for the "Eqchecker" extension by CompilerAI.
   
4. Check the version number of the "Eqchecker" extension. It should be at least 0.9.0.
   
5. Install the "Eqchecker" extension.
   
6. Wait for the extension to get installed.
   

Authenticate using your email address

1. Click on the second icon from the top on the left pane, labeled "Explorer" (Ctrl+Shift+E). Expand the "Equivalence Checks" and "Search Tree" panes by clicking on them.
   
2. Click on "Login" in the "Equivalence Checks" pane.
   
3. Enter your email address. Each email address is given a free quota of ten equivalence checks per month. We need to enforce this quota due to the compute intensive nature of an equivalence check. After you enter your email address and press enter, a One-Time-Password (OTP) will be sent to your email address.
   
4. Enter the four digit OTP received on your email address.
   

Start an equivalence check

1. Click on the first icon from the top on the left pane to open a command menu. Open the files (or create new files) in the editor, for which you would like to compute equivalence or perform verified compilation.
   
2. Click on "Start an Eqcheck" button to start an equivalence check. The button displays the email address of the current user and the number of remaining equivalence checks in her quota. Upon clicking this button, you are presented a drop-down menu of potential equivalence checks (or verified compilations) that you can perform on the opened files.

   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.

   
3. After an equivalence check (or verified compilation) begins, the progress of the compilation is shown as an eqcheck entry in the "Equivalence Checks" pane. The status of the corresponding entry updates as the equivalence check proceeds.

   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.

   
4. A successful equivalence check is represented by a green-coloured eqcheck pane, labeled "Found proof and safety".
   

View an equivalence proof and the search tree for a proof

1. For a successful equivalence check, you can right-click on the eqcheck entry to select "View Proof".
   
2. The visual proof is represented as a "Product Graph". Each edge of the product graph encodes the lockstep execution of the two programs being compared for equivalence. Each node of the product graph represents the correlated PC (program counter) addresses of the two programs.

   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.

   
3. Our equivalence checker constructs the equivalence proof incrementally. The proof construction is designed as a search algorithm. It is possible to view the search tree, both for an ongoing equivalence check, and for a completed equivalence check. This can be done by right-clicking on an eqcheck entry and selecting "View Search Tree".

   If the equivalence checker fails to successfully prove equivalence, the user may inspect the search tree to understand the reasons for the equivalence failure.

   
4. The search tree is displayed in the "Search Tree" pane in a tree representation. The tree represents all the different product-graphs explored by the equivalence checker before arriving at a final proof.

   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.

   

Save and load a session

Examples of successful equivalence checks with proofs

• Testsuite for Vectorizing Compilers at O3 optimization: session name tsvc.
  The compilations of these programs involve aggressive loop vectorizing transformations.
• The bzip2 compression utility at O1 optimization: session name bzip2.
  These are larger functions with complex control flow and memory allocation patterns.

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.