江　南,何炎祥,張曉瞳

(1.武漢大學(xué)計(jì)算機(jī)學(xué)院,湖北武漢430072;2.武漢大學(xué)軟件工程國家重點(diǎn)實(shí)驗(yàn)室,湖北武漢430072;3.湖北工業(yè)大學(xué)計(jì)算機(jī)學(xué)院,湖北武漢430070)

mJava到Micro-Dalvik虛擬機(jī)的編譯驗(yàn)證

江南1,3,何炎祥1,2,張曉瞳1,2

(1.武漢大學(xué)計(jì)算機(jī)學(xué)院,湖北武漢430072;2.武漢大學(xué)軟件工程國家重點(diǎn)實(shí)驗(yàn)室,湖北武漢430072;3.湖北工業(yè)大學(xué)計(jì)算機(jī)學(xué)院,湖北武漢430070)

針對類Java的面向?qū)ο笳Z言mJava到類Dalvik的寄存器架構(gòu)虛擬機(jī)Micro-Dalvik的編譯驗(yàn)證,給出了mJava語言和Micro-Dalvik的操作語義.從mJava語言程序到Micro-Dalvik虛擬機(jī)指令的編譯分為兩步,首先將mJava語言程序中的本地變量名轉(zhuǎn)換為相應(yīng)的序號,得到一個(gè)中間語言程序,再將該中間語言程序翻譯成Micro-Dalvik虛擬機(jī)指令程序.在給出中間語言的操作語義后,構(gòu)造了mJava語言程序與編譯后的中間語言程序的語義保持定理并證明,以及構(gòu)造了中間語言程序的語義與編譯后的Micro-Dalvik虛擬機(jī)程序的語義保持定理并證明.整個(gè)形式化編譯驗(yàn)證在定理證明助手Isabelle/HOL中進(jìn)行了機(jī)器檢測.mJava語言和Micro-Dalvik虛擬機(jī)分別對Java語言和Dalvik虛擬機(jī)進(jìn)行了抽象,是我們兼顧語言的真實(shí)性和形式化的清晰性的結(jié)果.但是,所有形式化的語義嚴(yán)格遵從語言規(guī)范中的定義,并與Dalvik VM的實(shí)現(xiàn)保持一致,從這種意義上講,該編譯器并不是一個(gè)實(shí)驗(yàn)性質(zhì)的假想編譯器,而是有其實(shí)用意義的.

編譯驗(yàn)證;定理證明;操作語義;機(jī)器檢測;寄存器架構(gòu);面向?qū)ο笳Z言

1　引言

編譯器是將高級語言編寫的程序轉(zhuǎn)換到能在硬件平臺上運(yùn)行的指令集的重要系統(tǒng)軟件.商用編譯器雖然經(jīng)過大量測試,但仍然存在許多問題,這些問題不斷公布在其缺陷列表的網(wǎng)站上[1～3].編譯器錯誤產(chǎn)生的原因可以歸納為兩點(diǎn),其一是高級語言的語義規(guī)范通常復(fù)雜,且以自然語言書寫,導(dǎo)致編譯器難以理解一些模糊的語義定義,不知道它應(yīng)該將之翻譯為怎樣的機(jī)器指令,只能采取試著運(yùn)行再觀察的態(tài)度(run it and see)[4];其二是編譯器本身作為一個(gè)復(fù)雜的軟件,也可能有錯.這些錯誤對于安全攸關(guān)的軟件系統(tǒng)來說,即使出現(xiàn)概率很小,也可能造成重大的人員傷亡與經(jīng)濟(jì)損失.由于編譯器的不可信,實(shí)踐中,一些控制系統(tǒng)的關(guān)鍵部分不得不采用匯編語言編寫并在匯編級進(jìn)行驗(yàn)證[1].但是,隨著安全攸關(guān)的軟件大小和復(fù)雜度與日俱增,使用匯編語言來開發(fā)這些軟件已不可行[4].因此,迫切需要構(gòu)建一個(gè)經(jīng)過形式化驗(yàn)證的編譯器,這個(gè)證明正確的編譯器能夠保證最后運(yùn)行的機(jī)器程序是無錯的.

