关键词:
CompCert
编译器
编译器重定向
龙芯架构
形式化验证的编译器
Coq
摘要:
CompCert是著名的C语言可信编译器,它借助于交互式定理证明工具Coq实现,能够确保生成的目标汇编代码保持源代码的语义,具有极高的可信度,近年来被广泛应用于学术界和工业界的许多安全攸关任务的研发工作中。CompCert编译器的当前版本支持多种目标机结构,然而目前尚缺乏针对国内自主研发处理器的版本,如龙芯(Loongson)处理器体系结构(LoongArch)。将CompCert重定向到龙芯等国产处理器,对我国安全攸关软件领域的发展大有裨益。本文对CompCert编译器的设计理念、框架结构和龙芯架构的特点进行分析,改造CompCert编译器的后端,使其可以生成能在龙芯处理器上运行的汇编代码,并细致阐述不同模块的工作内容。重定向到龙芯处理器的CompCert编译器具有接近GCC-O1的性能,可满足许多场景的使用。