论文部分内容阅读
编译器是将高级语言编写的程序转换到能在目标平台上运行指令集的重要系统软件。但是,由于高级语言的规范复杂,多以自然语言描述,导致编译器编写者在实现语言时,对一些模糊的语义定义理解困难,不知道应该翻译为怎样的机器指令；此外,编译器本身是一个大型复杂的软件,即使编译器编写者明确知道了语言的准确定义,他们在实现该编程语言时也很可能存在编码问题。因此,大多数编译器虽然在发布前已经进行了大量测试,但仍存在许多问题。这些问题对于安全攸关的软件系统来说,即使出现概率很小,也可能造成重大的人员伤亡与经济损失。因此,通过测试手段检测的编译器仍然是不可信任的。编译器问题使得在高级语言程序上进行程序验证的努力很可能付之东流,因此,需要对编译器的正确性进行形式化证明。本文以“语义等同性”来形式化定义编译器的正确性为指导思想,研究了一个机器检测的验证编译器,它的源语言是符合面向对象(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子集正确性的可行性。本文给出的形式化定义和证明较为清晰和直观,易于扩展,可维护性高,应该有潜力应用于安全攸关的工业软件开发中。