Evaluating Value-Graph Translation Validation for LLVM

Download Now Date Added: Feb 2011
Format: PDF

Translation validators are static analyzers that attempt to verify that program transformations preserve semantics. Normalizing translation validators do so by trying to match the value-graphs of an original function and it's transformed counterpart. In this paper, the authors present the design of such a validator for LLVM's intra-procedural optimizations, a design that does not require any instrumentation of the optimizer, nor any rewriting of the source code to compile, and needs to run only once to validate a pipeline of optimizations. They present the results of their preliminary experiments on a set of benchmarks that include GCC, a perl interpreter, sqlite3, and other C programs.