為了得到一個(gè)驗(yàn)證的編譯器,McCarthy和Painter進(jìn)行了首次嘗試[5].其源語言是由代表數(shù)值的常量或者變量以及加運(yùn)算所組成的算術(shù)表達(dá)式,目標(biāo)機(jī)器是具有一個(gè)累加寄存器的簡單馮諾依曼機(jī)器[1,5].他們使用抽象語法來定義語義,這種方法成為定義編程語言語義的典范[6],但是他們的方法被認(rèn)為過于泛化[7,8].相對普通程序的驗(yàn)證而言,編譯器可以被更好地結(jié)構(gòu)化,因此,Morris提出使用嚴(yán)格定義的數(shù)學(xué)結(jié)構(gòu)來表達(dá)編譯器正確性問題的本質(zhì)[1].所表達(dá)的驗(yàn)證思想是:編譯器被定義為由源程序到目標(biāo)程序的數(shù)學(xué)函數(shù);語義定義為程序到數(shù)學(xué)值的映射函數(shù),該值可以是非常復(fù)雜的類型;目標(biāo)語義函數(shù)表示的語義代表源語義函數(shù)所表示的語義[7].這種驗(yàn)證思想流行于后來的大多數(shù)編譯器驗(yàn)證研究中[8].

盡管Morris給出了指導(dǎo)性方法,編程語言的語義以及編譯前后兩種語言語義的保持性定義和證明并不容易.研究者們采取不同的語義,對應(yīng)于不同的證明方式,在命令式語言的編譯器驗(yàn)證領(lǐng)域進(jìn)行了深入研究,這些方法可以歸納為兩大類別.

(1) 先定義源語言和目標(biāo)語言的語義,再定義編譯規(guī)則,最后構(gòu)造語義保持定理,證明采用歸納[9～11].代表性成果包括:Stepney基于指稱語義,完成了從一個(gè)假定的編程語言到匯編語言的編譯驗(yàn)證[4];Polak同樣基于指稱語義,驗(yàn)證了一個(gè)Pascal語言子集的編譯器[12];Leroy等人基于操作語義,開發(fā)了CompCert編譯器,其源語言是C語言子集,目標(biāo)語言是PowerPC匯編代碼[13～15];Klein和Nipkow等人驗(yàn)證了一個(gè)稱為Jinja的Java子集到Java虛擬機(jī)(Virtual Machine,VM)字節(jié)碼的編譯器[16,17].

(2) 定義程序轉(zhuǎn)換規(guī)則,源語言程序按照轉(zhuǎn)換規(guī)則被逐步精化為可執(zhí)行的目標(biāo)語言程序.轉(zhuǎn)換規(guī)則即是編譯器行為,規(guī)則的可靠性保證編譯的正確性.這種方法通常采用代數(shù)語義.Hoare、He、以及Sampaio等人使用這種方法將源程序精化為范式,范式和相關(guān)的精化定理可用于針對不同目標(biāo)機(jī)器的編譯器設(shè)計(jì)[18,19].Duran等人將該方法擴(kuò)展到了一種類似Java的面向?qū)ο笳Z言[20].

McCarthy 于1961年也指出,我們應(yīng)該證明程序符合其規(guī)范,而不是測試,并且證明需要經(jīng)過某個(gè)計(jì)算機(jī)程序的檢查.編譯器作為一個(gè)特殊的程序,其規(guī)范與源、目標(biāo)語言的語義直接相關(guān),真實(shí)語言的語義往往龐大而復(fù)雜,譬如Java官方語言規(guī)范有近700頁的描述,JVM規(guī)范有約600頁,這些加大了形義定義的困難性,以及語義保持及證明的復(fù)雜性.定理證明系統(tǒng),如Coq、 Isabelle/HOL、ACL2、PVS等的出現(xiàn)在編譯器驗(yàn)證的實(shí)用性方面起到了關(guān)鍵作用.在定理證明系統(tǒng)的支持下進(jìn)行語義表達(dá)和證明更為高效,經(jīng)過機(jī)器檢測的編譯器具有更高的可靠性和可維護(hù)性[16,21～23].CompCert的整個(gè)開發(fā)工作在定理證明助手Coq中完成,其源語言是一個(gè)C語言子集,包括了能夠運(yùn)用于編程安全攸關(guān)的工業(yè)嵌入式軟件所需要的語法成份,所產(chǎn)生代碼的執(zhí)行性能接近于O1優(yōu)化級GCC[15].

