CompCert编译器目标代码生成机制分析  

Analysis of Target Code Generation Mechanism of CompCert Compiler

作　　者：杨萍[1] 王生原[2] YANG Ping;WANG Sheng-yuan(School of Information Science,Beijing Language and Culture University,Beijing 100083,China;Department of Computer Science and Technology,Tsinghua University,Beijing 100084,China)

机构地区：[1]北京语言大学信息科学学院,北京100083 [2]清华大学计算机系,北京100084

出　　处：《计算机科学》2020年第9期17-23,共7页Computer Science

基　　金：国家核高基重大专项(2017ZX01030-301-003)。

摘　　要：CompCert是著名的C语言可信编译器,是经过形式化验证的编译器的杰出代表,近年来被广泛应用于学术界和工业界的许多研发工作中。CompCert编译器的当前版本支持多种目标机结构。文中对CompCert编译器目标代码生成机制进行剖析,主要介绍其设计逻辑、翻译过程、语义保持性以及代码结构,并给出了CompCert编译器重定向设计的要点。文中工作有助于实现CompCert重定向,比如实现面向重要国产处理器的后端。CompCert is a well-known C-language trustworthy compiler,which is one of the outstanding representatives among the formally verified compilers.In recent years,CompCert has been widely used in many research and development work in academia and industry.The current version of the CompCert compiler supports a variety of target architectures.The target code generation mechanism of CompCert compiler is analyzed,by mainly introducing the design logic,the translation,the semantic preseving and the code structure.Finally,as a summary,the key points for retargeting the CompCert compiler are given.The paper is helpful to retarget the Compcert compiler,for example,we can construct a back-end for some important domestic processor.

关 键 词：CompCert 形式化验证的编译器 目标代码生成 编译器重定向 

分 类 号：TP314[自动化与计算机技术—计算机软件与理论]