计算机科学 ›› 2020, Vol. 47 ›› Issue (6): 8-15.doi: 10.11896/jsjkx.191000173
李凌, 李璜华, 王生原
LI Ling, LI Huang-hua, WANG Sheng-yuan
摘要： Jourdan等在其2012年发表的论文“Validating LR(1) Parsers”中提出了一种形式化验证语法分析器的方法,并将其成功地应用于CompCert编译器(2.3以上版本)的语法分析器验证中。借助这种方法,文中完成了L2C 项目中的Lustre*语言语法分析器的形式化验证,实现了开源L2C编译器前端语法分析器的两个选项之一。首先对这一语法分析器的实现进行了论述,其中包括有参考价值的技术细节;随后分析了该语法分析器的运行性能及正确性;最后对如何将这一方法推广至更一般的应用场景进行了总结。
中图分类号:
| [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] | 蹇奇芮, 陈泽茂, 武晓康. 面向无人机通信的认证和密钥协商协议 Authentication and Key Agreement Protocol for UAV Communication 计算机科学, 2022, 49(8): 306-313. https://doi.org/10.11896/jsjkx.220200098 |
| [2] | 冉丹, 陈哲, 孙毅, 杨志斌. 基于程序转化的SCADE模型检测 SCADE Model Checking Based on Program Transformation 计算机科学, 2021, 48(12): 125-130. https://doi.org/10.11896/jsjkx.201100080 |
| [3] | 孙小祥, 陈哲. 基于定理证明的内存安全性动态检测算法的正确性研究 Study on Correctness of Memory Security Dynamic Detection Algorithm Based on Theorem Proving 计算机科学, 2021, 48(1): 268-272. https://doi.org/10.11896/jsjkx.200100097 |
| [4] | 杨萍, 王生原. CompCert编译器目标代码生成机制分析 Analysis of Target Code Generation Mechanism of CompCert Compiler 计算机科学, 2020, 47(9): 17-23. https://doi.org/10.11896/jsjkx.200400018 |
| [5] | 范永乾, 陈钢, 崔敏. 基于COQ的有限域GF(2n)的形式化研究 Formalization of Finite Field GF(2n) Based on COQ 计算机科学, 2020, 47(12): 311-318. https://doi.org/10.11896/jsjkx.190900197 |
| [6] | 马振威,陈钢. 基于Coq记录的矩阵形式化方法 Matrix Formalization Based on Coq Record 计算机科学, 2019, 46(7): 139-145. https://doi.org/10.11896/j.issn.1002-137X.2019.07.022 |
| [7] | 陈昊,罗蕾,李允,陈丽蓉. 安全虚拟机监视器的形式化验证研究 Study on Formal Verification of Secure Virtual Machine Monitor 计算机科学, 2019, 46(3): 170-179. https://doi.org/10.11896/j.issn.1002-137X.2019.03.026 |
| [8] | 薛竹君,杨树强,束阳雪. 基于实体关系网络的微博文本摘要 Microblog Text Summarization Based on Entity Relation Network 计算机科学, 2016, 43(9): 77-81. https://doi.org/10.11896/j.issn.1002-137X.2016.09.014 |
| [9] | 李艳春,李晓娟,关永,王瑞,张杰,魏洪兴. 基于xMAS模型的SpaceWire信誉逻辑的形式化验证 xMAS-based Formal Verification of SpaceWire Credit Logic 计算机科学, 2016, 43(2): 113-117. https://doi.org/10.11896/j.issn.1002-137X.2016.02.026 |
| [10] | 杨秀梅,关永,施智平,吴爱轩,张倩颖,张杰. 函数矩阵及其微积分的高阶逻辑形式化 Higher-order Logic Formalization of Function Matrix and its Calculus 计算机科学, 2016, 43(11): 24-29. https://doi.org/10.11896/j.issn.1002-137X.2016.11.005 |
| [11] | 陈丽蓉,李允,罗蕾. 嵌入式操作系统的形式化验证研究 Research on Formal Verification of Embedded Operating System 计算机科学, 2015, 42(8): 203-214. |
| [12] | 刘洋,杨斐,石刚,闫鑫,王生原,董渊. 可信编译器构造的翻译确认方法简述 Brief Overview of Translation Validation Method in Trusted Compiler Construction 计算机科学, 2014, 41(Z6): 334-338. |
| [13] | 周宽久,任龙涛,王小龙,勇嘉伟,侯刚. 基于层次化时间STM软件设计的形式化验证 Modeling and Formal Verification for Software Designs Based on Hierarchical Timed State Transition Matrix 计算机科学, 2014, 41(8): 42-46. https://doi.org/10.11896/j.issn.1002-137X.2014.08.008 |
| [14] | 李倩,郁文生. 空间生命支持系统中VCCR子系统的安全性验证 Safety Verification for VCCR Subsystem of Space Life Support System 计算机科学, 2014, 41(6): 193-198. https://doi.org/10.11896/j.issn.1002-137X.2014.06.038 |
| [15] | 李敏,罗惠琼,唐春玲,王强. Web交互模型的形式化验证研究 Research on Formal Verification of Web Interaction Model 计算机科学, 2014, 41(2): 219-221. |
|
||
首页