导读:本文包含了编译器验证论文开题报告文献综述及选题提纲参考文献，主要关键词:堆栈机器,编译器,定理证明器,形式化方法
编译器验证论文文献综述
陈飞扬,徐文涛,孙绍山,朱浩,钱振江[1]（2019）在《堆栈机器简单编译器在Isabelle/HOL中的验证》一文中研究指出堆栈机器(stack machine)作为一种计算模型,不仅执行部分高级语言的效率很高,而且其编译器也简单、快速.在形式化领域,目前已有不少定理证明器用来验证模型的正确性.本文对堆栈机器的简单编译器进行介绍,对布尔表达式和算术表达式、机器指令、编译器、机器运行行为在Isabelle/HOL中进行形式化,验证编译器的正确性.(本文来源于《常熟理工学院学报》期刊2019年05期）
魏国,麦先根,张旻[2]（2019）在《基于CVSA的无虚拟机主机端编译器验证适配设计与实现》一文中研究指出编译器厂商不断向编译器提供新的非一致性扩展,但这些扩展是否会造成程序的问题,就需要有相应的工具进行检查。CVSA是国际公认的C编译器一致性验证工具,但在验证交叉编译器时具有用况约束。提供一种适配CVSA的设计和实现,以扩展CVSA的使用范围。(本文来源于《信息通信》期刊2019年05期）
江南[3]（2016）在《机器检测的验证编译器：从_mJava到Micro-Dalvik虚拟机》一文中研究指出编译器是将高级语言编写的程序转换到能在目标平台上运行指令集的重要系统软件。但是,由于高级语言的规范复杂,多以自然语言描述,导致编译器编写者在实现语言时,对一些模糊的语义定义理解困难,不知道应该翻译为怎样的机器指令；此外,编译器本身是一个大型复杂的软件,即使编译器编写者明确知道了语言的准确定义,他们在实现该编程语言时也很可能存在编码问题。因此,大多数编译器虽然在发布前已经进行了大量测试,但仍存在许多问题。这些问题对于安全攸关的软件系统来说,即使出现概率很小,也可能造成重大的人员伤亡与经济损失。因此,通过测试手段检测的编译器仍然是不可信任的。编译器问题使得在高级语言程序上进行程序验证的努力很可能付之东流,因此,需要对编译器的正确性进行形式化证明。本文以“语义等同性”来形式化定义编译器的正确性为指导思想,研究了一个机器检测的验证编译器,它的源语言是符合面向对象(Object-Oriented,OO)语言特性的一个具有较大实用性的Java语言子集mJava,目标语言是一种寄存器架构的虚拟机(Virtual Machine,VM),Micro-Dalvik,以Android Dalvik VM作为参考。为了达到这个研究目标,使用定理证明助手Isabelle/HOL,本文从以下叁个方面展开了研究。(1)机器检测的mJava源语言及目标机器Micro-Dalvik VM语言的形式语义对于mJava源语言,定义了一个具有较大实用性的Java语言子集,除了块、顺序、条件、循环语句等基本语法结构外,它包括封装、继承、方法重载和覆盖以及异常处理等。然后基于抽象语法,归纳定义了每一个抽象语法结构的语义规则,从而定义出mJava语言的大步操作语义(big-step operational semantics),并定义mJava源语言表达式的类型规则以及程序的良构性。对于目标机器,对Dalvik VM指令集进行抽象,支持封装、继承、方法重载和覆盖以及异常处理等,得到Micro-Dalvik VM指令集,定义Micro-Dalvik VM状态,定义单条指令执行的语义函数和语义关系,程序执行是任意有限步的单条指令执行,是单条指令执行语义关系的自反传递闭包。(2) mJava程序到Micro-Dalvik VM程序的编译及正确性证明定义了中间语言程序Ji_prog的抽象语法和语义,通过生成中间语言程序,将mJava程序分两步翻译成Micro-Dalvik目标机器指令程序。首先,mJava源程序中的本地变量名按照其声明顺序转换为所对应的序号,成为中间语言程序；然后,将组成Ji_prog程序中的每个子表达式转换成一条或多条Micro-Dalvik指令,并生成异常表。编译正确性的证明也分为两步,对编译前后的语义等同性分别进行归纳证明,从而证明了编译mJava程序到Micro-Dalvik VM程序的正确性。(3)Micro-Dalvik字节码验证器和类型保持的编译字节码验证器(Bytecode Verifier,BV)是DalvikVM的重要组成部分,其主要任务是类型检查。因此,从类型的角度对Micro-Dalvik虚拟机进一步展开研究。首先基于数据流分析算法,定义了Micor-Dalvik VM的类型系统,并证明了它的可靠性。接着实现了一个可执行的字节码验证器,证明了它的正确性。最后,对于良类型(well-typed)的mJava程序,证明编译后生成的字节码程序通过了字节码验证器的检查,从而证明了语义等同的验证编译器也保持了类型的可靠性,于是进一步奠定了它的正确性。因此,本文在定理证明助手Isabelle/HOL的支持下,验证了一个具有面向对象特性的源语言,mJava,编译到寄存器架构的虚拟机,Micro-Dalvik的语义等同性,并证明了良类型的mJava源程序经该验证编译器编译后,所生成的字节码程序的类型可靠性。在这个实现过程中,提出了一个较为完整的寄存器架构的Micro-Dalvik VM形式模型,该模型包括了虚拟机的抽象语法和语义,以及一个基于数据流分析算法的类型系统,证明了该类型系统的可靠性,并实现了一个证明正确的字节码验证器。同时,本文研究工作也证实了机器(交互式定理证明工具Isabelle/HOL)验证一个复杂程序,即编译Java语言子集到Dalvik VM子集正确性的可行性。本文给出的形式化定义和证明较为清晰和直观,易于扩展,可维护性高,应该有潜力应用于安全攸关的工业软件开发中。(本文来源于《武汉大学》期刊2016-10-01）
盛枫,窦亮,杨宗源[4]（2015）在《基于Coq的命令式语言编译器机械验证的研究与实现》一文中研究指出软件的可靠性和可信性越来越受到人们的关注,而编译器作为软件开发的基础,其正确性的验证一直都是个重要且迫切的问题.设计和实现一个小型命令式语言IMP的编译器,该编译器将IMP源代码转换成定理证明器Coq接受的函数式语言表示形式的代码,通过语义分析得到IMP目标代码,在堆栈中执行得到结果.本文的重点是使用交互式定理证明器Coq机械验证函数式语言表示形式的源代码编译执行前后的属性和行为均保持一致.本文的工作为使用堆栈的编译器和其他软件系统的机械化形式验证提供了一种新的思路和方法.(本文来源于《小型微型计算机系统》期刊2015年09期）
刘晓庆[5]（2014）在《嵌入式SRAM编译器设计与IP验证》一文中研究指出近年来随着半导体存储器技术的快速发展,静态随机存储器(SRAM)因其速度快的特性被广泛应用于各种高速存取场合。SRAM只需长期提供电源,而无需定期的刷新存储单元,是一种静止存取的内存。在现代处理器架构中,SRAM作为高性能系统中不可或缺的一部分,通常作为多级缓存以弥补处理器与DRAM存取时间的差距。随着嵌入式系统的逐渐发展,SRAM常作为电路的一部分嵌入到SOC芯片中。传统全定制SRAM设计周期较长,并且人员需求大、开发成本高。在ASIC芯片设计中,存储器的容量根据用户应用的需求有很大的变化。如何正确快速地设计SRAM和产生SRAM IP核已经成为一个难题。然而,SRAM编译器可满足大多数容量可变的构架,是一种单元库设计与自动化程序结合的软件。预先建好的模板和单元库可以简化编译器代码编写和降低生成IP核的复杂性。本论文基于SRAM电路设计与仿真为SRAM编译器提供的准备文件,开发了一套自动产生SRAM IP核,容量范围为64B-512K的SRAM编译器。该编译器根据仿真数据表、模板和子单元库生成Lib库、CDL和版图等IP核。首先针对28nm工艺的Lib库文件提出一种Detail Power电路的参数提取方案,此方案可分析出不同端口的翻转对SRAM功耗的影响。考虑到长导线电阻电容特性对信号传输的影响,采用π型RC结构建模导线自身的电阻电容和连接器件。根据电路的网表和建模参数,使用Hspice工具仿真出SRAM每个端口的功耗,并开发Lib Viewer工具抓取Lib库数据,以线性图的形式进行数据分析。接着针对CDL和版图提出各自的拼接算法和开发相应的分析处理工具,包括以GUI形式查看CDL并生成树状图的CDL Viewer工具和抓取版图子单元SM选项以实现版图修改和添加Power Ring的GDS Builder工具。最后本文实现了SRAM编译器IP核的验证,以及通过SRAM性能参数(读写余量、关键点电压差等)评估了编译器设计的合理性。目前此SRAM编译器已被成功的移植到180nn、130nm、65nm和40nm工艺节点的SRAM设计中。(本文来源于《安徽大学》期刊2014-05-01）
龚才[6]（2014）在《嵌入式SRAM编译器时序功耗模型的建立与验证》一文中研究指出嵌入式存储器作为SoC系统中的重要组成部分,其在SoC中的作用日益增加。首先,SoC芯片数据通道的关键路径上存在一些SRAM,使芯片的速度受到SRAM的访问速度的直接制约；其次,SRAM的功耗占据SoC芯片整体功耗的比重逐渐增加,它由SRAM存储容量和读写速度的增加造成的；再次,芯片的面积和成本受到SRAM集成度的影响,而这可以通过使用高水平的设计技术和先进的物理实现技术降低影响；总体来讲就是SoC各性能的发展瓶颈是SoC中SRAM造成的,如速度(频率)、功耗和面积。所以制作位于关键路径上的SRAM对实现SoC芯片整体性能的提高,功耗以及成本的降低非常有利,这些SRAM具有高速、低功耗、高密度等特性。当今半导体行业通常利用全定制和SRAM编译器两种设计方法产生需要的存储器。本文采用SRAM编译器快速生成用户群体各自所需的SRAM IP核,采用了确保SRAM稳定性和高性能等的全定制设计方法。用户能够从产生的Datasheet文件中用户可以直接读取SRAM的性能参数,包括时序和功耗等,其中Datasheet文件中的数据来源于Lib库中参数模型解析的结果,对SRAM的性能参数我们通过建立模型的方法表明。常用建模方案有解析模型法和统计模型法。目前的编译器普遍还存在的问题是设计周期长,对具体SRAM电路结构的依赖程度比较高,开发过程中的重复性投入,设计效率低下。本文基于SRAM的研究分析的基础上,对编译器设计中涉及到的参数模型重新整理分析,针对不同容量的SRAM分别提出了新的时序、功耗模型方案。首先,针对大容量SRAM字线负载过大的问题使用了分等级字线译码结构技术,使工作的字线上负载大幅度的降低；其次,对于那些容量大于32KB的SRAM利用分模块译码技术,使每次只有一个模块处于工作状态,更有利于提高SRAM的性能和降低功耗；再次,建立了不同容量SRAM的时序功耗模型；最后,制作了SRAM编译器的Lib、Datasheet等模板文件,并对其进行验证。采用上述方案可以从提高SRAM编译器的通用性及灵活性,从下面几个方面能很好的进行说明：一、自主选择架构,根据用户的要求实现最优SRAM架构的选择,以平衡面积、延时、功耗的要求；二、通用性强,只要提供相应的模板文件及特定工艺的单元库,就可编译生成任何类型的存储器；叁、较好的时序及功耗计算方法,能够基于选择的SRAM结构合理的选择Lib库文件中的参数模型。(本文来源于《安徽大学》期刊2014-04-01）
高蕾[7]（2014）在《C编译器测试验证技术研究与应用》一文中研究指出从程序开发角度看,作为最常使用的系统软件之一,编译器的重要性不言而喻,对编译器的测试技术的研究一直是软件测试领域的一个重要分支。针对目前较常用的C编程语言,现有编译器测试验证工具(如SuperTest、CVSA C等)主要关注编译器对语言标准一致性的实现,本文的研究对象是一种编译器随机差分测试工具--Csmith,主要侧重于查找编译器编译中间过程的错误。Csmith使用自定义的语法子集,随机生成测试用例。其问题在于其只考虑了一个最基本的语法子集,且采用硬编码方式进行实现。本文使用基于语法的Purdom算法实现测试用例的自动生成,提高了Csmith对C语言语法规则的覆盖度和扩展性。’此外,Csmith生成的测试用例中有约10%是不能正常结束的,本文对此类测试用例添加了人工控制机制,使得用户可以控制此类测试用例的生成与否。本文对GCC编译器进行了测试验证,实验结果表明,本文所提的改进方法和实现是有效的。(本文来源于《北京邮电大学》期刊2014-01-20）
王秀丽[8]（2011）在《汽车电子控制领域编译器安全验证策略》一文中研究指出编译器验证是汽车电子软件开发过程中的重要一环.在分析了相关安全要求和通用验证方法的基础上,提出了一种基于测试的编译器安全验证策略,并给出了具体实现过程.(本文来源于《上海交通大学学报》期刊2011年S1期）
[9]（2011）在《Wind River Diab编译器加速汽车电子系统开发与测试验证》一文中研究指出全球嵌入式及移动应用软件领导厂商风河(Wind River)近日宣布,居全球汽车产业领导地位的系统及材料供应商Conti-nental选用Wind River Diab编译器(Compiler)开发其驾驶及汽车控制系统,其中包含刹车、引擎控制以及电力管理等子系(本文来源于《工业控制计算机》期刊2011年04期）
俞甲子[10]（2008）在《GCC编译器安全验证方法研究》一文中研究指出编译器作为计算机软件中最为基础的软件之一,与操作系统、数据库系统一起被列为构成计算机系统软件的关键性的基础设施。而编译器作为任何软件的产生器,它的安全性、可靠性和稳定性更是至关重要。特别是在那些对软件的可靠性要求十分高的特殊环境里面,我们必须保证编译器编译出来的代码是对程序源代码的正确、真实的反应,保证编译器在编译过程中逻辑上的正确性以及行为上的透明性。本文首先研究了目前国内外对于软件验证,特别是编译器验证领域的一些工作进展。主要包括形式化的验证方法、模型校验、目标文件结构比较等等方法,分析并讨论了这些方法在理论上的优缺点以及它们在实践应用中的效果。本文对于编译器的安全性的关注点在于:验证编译器是否在编译阶段在输出目标代码中插入恶意的代码或者后门程序。之后本文提出了两种可行的编译器验证方案:编译器代码分析及对比验证以及目标码逻辑结构对比验证。在第一个方案中,我们以GCC编译器为例,试图将GCC编译器源代码中的所有函数分成两类:对于那些会在函数内部改变它的输入数据的函数,影响编译器最终输出结果的,我们将它们归类为第一类;对于那些在函数内部不会改变输入数据的函数,不影响编译器最终输出结果的,我们将它们归类为第二类。对于第二类函数,我们在函数的入口处将所有输入数据保存,然后在函数返回时将所有输入数据与之前保存的数据进行对比,如果对比成功,则证明该函数的确没有改变编译器的最终输出结果;对于第一类函数,我们将人工地检查这些函数的代码并且由一组独立的小组将这些函数根据描述重新实现,然后对比原先这些函数的运行结果以及独立实现的函数运行结果,如果结果一致,则表示该函数安全。第二个方案中,本文采用了一种对比编译器的输出目标文件与源文件的控制流逻辑结构的方案。在这个方案中,我们采用GCC编译器编译一份源代码,然后提取源代码和编译以后目标码的控制流图的结构,使用同构图算法对这两个控制流图进行比较,如果这两份控制流图的逻辑对比一致,那么可以证明该编译器在编译过程中没有插入恶意代码,即证明这目标编译器在行为上安全的。最终,本文提出将这两种方案相互结合的综合的编译器安全验证方法,使得一方面能够大大减轻编译器验证的工作量,另一方面又能够保证验证的完整性。本文所提出的方法和结论可以进一步地推广到其他的编译器和硬件平台的验证工作中去,它们应该有着更广泛的应用前景。(本文来源于《浙江大学》期刊2008-08-15）
编译器验证论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
编译器厂商不断向编译器提供新的非一致性扩展,但这些扩展是否会造成程序的问题,就需要有相应的工具进行检查。CVSA是国际公认的C编译器一致性验证工具,但在验证交叉编译器时具有用况约束。提供一种适配CVSA的设计和实现,以扩展CVSA的使用范围。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
编译器验证论文参考文献
[1].陈飞扬,徐文涛,孙绍山,朱浩,钱振江.堆栈机器简单编译器在Isabelle/HOL中的验证[J].常熟理工学院学报.2019
[2].魏国,麦先根,张旻.基于CVSA的无虚拟机主机端编译器验证适配设计与实现[J].信息通信.2019
[3].江南.机器检测的验证编译器：从_mJava到Micro-Dalvik虚拟机[D].武汉大学.2016
[4].盛枫,窦亮,杨宗源.基于Coq的命令式语言编译器机械验证的研究与实现[J].小型微型计算机系统.2015
[5].刘晓庆.嵌入式SRAM编译器设计与IP验证[D].安徽大学.2014
[6].龚才.嵌入式SRAM编译器时序功耗模型的建立与验证[D].安徽大学.2014
[7].高蕾.C编译器测试验证技术研究与应用[D].北京邮电大学.2014
[8].王秀丽.汽车电子控制领域编译器安全验证策略[J].上海交通大学学报.2011
[9]..WindRiverDiab编译器加速汽车电子系统开发与测试验证[J].工业控制计算机.2011
[10].俞甲子.GCC编译器安全验证方法研究[D].浙江大学.2008