Computer Science ›› 2020, Vol. 47 ›› Issue (6): 8-15.doi: 10.11896/jsjkx.191000173

• Intelligent Software Engineering • Previous Articles     Next Articles

Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design

LI Ling, LI Huang-hua, WANG Sheng-yuan   

  1. Department of Computer Science and Technology,Tsinghua University,Beijing 100084,China
  • Received:2019-10-28 Online:2020-06-15 Published:2020-06-10
  • About author:LI Ling,born in 1995,undergraduate student.His main research interests include formal verification and so on.
    WANG Sheng-yuan,born in 1964,Ph.D,associate professor,is a senior member of China Computer Federation.His research interests include programming languages and systems,and formal verification
  • Supported by:
    This work was supported by the National Science and Technology Major Project (2017ZX01030-301-003)

Abstract: Jourdan and others presented a method to formally verify a parser in their paper Validating LR(1) Parsers published in 2012,and successfully applied it to the parser verification of CompCert compiler(version 2.3 and above).With this method,formal validation of the Lustre* parser is completed,which is a part of the Open L2C project,and one of the two options of the front-end parser of the Open L2C compiler is implemented.Firstly,this paper discussesthe implementation of the parser,inclu- ding some valuable technical details.Thenit analyzes the running performance and correctness of the parser.And finally,how to apply this method tomore general parsersis summarized.

Key words: Syntax parsing, LR(1) parser, Formal verification, Lustre* language, CompCert, Coq

CLC Number: 

  • TP314