在近半個(gè)世紀(jì)的探索研究之后,過程式語言的編譯驗(yàn)證得到了較好的理解與實(shí)施,出現(xiàn)了象CompCert這個(gè)被廣泛認(rèn)可的C語言的驗(yàn)證編譯器.Eiffel語言設(shè)計(jì)中缺陷的發(fā)現(xiàn)促使編程語言,特別是面向?qū)ο笳Z言的設(shè)計(jì)們致力于證明語言的類型可靠性,導(dǎo)致了Java語言、Java虛擬機(jī)(JVM)、JVM字節(jié)碼驗(yàn)證的形式化得到了廣泛研究[24～28];近幾年來由于Android成為一個(gè)廣泛使用的移動設(shè)備平臺,雖然該平臺上的應(yīng)用程序用Javia編寫,但是被編譯成了Dalvik字節(jié)碼,而不是Java字節(jié)碼,使得已有的Java程序分析工具不能直接使用或者難以使用,而運(yùn)行在這個(gè)平臺上的應(yīng)用程序的安全性和可靠性問題變得越來越重要,因此,Android Dalvik VM程序的靜態(tài)分析以及形式化研究也陸續(xù)展開[29～31].雖然象Java語言、JVM、以及Android Dalvik VM的形式化研究以及JVM字節(jié)碼驗(yàn)證都取得了一定進(jìn)展,然而在支持OO語言所增加的封裝、繼承、方法覆蓋、動態(tài)綁定和多態(tài)等語言特性的編譯驗(yàn)證領(lǐng)域,目前成果并不多見,還有待深入研究.文獻(xiàn)[20]使用代數(shù)的方法構(gòu)造了一個(gè)類Java語言到JVM的編譯器,文獻(xiàn)[24]使用抽象狀態(tài)機(jī)定義了Java語言,并對編譯到Java VM的正確性進(jìn)行了證明,但他們都未經(jīng)過機(jī)器檢測.目前尚未見有針對Dalvik VM的編譯驗(yàn)證.

本文使用定理證明助手Isabelle/HOL[32]形式化驗(yàn)證一個(gè)編譯器,其源語言mJava是一個(gè)較為完善的符合OO特點(diǎn)的順序語言子集,目標(biāo)機(jī)器以典型寄存器架構(gòu)的虛擬機(jī)Android Dalvik VM為參考.

2　mJava的形式化

本文討論的源語言稱為mJava,mJava包括了封裝、繼承、多態(tài)、異常處理,目前暫未考慮線程和數(shù)組.式(1)定義了mJava語言的語法成分,其中,′a是類型變量,因此可以用來同時(shí)表達(dá)mJava程序的語法和編譯時(shí)生成的中間語言程序的語法.本地變量的聲明出現(xiàn)在塊語句中,它是一個(gè)變量名和其類型組成的二元組的列表.

′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取代了類型參數(shù)′a,表示mJava程序的合法語句是式(1)中的15個(gè)表達(dá)式語句;J-mb表示mJava程序的方法體,它是形參變量名列表和J-epr組成的二元組.因此得到mJava程序的定義.

J-prog=J-mb prog

J-mb=vname list×J-epr

J-epr=vname epr

(3)

mJava程序狀態(tài)(state)的完整定義如式(4)所示,它是堆(heap)和本地變量(locals)的二元組;堆是地址(addr)到對象(obj)的映射;地址是自然數(shù)類型nat;對象是類名和其成員變量(fields)的二元組;成員變量和本地變量的區(qū)別是:成員變量的定義中包括了定義該成員變量的類名,因此是其名稱和該類名所組成的的二元組到其值的映射,而本地變量則僅是其名稱到值的映射.值由val定義,可以是空引用值(Null)、布爾值(Bool bool)、整數(shù)值(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)的方式給出,其語義規(guī)則的形式如式(5)所示,表示:執(zhí)行程序P中組成方法體的表達(dá)式e,從初始狀態(tài)(h,l)到達(dá)新的狀態(tài)(h′,l′),e計(jì)算到e′.

P

(5)

方法調(diào)用時(shí)的參數(shù)是表達(dá)式列表,為了對表達(dá)式列表進(jìn)行計(jì)算,擴(kuò)展了式(5)的定義為:如果表達(dá)式列表為空,則狀態(tài)不發(fā)生改變;如果表達(dá)式形如e#es,其中,#是單個(gè)元素e加在列表es的首部,則先計(jì)算單個(gè)表示式e的值,剩余列表再按形如e#es進(jìn)行遞歸計(jì)算,每次計(jì)算的值組成新的值列表.

語義規(guī)則參照J(rèn)ava語言規(guī)范[34].在此給出較為復(fù)雜的方法調(diào)用e.M(ps)在當(dāng)前狀態(tài)s0下的語義計(jì)算規(guī)則,如式(6)所示.

(6)

