计算机科学 ›› 2024, Vol. 51 ›› Issue (11A): 240200115-9.doi: 10.11896/jsjkx.240200115
胡少儒, 王隽伟, 王生原
HU Shaoru, WANG Juanwei, WANG Shengyuan
摘要： CompCert是著名的C语言可信编译器,它借助于交互式定理证明工具Coq实现,能够确保生成的目标汇编代码保持源代码的语义,具有极高的可信度,近年来被广泛应用于学术界和工业界的许多安全攸关任务的研发工作中。CompCert编译器的当前版本支持多种目标机结构,然而目前尚缺乏针对国内自主研发处理器的版本,如龙芯(Loongson)处理器体系结构(LoongArch)。将CompCert重定向到龙芯等国产处理器,对我国安全攸关软件领域的发展大有裨益。本文对 CompCert 编译器的设计理念、框架结构和龙芯架构的特点进行分析,改造 CompCert 编译器的后端,使其可以生成能在龙芯处理器上运行的汇编代码,并细致阐述不同模块的工作内容。重定向到龙芯处理器的 CompCert 编译器具有接近 GCC-O1 的性能,可满足许多场景的使用。
中图分类号:
| [1]YANG X J,CHEN Y,ERIC E,et al.Finding and understanding bugs in C compilers[C]//Proceedings of the 2011 ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI 2011).2011:283-294. [2]ZHANG Q R,SUN C N,SU Z D.Skeletal Program Enume-ration for Rigorous Compiler Testing[C]//Proceedings of the 2017 ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI 2017).2017. [3]MCCARTHY JPAINTER J.Correctness of a compiler for arithmetical expressions[C]//Mathematical Aspects of Computer Science,volume 19 of Proceedings of Symposia in Applied Ma-thematics.1967:33-41. [4]MILNER R,WEYHRAUCH R.Proving compiler correctness in a mechanized logic[C]//Proceedings of 7th Annual Machine Intelligence Workshop,volume 7 of Machine Intelligence.1972:51-72. [5]DAVE M A.Compiler verification:a bibliography[J].ACMSIGSOFT Software Engineering Notes,2003,28(6):2-2. [6]LEROY X.Formal verification of a realistic compiler[C]//Communications of The ACM.2009:107-115. [7]LEROY X.Formal certification of a compiler back-end or:pro-gramming a compiler with a proof assistant[C]//Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.2006:42-54. [8]PNUELI A,SIEGEL M,SINGERMAN E.Translation Valida- tion[C]//Proceedings of TACAS'98,Lecture Notes in Compu-ter Science.1998:151-166. [9]KÄSTNER D,LEROY X,BLAZY S,et al.Closing the gap－the formally verified optimizing compiler CompCert[C]//Developments in System Safety Engineering:Proceedings of the Twenty-fifth Safety-critical Systems Symposium(SSS'17).2017:163-180. [10]LEROY X,BLAZY S.Formal verification of a C-like memory model and its uses for verifying program transformations[J].Journal of Automated Reasoning,2008,41(1):1-31. [11]YANG P,WANG S Y.Analysis of Target Code GenerationMechanism of CompCert Compiler[J].Computer Science,2020,47(9):17-23. [12]LEROY X.A formally verified compiler back-end[J].Journal of Automated Reasoning,2009,43(4):363-446. [13]GEORGE L,APPEL A W.Iterated register coalescing[J].ACM Trans.Prog.Lang.Syst.,1996,18(3):300-324. [14]RIDEAU S,LEROY X.Validating register allocation and spilling[C]//CC 2010.2010:224-243. [15]BLAZY S,ROBILLARD B,APPEL A W.Formal verification of coalescing graph-coloring register allocation[C]//ESOP 2010.2010:145-164. [16]龙芯中科.从必然王国到自由王国,龙芯重磅推出自主指令系统架构 LoongArch [EB/OL].[2021-05-10].https://www.loongson.cn/newsDetails/1913. [17]龙芯中科.重磅发布｜基于龙芯架构的新一代处理器龙芯 3A5000 正式发布[EB/OL].[2021-09-03].https://www.loongson.cn/newsDetails/22. [18]龙芯中科技术股份有限公司.龙芯架构参考手册[M].2021. [19]胡伟武等.计算机体系结构基础[M].机械工业出版社,2021. [20]Loongson Technology Corporation Limited.Loongarch elf abispecification[OL].https://loongson.github.io/LoongArch-Documentation/LoongArch-ELF-ABI-EN.html. [21]LEROY X,BLAZY S,KÄSTNER D,et al.CompCert－A Formally Verified Optimizing Compiler [C]//ERTS 2016.2016.. [22]胡少儒.CompCert 编译器的龙芯处理器重定向[D].Beijing:Tsinghua University,2022. [23]王隽伟.机器证明的CompCert编译器龙芯处理器后端[D].Beijing:Tsinghua University,2023. |
|
||
首页