ISSN 1000-1239 CN 11-1777/TP

Journal of Computer Research and Development ›› 2019, Vol. 56 ›› Issue (9): 2001-2011.doi: 10.7544/issn1000-1239.2019.20180513

Previous Articles     Next Articles

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).

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

CLC Number: