Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Automatic Rootcausing for Program Equivalence Failures in Binaries

Shuvendu Lahiri, Rohit Sinha, and Chris Hawblitzel


Equivalence checking of imperative programs has several applications including compiler validation and cross-version verification.
Debugging equivalence failures can be tedious for large examples, especially for binary programs.
In this paper, we propose a simple yet precise notion of rootcause for equivalence failures that leverages semantic similarity between two programs.
Unlike existing works on program repair, our definition of rootcause avoids the need for a template of fixes or the need for a complete repair to ensure equivalence.
We show progressively weaker checks for detecting rootcauses that can be applicable even when multiple fixes are required to make the two programs equivalent.
We provide optimizations based on Maximum Satisfiability (MAXSAT) and binary search to prune the search space of such rootcauses.
We have implemented the techniques and provide an evaluation on a set of real-world compiler validation binary benchmarks.


Publication typeTechReport
> Publications > Automatic Rootcausing for Program Equivalence Failures in Binaries