基于模拟关系的编译优化实现正确性验证方法

• 作者: 何炎祥 刘健博 吴伟 徐超 陈勇
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 编译优化 正确性 模拟关系 定理证明
• 年，卷（期）: 2012,（11）
• 所属期刊栏目: 学术论文
• 页码范围: 2171-2176
• 页数: 6页
• 分类号: TP309.1
• 字数: 5077字
• 语种: 中文
• DOI: 10.3969/j.issn.0372-2112.2012.11.005

摘要

编译器中通常采用各种优化方法来提高目标代码的质量,为了实现较好的效果,一些编译优化算法通常十分复杂,很容易给可靠性和安全性带来隐患.现有的编译器缺陷大部分是由优化阶段引起的.传统的编译优化正确性研究大部分只关注优化算法的正确性,但是只有该算法被正确的实现了才能确保实际运行的优化过程是正确的.本文提出一种基于模拟关系的方法来验证编译优化实现的正确性.在每次优化结束后,我们通过建立优化前代码和优化后代码之间的模拟关系生成优化正确应满足的逻辑条件,然后验证逻辑条件是否成立从而判定编译优化的实现是否正确性.以优化编译中的常量折叠优化和变量替换的验证作为示例显示了本方法的有效性和可靠性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	何炎祥	武汉大学计算机学院	11	71	6.0	8.0
5	徐超	武汉大学计算机学院	27	75	5.0	7.0
11	陈勇	武汉大学计算机学院	58	540	11.0	21.0
13	吴伟	武汉大学计算机学院	30	81	5.0	7.0