ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2019, Vol. 56 ›› Issue (9): 2001-2011.doi: 10.7544/issn1000-1239.2019.20180513

• 系统结构 • 上一篇    下一篇

二进制翻译正确性及优化方法的形式化模型

傅立国,庞建民,王军,张家豪,岳峰   

  1. (数学工程与先进计算国家重点实验室(战略支援部队信息工程大学) 郑州 450002) (flg_njlg@163.com)
  • 出版日期: 2019-09-10
  • 基金资助: 
    国家自然科学基金项目(61472447)

Formal Model of Correctness and Optimization on Binary Translation

Fu Liguo, Pang Jianmin, Wang Jun, Zhang Jiahao, Yue Feng   

  1. (State Key Laboratory of Mathematical Engineering and Advanced Computing (Strategic Support Force Information Engineering University), Zhengzhou 450002)
  • Online: 2019-09-10
  • Supported by: 
    This work was supported by the National Natural Science Foundation of China (61472447).

摘要: 二进制翻译在体系结构设计、程序性能优化、安全性分析以及软件移植等领域的研究中备受关注.不同应用场景对二进制翻译的需求各不相同,却总聚焦于翻译的正确性和翻译的效率2个方面.翻译的正确性用于评判翻译前后程序在逻辑功能上是否具有等价性,而等价的证明依赖于适当的形式化模型.为了满足研究二进制翻译正确性以及翻译优化方法对理论模型的需求,对已有理论模型进行了深入的剖析,并进一步构建了新的基于后继关系的映射模型.该模型既能够形式化地描述正确翻译的二进制翻译过程所具备的性质和构造方法,也可以在翻译过程形式化描述的基础上对翻译过程优化方法的特征和性质进行描述.通过构建翻译正确性及翻译过程优化方法的形式化模型,为二进制翻译技术中关于翻译过程的实现以及优化方法的策略组合等进一步研究提供了更强的理论支撑.

关键词: 二进制翻译, 翻译正确性, 效率, 翻译优化, 形式化模型

Abstract: Binary translation has attracted more and more attention in the fields of architecture optimization, program performance optimization, security analysis, software transplantation and so on. Although there are totally different requirements on the application of binary translation techniques in these various fields, the researchers are always focusing their attention on two aspects: the correctness of translation and the efficiency of translation. The correctness of translation refers to the equivalent logical functions between the program before and after the translation, so an appropriate formal model for the translation needs to be built at first. According to the current research needs on correctness and optimization of binary translation technique, twice mapping model based on subsequent relations could have been constructed firstly; then the properties and construction methods of a correct process on translation should have been described formally; based on the formal description, the optimization methods of translation would be classified and analyzed on their diverse characteristics and various properties finally. This paper provides a more powerful theoretical support for the further research on the strategy pattern combination of translation methods and optimization methods in the binary translation technology by constructing a formal model of binary translation based on correctness and optimization.

Key words: binary translation, translation correctness, efficiency, translation optimization, formal model

中图分类号: