The Straight-Line Automatic Programming Problem

Joshi, Rajeev ; Nelson, Greg ; Zhou, Yunhong

HP Development Company

关键词: super-optimization;    code generation;    straight-line automatic programming problem;   

RP-ID  :  HPL-2003-236

学科分类：计算机科学（综合）

美国|英语

来源: HP Labs

【 摘 要 】

The paper presents a design for the Denali-2 super- optimizer, which will generate minimum-instruction- length machine code for realistic machine architectures using automatic theorem-proving technology: specifically, using E-graph matching (a technique for pattern matching in the presence of equality information) and boolean satisfiability solving. The paper presents a precise definition of the underlying automatic programming problem solved by the Denali-2 super-optimizer. It sketches the E-graph matching phase and presents a detailed exposition and proof of correctness of the reduction of the automatic programming problem to the boolean satisfiability problem.