式(6)表示:當(dāng)對方法調(diào)用語句進(jìn)行計(jì)算時(shí),首先計(jì)算e,得到其值addr a,到達(dá)新的狀態(tài)s1,addr a代表調(diào)用方法的對象的地址;接著,在狀態(tài)s1下,計(jì)算形參表達(dá)式列表,得到形參值列表,并更新狀態(tài)到(h2,l2);如果在堆h2中,地址a代表著一個(gè)對象(C,fs),Ts 是形參計(jì)算得到的值列表所對應(yīng)的類型列表,對于程序P中的類C而言,方法名為M,形參類型列表為Ts的方法是可見的,這個(gè)方法的返值類型是T,方法體是(pns,body),通過seesMethod完成;形參值列表長度與形參名列表長度相等,則為這個(gè)調(diào)用方法建立新的本地變量l2′,在這個(gè)新的映射中,this映射到地址a,形參名列表映射到值列表,其中,加了中括號的映射符號代表兩個(gè)列表的各個(gè)元素按照順序?qū)?yīng)映射;最后,在狀態(tài)(h2,l2′)下,執(zhí)行調(diào)用方法的方法體,得到e′,和新的狀態(tài)(h3,l3).所有這些計(jì)算完成后,方法調(diào)用語句的最終結(jié)果為e′,堆狀態(tài)為h3,但是本地變量恢復(fù)到調(diào)用方法前的本地變量l2.

函數(shù)seesMethod調(diào)用了歸納定義的謂詞seesMethodDef,它的歸納定義如式(7)所示.式(7)獲得一個(gè)映射,即映射方法名和方法參數(shù)列表的二元組到返值和方法體的二元組,因此,根據(jù)給定的(M,Ts),式(8)可以查找到其對應(yīng)的方法m.式(7)的實(shí)現(xiàn)為,由函數(shù)getClassDef獲得指定類名的類定義為(D,fs,ms),如果對象類不是類Object,則按類層次關(guān)系向上查找類中定義的方法列表.函數(shù)map-of中的lambda演算將表示方法的四元組變換成三元組,其中第一個(gè)元素為二元組(mName,Ts),然后map-of函數(shù)中的將元組列表轉(zhuǎn)換成一個(gè)映射,這個(gè)映射與第一個(gè)lambda演算形成函數(shù)組合.父類獲得的映射在++運(yùn)算符的左邊,子類獲得的映射在右邊,如果m1和m2代表兩個(gè)映射,m1++m2運(yùn)算規(guī)則是:如果在映射m2中查找到對應(yīng)在的方法,則結(jié)果為該方法,若沒有找到對應(yīng)的方法,即為None,再在映射m1中查找是否有對應(yīng)的方法.最后的效果為:如果父類和子類具有同名同參數(shù)列表的方法,由于子類中的查找在前,結(jié)果為子類中定義的方法,即子類覆蓋了父類的方法.由于方法查找時(shí),方法名和形參類型同時(shí)作為參數(shù),因此對于同名而不同形參的方法,視為不同的方法,即方法重載.

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)

以上方法覆蓋要求方法名和參數(shù)類型相同,返值類型不大于被覆蓋方法的返值類型,式(9) 給出了這個(gè)定義,它是定義程序well-formedness的一個(gè)重要組成部分.

