Evaluating value-graph translation validation for LLVM
Author(s) -
Jean-Baptiste Tristan,
Paul Govereau,
Greg Morrisett
Publication year - 2011
Publication title -
digital access to scholarship at harvard (dash) (harvard university)
Language(s) - English
Resource type - Conference proceedings
ISSN - 0362-1340
DOI - 10.1145/1993498.1993533
Subject(s) - computer science , validator , programming language , compiler , rewriting , perl , call graph , graph , compile time , just in time compilation , source code , optimizing compiler , set (abstract data type) , theoretical computer science , world wide web
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 its transformed counterpart. In this paper, we 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. We present the results of our preliminary experiments on a set of benchmarks that include GCC, a perl interpreter, SQLite3, and other C programs.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom