期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到4篇文章
< 1 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
面向龙芯处理器的一种CompCert可信编译器重定向实现
1
作者 胡少儒 王隽伟 王生原 《计算机科学》 CSCD 北大核心 2024年第S02期747-755,共9页
CompCert是著名的C语言可信编译器,它借助于交互式定理证明工具Coq实现,能够确保生成的目标汇编代码保持源代码的语义,具有极高的可信度,近年来被广泛应用于学术界和工业界的许多安全攸关任务的研发工作中。CompCert编译器的当前版本支... CompCert是著名的C语言可信编译器,它借助于交互式定理证明工具Coq实现,能够确保生成的目标汇编代码保持源代码的语义,具有极高的可信度,近年来被广泛应用于学术界和工业界的许多安全攸关任务的研发工作中。CompCert编译器的当前版本支持多种目标机结构,然而目前尚缺乏针对国内自主研发处理器的版本,如龙芯(Loongson)处理器体系结构(LoongArch)。将CompCert重定向到龙芯等国产处理器,对我国安全攸关软件领域的发展大有裨益。本文对CompCert编译器的设计理念、框架结构和龙芯架构的特点进行分析,改造CompCert编译器的后端,使其可以生成能在龙芯处理器上运行的汇编代码,并细致阐述不同模块的工作内容。重定向到龙芯处理器的CompCert编译器具有接近GCC-O1的性能,可满足许多场景的使用。 展开更多
关键词 compcert 编译器 编译器重定向 龙芯架构 形式化验证的编译器 COQ
在线阅读 下载PDF
在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程 被引量：2
2
作者 李凌 李璜华 王生原 《计算机科学》 CSCD 北大核心 2020年第6期8-15,共8页
Jourdan等在其2012年发表的论文“Validating LR(1)Parsers”中提出了一种形式化验证语法分析器的方法,并将其成功地应用于CompCert编译器(2.3以上版本)的语法分析器验证中。借助这种方法,文中完成了L2C项目中的Lustre*语言语法分析器... Jourdan等在其2012年发表的论文“Validating LR(1)Parsers”中提出了一种形式化验证语法分析器的方法,并将其成功地应用于CompCert编译器(2.3以上版本)的语法分析器验证中。借助这种方法,文中完成了L2C项目中的Lustre*语言语法分析器的形式化验证,实现了开源L2C编译器前端语法分析器的两个选项之一。首先对这一语法分析器的实现进行了论述,其中包括有参考价值的技术细节;随后分析了该语法分析器的运行性能及正确性;最后对如何将这一方法推广至更一般的应用场景进行了总结。 展开更多
关键词 语法分析 LR(1)分析器 形式化验证 Lustre*语言 compcert COQ
在线阅读 下载PDF
CompCert编译器目标代码生成机制分析 被引量：2
3
作者 杨萍 王生原 《计算机科学》 CSCD 北大核心 2020年第9期17-23,共7页
CompCert是著名的C语言可信编译器,是经过形式化验证的编译器的杰出代表,近年来被广泛应用于学术界和工业界的许多研发工作中。CompCert编译器的当前版本支持多种目标机结构。文中对CompCert编译器目标代码生成机制进行剖析,主要介绍其... CompCert是著名的C语言可信编译器,是经过形式化验证的编译器的杰出代表,近年来被广泛应用于学术界和工业界的许多研发工作中。CompCert编译器的当前版本支持多种目标机结构。文中对CompCert编译器目标代码生成机制进行剖析,主要介绍其设计逻辑、翻译过程、语义保持性以及代码结构,并给出了CompCert编译器重定向设计的要点。文中工作有助于实现CompCert重定向,比如实现面向重要国产处理器的后端。 展开更多
关键词 compcert 形式化验证的编译器 目标代码生成 编译器重定向
在线阅读 下载PDF
一个C语言安全子集的可信编译器 被引量：3
4
作者 王蕾 石刚 +2 位作者 董渊 白晓颖 王生原 《计算机科学》 CSCD 北大核心 2013年第9期30-34,共5页
以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器。然后以我国安全领域C语言安全... 以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器。然后以我国安全领域C语言安全子集标准《航天型号软件C语言安全子集》为依据构造测试用例、创新测试方法,并以此对CompCert编译器进行测试评估。之后依据测试结果,为CompCert编译器增加未支持的C语言标准特性,裁剪不符合C语言安全子集要求的特性,构建符合C语言安全子集标准的可信编译器。最后的实测结果表明,所实现的编译器符合C语言安全子集标准的要求,且没有降低C代码的执行效率。 展开更多
关键词 可信计算 compcert C安全子集 经过验证的编译器
在线阅读 下载PDF
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 下一页 到第 页
使用帮助 返回顶部