mJava到Micro-Dalvik虚拟机的编译验证

江　南,何炎祥,张晓瞳

(1.武汉大学计算机学院,湖北武汉430072;2.武汉大学软件工程国家重点实验室,湖北武汉430072;3.湖北工业大学计算机学院,湖北武汉430070)

mJava到Micro-Dalvik虚拟机的编译验证

江南1,3,何炎祥1,2,张晓瞳1,2

(1.武汉大学计算机学院,湖北武汉430072;2.武汉大学软件工程国家重点实验室,湖北武汉430072;3.湖北工业大学计算机学院,湖北武汉430070)

针对类Java的面向对象语言mJava到类Dalvik的寄存器架构虚拟机Micro-Dalvik的编译验证,给出了mJava语言和Micro-Dalvik的操作语义.从mJava语言程序到Micro-Dalvik虚拟机指令的编译分为两步,首先将mJava语言程序中的本地变量名转换为相应的序号,得到一个中间语言程序,再将该中间语言程序翻译成Micro-Dalvik虚拟机指令程序.在给出中间语言的操作语义后,构造了mJava语言程序与编译后的中间语言程序的语义保持定理并证明,以及构造了中间语言程序的语义与编译后的Micro-Dalvik虚拟机程序的语义保持定理并证明.整个形式化编译验证在定理证明助手Isabelle/HOL中进行了机器检测.mJava语言和Micro-Dalvik虚拟机分别对Java语言和Dalvik虚拟机进行了抽象,是我们兼顾语言的真实性和形式化的清晰性的结果.但是,所有形式化的语义严格遵从语言规范中的定义,并与Dalvik VM的实现保持一致,从这种意义上讲,该编译器并不是一个实验性质的假想编译器,而是有其实用意义的.

编译验证;定理证明;操作语义;机器检测;寄存器架构;面向对象语言

1　引言

编译器是将高级语言编写的程序转换到能在硬件平台上运行的指令集的重要系统软件.商用编译器虽然经过大量测试,但仍然存在许多问题,这些问题不断公布在其缺陷列表的网站上[1～3].编译器错误产生的原因可以归纳为两点,其一是高级语言的语义规范通常复杂,且以自然语言书写,导致编译器难以理解一些模糊的语义定义,不知道它应该将之翻译为怎样的机器指令,只能采取试着运行再观察的态度(run it and see)[4];其二是编译器本身作为一个复杂的软件,也可能有错.这些错误对于安全攸关的软件系统来说,即使出现概率很小,也可能造成重大的人员伤亡与经济损失.由于编译器的不可信,实践中,一些控制系统的关键部分不得不采用汇编语言编写并在汇编级进行验证[1].但是,随着安全攸关的软件大小和复杂度与日俱增,使用汇编语言来开发这些软件已不可行[4].因此,迫切需要构建一个经过形式化验证的编译器,这个证明正确的编译器能够保证最后运行的机器程序是无错的.

为了得到一个验证的编译器,McCarthy和Painter进行了首次尝试[5].其源语言是由代表数值的常量或者变量以及加运算所组成的算术表达式,目标机器是具有一个累加寄存器的简单冯诺依曼机器[1,5].他们使用抽象语法来定义语义,这种方法成为定义编程语言语义的典范[6],但是他们的方法被认为过于泛化[7,8].相对普通程序的验证而言,编译器可以被更好地结构化,因此,Morris提出使用严格定义的数学结构来表达编译器正确性问题的本质[1].所表达的验证思想是:编译器被定义为由源程序到目标程序的数学函数;语义定义为程序到数学值的映射函数,该值可以是非常复杂的类型;目标语义函数表示的语义代表源语义函数所表示的语义[7].这种验证思想流行于后来的大多数编译器验证研究中[8].

尽管Morris给出了指导性方法,编程语言的语义以及编译前后两种语言语义的保持性定义和证明并不容易.研究者们采取不同的语义,对应于不同的证明方式,在命令式语言的编译器验证领域进行了深入研究,这些方法可以归纳为两大类别.

(1) 先定义源语言和目标语言的语义,再定义编译规则,最后构造语义保持定理,证明采用归纳[9～11].代表性成果包括:Stepney基于指称语义,完成了从一个假定的编程语言到汇编语言的编译验证[4];Polak同样基于指称语义,验证了一个Pascal语言子集的编译器[12];Leroy等人基于操作语义,开发了CompCert编译器,其源语言是C语言子集,目标语言是PowerPC汇编代码[13～15];Klein和Nipkow等人验证了一个称为Jinja的Java子集到Java虚拟机(Virtual Machine,VM)字节码的编译器[16,17].

(2) 定义程序转换规则,源语言程序按照转换规则被逐步精化为可执行的目标语言程序.转换规则即是编译器行为,规则的可靠性保证编译的正确性.这种方法通常采用代数语义.Hoare、He、以及Sampaio等人使用这种方法将源程序精化为范式,范式和相关的精化定理可用于针对不同目标机器的编译器设计[18,19].Duran等人将该方法扩展到了一种类似Java的面向对象语言[20].

