Computer Science

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)

PDF (PC)

1498

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: CompCert, Coq, Formal verification, LR(1) parser, Lustre* language, Syntax parsing

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].http://compcert.inria.fr/.
[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].http://www.ansys.com/products/embedded-software/ansys-scade-suite.
[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].http://soft.cs.tsinghua.edu.cn/l2c.
[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].http://soft.cs.tsinghua.edu.cn/~wang/projects/L2C/Languages/LustreStar-v6.pdf.
[17]POTTIER F,RÉGIS-GIANAS Y.Menhir Reference Manual [OL].http://gallium.inria.fr/~fpottier/menhir/manual.pdf.
[18]Abstract Syntax of Lustre* for the Open Source L2C Compiler[OL].http://soft.cs.tsinghua.edu.cn/~wang/projects/L2C/Languages/LustreStar-AST.pdf.
[19]POTTIER F,RÉGIS-GIANASY.The Menhir parser generator[OL].http://gallium.inria.fr/fpottier/menhir,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] JIAN Qi-rui, CHEN Ze-mao, WU Xiao-kang. Authentication and Key Agreement Protocol for UAV Communication [J]. Computer Science, 2022, 49(8): 306-313.
[2] WANG Ran-ran, WANG Yong, CAI Yu-tong, JIANG Zheng-tao, DAI Gui-ping. Formal Verification of Yahalom Protocol Based on Process Algebra [J]. Computer Science, 2021, 48(6A): 481-484.
[3] 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.
[4] YANG Ping, WANG Sheng-yuan. Analysis of Target Code Generation Mechanism of CompCert Compiler [J]. Computer Science, 2020, 47(9): 17-23.
[5] FAN Yong-qian, CHEN Gang, CUI Min. Formalization of Finite Field GF(2n) Based on COQ [J]. Computer Science, 2020, 47(12): 311-318.
[6] MA Zhen-wei,CHEN Gang. Matrix Formalization Based on Coq Record [J]. Computer Science, 2019, 46(7): 139-145.
[7] 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.
[8] 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.
[9] 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.
[10] 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.
[11] CHEN Li-rong, LI Yun and LUO Lei. Research on Formal Verification of Embedded Operating System [J]. Computer Science, 2015, 42(8): 203-214.
[12] 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.
[13] 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.
[14] LI Qian and YU Wen-sheng. Safety Verification for VCCR Subsystem of Space Life Support System [J]. Computer Science, 2014, 41(6): 193-198.
[15] 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.
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.