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

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, Formally Verified compilers, Target code generation, Compiler retargeting

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   
[1] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[2] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99 .
[3] ZHOU Yan-ping and YE Qiao-lin. L1-norm Distance Based Least Squares Twin Support Vector Machine[J]. Computer Science, 2018, 45(4): 100 -105 .
[4] SHI Chao, XIE Zai-peng, LIU Han and LV Xin. Optimization of Container Deployment Strategy Based on Stable Matching[J]. Computer Science, 2018, 45(4): 131 -136 .
[5] PANG Bo, JIN Qian-kun, HENIGULI·Wu Mai Er and QI Xing-bin. Routing Scheme Based on Network Slicing and ILP Model in SDN[J]. Computer Science, 2018, 45(4): 143 -147 .
[6] ZHENG Xiu-lin, SONG Hai-yan and FU Yi-peng. Distinguishing Attack of MORUS-1280-128[J]. Computer Science, 2018, 45(4): 152 -156 .
[7] WU Shu, ZHOU An-min and ZUO Zheng. PDiOS:Private API Call Detection in iOS Applications[J]. Computer Science, 2018, 45(4): 163 -168 .
[8] LIU Qin. Study on Data Quality Based on Constraint in Computer Forensics[J]. Computer Science, 2018, 45(4): 169 -172 .
[9] ZHU Shu-qin, WANG Wen-hong and LI Jun-qing. Chosen Plaintext Attack on Chaotic Image Encryption Algorithm Based on Perceptron Model[J]. Computer Science, 2018, 45(4): 178 -181 .
[10] GUO Jun-xia, GUO Ren-fei, XU Nan-shan and ZHAO Rui-lian. Study on Construction of EFSM Model for Web Application Based on Session[J]. Computer Science, 2018, 45(4): 203 -207 .