McCarthy 于1961年也指出,我们应该证明程序符合其规范,而不是测试,并且证明需要经过某个计算机程序的检查.编译器作为一个特殊的程序,其规范与源、目标语言的语义直接相关,真实语言的语义往往庞大而复杂,譬如Java官方语言规范有近700页的描述,JVM规范有约600页,这些加大了形义定义的困难性,以及语义保持及证明的复杂性.定理证明系统,如Coq、 Isabelle/HOL、ACL2、PVS等的出现在编译器验证的实用性方面起到了关键作用.在定理证明系统的支持下进行语义表达和证明更为高效,经过机器检测的编译器具有更高的可靠性和可维护性[16,21～23].CompCert的整个开发工作在定理证明助手Coq中完成,其源语言是一个C语言子集,包括了能够运用于编程安全攸关的工业嵌入式软件所需要的语法成份,所产生代码的执行性能接近于O1优化级GCC[15].

在近半个世纪的探索研究之后,过程式语言的编译验证得到了较好的理解与实施,出现了象CompCert这个被广泛认可的C语言的验证编译器.Eiffel语言设计中缺陷的发现促使编程语言,特别是面向对象语言的设计们致力于证明语言的类型可靠性,导致了Java语言、Java虚拟机(JVM)、JVM字节码验证的形式化得到了广泛研究[24～28];近几年来由于Android成为一个广泛使用的移动设备平台,虽然该平台上的应用程序用Javia编写,但是被编译成了Dalvik字节码,而不是Java字节码,使得已有的Java程序分析工具不能直接使用或者难以使用,而运行在这个平台上的应用程序的安全性和可靠性问题变得越来越重要,因此,Android Dalvik VM程序的静态分析以及形式化研究也陆续展开[29～31].虽然象Java语言、JVM、以及Android Dalvik VM的形式化研究以及JVM字节码验证都取得了一定进展,然而在支持OO语言所增加的封装、继承、方法覆盖、动态绑定和多态等语言特性的编译验证领域,目前成果并不多见,还有待深入研究.文献[20]使用代数的方法构造了一个类Java语言到JVM的编译器,文献[24]使用抽象状态机定义了Java语言,并对编译到Java VM的正确性进行了证明,但他们都未经过机器检测.目前尚未见有针对Dalvik VM的编译验证.

本文使用定理证明助手Isabelle/HOL[32]形式化验证一个编译器,其源语言mJava是一个较为完善的符合OO特点的顺序语言子集,目标机器以典型寄存器架构的虚拟机Android Dalvik VM为参考.

2　mJava的形式化

本文讨论的源语言称为mJava,mJava包括了封装、继承、多态、异常处理,目前暂未考虑线程和数组.式(1)定义了mJava语言的语法成分,其中,′a是类型变量,因此可以用来同时表达mJava程序的语法和编译时生成的中间语言程序的语法.本地变量的声明出现在块语句中,它是一个变量名和其类型组成的二元组的列表.

′a epr=Val val

|Var ′a

|Binop (′a epr) bop (′a epr)-<<->>-

|New cname

|LAss ′a(′a epr)-:=-

|Cond (′a epr) (′a epr) (′a epr)if(-)-else-

|Seq (′a epr) (′a epr)-;;-

|Block((′a×ty) list)(′a epr){-;-}

|ThrowEx(′a epr)

|Cast cname (′a epr)

|TryCatch(′a epr)cname ′a(′a epr)try-catch(--)-

|FAcc(′a epr)vname cname-·-{-}

|FAss (′a epr) vname cname(′a epr)-·-{-}:=-

|Call (′a epr)mname (′a epr list)-·-(-)

|While (′a epr)(′a epr)

(1)

式(2)中的′m是类型变量,可以用来代表mJava和Micro-Dalvik程序中的方法体;ty代表类型,可以是空类型Void,布尔类型Boolean,整型Integer,空引用类型NT,类类型Class cname.式(2)表示,程序(prog)是类声明(cdecl)的列表;类声明是类名和类(class)的二元组;类是由其超类名、变量声明(vdecl)列表以及成员方法声明(mdecl)列表组成的三元组;变量声明是变量名和其类型的二元组,方法声明是由其方法名、形参类型列表、返值类型和方法体组成的四元组.

′m prog=′m cdecl list

′m cdecl=cname×′m class

′m class=cname×vdecl list×′m mdecl list

vdecl=vname×ty

′m mdecl=mname×ty list×ty×′m

(2)

mJava语言程序如式(3)所示,其中,J-epr使用变量名vname取代了类型参数′a,表示mJava程序的合法语句是式(1)中的15个表达式语句;J-mb表示mJava程序的方法体,它是形参变量名列表和J-epr组成的二元组.因此得到mJava程序的定义.

J-prog=J-mb prog

J-mb=vname list×J-epr

J-epr=vname epr

(3)

mJava程序状态(state)的完整定义如式(4)所示,它是堆(heap)和本地变量(locals)的二元组;堆是地址(addr)到对象(obj)的映射;地址是自然数类型nat;对象是类名和其成员变量(fields)的二元组;成员变量和本地变量的区别是:成员变量的定义中包括了定义该成员变量的类名,因此是其名称和该类名所组成的的二元组到其值的映射,而本地变量则仅是其名称到值的映射.值由val定义,可以是空引用值(Null)、布尔值(Bool bool)、整数值(Intg int)、以及对象的地址(Addr addr).

state=heap×locals

heap=addr⇀obj

addr=nat

obj=cname×fields

fields=vname×cname⇀val

locals=vname⇀val

(4)