[1]KNIGHT J C.Safety critical systems:challenges and directions[C]//Proceedings of the 24th International Conference on Software Engineering.2002:547-550.
[2]LEROYX.Formal verification of a realistic compiler[J].Communications of the ACM,2009,52(7):107-115.
[3]BERTOT Y,CASTÉRAN P.Interactive theorem proving and program development:Coq’Art:the calculus of inductive constructions[M].Springer Science & Business Media,2013.
[4]MORRISETT G.Technical Perspective A Compiler’s Story[J].Communications of the ACM,2009,52(7):106-106.
[5]JOURDAN J H,POTTIER F,LEROY X.Validating LR (1) parsers[C]//European Symposium on Programming.Berlin:Springer,2012:397-416.
[6]BARTHWAL A,NORRISH M.Verified,executable parsing [C]//European Symposium on Programming.Berlin:Springer,2009:160-174.
[7]MCPEAK S,NECULAG C.Elkhound:A fast,practical GLR parser generator[C]//International Conference on Compiler Construction.Berlin:Springer,2004:73-88.
[8]CompCert home[OL].
[9]JOURDAN J H,POTTIER F.A simple,possibly correct LR parser for C11[J].ACM Transactions on Programming Languages and Systems (TOPLAS),2017,39(4):1-36.
[10]SHI G,WANG SY,DONG Y,et al.Construction for the trustworthy compiler of a synchronous data-flow language[J].Ruan Jian Xue Bao,2014,25(2):341-356.
[11]LIU Y,GAN Y K,WANG S Y,et al.Trustworthy translation for eliminating high-order operation of a synchronous dataflow language[J].Ruan Jian Xue Bao,2015,26(2):332-347.
[12]Scade home[OL].
[13]SHANG S,GAN Y K,SHI G,et al.Key translations of the trustworthy compiler L2C and its design and implementation[J].Ruan Jian Xue Bao,2017,28(5):1233-1246.
[14]Open L2C home[OL].
[15]KANG Y X,GAN Y K,WANG S Y.Comparison of two trustworthy compilers Vélus and L2C for synchronous languages[J].Ruan Jian Xue Bao,2019,30(7):2003-2018.
[16]Syntax of Lustre* for the Open Source L2C Compiler[OL].
[17]POTTIER F,RÉGIS-GIANAS Y.Menhir Reference Manual [OL].
[18]Abstract Syntax of Lustre* for the Open Source L2C Compiler[OL].
[19]POTTIER F,RÉGIS-GIANASY.The Menhir parser generator[OL].,2016.
[20]POTTIER F.Reachability and error diagnosis in LR (1) parsers[C]//Proceedings of the 25th International Conference on Compiler Construction.2016:88-98.
[21]RIDGE T.Simple,functional,sound and complete parsing for all context-free grammars[C]//International Conference on Certified Programs and Proofs.Berlin:Springer,2011:103-118.
[1] SUN Xiao-xiang, CHEN Zhe. Study on Correctness of Memory Security Dynamic Detection Algorithm Based on Theorem Proving [J]. Computer Science, 2021, 48(1): 268-272.
[2] YANG Ping, WANG Sheng-yuan. Analysis of Target Code Generation Mechanism of CompCert Compiler [J]. Computer Science, 2020, 47(9): 17-23.
[3] FAN Yong-qian, CHEN Gang, CUI Min. Formalization of Finite Field GF(2n) Based on COQ [J]. Computer Science, 2020, 47(12): 311-318.
[4] MA Zhen-wei,CHEN Gang. Matrix Formalization Based on Coq Record [J]. Computer Science, 2019, 46(7): 139-145.
[5] CHEN Hao, LUO Lei, LI Yun, CHEN Li-rong. Study on Formal Verification of Secure Virtual Machine Monitor [J]. Computer Science, 2019, 46(3): 170-179.
[6] XUE Zhu-jun, YANG Shu-qiang and SHU Yang-xue. Microblog Text Summarization Based on Entity Relation Network [J]. Computer Science, 2016, 43(9): 77-81.
[7] LI Yan-chun, LI Xiao-juan, GUAN Yong, WANG Rui, ZHANG Jie and WEI Hong-xing. xMAS-based Formal Verification of SpaceWire Credit Logic [J]. Computer Science, 2016, 43(2): 113-117.
[8] YANG Xiu-mei, GUAN Yong, SHI Zhi-ping, WU Ai-xuan, ZHANG Qian-ying and ZHANG Jie. Higher-order Logic Formalization of Function Matrix and its Calculus [J]. Computer Science, 2016, 43(11): 24-29.
[9] CHEN Li-rong, LI Yun and LUO Lei. Research on Formal Verification of Embedded Operating System [J]. Computer Science, 2015, 42(8): 203-214.
[10] LIU Yang,YANG Fei,SHI Gang,YAN Xin,WANG Sheng-yuan and DONG Yuan. Brief Overview of Translation Validation Method in Trusted Compiler Construction [J]. Computer Science, 2014, 41(Z6): 334-338.
[11] ZHOU Kuan-jiu,REN Long-tao,WANG Xiao-long,YONG Jia-wei and HOU Gang. Modeling and Formal Verification for Software Designs Based on Hierarchical Timed State Transition Matrix [J]. Computer Science, 2014, 41(8): 42-46.
[12] LI Qian and YU Wen-sheng. Safety Verification for VCCR Subsystem of Space Life Support System [J]. Computer Science, 2014, 41(6): 193-198.
[13] LI Min,LUO Hui-qiong,TANG Chun-ling and WANG Qiang. Research on Formal Verification of Web Interaction Model [J]. Computer Science, 2014, 41(2): 219-221.
[14] HOU Gang,ZHOU Kuan-jiu,YONG Jia-wei,REN Long-tao and WANG Xiao-long. Survey of State Explosion Problem in Model Checking [J]. Computer Science, 2013, 40(Z6): 77-86.
[15] LI Li,ZHAO Wen-juan and FAN Xiao-zhong. Chinese Chunk Dependency Relationship Parsing Based on Words Dependency [J]. Computer Science, 2013, 40(Z11): 259-262.
Full text



[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75 .
[2] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[3] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[4] 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 .
[5] 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 .
[6] LIU Bo-yi, TANG Xiang-yan and CHENG Jie-ren. Recognition Method for Corn Borer Based on Templates Matching in Muliple Growth Periods[J]. Computer Science, 2018, 45(4): 106 -111 .
[7] GENG Hai-jun, SHI Xin-gang, WANG Zhi-liang, YIN Xia and YIN Shao-ping. Energy-efficient Intra-domain Routing Algorithm Based on Directed Acyclic Graph[J]. Computer Science, 2018, 45(4): 112 -116 .
[8] WANG Zhen-chao, HOU Huan-huan and LIAN Rui. Path Optimization Scheme for Restraining Degree of Disorder in CMT[J]. Computer Science, 2018, 45(4): 122 -125 .
[9] YANG Yu-qi, ZHANG Guo-an and JIN Xi-long. Dual-cluster-head Routing Protocol Based on Vehicle Density in VANETs[J]. Computer Science, 2018, 45(4): 126 -130 .
[10] HAN Kui-kui, XIE Zai-peng and LV Xin. Fog Computing Task Scheduling Strategy Based on Improved Genetic Algorithm[J]. Computer Science, 2018, 45(4): 137 -142 .