面向龙芯处理器的一种CompCert可信编译器重定向实现  

Implementation of Retargeting CompCert Trusted Compiler for Loongson Processors

作　　者：胡少儒 王隽伟 王生原[1] HU Shaoru;WANG Juanwei;WANG Shengyuan(Department of Computer Science and Technology,Tsinghua University,Beijing 100084,China)

机构地区：[1]清华大学计算机系,北京100084

出　　处：《计算机科学》2024年第S02期747-755,共9页Computer Science

基　　金：国家重点研发计划(2022YFB3305204)。

摘　　要：CompCert是著名的C语言可信编译器,它借助于交互式定理证明工具Coq实现,能够确保生成的目标汇编代码保持源代码的语义,具有极高的可信度,近年来被广泛应用于学术界和工业界的许多安全攸关任务的研发工作中。CompCert编译器的当前版本支持多种目标机结构,然而目前尚缺乏针对国内自主研发处理器的版本,如龙芯(Loongson)处理器体系结构(LoongArch)。将CompCert重定向到龙芯等国产处理器,对我国安全攸关软件领域的发展大有裨益。本文对CompCert编译器的设计理念、框架结构和龙芯架构的特点进行分析,改造CompCert编译器的后端,使其可以生成能在龙芯处理器上运行的汇编代码,并细致阐述不同模块的工作内容。重定向到龙芯处理器的CompCert编译器具有接近GCC-O1的性能,可满足许多场景的使用。CompCert is a well-known trustworthy C-language compiler,which is highly credible and has been widely used in many research and development work in academia and industry in recent years.CompCert proves the property that the target assembly code it produces can keep the semantics of the source code,with Coq,an interactive proof assistant.The CompCert compiler now supports multiple target machine architectures,but there is currently a lack of versions specifically designed for domestically developed processors,such as the Loongson processor architecture(LoongArch).Retargetting CompCert to domestic processors such as Loongson is of great benefit to the development of safety-critical software in China.This paper analyzes the design and the structure of the CompCert compiler backend and the characteristics of Loongarch,revises the backend of the CompCert compiler to make it available to generate the assembly code suitable to run on the Loongson processor,and presents the work of the different modules.The revised CompCert compiler,which retargets to Loongson processors,has performance competitive with GCC at optimization level 1,and can meet the needs of various scenarios.

关 键 词：CompCert 编译器 编译器重定向 龙芯架构 形式化验证的编译器 COQ 

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