程序的语义定义采取大步操作语义(Big-Step Operational Semantics)[32,33],以归纳谓词(inductively defined predicate)的方式给出,其语义规则的形式如式(5)所示,表示:执行程序P中组成方法体的表达式e,从初始状态(h,l)到达新的状态(h′,l′),e计算到e′.

P

(5)

方法调用时的参数是表达式列表,为了对表达式列表进行计算,扩展了式(5)的定义为:如果表达式列表为空,则状态不发生改变;如果表达式形如e#es,其中,#是单个元素e加在列表es的首部,则先计算单个表示式e的值,剩余列表再按形如e#es进行递归计算,每次计算的值组成新的值列表.

语义规则参照Java语言规范[34].在此给出较为复杂的方法调用e.M(ps)在当前状态s0下的语义计算规则,如式(6)所示.

(6)

式(6)表示:当对方法调用语句进行计算时,首先计算e,得到其值addr a,到达新的状态s1,addr a代表调用方法的对象的地址;接着,在状态s1下,计算形参表达式列表,得到形参值列表,并更新状态到(h2,l2);如果在堆h2中,地址a代表着一个对象(C,fs),Ts 是形参计算得到的值列表所对应的类型列表,对于程序P中的类C而言,方法名为M,形参类型列表为Ts的方法是可见的,这个方法的返值类型是T,方法体是(pns,body),通过seesMethod完成;形参值列表长度与形参名列表长度相等,则为这个调用方法建立新的本地变量l2′,在这个新的映射中,this映射到地址a,形参名列表映射到值列表,其中,加了中括号的映射符号代表两个列表的各个元素按照顺序对应映射;最后,在状态(h2,l2′)下,执行调用方法的方法体,得到e′,和新的状态(h3,l3).所有这些计算完成后,方法调用语句的最终结果为e′,堆状态为h3,但是本地变量恢复到调用方法前的本地变量l2.

函数seesMethod调用了归纳定义的谓词seesMethodDef,它的归纳定义如式(7)所示.式(7)获得一个映射,即映射方法名和方法参数列表的二元组到返值和方法体的二元组,因此,根据给定的(M,Ts),式(8)可以查找到其对应的方法m.式(7)的实现为,由函数getClassDef获得指定类名的类定义为(D,fs,ms),如果对象类不是类Object,则按类层次关系向上查找类中定义的方法列表.函数map-of中的lambda演算将表示方法的四元组变换成三元组,其中第一个元素为二元组(mName,Ts),然后map-of函数中的将元组列表转换成一个映射,这个映射与第一个lambda演算形成函数组合.父类获得的映射在++运算符的左边,子类获得的映射在右边,如果m1和m2代表两个映射,m1++m2运算规则是:如果在映射m2中查找到对应在的方法,则结果为该方法,若没有找到对应的方法,即为None,再在映射m1中查找是否有对应的方法.最后的效果为:如果父类和子类具有同名同参数列表的方法,由于子类中的查找在前,结果为子类中定义的方法,即子类覆盖了父类的方法.由于方法查找时,方法名和形参类型同时作为参数,因此对于同名而不同形参的方法,视为不同的方法,即方法重载.

seesMethodDefInduct:

seesMethodDef P C MmNameTs′

(7)

seesMethod P C M Ts T m D≡

∃Mm. seesMethodDef P C Mm∧

Mm(M,Ts)=⎣((T,m),D)」

(8)

以上方法覆盖要求方法名和参数类型相同,返值类型不大于被覆盖方法的返值类型,式(9) 给出了这个定义,它是定义程序well-formedness的一个重要组成部分.

