Verifying Implementation Correctness of Compiling Optimization Based on Simulation Relation

XU Chao; HE Yan-xiang; WU Wei; CHEN Yong; LIU Jian-bo

doi:10.3969/j.issn.0372-2112.2012.11.005

您当前的位置：

首页 >

文章列表页 >

Verifying Implementation Correctness of Compiling Optimization Based on Simulation Relation

更新时间：2025-07-16

- Verifying Implementation Correctness of Compiling Optimization Based on Simulation Relation
- Acta Electronica Sinica Vol. 40, Issue 11, Pages: 2171-2176(2012)
- 作者机构：
  
  1. 武汉大学计算机学院,湖北,武汉,430072
  2. 徐州工业职业技术学院,江苏,徐州,221000
  3. 软件工程国家重点实验室,湖北,武汉,430072
  4. 武汉大学计算机学院湖北武汉,430072
  5. 徐州工业职业技术学院江苏徐州,221000
  6. 软件工程国家重点实验室湖北武汉,430072
- 作者简介：
- 基金信息：
  
  Key Program supported by National Natural Science Foundation of China (No.91118003);National Natural Science Foundation of China (No.61170022)
- DOI：10.3969/j.issn.0372-2112.2012.11.005
  CLC： TP309.1
- Published：2012
- 稿件说明：
移动端阅览
XU Chao, HE Yan-xiang, WU Wei, et al. Verifying Implementation Correctness of Compiling Optimization Based on Simulation Relation[J]. Acta Electronica Sinica, 2012, 40(11): 2171-2176.
DOI：

XU Chao, HE Yan-xiang, WU Wei, et al. Verifying Implementation Correctness of Compiling Optimization Based on Simulation Relation[J]. Acta Electronica Sinica, 2012, 40(11): 2171-2176. DOI： 10.3969/j.issn.0372-2112.2012.11.005.

摘要

编译器中通常采用各种优化方法来提高目标代码的质量

为了实现较好的效果

一些编译优化算法通常十分复杂

很容易给可靠性和安全性带来隐患.现有的编译器缺陷大部分是由优化阶段引起的.传统的编译优化正确性研究大部分只关注优化算法的正确性

但是只有该算法被正确的实现了才能确保实际运行的优化过程是正确的.本文提出一种基于模拟关系的方法来验证编译优化实现的正确性.在每次优化结束后

我们通过建立优化前代码和优化后代码之间的模拟关系生成优化正确应满足的逻辑条件

然后验证逻辑条件是否成立从而判定编译优化的实现是否正确性.以优化编译中的常量折叠优化和变量替换的验证作为示例显示了本方法的有效性和可靠性.

Abstract

Many optimization methods are used to raise the quality of target code in the process of compiling.Because some optimization methods for compiling are too complicated

hidden dangers won't be avoided for reliability and security of compiling.The existing defects of compiler are usually caused at the optimization phase.Mostly traditional correctness of compiling optimization only focus on correctness of optimization algorithm

but only when the algorithm is implemented correctly

the optimization process run in practice can be proved to be correct.This paper proposes a method based on simulation relation to verify correctness of compiling optimization realization.We build up simulation relation between code before optimization and code after optimization to generate logic condition that the correctness optimization should satisfy

and then we verify it if logic condition is satisfied or not to judge if compiling optimization realization is correct or not after each optimization is finished.The method is proved to be effective and reliable by verifying statement exchange and variable substitution in the process of optimization compiling.

关键词

Keywords

references

Views

1576

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

A Private Process Modeling Approach Guaranteeing Correctness

Formal Verification of _mJava Compiler Targeting Micro-Dalvik Virtual Machine

Research on Method of Formal Design and Verification of Memory Management Based on Microkernel Architecture

Related Author

MO Qi

DA Jian

DAI Fei

ZHU Rui

LIN Lei-lei

LI Tong

JIANG Nan

HE Yan-xiang

Related Institution

School of Big Data and Intelligent Engineering Southwest Forestry University. Kunming Yunnan China

Department of Information Engineering Huai'an Open University. Huai'an Jiangsu China

Key Laboratory of Software Engineering in Yunnan Province Yunnan University. Kunming Yunnan China

School of Software Yunnan University. Kunming Yunnan China

School of Big Data and Intelligent Engineering, Southwest Forestry University.

⁰