λ(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的操作語義

目標(biāo)機(jī)器是寄存器架構(gòu)的虛擬機(jī)Micro-Dalvik,參考Android Dalvik[35～38 ].Micro-Dalvik虛擬機(jī)的抽象指令如式(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虛擬機(jī)程序定義如式(11)所示,其中,Micro-Dalvik程序(dvm-prog)的定義是將式(2)中第一行的類型變量′m替換為其方法體(dvm-mb),它是三元組,第一個(gè)分量表示寄存器個(gè)數(shù)(不計(jì)this和實(shí)參的后N個(gè)寄存器),該值在編譯時(shí)確定,第二個(gè)分量是指令列表,最后一個(gè)分量是編譯時(shí)生成的異常表(ex-table).異常表是異常表項(xiàng)(ex-entry)的列表,一個(gè)異常表項(xiàng)由try塊起始指令程序計(jì)數(shù)pc、結(jié)束指令程序計(jì)數(shù)pc、捕獲異常類型cname以及對應(yīng)的catch塊的起始指令程序計(jì)數(shù)pc組成.pc是自然數(shù)類型的別名.

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虛擬機(jī)狀態(tài)dvm-state,它由是否產(chǎn)生異常、堆(heap)、棧楨(frame)列表和方法返回值組成,如果有異常產(chǎn)生,val option的值為異常對象的地址(Addr a),否則其值為None.棧楨由捕獲的異常、寄存器中存放的值的列表、方法所在的類名、方法名、形參列表以及程序計(jì)數(shù)組成,如果捕獲到異常,xcptval的值為異常對象的地址.堆(heap)的定義與源語言mJava相同,如式(4)所示.

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

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

(12)

Micro-Dalvik虛擬機(jī)程序的操作語義與源mJava程序大步操作語義的定義方式不同,它先定義函數(shù)run,通過調(diào)用函數(shù)run-instr給出了單步執(zhí)行的狀態(tài)轉(zhuǎn)換,如式(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)

使用上述函數(shù)式的定義,關(guān)系方式的語義定義runRel實(shí)現(xiàn)為狀態(tài)轉(zhuǎn)換的集合,因此,程序的執(zhí)行runProg由任意有限步的單步執(zhí)行組成,為了方便表示,將Micro-Dalvik虛擬機(jī)程序的語義定義runProg P σ σ′寫為如式(14)的形式,它表示在初始虛擬機(jī)狀態(tài)σ下執(zhí)行程序P,到達(dá)新的狀態(tài)σ′.

Pσ′

(14)

狀態(tài)轉(zhuǎn)換函數(shù)run-instr以及詳細(xì)闡述可詳見文獻(xiàn)[39].

4　編譯及證明

4.1mJava到Micro-Dalvik VM的編譯

4.1.1mJava程序的編譯方法

在不考慮優(yōu)化的情況下,mJava源程序J-prog到Micro-Dalvik VM目標(biāo)程序dvm-prog的翻譯是將組成源程序方法體的抽象表達(dá)式J-epr中的每一個(gè)構(gòu)造器所構(gòu)造的語句翻譯成一條或多條目標(biāo)機(jī)器指令,即instr定義的指令.由于源程序中的本地變量名不再出現(xiàn)在機(jī)器指令中,這些值按照其聲明的順序存儲在一片連續(xù)的寄存器中,為避免一遍翻譯及證明的復(fù)雜,定義一個(gè)中間語言Ji-prog,如式(15)所示.

Ji-prog=Ji-mb prog

Ji-mb=nat ×Ji-epr

Ji-epr=nat epr

(15)

其中,Ji-epr用 nat取代了式(1)中的類型變量′a,即中間語言程序中的語句中不再出現(xiàn)方法本量名,而是方法變量名對應(yīng)的序號.Ji-mb中的 nat是方法形參個(gè)數(shù)(不包括this),將用于指定代碼生成時(shí)可用的寄存器序號.因此,將式(2)中第一行的類型變量′m用Ji-mb替換后,得到中間語言程序的定義Ji-prog.

編譯分為兩步,第一步是中間代碼生成,用于消除本地變量名,將J-prog翻譯成Ji-Prog,由cEpr1完成;第二步是代碼生成,將Ji-prog翻譯成dvm-prog,由cEpr2和cEprex2共同完成.我們將在下一小節(jié)4.1.2以及4.1.3中分別予以討論.

對方法進(jìn)行編譯的函數(shù)如式(16)所示,表示:給定的一個(gè)方法(M,Ts,T,m)和一個(gè)編譯函數(shù)f,編譯后的結(jié)果為(M,Ts,T,f m).

cMethod f≡

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

(16)

對應(yīng)于源程序方法體J-mb和中間語言程序方法體Ji-mb,相應(yīng)的f函數(shù)都是lambda運(yùn)算,分別如式(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)

其中,函數(shù)maxLocals歸納計(jì)算出方法體中嵌套變量的最大深度,因此,idx是起始可用的寄存器序號,式(19)給出了塊語名和捕獲異常語句的計(jì)算規(guī)則.函數(shù)maxWS歸納得到所需要的最大計(jì)算空間,式(20)給出了創(chuàng)建對象、變量訪問、條件以及方法調(diào)用的計(jì)算規(guī)則.

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)

函數(shù)genMoveps生成Move指令,將實(shí)參值順序放到序號從0開始的寄存器中,如式(21)所示.

genMoveps 0regs=[]

genMoveps (Suc m) regs=

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

(21)

主體編譯函數(shù)如式(22)所示,使用運(yùn)算°組合兩步編譯函數(shù),完成從mJava程序到Micro-Dalvik虛擬機(jī)程序的編譯.

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生成

為了得到本地變量聲明序號,需要知道當(dāng)前本地變量環(huán)境,參數(shù)Vars::vname list代表這個(gè)環(huán)境,初始本地變量環(huán)境為this和方法形參名,在式(17)給出.

由mJava源程序到中間語言程序的轉(zhuǎn)換由函數(shù)cEpr1完成,在給定當(dāng)前變量環(huán)境下,計(jì)算表達(dá)式中出現(xiàn)的變量名的序號.因此,除了本地變量名被轉(zhuǎn)換成了其對應(yīng)的序號外,其余與源程序相同.式(23)給出了編譯塊表達(dá)式語句的方法,其他表達(dá)式的語句的編譯較為直接,不再贅述.

cEpr1Vars {vts;e}={

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

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

(23)

4.1.3目標(biāo)Micro-Dalvik虛擬機(jī)代碼生成

目標(biāo)代碼的生成包括虛擬機(jī)指令的生成cEpr2和異常表項(xiàng)的生成cEprex2.由于Dalvik這種寄存器架構(gòu)的虛擬機(jī)沒有操作數(shù)棧,它使用了額外的指令,即MoveResult指令存放方法的返回值,以及使用MoveException指令存放捕獲到的異常對象.因此,編譯時(shí),方法調(diào)用指令之后緊跟一條MoveResult指令.在編譯異常處理塊時(shí),首先添加一條MoveException指令.

針對每一個(gè)Ji表達(dá)式語句,指令生成方法是直接的.式(24)給出了異常捕獲語句的指令生成方法,其中參數(shù)idx表示編譯時(shí)可用的第一個(gè)寄存器序號,初始序號為方法形參個(gè)數(shù)+1(this)與方法本地變量個(gè)數(shù)的和.

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)

由于異常表項(xiàng)中的程序指令計(jì)數(shù)是絕對程序指令計(jì)數(shù),而不是如跳轉(zhuǎn)指令中的相對偏移量,所以異常表項(xiàng)生成函數(shù)cEprex2包括了一個(gè)參數(shù),代表當(dāng)前的程序指令計(jì)數(shù),針對異常捕獲語句的異常表項(xiàng)生成如式(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é)中定義的中間語言程序Ji-prog,我們還未定義其語義,因此,在本節(jié)先給出它的大步操作語義;再構(gòu)造J-prog和和編譯后的Ji-prog語義保持定理并證明,以及Ji-prog和編譯后的dvm-prog語義保持定理并證明,最后由這兩步的語義保持,證明J-prog到dvm-prog程序的編譯的正確性.

4.2.1Ji-prog的大步操作語義

與源程序J-prog的狀態(tài)比較,中間語言程序Ji-prog由于消除了變量名,狀態(tài)表示中,本地變量不再是變量名到其值的映射函數(shù),而是一系列值,如式(26)所示.

state1=heap×(val list)

(26)

Ji-prog的大步操作語義的計(jì)算規(guī)則與J-prog的大步操作語義規(guī)則基本相同.式(27)給出它的方法調(diào)用的語義規(guī)則.

(27)

4.2.2J-prog到Ji-prog的編譯正確性

定理1

定理1表示:若mJava程序是良構(gòu)的(well-formed),編譯前J-Prog的狀態(tài)與編譯后的Ji-prog的狀態(tài)保持.

程序P是良構(gòu)的,除式(7)描述的以外,完整的良構(gòu)性條件描述為:程序P中定義的所有類是良構(gòu)的,且類名不重復(fù).一個(gè)類C是良構(gòu)的,當(dāng)且僅當(dāng)C中定義的成員變量名不重復(fù);成員變量的類型是P中合法類型;沒有同名且同參數(shù)的方法;所有方法體是良構(gòu)的;若C不是根類Object,如果C的父類是D,則D不可能是C的子類,即不存在父子類的循環(huán)定義;若子類方法覆蓋父類方法,子類方法的返值類型不大于父類型,如式(7)所示.一個(gè)方法體是良構(gòu)的,當(dāng)且僅當(dāng)形參名列表的長度與方法形參類型列表長度相同;形參名沒有重復(fù);this不出現(xiàn)在形參名列表中;不存在嵌套塊中變量重復(fù)聲明;不會出現(xiàn)未聲明變量的使用.

按照J(rèn)-Prog到Ji-prog的翻譯:J-prog中的本地變量名轉(zhuǎn)換為對應(yīng)的序號,如果J-prog的狀態(tài)由(h,l)轉(zhuǎn)換到(h′,l′),Ji-prog的狀態(tài)中堆也轉(zhuǎn)換到h′,設(shè)本地變量狀態(tài)轉(zhuǎn)換到ls′,則l′和ls′之間的保持關(guān)系為:對于所有在映射l′已賦值的變量(l′ V的值不等于None,表示為?a∈dom l′),其值與ls′中對應(yīng)的值相同,當(dāng)然,需要滿足的前提是J-prog和Ji-prog程序執(zhí)行前的狀態(tài)l和ls之間也需要滿足這個(gè)關(guān)系;同時(shí),函數(shù)fv保證J-prog程序中出現(xiàn)的變量名都是方法體中聲明的變量、this或者方法的形參;ls′的大小不小于計(jì)算e時(shí)所需的本地變量個(gè)數(shù);沒有嵌套塊中變量的重復(fù)聲明.函數(shù)fin1表示fin1(Val v)=val v,fin1(ThrowEx a)=ThrowEx a.

又J-prog的try-catch的語義定義為:

聯(lián)合IH1和IH2,滿足J-prog的try-catch的語義規(guī)則的前提,于是有:

又J-prog程序try-catch的編譯規(guī)則為:

而Ji-prog的try-catch語義規(guī)則前提為:

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

因此,結(jié)合IH2,ls2即是待要證明存在的本地變量列表,即?ls2使得:

cPrg1P1[cEpr1Vars e,(h,ls)]

其中,l2(V:=l1V)是計(jì)算e之后的本地變量狀態(tài).

證畢.

4.2.3Ji-prog到dvm-prog的編譯正確性

定理2

定理2表示:給定程序Ji-Prog,其類C具有可執(zhí)行的方法M,即(M,Ts,T,(n,body)),在狀態(tài)(h,ls)下執(zhí)行其方法體body,到達(dá)新的狀態(tài)(h′,ls′);等價(jià)于在機(jī)器狀態(tài)(None,h,[(Unit,ls,C,M,ts,0)],Unit)下執(zhí)行編譯后的程序cPrg2P1,,則執(zhí)行后的機(jī)器狀態(tài)中,堆也應(yīng)該是h′,程序執(zhí)行完畢,楨棧為空.exception e′為None或某個(gè)產(chǎn)生的異常對象地址.

定理2直觀地表達(dá)了編譯前后的語義保持性,但是其表達(dá)的是方法體內(nèi)所有語句全部執(zhí)行完畢后的語義,不能進(jìn)行歸納證明.因此,代替方法體全部執(zhí)行完畢來表示語義,而是給定正在執(zhí)行的指令計(jì)數(shù),并按照J(rèn)i-Prog執(zhí)行其表達(dá)式的結(jié)果是正常值還是拋出異常兩方面分別構(gòu)造語義保持,從而構(gòu)造定理3,如下所示.

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

C,M,ts,pc1)# frs retv)))其中:P,C,M,ts,pc?cEpr2idx e 表示當(dāng)前棧楨的指針不會超出被編譯表達(dá)式所對應(yīng)的指令, pc指向表達(dá)式e編譯后對應(yīng)的第一條指令.

