摘要
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.
作者
杨萍
王生原
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)
出处
《计算机科学》
CSCD
北大核心
2020年第9期17-23,共7页
Computer Science
基金
国家核高基重大专项(2017ZX01030-301-003)。
