计算机科学 ›› 2020, Vol. 47 ›› Issue (6): 8-15.doi: 10.11896/jsjkx.191000173

• 智能软件工程 • 上一篇    下一篇

在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程

李凌, 李璜华, 王生原   

  1. 清华大学计算机科学与技术系 北京100084
  • 收稿日期:2019-10-28 出版日期:2020-06-15 发布日期:2020-06-10
  • 通讯作者: 王生原(wwssyy@tsinghua.edu.cn)
  • 作者简介:liling14@tsinghua.org.cn
  • 基金资助:
    核高基重大专项(2017ZX01030-301-003)

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)

摘要: Jourdan等在其2012年发表的论文“Validating LR(1) Parsers”中提出了一种形式化验证语法分析器的方法,并将其成功地应用于CompCert编译器(2.3以上版本)的语法分析器验证中。借助这种方法,文中完成了L2C 项目中的Lustre*语言语法分析器的形式化验证,实现了开源L2C编译器前端语法分析器的两个选项之一。首先对这一语法分析器的实现进行了论述,其中包括有参考价值的技术细节;随后分析了该语法分析器的运行性能及正确性;最后对如何将这一方法推广至更一般的应用场景进行了总结。

关键词: 语法分析, LR(1)分析器, 形式化验证, Lustre*语言, CompCert, Coq

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

中图分类号: 

  • 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] 孙小祥, 陈哲. 基于定理证明的内存安全性动态检测算法的正确性研究[J]. 计算机科学, 2021, 48(1): 268-272.
[2] 杨萍, 王生原. CompCert编译器目标代码生成机制分析[J]. 计算机科学, 2020, 47(9): 17-23.
[3] 范永乾, 陈钢, 崔敏. 基于COQ的有限域GF(2n)的形式化研究[J]. 计算机科学, 2020, 47(12): 311-318.
[4] 马振威,陈钢. 基于Coq记录的矩阵形式化方法[J]. 计算机科学, 2019, 46(7): 139-145.
[5] 陈昊,罗蕾,李允,陈丽蓉. 安全虚拟机监视器的形式化验证研究[J]. 计算机科学, 2019, 46(3): 170-179.
[6] 薛竹君,杨树强,束阳雪. 基于实体关系网络的微博文本摘要[J]. 计算机科学, 2016, 43(9): 77-81.
[7] 李艳春,李晓娟,关永,王瑞,张杰,魏洪兴. 基于xMAS模型的SpaceWire信誉逻辑的形式化验证[J]. 计算机科学, 2016, 43(2): 113-117.
[8] 杨秀梅,关永,施智平,吴爱轩,张倩颖,张杰. 函数矩阵及其微积分的高阶逻辑形式化[J]. 计算机科学, 2016, 43(11): 24-29.
[9] 陈丽蓉,李允,罗蕾. 嵌入式操作系统的形式化验证研究[J]. 计算机科学, 2015, 42(8): 203-214.
[10] 刘洋,杨斐,石刚,闫鑫,王生原,董渊. 可信编译器构造的翻译确认方法简述[J]. 计算机科学, 2014, 41(Z6): 334-338.
[11] 周宽久,任龙涛,王小龙,勇嘉伟,侯刚. 基于层次化时间STM软件设计的形式化验证[J]. 计算机科学, 2014, 41(8): 42-46.
[12] 李倩,郁文生. 空间生命支持系统中VCCR子系统的安全性验证[J]. 计算机科学, 2014, 41(6): 193-198.
[13] 李敏,罗惠琼,唐春玲,王强. Web交互模型的形式化验证研究[J]. 计算机科学, 2014, 41(2): 219-221.
[14] 侯刚,周宽久,勇嘉伟,任龙涛,王小龙. 模型检测中状态爆炸问题研究综述[J]. 计算机科学, 2013, 40(Z6): 77-86.
[15] 王蕾,石刚,董渊,白晓颖,王生原. 一个C语言安全子集的可信编译器[J]. 计算机科学, 2013, 40(9): 30-34.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] 雷丽晖,王静. 可能性测度下的LTL模型检测并行化研究[J]. 计算机科学, 2018, 45(4): 71 -75 .
[2] 张佳男,肖鸣宇. 带权混合支配问题的近似算法研究[J]. 计算机科学, 2018, 45(4): 83 -88 .
[3] 伍建辉,黄中祥,李武,吴健辉,彭鑫,张生. 城市道路建设时序决策的鲁棒优化[J]. 计算机科学, 2018, 45(4): 89 -93 .
[4] 史雯隽,武继刚,罗裕春. 针对移动云计算任务迁移的快速高效调度算法[J]. 计算机科学, 2018, 45(4): 94 -99 .
[5] 周燕萍,业巧林. 基于L1-范数距离的最小二乘对支持向量机[J]. 计算机科学, 2018, 45(4): 100 -105 .
[6] 刘博艺,唐湘滟,程杰仁. 基于多生长时期模板匹配的玉米螟识别方法[J]. 计算机科学, 2018, 45(4): 106 -111 .
[7] 耿海军,施新刚,王之梁,尹霞,尹少平. 基于有向无环图的互联网域内节能路由算法[J]. 计算机科学, 2018, 45(4): 112 -116 .
[8] 王振朝,侯欢欢,连蕊. 抑制CMT中乱序程度的路径优化方案[J]. 计算机科学, 2018, 45(4): 122 -125 .
[9] 杨羽琦,章国安,金喜龙. 车载自组织网络中基于车辆密度的双簇头路由协议[J]. 计算机科学, 2018, 45(4): 126 -130 .
[10] 韩奎奎,谢在鹏,吕鑫. 一种基于改进遗传算法的雾计算任务调度策略[J]. 计算机科学, 2018, 45(4): 137 -142 .