Computer Science

Computer Science ›› 2020, Vol. 47 ›› Issue (9): 17-23.doi: 10.11896/jsjkx.200400018

• Computer Software • Previous Articles     Next Articles

Analysis of Target Code Generation Mechanism of CompCert Compiler

YANG Ping1, WANG Sheng-yuan2   

  1. 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).

PDF (PC)

1347

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

CLC Number: 

  • TP314
[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 12th 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 47th 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.
[1] LI Ling, LI Huang-hua, WANG Sheng-yuan. Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design [J]. Computer Science, 2020, 47(6): 8-15.
[2] WANG Lei,SHI Gang,DONG Yuan,BAI Xiao-ying and WANG Sheng-yuan. Trusted Compiler for Safe Subset of C Language [J]. Computer Science, 2013, 40(9): 30-34.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.