Evaluating value-graph translation validation for LLVM

PLDI(2011)

引用 145|浏览113
暂无评分
摘要
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.
更多
查看译文
关键词
intra-procedural optimizations,perl interpreter,original function,value-graph translation validation,normalizing translation validators,source code,program transformation,preliminary experiment,c program,static analyzer,translation validators,optimization,languages,theory,algorithms,verification,reliability
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要