λ(C,(D,fs,ms)). (∀m∈set ms.distinct-fst

(map(λ(M,Ts,T,mb).((M,Ts),T,mb)) ms) ∧

(∀(M,Ts,T,mb)∈ms. ∀D′ T′ m′.

(9)

3　Micro-Dalvik的操作语义

目标机器是寄存器架构的虚拟机Micro-Dalvik,参考Android Dalvik[35～38 ].Micro-Dalvik虚拟机的抽象指令如式(10)所示.

instr=Const nat nat

|Iget nat nat vname vname

|Iput nat nat vname vname

|AriBinop ariop nat nat nat

|Cmpeq/ne/gt/ge/lt/le nat nat nat

|IFfalse idx int

|Goto branchoffset

|Return nat

|Invoke nat nat mname

|NewIntance nat cname

|Throw nat

|CheckCast nat cname

|Move nat nat

|MoveResult nat

|MoveException nat

(10)

Micro-Dalvik虚拟机程序定义如式(11)所示,其中,Micro-Dalvik程序(dvm-prog)的定义是将式(2)中第一行的类型变量′m替换为其方法体(dvm-mb),它是三元组,第一个分量表示寄存器个数(不计this和实参的后N个寄存器),该值在编译时确定,第二个分量是指令列表,最后一个分量是编译时生成的异常表(ex-table).异常表是异常表项(ex-entry)的列表,一个异常表项由try块起始指令程序计数pc、结束指令程序计数pc、捕获异常类型cname以及对应的catch块的起始指令程序计数pc组成.pc是自然数类型的别名.

dvm-prog=dvm-mb prog

dvm-mb=nat×instr list×ex-table

ex-table=ex-entry list

ex-entry=pc×pc×cname×pc

(11)

式(12)给出了Micro-Dalvik虚拟机状态dvm-state,它由是否产生异常、堆(heap)、栈桢(frame)列表和方法返回值组成,如果有异常产生,val option的值为异常对象的地址(Addr a),否则其值为None.栈桢由捕获的异常、寄存器中存放的值的列表、方法所在的类名、方法名、形参列表以及程序计数组成,如果捕获到异常,xcptval的值为异常对象的地址.堆(heap)的定义与源语言mJava相同,如式(4)所示.

dvm-state=val option×heap×frame list×rtval

frame=xcptval×val list×cname×mname×ty list×pc

(12)

Micro-Dalvik虚拟机程序的操作语义与源mJava程序大步操作语义的定义方式不同,它先定义函数run,通过调用函数run-instr给出了单步执行的状态转换,如式(13)所示.

run(P,xp,h,[],r)=None

run(P,xp,h,(x,reg,C,M,ts,pc)#frs,r)=

(let i=instrs-of P C M ts!pc;(xp,h′,frs′,r′)=

run-instr i P h x reg C M ts pc frs r in

(13)

使用上述函数式的定义,关系方式的语义定义runRel实现为状态转换的集合,因此,程序的执行runProg由任意有限步的单步执行组成,为了方便表示,将Micro-Dalvik虚拟机程序的语义定义runProg P σ σ′写为如式(14)的形式,它表示在初始虚拟机状态σ下执行程序P,到达新的状态σ′.

Pσ′

(14)

状态转换函数run-instr以及详细阐述可详见文献[39].

4　编译及证明

4.1mJava到Micro-Dalvik VM的编译

4.1.1mJava程序的编译方法

在不考虑优化的情况下,mJava源程序J-prog到Micro-Dalvik VM目标程序dvm-prog的翻译是将组成源程序方法体的抽象表达式J-epr中的每一个构造器所构造的语句翻译成一条或多条目标机器指令,即instr定义的指令.由于源程序中的本地变量名不再出现在机器指令中,这些值按照其声明的顺序存储在一片连续的寄存器中,为避免一遍翻译及证明的复杂,定义一个中间语言Ji-prog,如式(15)所示.

Ji-prog=Ji-mb prog

Ji-mb=nat ×Ji-epr

Ji-epr=nat epr

(15)

其中,Ji-epr用 nat取代了式(1)中的类型变量′a,即中间语言程序中的语句中不再出现方法本量名,而是方法变量名对应的序号.Ji-mb中的 nat是方法形参个数(不包括this),将用于指定代码生成时可用的寄存器序号.因此,将式(2)中第一行的类型变量′m用Ji-mb替换后,得到中间语言程序的定义Ji-prog.

编译分为两步,第一步是中间代码生成,用于消除本地变量名,将J-prog翻译成Ji-Prog,由cEpr1完成;第二步是代码生成,将Ji-prog翻译成dvm-prog,由cEpr2和cEprex2共同完成.我们将在下一小节4.1.2以及4.1.3中分别予以讨论.

对方法进行编译的函数如式(16)所示,表示:给定的一个方法(M,Ts,T,m)和一个编译函数f,编译后的结果为(M,Ts,T,f m).

cMethod f≡

λ(M,Ts,T,m).(M,Ts,T,f m)

(16)

对应于源程序方法体J-mb和中间语言程序方法体Ji-mb,相应的f函数都是lambda运算,分别如式(17)和(18)所示.

λ(pns,body).

(length pns,cEpr1(this#pns) body)

(17)

λ(n,body).let locals=maxLocals body;

idx=1+n+locals;

ws=maxWS body;regs=idx+ws;

is=cEpr2idx body;xt=cEprex2idx body 0;

moveps=genMoveps (n+1) regs

in (regs,moveps@is@ [Return idx],xt)

(18)

其中,函数maxLocals归纳计算出方法体中嵌套变量的最大深度,因此,idx是起始可用的寄存器序号,式(19)给出了块语名和捕获异常语句的计算规则.函数maxWS归纳得到所需要的最大计算空间,式(20)给出了创建对象、变量访问、条件以及方法调用的计算规则.

maxLocals{vts;e}=maxLocals e+size vts

maxLocals(try e catch(C V) e′)=

max (maxLocals e)(maxLocals e′+1)

(19)

maxWS{NewInstance n C }=1

maxWS (Var i)=1

maxWS(if (e)e1else e2)=

max (maxWS e) (max (maxWS e1)(maxWS e2))

maxWS(e·M(es))=

max (maxWS e) (maxWS es)+1

(20)

函数genMoveps生成Move指令,将实参值顺序放到序号从0开始的寄存器中,如式(21)所示.

genMoveps 0regs=[]

genMoveps (Suc m) regs=

[Move m (regs+m)] @genMoveps m regs

(21)

主体编译函数如式(22)所示,使用运算°组合两步编译函数,完成从mJava程序到Micro-Dalvik虚拟机程序的编译.

J2DVM≡cPrg2°cPrg1

cPrg1≡cPrg式(25)

cPrg2≡cPrg式 (26)

cPrg f≡ map (cClass f)

cClass f≡λ(C,D,fs,ms).

(C,D,fs,map(cMethod f) ms)

(22)

4.1.2中间代码程序Ji-prog生成

为了得到本地变量声明序号,需要知道当前本地变量环境,参数Vars::vname list代表这个环境,初始本地变量环境为this和方法形参名,在式(17)给出.

由mJava源程序到中间语言程序的转换由函数cEpr1完成,在给定当前变量环境下,计算表达式中出现的变量名的序号.因此,除了本地变量名被转换成了其对应的序号外,其余与源程序相同.式(23)给出了编译块表达式语句的方法,其他表达式的语句的编译较为直接,不再赘述.

cEpr1Vars {vts;e}={

enumerate(size Vars)(map(λ(vn,t).t)vts);

cEpr1Vars@(map(λ(vn,t).vn)vts))e}

(23)

4.1.3目标Micro-Dalvik虚拟机代码生成

目标代码的生成包括虚拟机指令的生成cEpr2和异常表项的生成cEprex2.由于Dalvik这种寄存器架构的虚拟机没有操作数栈,它使用了额外的指令,即MoveResult指令存放方法的返回值,以及使用MoveException指令存放捕获到的异常对象.因此,编译时,方法调用指令之后紧跟一条MoveResult指令.在编译异常处理块时,首先添加一条MoveException指令.

针对每一个Ji表达式语句,指令生成方法是直接的.式(24)给出了异常捕获语句的指令生成方法,其中参数idx表示编译时可用的第一个寄存器序号,初始序号为方法形参个数+1(this)与方法本地变量个数的和.

cEpr2idx (try e catch(C i) e′)=

(let try=cEpr2idx e;

catch=[MoveException idx ] @ cEpr2(idx+1) e′

in try@ [Goto (int(size catch)+1)]@catch)

(24)

由于异常表项中的程序指令计数是绝对程序指令计数,而不是如跳转指令中的相对偏移量,所以异常表项生成函数cEprex2包括了一个参数,代表当前的程序指令计数,针对异常捕获语句的异常表项生成如式(25) 所示.

cEprex2idx (try e catch(C V) e′)pc=(let

cEprex2 idx e pc@ cEprex2 (idx+1) e′ (pc′+2)

(25)

4.2编译正确性证明

编译正确性在于编译前后两种程序语义的保持.对于4.1节中定义的中间语言程序Ji-prog,我们还未定义其语义,因此,在本节先给出它的大步操作语义;再构造J-prog和和编译后的Ji-prog语义保持定理并证明,以及Ji-prog和编译后的dvm-prog语义保持定理并证明,最后由这两步的语义保持,证明J-prog到dvm-prog程序的编译的正确性.

4.2.1Ji-prog的大步操作语义

与源程序J-prog的状态比较,中间语言程序Ji-prog由于消除了变量名,状态表示中,本地变量不再是变量名到其值的映射函数,而是一系列值,如式(26)所示.

state1=heap×(val list)

(26)

Ji-prog的大步操作语义的计算规则与J-prog的大步操作语义规则基本相同.式(27)给出它的方法调用的语义规则.

(27)

4.2.2J-prog到Ji-prog的编译正确性

定理1

定理1表示:若mJava程序是良构的(well-formed),编译前J-Prog的状态与编译后的Ji-prog的状态保持.

程序P是良构的,除式(7)描述的以外,完整的良构性条件描述为:程序P中定义的所有类是良构的,且类名不重复.一个类C是良构的,当且仅当C中定义的成员变量名不重复;成员变量的类型是P中合法类型;没有同名且同参数的方法;所有方法体是良构的;若C不是根类Object,如果C的父类是D,则D不可能是C的子类,即不存在父子类的循环定义;若子类方法覆盖父类方法,子类方法的返值类型不大于父类型,如式(7)所示.一个方法体是良构的,当且仅当形参名列表的长度与方法形参类型列表长度相同;形参名没有重复;this不出现在形参名列表中;不存在嵌套块中变量重复声明;不会出现未声明变量的使用.

按照J-Prog到Ji-prog的翻译:J-prog中的本地变量名转换为对应的序号,如果J-prog的状态由(h,l)转换到(h′,l′),Ji-prog的状态中堆也转换到h′,设本地变量状态转换到ls′,则l′和ls′之间的保持关系为:对于所有在映射l′已赋值的变量(l′ V的值不等于None,表示为∀a∈dom l′),其值与ls′中对应的值相同,当然,需要满足的前提是J-prog和Ji-prog程序执行前的状态l和ls之间也需要满足这个关系;同时,函数fv保证J-prog程序中出现的变量名都是方法体中声明的变量、this或者方法的形参;ls′的大小不小于计算e时所需的本地变量个数;没有嵌套块中变量的重复声明.函数fin1表示fin1(Val v)=val v,fin1(ThrowEx a)=ThrowEx a.

又J-prog的try-catch的语义定义为:

联合IH1和IH2,满足J-prog的try-catch的语义规则的前提,于是有:

又J-prog程序try-catch的编译规则为:

而Ji-prog的try-catch语义规则前提为:

h1a=|(D,fs)|;PD≤*C;

因此,结合IH2,ls2即是待要证明存在的本地变量列表,即∃ls2使得:

cPrg1P1[cEpr1Vars e,(h,ls)]

其中,l2(V:=l1V)是计算e之后的本地变量状态.

证毕.

4.2.3Ji-prog到dvm-prog的编译正确性

定理2

定理2表示:给定程序Ji-Prog,其类C具有可执行的方法M,即(M,Ts,T,(n,body)),在状态(h,ls)下执行其方法体body,到达新的状态(h′,ls′);等价于在机器状态(None,h,[(Unit,ls,C,M,ts,0)],Unit)下执行编译后的程序cPrg2P1,,则执行后的机器状态中,堆也应该是h′,程序执行完毕,桢栈为空.exception e′为None或某个产生的异常对象地址.

定理2直观地表达了编译前后的语义保持性,但是其表达的是方法体内所有语句全部执行完毕后的语义,不能进行归纳证明.因此,代替方法体全部执行完毕来表示语义,而是给定正在执行的指令计数,并按照Ji-Prog执行其表达式的结果是正常值还是抛出异常两方面分别构造语义保持,从而构造定理3,如下所示.

(e′=ThrowEx (Val(Addr xa))→

C,M,ts,pc1)# frs retv)))其中:P,C,M,ts,pc▷cEpr2idx e 表示当前栈桢的指针不会超出被编译表达式所对应的指令, pc指向表达式e编译后对应的第一条指令.

证明在计算规则

令e=try e1catch(C i)e2,

定理的前提条件之一e的语义定义为:

上式表明:如果执行e1时系统抛出了异常,状态转换为(h1,ls1);该异常能够被捕获,即异常类型是捕获异常类型的子类型,并且变量的索引号不超出本地变量最大索引号;在对ls1进行更新,即(h1,ls1[i:=Addr a])状态下执行e2,计算得到e2′,到达状态(h2,ls2);则执行e后得到e2′,到达状态为(h2,ls2).

令σ0=(None, h0,(xt,ls0, C,M,ts,pc)#frs,retv)

其中,pc满足:P,C,M,ts,pc▷cEpr2idx e

因此,pc也满足:P,C,M,ts,pc▷cEpr2idx e1

因此,由:

P11[e1,(h0,ls0)][ThrowEx a,(h1,ls1)],

根据归纳假定得到:∃pc1,使得:

由于此处考虑的是捕获到异常的语义,lookupHandler函数返回一个机器状态,于是有:

其中,pc1′=pc+|cEpr2idx e1|+1.

于是有:P,C,M,pc1′▷cEpr2idx e2.令σ1表示状态:

(None,h1,(xt,ls1[i:=Addr a],C,M,ts,pc1′)#frs

因此,由

P11[e2,(h1,ls1[i:=Addr a])][e2′,(h2,ls2]

根据归纳假定得到:

如果e2′=Val v,则有:

e2′=ThrowEx a,则存在pc2,使得:

又由try..catch的编译规则:

又因为:

pc1′≤ pc2,pc2

所以有:pc≤pc2,pc2

因此,由机器状态转换的传递性,得到待证目标:假定P,C,M,ts,pc▷cEpr2idx e ,若

P11[try e1catch (C i),(h0,ls0)][e2′,(h2,ls2)],则:1)如果e2′=Val v,则有:

C,M,ts,pc+|cEpr2idx e|)#frs,retv)

2)如果e2′=ThrowEx a,则存在pc2,使得:

pc≤ pc2∧ pc2< pc +|cEpr2idx e|∧

证毕.

定理2通过定理3得到证明,即将定理2的前提应用到已经得到证明的定理3上,从而得到定理2.证明过程如下.

证明

由定理2的前提:

seesMethod P1C M Ts T (n,body) C

可以得到:

cPrg2P1,C,M,ts,0▷cEpr2idx body

令σ0=(None,h,[(Unit,ls,C,M,ts,0)],Unit)

联合定理2的另一前提:

P11[body,(h,ls)][e′,(h′,ls′)]

应用到定理3,得到:

如果e′=Val v,则

cPrg2P1

(None,h′,[(Unit,ls′,C,M,ts,|cEpr2idx body|],Unit),因此有:

cPrg2P1(None,h′,[],Unit)

如果e′=ThrowEx a,则存在pc,使得:

0≤pc∧pc<|cEpr2idx body|∧

cPrg2P

lookupH P a h′[(Unit,ls′,C,M,ts,pc)] Unit

因此有:

cPrg2P1(|a|,h′,[],Unit)

综合两种情况,得到:

cPrg2P1(exception e′,h′,[],Unit)

证毕.

4.2.4J-prog到dvm-prog的编译正确性

已经证明了编译J-prog到Ji-prog以及编译Ji-prog到dvm-prog的正确性,因此,J-prog到dvm-prog的编译正确性定理可以构造为:

定理4

组合定理1和定理2,即由源程序到中间程序的翻译正确性,以及中间程序到目标程序的正确性都得到证明后,源程序到目标程序的正确性即建立.

整个编译证明的重点在定理3的归纳证明上,它包括42个case分析,异常捕获是最为复杂、因此最具有代表性的证明case之一,我们给出了其证明过程,其他case的证明方法类似,在此不作详述.

5　结论和下一步研究

本文在定理证明助手Isabelle/HOL的支持下,设计并实现了一个机器验证的编译器,源语言是类Java的面向对象语言mJava,目标机器是类Dalvik的寄存器架构虚拟机Micro-Dalvik.式(1)所定义的的子集考虑到了一个Java程序的核心特性,包括类的定义(实例变量和实例方法),对象创建、继承关系、方法覆盖、静态重载、简单类型和引用类型以及异常抛出和捕获机制.从这种意义上讲,它不是一个假想的语言和目标机器,具有较大实用性.未被考虑的包机制和访问权限、数组和线程、构造方法、类变量和类方法以及finally语句和finalize方法等将在本文基础上进行扩展,譬如给式(2)中的类名cname加上包名,形成限定名来建模包的概念,可以增加一个类型来描述Java语言规范中定义的四种访问权限,加入到类声明和方法声明的定义中,因此式(2)中的′m cdecl由二元组将变成三元组,′m mdecl由三元组将变成四元组,这些改变将导致成员变量和成员方法查找的重新定义.

需要指出的是,我们形式化的是顺序OO语言,并未对并发特性进行编译验证.关于并发特性的OO语言编译验证,文献[40]在文献[16]的基础上进行了针对Java线程的讨论.文献[41]给出了一个针对C/C++并发特性的编译证明,这个编译证明相当抽象;同时,作者也指出:距离完整的C++正确性证明仍然还很漫长,未来他们考虑得到一个具体的操作语义以及编译C++代码片段.这些工作对我们将支持并发的Java编译到Dalvik VM有一定的借鉴意义.本文未包括的另一个语言特性是数组.考虑到Java在运行时动态创建数组,并在运行时对数组赋值进行类型检查,我们拟在本文的基础上,证明该编译器也保持了类型的可靠性,围绕类型系统,再去完整地分析数组问题.

因此,下一步我们将进一步解决完善这个编译器能够支持的语法特性,并对目标虚拟机Micro-Dalvik类型系统的可靠性进行研究和证明.

[1]何炎祥,吴伟.可信编译理论与关键技术[M]. 北京:科学出版社,2013.

He YX,Wu W.Theory and Key Technology of Trusted Compiler[M].Beijing:Science Press,2013.(in Chinese)

[2]Boyle MJ,Resler DR,Winter LV.Do you trust your compiler[J].Computer,1999,32(5):65-73.

[3]何炎祥,吴伟,刘陶,李清安,陈勇,胡明昊,刘健博,石谦.可信编译理论及其核心实现技术:研究综述[J].计算机科学与探索,2011,5(1):1-22.

He YX,Wu W,Liu T,Li QA,Chen Y,Hu MH,Liu JB,Shi Q.Theory and key implementation techniques of trusted compiler:A survey[J].Journal of Frontiers of Computer Science and Technology,2011,5(1):1-22.(in Chinese)

[4]Stepney S.High Integrity Compilation:A Case Study[M].Hatfield:Prentice Hall International (UK) Ltd,1993.

[5]McCarthy J,Painter J.Correctness of a compiler for arithmetic expression[A].Proceedings of the Symposium in Applied Mathematics[C].Rhode Island,USA,1967.33-41.

[6]Plotkin DG.The Origins of structural operational semantics[J].The Journal of Logic and Algebraic Programming,2004,6:3-15.

[7]Morris LF.Advice on structuring compilers and proving them correct[A].Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages(POPL′73)[C].Boston:ACM Press,1973.144-152.

[8]Zadarnowski P.C lambda calculus & compiler verification[D].Sydney:University of New South Wales,2011.

[9]Burstall MR.Proving properties of programs by structural induction[J].The Computer Journal,1969,12(1):41-48.

[10]Nipkow T,Paulson CL,Wenzel M.A Proof for Higher-Order Logic[M].Berlin:Springer-Verlag,2010.

[11]Yves B,Pierre C.Interactive Theorem Proving and Program Development:Coq′Art:the Calculus of Inductive Constructions[M].Berlin:Springer-Verlag,2004.

[12]Polak W.Compiler Specification and Verification[Z].California:Stanford University,Lecture Notes in Computer Science:124,Secaucus:New York,1981.

[13]Blazy S,Dargaye Z,Leroy X.Formal verification of a C compiler front-end[A].Proceedings of the 14th International Symposium on Formal Methods[C].Hamilton:Springer Berlin Heidelberg,2006.460-475.

[14]Leroy X.A formally verified compiler backend[J].Journal of Automated Reasoning,2009,43(4):363-446.

[15]Leroy X.Formal verification of a realistic compiler[J].Communications of the ACM,2009,52(7):107-115.

[16]Klein G,Nipkow T.A machine-checked model for Java-like language,virtual machine and compiler[J].ACM Transactions on Programming Languages and Systems,2006,28(4):619 695.

[17]Strecker M.Formal verification of a Java compiler in Isabelle[A].Proceedings of 18th International Conference on Automated Deduction[C].New York,USA,2002.63-67.

[18]Hoare CAR,He J,Sampaio A.Normal form approach to compiler design[J].Acta Informatic,1993,30:701-739.

[19]Sampaio A.An algebraic approach to the design of compilers:4 (AMAST Series in Computing)[Z].World Scientific,1997.

[20]Duran A A,Cavalcanti A,Sampaio A.An algebraic approach to the design of compilers for object-oriented languages[J].Formal Aspects of Computing,2010,22:489-535.

[21]Milner R,Weyhauch R.Proving compiler correctness in a mechanized logic[J].Machine Intelligence,1972,7(3):51-70.

[22]Leroy X.Mechanized semantics for compiler verification[A].Proceedings of the10th Asian Symposium on Programming Language and System[C].Kyoto,Japan,2012.386-388.

[23]Nipkow T,Oheimb D V.Javalight is type-safe:definitely[A].Proceedings of the 25th ACM Symposium on Principles of Programming Languages[C].New York,USA,1998.161-170.

[24]Stark R,Schmid J,Borger E.Java and the Java Virtual Machine Definition,Verification,Validation[M].New York:Springer,2001.

[25]Drossopoulou S,Eisenbach S.Describing the semantics of Java and proving type soundness[A].Formal Syntax and Semantics of a Java[C].New York:Springer,1999.41-82.

[26]Syme D.Proving Java type soundness[A].Formal Syntax and Semantics of Java[C].New York:Springer,1999.83-118.

[27]Oheimb DV,Nipkow T.Machine-checking the Java specification:proving type-safety[A].Formal Syntax and Semantics of a Java[C].New York:Springer,1999.119-156.

[28]Oheimb DV.Analyzing Java in Isabelle/HOL:formalization,type safety and Hoare logic[D].Munich:Technical University of Munich,2001.

[29]Payet é,Spoto F.An operational semantics of android activities[A].Proceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation[C].New York:ACM Press,2014.121-132.

[30]Jeon JS,Micinski KK,Foster JS.SymDroid:symbolic execution for Dalvik bytecode[R].CS-TR-5022,Department of Computer Science,University of Maryland,College Park,2012.

[31]Erik RW.Formalization and analysis of Dalvik bytecode[J].Science of Computer Programming-Special Issue on Bytecode,2012,92:25-55.

[32]Nipkow T,Klein G.Concrete Semantics:with Isabelle/HOL[M].Berlin:Springer-Verlag,2015.

[33]Kahn G.Natural semantics[A].Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science[C].London,Britain,1987.22-39.

[34]J Gosling,B Joy,G Steele,G Bracha.The Java Language Specification[M].Addison-Wesley,2005.

[35]Paller G.Dalvik Opcodes[OL]. http://pallergabor.uw.hu/androidblog/dalvik-opcodes.html,2012.

[36]Android Source Code[OL].git://android.git.kernel.org/platform/development/pdk/docs/guide/dalvik.jd.

[37]Ehringer D.The Dalvik Virtual Machine Architecture[OL].http://davidehringer.com/software/android/,2010.

[38]Security Engineering Research Group.Analysis of Dalvik virtual machine and class path library[R].Pakistan:Institute of Management Sciences Peshawar,2009.

[39]何炎祥,江南,李清安,张军,沈凡凡.一个机器检测的Micro-Dalvik 虚拟机模型[J].软件学报,2015,26(2):364-379.

HE Yan-Xiang,JIANG Nan,LI Qing-An,ZHANG Jun,SHEN Fan-Fan.Machine-checked model for micro-Dalvik virtual machine[J].Journal of Software,2015,26(2):364-379.(in Chinese)

[40]Lochbihler A.Verifying a compiler for Java threads[A].Programming Languages and Systems[C].Berlin Heidelberg:Springer,2010.427-447.

[41]M Batty,K Memarian,S Owens,S Sarkar,P Sewell.Clarifying and compiling c/c++ concurrency:from c++11 to POWER[A].Proceedings of the Symposium on Principles of Programming Languages POPL2012[C].USA,2012.509-520.

江南女，1976年4月出生,湖北武汉人.2003年毕业于湖北工学院电子与计算机科学系,获硕士学位,其后留校任教,2009年1月至2009年8月在美国佐治亚理工学院作访问研究,2012开始在武汉大学计算机学院攻读博士学位,从事可信软件、可信编译的研究.

E-mail:nanjiang@whu.edu.cn

何炎祥男,1952年1月出生,湖北应城人.教授、博士生导师.1973年、1986年和1999年分别在武汉大学、美国Oregon大学和武汉大学获学士、硕士和博士学位.现任教于武汉大学计算机学院,主要从事可信软件、分布并行处理和软件工程等方面的研究工作.

Formal Verification ofmJava Compiler Targeting Micro-Dalvik Virtual Machine

JIANG Nan1,3,HE Yan-xiang1,2,ZHANG Xiao-tong1,2

(1.Computer School,Wuhan University,Wuhan,Hubei 430072,China; 2.State Key Laboratory of Software Engineering,Wuhan University,Wuhan,Hubei 430072,China; 3.Computer School,Hubei University of Technology,Wuhan,Hubei 430070,China)

This paper introduces a formal verification ofmJava compiler targeting Micro-Dalvik virtual machine(VM) wheremJava is an object-oriented language similar to Java,and Micro-Dalvik is a Dalvik-like VM of the register-based architecture.The operational semantics ofmJava and Micro-Dalvik VM are defined.The compiler operates in two stages.First it replaces the names of local variables by their corresponding indices and hence translatesmJava into an intermediate language.Then it generates the Micro-Dalvik VM instructions.After defining the operational semantics of the intermediate language,the correctness of the two stages are formulated in terms of the preservation of the semantics and is proved respectively.The whole formalization is machine-checked in the theorem proof assistant Isabelle/HOL.ThemJava language and Micro-Dalvik VM are more abstract than the comparable Java and the Dalvik VM,respectively,which is a result of a compromise between the the realism of the language and the clarity of the formalization.However,mJava language and Micro-Dalvik VM exhibit core features of an object-oriented programming language and a register-based architecture,respectively,and thus in this sense,this verified compiler is non-trivial.

compiler verification;theorem proving;formal semantics;machine-check;register-based architecture;object-oriented

2015-12-01;

2016-03-10;责任编辑:李勇锋

国家自然科学基金(No.61373039)

TP311

A

0372-2112 (2016)07-1619-11

��学报URL:http://www.ejournal.org.cn

10.3969/j.issn.0372-2112.2016.07.015