證明在計(jì)算規(guī)則

令e=try e1catch(C i)e2,

定理的前提條件之一e的語義定義為:

上式表明:如果執(zhí)行e1時(shí)系統(tǒng)拋出了異常,狀態(tài)轉(zhuǎn)換為(h1,ls1);該異常能夠被捕獲,即異常類型是捕獲異常類型的子類型,并且變量的索引號不超出本地變量最大索引號;在對ls1進(jìn)行更新,即(h1,ls1[i:=Addr a])狀態(tài)下執(zhí)行e2,計(jì)算得到e2′,到達(dá)狀態(tài)(h2,ls2);則執(zhí)行e后得到e2′,到達(dá)狀態(tài)為(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)],

根據(jù)歸納假定得到:?pc1,使得:

由于此處考慮的是捕獲到異常的語義,lookupHandler函數(shù)返回一個(gè)機(jī)器狀態(tài),于是有:

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

于是有:P,C,M,pc1′?cEpr2idx e2.令σ1表示狀態(tài):

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

因此,由

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

根據(jù)歸納假定得到:

如果e2′=Val v,則有:

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

又由try..catch的編譯規(guī)則:

又因?yàn)?

pc1′≤ pc2,pc2

所以有:pc≤pc2,pc2

因此,由機(jī)器狀態(tài)轉(zhuǎn)換的傳遞性,得到待證目標(biāo):假定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的前提應(yīng)用到已經(jīng)得到證明的定理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)

