Equivalence checking and Verified compilation

The use of safety-critical software applications is growing rapidly in aerospace, defence, automobile, transportation, cybersecurity, and energy sectors. Given the catastrophic costs of a software bug in these sectors, it is not sufficient to use an off-the-shelf commodity compiler to compile the source code to executable code. A modern compiler has millions of lines of code, and tens of bugs are discovered in popular compilers every month. A compiler bug may yield buggy executable code, even when the source code was correct.

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.

Apply for Jobs

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).
    Click on the Extensions icon on the left
  3. Search for the "Eqchecker" extension by CompilerAI.
    Type Eqchecker in the extension search box
  4. Check the version number of the "Eqchecker" extension. It should be at least 0.9.0.
    Check the Eqchecker extension version
  5. Install the "Eqchecker" extension.
    Install the Eqchecker extension
  6. Wait for the extension to get installed.
    Check that the Eqchecker extension is 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.
    Explorer view. Expand the "Equivalence Checks" and "Search Tree" panes
  2. Click on "Login" in the "Equivalence Checks" pane.
    Click on Login
  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.
    Enter your email address
  4. Enter the four digit OTP received on your email address.
    Enter the 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.
    Open files for which you want to compute equivalence
  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.cstrlen_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.

    Start an equivalence check
  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.

    The progress of an equivalence check is available in the eqcheck entry
  4. A successful equivalence check is represented by a green-coloured eqcheck pane, labeled "Found proof and safety".
    Successful equivalence check represented by a green eqcheck entry

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".
    Click on "View Proof" to view a successful equivalence 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.

    Click on the product-graph edges to view the correlated paths in the two programs determined to be equivalent
  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.

    Click on "View Search Tree" to view the search tree of an (ongoing or completed) equivalence check
  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.

    Explore the search tree by clicking on its nodes

Save and load a session

You can save a session (potentially with multiple ongoing equivalence checks) and load it later (potentially on a different machine). To access this feature, right-click on the "Start an Eqcheck" button.
Explore the search tree by clicking on its nodes

Examples of successful equivalence checks with proofs

Each example entry shown below can be accessed by using the "Load Session" option in the equivalence checker with the corresponding session name (provided with each entry). We use the Clang-12 compiler for each compilation (which is validated by our equivalence checker).

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.