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

doi:10.11896/jsjkx.200400018

计算机科学 ›› 2020, Vol. 47 ›› Issue (9): 17-23.doi: 10.11896/jsjkx.200400018

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

杨萍¹, 王生原²

1 北京语言大学信息科学学院北京100083
2 清华大学计算机系北京100084

收稿日期:2020-04-07 发布日期:2020-09-10
通讯作者: 王生原(wwssyy@tsinghua.edu.cn)
作者简介:yangp@blcu.edu.cn
基金资助:
国家核高基重大专项(2017ZX01030-301-003)

Analysis of Target Code Generation Mechanism of CompCert Compiler

YANG Ping¹, WANG Sheng-yuan²

1 School of Information Science,Beijing Language and Culture University,Beijing 100083,China
2 Department of Computer Science and Technology,Tsinghua University,Beijing 100084,China

Received:2020-04-07 Published:2020-09-10
About author:YANG Ping,born in 1964,Ms.D,associate professor.Her main research interestes include programming languages and systems,artificial languages,compilers and artificial intelligence.
WANG Sheng-yuan,born in 1964,Ph.D,associate professor.Hismain research interestes include programming languages and systems,compilers and formal methods.
Supported by:
National Science and Technology Major Project of the Ministry of Science and Technology of China (2017ZX01030-301-003).

摘要/Abstract

摘要： CompCert是著名的C语言可信编译器,是经过形式化验证的编译器的杰出代表,近年来被广泛应用于学术界和工业界的许多研发工作中。CompCert编译器的当前版本支持多种目标机结构。文中对CompCert编译器目标代码生成机制进行剖析,主要介绍其设计逻辑、翻译过程、语义保持性以及代码结构,并给出了CompCert编译器重定向设计的要点。文中工作有助于实现CompCert重定向,比如实现面向重要国产处理器的后端。

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

Abstract: 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.

Key words: CompCert, Compiler retargeting, Formally Verified compilers, Target code generation

中图分类号:

TP314

杨萍, 王生原. CompCert编译器目标代码生成机制分析[J]. 计算机科学, 2020, 47(9): 17-23. https://doi.org/10.11896/jsjkx.200400018

YANG Ping, WANG Sheng-yuan. Analysis of Target Code Generation Mechanism of CompCert Compiler[J]. Computer Science, 2020, 47(9): 17-23. https://doi.org/10.11896/jsjkx.200400018

参考文献

[1] KNIGHT J C.Safety critical systems:challenges and directions[C]//Proceedings of the 24th International Conference on Software Engineering(ICSE 2002).2002:547-550.
[2] LEROY X.Formal verification of a realistic compiler[J].Communications of The ACM,2009,52(7):107-115.
[3] KLEIN G,ELPHINSTONE K,HEISTER G,et al.seL4:formal verification of an OS kernel [C]//Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP’09).2009:207-220.
[4] GU R H,SHAO Z,CHEN H,et al.CertiKOS:An Extensible Architecture for Building Certified Concurrent OS Kernels [C]//Proceedings of the 12^th USENIX Symposium on Operating Systems Design and Implementation (OSDI’16).2016:653-669.
[5] CompCert Main Page [EB/OL].http://compcert.inria.fr/.
[6] BLAZY S,LEROY X.Mechanized semantics for the Clight subset of the C language [J].Journal of Automated Reasoning,2009,43(3):263-288.
[7] BLAZY S,LEROY X.Mechanized semantics for the Clight subset of the C language [J].Journal of Automated Reasoning,2009,43(3):263-288.
[8] BERTOT Y,CASTRAN P.Interactive Theorem Proving andProgram Development - Coq’Art:The Calculus of Inductive Constructions [M]//Texts in Theoretical Computer Science.An EATCS Series,Springer Verlag,2004.
[9] MORRISETT G.TechnicalPerspective:A Compiler’s Story[J].Communications of the ACM,2009,52(7):106-106.
[10] YANG X,CHEN Y,EIDE E,REGEHR J.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.
[11] LEROY X.Formal certification of a compiler back-end or:programming a compiler with a proof assistant [J].Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages,2006,41(1):42-54.
[12] TRISTAN J B,LEROY X.A simple,verified validator for software pipelining [C]//POPL.2010:83-92.
[13] BARTHE G,DEMANGE D,PICHARDIE D.A formally verified SSA-based middle-end - Static Single Assignment meets CompCert [C]//Programming Languages and Systems(ESOP 2012).2012:47-66.
[14] JOURDAN J H,LAPORTE V,BLAZY S,et al.A formally-verified c static analyzer [C]//Proceedings of POPL’15.Mumbai,India,ACM Press.2015:247-259.
[15] BOURTE T,BRUN L,et al.A Formally Verified Compiler for Lustre [C]//Proceedings of the Programming Language Design and Implementation.2017:586-601.
[16] SHANG S,GAN Y K,et al.Key Translations of the Trustworthy Compiler L2C and Its Design and Implementation[J].Jour-.nal of Software,2017,28(5):1233-1246.
[17] KANG Y X,GAN Y K,WANG S Y.Key Analysis and Comparison of two Trustworthy Compilers Vélus and L2C for Synchronous Languages [J].Journal of Software,2019,30(7):2003-2017.
[18] BOURTE T,BRUN L,POUZET M.Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset [C]//Proceedings of the 47^th ACM SIGPLAN Symposium on Principles of Programming Languages.New Orleans,LA,USA,2020.
[19] JIANG H,LIANG H,et al.Towards Certified Separate Compilation for Concurrent Programs [C]//Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation.2019:111-125.
[20] JOURDAN J H,POTTIER F,LEROY X.Validating LR(1)parsers [C]//Programming Languages and Systems -- 21st European Symposium on Programming(ESOP 2012).7211 of Lecture Notes in Computer Science.2012:397-416.
[21] LEROY X.A formally verified compiler back-end [J].Journal of Automated Reasoning,2009,43(4):363-446.
[22] PNUELI A,SIEGEL M and SINERMAN E.Translation Validation [C]//Proceedings of TACAS’98.1998:151-166.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

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

Analysis of Target Code Generation Mechanism of CompCert Compiler

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 2

Metrics

本文评价

推荐阅读 0

[1]	李凌, 李璜华, 王生原. 在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程 Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design 计算机科学, 2020, 47(6): 8-15. https://doi.org/10.11896/jsjkx.191000173
[2]	王蕾,石刚,董渊,白晓颖,王生原. 一个C语言安全子集的可信编译器 Trusted Compiler for Safe Subset of C Language 计算机科学, 2013, 40(9): 30-34.