聯(lián)合定理2的另一前提:

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

應(yīng)用到定理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īng)證明了編譯J-prog到Ji-prog以及編譯Ji-prog到dvm-prog的正確性,因此,J-prog到dvm-prog的編譯正確性定理可以構(gòu)造為:

定理4

組合定理1和定理2,即由源程序到中間程序的翻譯正確性,以及中間程序到目標(biāo)程序的正確性都得到證明后,源程序到目標(biāo)程序的正確性即建立.

整個(gè)編譯證明的重點(diǎn)在定理3的歸納證明上,它包括42個(gè)case分析,異常捕獲是最為復(fù)雜、因此最具有代表性的證明case之一,我們給出了其證明過程,其他case的證明方法類似,在此不作詳述.

5　結(jié)論和下一步研究

本文在定理證明助手Isabelle/HOL的支持下,設(shè)計(jì)并實(shí)現(xiàn)了一個(gè)機(jī)器驗(yàn)證的編譯器,源語言是類Java的面向?qū)ο笳Z言mJava,目標(biāo)機(jī)器是類Dalvik的寄存器架構(gòu)虛擬機(jī)Micro-Dalvik.式(1)所定義的的子集考慮到了一個(gè)Java程序的核心特性,包括類的定義(實(shí)例變量和實(shí)例方法),對象創(chuàng)建、繼承關(guān)系、方法覆蓋、靜態(tài)重載、簡單類型和引用類型以及異常拋出和捕獲機(jī)制.從這種意義上講,它不是一個(gè)假想的語言和目標(biāo)機(jī)器,具有較大實(shí)用性.未被考慮的包機(jī)制和訪問權(quán)限、數(shù)組和線程、構(gòu)造方法、類變量和類方法以及finally語句和finalize方法等將在本文基礎(chǔ)上進(jìn)行擴(kuò)展,譬如給式(2)中的類名cname加上包名,形成限定名來建模包的概念,可以增加一個(gè)類型來描述Java語言規(guī)范中定義的四種訪問權(quán)限,加入到類聲明和方法聲明的定義中,因此式(2)中的′m cdecl由二元組將變成三元組,′m mdecl由三元組將變成四元組,這些改變將導(dǎo)致成員變量和成員方法查找的重新定義.

需要指出的是,我們形式化的是順序OO語言,并未對并發(fā)特性進(jìn)行編譯驗(yàn)證.關(guān)于并發(fā)特性的OO語言編譯驗(yàn)證,文獻(xiàn)[40]在文獻(xiàn)[16]的基礎(chǔ)上進(jìn)行了針對Java線程的討論.文獻(xiàn)[41]給出了一個(gè)針對C/C++并發(fā)特性的編譯證明,這個(gè)編譯證明相當(dāng)抽象;同時(shí),作者也指出:距離完整的C++正確性證明仍然還很漫長,未來他們考慮得到一個(gè)具體的操作語義以及編譯C++代碼片段.這些工作對我們將支持并發(fā)的Java編譯到Dalvik VM有一定的借鑒意義.本文未包括的另一個(gè)語言特性是數(shù)組.考慮到Java在運(yùn)行時(shí)動態(tài)創(chuàng)建數(shù)組,并在運(yùn)行時(shí)對數(shù)組賦值進(jìn)行類型檢查,我們擬在本文的基礎(chǔ)上,證明該編譯器也保持了類型的可靠性,圍繞類型系統(tǒng),再去完整地分析數(shù)組問題.

因此,下一步我們將進(jìn)一步解決完善這個(gè)編譯器能夠支持的語法特性,并對目標(biāo)虛擬機(jī)Micro-Dalvik類型系統(tǒng)的可靠性進(jìn)行研究和證明.

[1]何炎祥,吳偉.可信編譯理論與關(guān)鍵技術(shù)[M]. 北京:科學(xué)出版社,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]何炎祥,吳偉,劉陶,李清安,陳勇,胡明昊,劉健博,石謙.可信編譯理論及其核心實(shí)現(xiàn)技術(shù):研究綜述[J].計(jì)算機(jī)科學(xué)與探索,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]何炎祥,江南,李清安,張軍,沈凡凡.一個(gè)機(jī)器檢測的Micro-Dalvik 虛擬機(jī)模型[J].軟件學(xué)報(bào),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年畢業(yè)于湖北工學(xué)院電子與計(jì)算機(jī)科學(xué)系,獲碩士學(xué)位,其后留校任教,2009年1月至2009年8月在美國佐治亞理工學(xué)院作訪問研究,2012開始在武漢大學(xué)計(jì)算機(jī)學(xué)院攻讀博士學(xué)位,從事可信軟件、可信編譯的研究.

E-mail:nanjiang@whu.edu.cn

何炎祥男,1952年1月出生,湖北應(yīng)城人.教授、博士生導(dǎo)師.1973年、1986年和1999年分別在武漢大學(xué)、美國Oregon大學(xué)和武漢大學(xué)獲學(xué)士、碩士和博士學(xué)位.現(xiàn)任教于武漢大學(xué)計(jì)算機(jī)學(xué)院,主要從事可信軟件、分布并行處理和軟件工程等方面的研究工作.

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;責(zé)任編輯:李勇鋒

國家自然科學(xué)基金(No.61373039)

TP311

A

0372-2112 (2016)07-1619-11

??學(xué)報(bào)URL:http://www.ejournal.org.cn

10.3969/j.issn.0372-2112.2016.07.015