二進(jìn)制翻譯正確性及優(yōu)化方法的形式化模型

傅立國(guó) 龐建民 王 軍 張家豪 岳 峰

(數(shù)學(xué)工程與先進(jìn)計(jì)算國(guó)家重點(diǎn)實(shí)驗(yàn)室(戰(zhàn)略支援部隊(duì)信息工程大學(xué)) 鄭州 450002)

傳統(tǒng)意義上的二進(jìn)制翻譯是指將源平臺(tái)指令集的指令序列翻譯成其他平臺(tái)指令集的指令序列的過程.隨著虛擬化技術(shù)應(yīng)用的興起，二進(jìn)制翻譯技術(shù)作為跨指令集架構(gòu)虛擬化實(shí)現(xiàn)的核心技術(shù)被廣泛關(guān)注[1].二進(jìn)制翻譯中的動(dòng)態(tài)翻譯方式既能夠在程序運(yùn)行期間動(dòng)態(tài)地解釋代碼片段，也能夠結(jié)合程序運(yùn)行的時(shí)空局部性特征實(shí)現(xiàn)性能調(diào)優(yōu)，亦可以再現(xiàn)程序在源平臺(tái)復(fù)雜的運(yùn)行時(shí)行為，從而成為體系結(jié)構(gòu)設(shè)計(jì)、程序性能優(yōu)化、安全性分析以及軟件移植的研究熱點(diǎn).

為實(shí)現(xiàn)二進(jìn)制程序到其他平臺(tái)的有效移植，需要確保二進(jìn)制翻譯過程的正確性和有效性.正確性要求源平臺(tái)二進(jìn)制程序的邏輯功能在宿主平臺(tái)上被予以等價(jià)的實(shí)現(xiàn)；有效性關(guān)注的是源平臺(tái)代碼在宿主平臺(tái)上運(yùn)行時(shí)的效率.因此，二進(jìn)制翻譯技術(shù)在應(yīng)用研究中的問題總是可以歸結(jié)為翻譯的正確性問題和翻譯的效率問題.

現(xiàn)有相關(guān)問題的研究大多是對(duì)限定翻譯系統(tǒng)工程實(shí)現(xiàn)的探討，局限于具體翻譯系統(tǒng)缺陷的修復(fù).以選定的翻譯器或者翻譯框架為條件，不利于深入研究二進(jìn)制翻譯的正確性和運(yùn)行效率.如用于精確處理中斷、精確處理異常還原的二進(jìn)制翻譯器，則更關(guān)注其翻譯的正確性；而用于軟件無源移植的翻譯器則更關(guān)注其運(yùn)行效率[2-3].

在設(shè)計(jì)二進(jìn)制翻譯器時(shí)，將翻譯過程的正確性和效率作為整體進(jìn)行研究，能夠預(yù)見和避免類似限定框架下存在的種種問題.例如，在新型體系架構(gòu)研發(fā)的研究中，為了解決傳統(tǒng)的通過功能模擬的方法收集典型行為特征速度很慢的問題，使用了動(dòng)態(tài)二進(jìn)制翻譯技術(shù)來加快程序行為分析.然而該方法卻也引入了分析誤差，可見追求翻譯的有效性時(shí)翻譯的正確性會(huì)受到影響[4].因此，翻譯正確性和翻譯效率以及兩者之間關(guān)聯(lián)性的研究對(duì)于二進(jìn)制翻譯系統(tǒng)框架的設(shè)計(jì)具有重要意義，特別是在對(duì)一些優(yōu)化方法的正確性進(jìn)行理論驗(yàn)證的過程中.

在現(xiàn)有的二進(jìn)制翻譯正確性驗(yàn)證相關(guān)的研究中，采用自動(dòng)化形式化的驗(yàn)證方法已經(jīng)比較普遍.如文獻(xiàn)[5]于2011年提出了對(duì)動(dòng)態(tài)翻譯過程中SIMD指令的翻譯進(jìn)行運(yùn)行時(shí)驗(yàn)證的方法；文獻(xiàn)[6]于2015年提出同時(shí)支持動(dòng)態(tài)翻譯和靜態(tài)翻譯的驗(yàn)證方法，卻局限于僅對(duì)部分制定翻譯結(jié)果的驗(yàn)證；文獻(xiàn)[7]于同年提出了使用形式化的方法討論操作數(shù)和操作數(shù)約束的優(yōu)化過程，然而該模型對(duì)于二進(jìn)制優(yōu)化方法的描述不具備通用性.因此為了能夠?qū)Ψg的正確性和優(yōu)化方法的有效性進(jìn)行一致性的研究，本文對(duì)翻譯過程及其優(yōu)化方法構(gòu)建適當(dāng)?shù)男问交Ｐ?

1 基于指令解釋的映射模型

文獻(xiàn)[8]借鑒文獻(xiàn)[9]中可計(jì)算代數(shù)系統(tǒng)中同構(gòu)的性質(zhì)，構(gòu)建了機(jī)器模擬過程和動(dòng)態(tài)二進(jìn)制翻譯過程的形式化模型.該模型將機(jī)器模擬的過程定義為由源機(jī)器狀態(tài)和指令解釋函數(shù)組成的有序?qū)Φ接伤拗鳈C(jī)器狀態(tài)和指令解釋函數(shù)組成的有序?qū)Φ挠成?；繼而在此基礎(chǔ)上，將動(dòng)態(tài)二進(jìn)制翻譯過程歸約為機(jī)器模擬過程的動(dòng)態(tài)優(yōu)化方法，從而描述了動(dòng)態(tài)二進(jìn)制翻譯過程相較于機(jī)器模擬過程所優(yōu)化的對(duì)象和方法.

1.1 機(jī)器模擬的形式化描述

定義1.機(jī)器描述1.機(jī)器為M=(S,I,γ).其中,S表示機(jī)器的狀態(tài)集；I表示機(jī)器的指令集；γ:I×S→S表示機(jī)器指令在指定機(jī)器狀態(tài)下的解釋函數(shù).

當(dāng)指令i∈I作用于狀態(tài)s∈S，其后繼狀態(tài)s′可表示為s′=γ(i,s).

定義2.解釋函數(shù).指令路徑i*=i0,i1,…,im-1∈I*的解釋函數(shù)為γ*:I*×S→S，表示進(jìn)行m次γ的迭代操作，即γ(im-1,…,γ(i2,γ(i1,γ(i0,s0)))…)=γ*(i*,s0).

1.2 機(jī)器模擬的性質(zhì)

Fig. 1 The mapping relation in machine simulation圖1 機(jī)器模擬中的映射關(guān)系

(1)

文獻(xiàn)[8]將動(dòng)態(tài)二進(jìn)制翻譯歸為機(jī)器模擬過程的動(dòng)態(tài)優(yōu)化技術(shù)，指出其實(shí)質(zhì)是源機(jī)器平臺(tái)上執(zhí)行路徑在宿主機(jī)器上的再次編譯，并參照式(1)給出了動(dòng)態(tài)二進(jìn)制翻譯的一般性質(zhì).

1.3 現(xiàn)有模型存在的不足

基于指令解釋的映射模型通過式(1)描述了機(jī)器模擬過程和動(dòng)態(tài)二進(jìn)制翻譯過程的一般性質(zhì).文獻(xiàn)[10]在協(xié)同設(shè)計(jì)虛擬機(jī)的模擬研究中使用文獻(xiàn)[8]中的模型對(duì)模擬過程中的一些性質(zhì)給予了形式化的論證，文獻(xiàn)[5-7]在使用這種描述方法的同時(shí)也暴露了該模型存在的一些不足.

1.3.1 確定的指令路徑

在該模型中，宿主機(jī)器對(duì)源機(jī)器的模擬和翻譯默認(rèn)源機(jī)器執(zhí)行前的初始狀態(tài)以及之后執(zhí)行的指令序列是確定的.而在實(shí)際翻譯過程中，僅加載待翻譯可執(zhí)行文件后的初始狀態(tài)以及機(jī)器指令執(zhí)行行為的相關(guān)解釋是已知的.在無法確定具體指令執(zhí)行路徑時(shí)，便無法通過映射得到宿主機(jī)的指令執(zhí)行路徑.

1.3.2 指令路徑的映射

假設(shè)源機(jī)器執(zhí)行的指令路徑是確定的.通過映射得到宿主機(jī)器的指令路徑，執(zhí)行該指令路徑使得宿主機(jī)器從初始狀態(tài)得到滿足條件的結(jié)束狀態(tài).然而對(duì)于模擬和翻譯過程，具體執(zhí)行的指令路徑只是一個(gè)實(shí)現(xiàn).以指令和固定的指令序列作為映射元素的翻譯方式，破壞了指令序列更高層次等價(jià)翻譯的可能性，這對(duì)于構(gòu)建更高形式優(yōu)化方法的描述是不利的.

1.3.3 指令路徑的執(zhí)行效率

該模型主要用于描述模擬和翻譯過程的正確性.僅使用狀態(tài)映射函數(shù)及其優(yōu)化函數(shù)描述本地指令路徑的執(zhí)行效率，不足以深入討論翻譯方法的優(yōu)化問題.將翻譯過程表示為指令路徑間的映射過于抽象，無法刻畫動(dòng)態(tài)翻譯過程的開銷.該模型的翻譯過程與源機(jī)器具體的指令路徑相關(guān)，優(yōu)化也是基于具體指令路徑的.不同的指令或者指令路徑其指令解釋函數(shù)可能是相同的，然而這些等價(jià)的指令(序列)若按照指令為單位的翻譯方式，其在宿主機(jī)器翻譯得到的指令(序列)之間執(zhí)行開銷的差距可能極其大.翻譯過程的優(yōu)化也包括求解更為有效的本地實(shí)現(xiàn).然而在指令映射的方法不足以描述生成的本地指令路徑的效率.

綜上所述，在分析翻譯效率時(shí)，該模型中的狀態(tài)映射函數(shù)及其優(yōu)化函數(shù)并不能涵蓋翻譯過程中所有重要的因素.能夠?qū)Ψg過程正確性和優(yōu)化方法有效性進(jìn)行分析的形式化模型，需要對(duì)影響翻譯正確性和翻譯效率的所有因素的概念加以定義，然后結(jié)合這些因素對(duì)二進(jìn)制翻譯的正確性和翻譯中優(yōu)化方法的定義和性質(zhì)進(jìn)行討論.

2 二進(jìn)制翻譯過程的抽象及其形式化

二進(jìn)制翻譯過程需要源機(jī)器架構(gòu)特征描述和二進(jìn)制可執(zhí)行文件一同作為輸入.由于宿主機(jī)器只能執(zhí)行本地指令序列，待翻譯的程序在宿主機(jī)器可以有2種存在形式：1)完整的宿主平臺(tái)可執(zhí)行文件；2)需要其他程序配合的零散的指令序列片段.然而不論是以哪種形式，本地存儲(chǔ)的指令序列在執(zhí)行時(shí)都是宿主機(jī)器對(duì)二進(jìn)制程序在源機(jī)器上執(zhí)行過程的模仿.

系統(tǒng)性地討論翻譯過程的正確性和翻譯過程的優(yōu)化，需要對(duì)二進(jìn)制翻譯過程進(jìn)行抽象.對(duì)二進(jìn)制翻譯過程的抽象即對(duì)源機(jī)器程序的執(zhí)行過程以及對(duì)該過程模仿過程的抽象，且兩者在本質(zhì)上都是機(jī)器的指令執(zhí)行過程.所以抽象機(jī)器上指令執(zhí)行的過程是刻畫二進(jìn)制翻譯過程的基礎(chǔ).

2.1 機(jī)器的抽象描述

基于指令解釋的映射模型本質(zhì)上是利用指令的操作語義描述指令執(zhí)行過程中機(jī)器狀態(tài)的變化過程，以算數(shù)表達(dá)式的形式用指令解釋函數(shù)定義了指令執(zhí)行的過程.機(jī)器M=(S,I,γ)從狀態(tài)s∈S執(zhí)行指令i到達(dá)狀態(tài)s′∈S的過程，指令解釋函數(shù)的操作語義可描述為

i,s→s′.

(2)

然而，基于這種描述的指令解釋函數(shù)在描述指令序列的解釋函數(shù)時(shí)，在對(duì)每條指令的解釋函數(shù)進(jìn)行復(fù)合操作的時(shí)候需要明確每條指令的解釋函數(shù)，這需要滿足以下2點(diǎn)：一是指令序列是已知的；二是每條指令的解釋函數(shù)是可表示的.為了弱化指令路徑對(duì)指令迭代執(zhí)行過程描述的限制，需要對(duì)指令執(zhí)行過程進(jìn)一步抽象.

文獻(xiàn)[11]將動(dòng)態(tài)二進(jìn)制翻譯過程概括為查找、翻譯和執(zhí)行3個(gè)過程的迭代.該描述與處理器從存儲(chǔ)器取指、譯指(取值)和執(zhí)行(返值)的執(zhí)行過程相符.因此，指令執(zhí)行的路徑是和機(jī)器狀態(tài)密切相關(guān)的，每個(gè)機(jī)器狀態(tài)的后繼狀態(tài)是通過執(zhí)行從該狀態(tài)中獲得的指令而得到的.因此機(jī)器指令的執(zhí)行過程可以描述為γ(i,s)=γ(f(s),s)=s′.其中f表示從執(zhí)行前的狀態(tài)s獲取指令i的過程.在狀態(tài)解釋函數(shù)γ中，2個(gè)參數(shù)都是狀態(tài)s的函數(shù)，可將其縮略為

γ(s)=s′.

(3)

如此，函數(shù)γ定義了一個(gè)機(jī)器狀態(tài)間的映射關(guān)系，描述了機(jī)器狀態(tài)在指令執(zhí)行中的狀態(tài)遷移過程.這種描述是對(duì)機(jī)器執(zhí)行指令的行為加以抽象，而并非對(duì)具體指令的執(zhí)行效果進(jìn)行描述.此時(shí)γ不再是機(jī)器指令解釋函數(shù)，而是機(jī)器指令執(zhí)行的指稱函數(shù).

使用狀態(tài)轉(zhuǎn)移函數(shù)可以表示任意指令和指令序列的執(zhí)行.根據(jù)指稱語義及其操作語義的一致性[12]，結(jié)合式(2)可將指令i∈I的狀態(tài)轉(zhuǎn)移函數(shù)表述成

γ(i)={(s,s′)|i,s→s′}.

(4)

式(4)中使用函數(shù)γ描述了指令i的指稱語義，稱為指令i的指稱.當(dāng)討論范圍擴(kuò)大為整個(gè)指令集I時(shí)，可以將指令集I的指稱語義以函數(shù)的形式表述為

γ=γ(I)=∪i∈I{(s,s′)|i,s→s′}.

綜合以上分析，對(duì)機(jī)器定義如下：

定義3.機(jī)器描述2.機(jī)器為M=(S,γ).其中，S表示機(jī)器的狀態(tài)集；γ:S→S表示機(jī)器指令集的指稱函數(shù).

指稱函數(shù)γ定義了狀態(tài)集S上的一個(gè)二元關(guān)系，表示指令執(zhí)行前后狀態(tài)的變換關(guān)系，故也可以將其稱作狀態(tài)遷移函數(shù).

2.2 程序執(zhí)行的抽象

重新定義機(jī)器描述后，程序執(zhí)行的過程也可以得到進(jìn)一步的抽象.設(shè)加載完可執(zhí)行文件后的機(jī)器狀態(tài)為s0∈S，程序執(zhí)行的過程可以用機(jī)器指令的迭代執(zhí)行過程表示，而程序執(zhí)行過程狀態(tài)和程序執(zhí)行結(jié)果的求解問題則被歸約為狀態(tài)s0后繼狀態(tài)的求解過程.

狀態(tài)s0及其后續(xù)狀態(tài)可以表述為有序集合{γ0(s0),γ1(s0),γ2(s0),…,γn(s0),…}.s0∈S,n∈N，其中γ0(s0)=s0.為了深入刻畫程序執(zhí)行的性質(zhì)，需要對(duì)該集合中元素間的關(guān)系進(jìn)一步討論.

定義4.狀態(tài)間的二元關(guān)系.在機(jī)器狀態(tài)集合上存在二元關(guān)系≤，對(duì)于狀態(tài)a和狀態(tài)b，如果b∈γ*(a)，記作a≤b.

性質(zhì)1.當(dāng)集合γ*(s0)中不存在2個(gè)相等的元素時(shí)，集合γ*(s0)上的二元關(guān)系≤為全序關(guān)系.

證明.

1) 對(duì)于任意狀態(tài)s=γ0(s)∈γ*(s)，因此有s≤s，自反性可證.

2) 設(shè)有狀態(tài)a和狀態(tài)b使得(a≤b)∧(b≤a).根據(jù)二元關(guān)系≤的定義可知b∈γ*(a)和a∈γ*(b)同時(shí)成立.當(dāng)b∈γ*(a)成立，由函數(shù)γ*的定義，不妨設(shè)b=γi(a),i≥0，帶入前提條件a∈γ*(b)有a∈{γi+0(a),γi+1(a),γi+2(a),…,γi+n(a),…},i≥0，因?yàn)閍=γ0(a)，所以僅當(dāng)i=0時(shí)(a≤b)∧(b≤a)滿足.此時(shí)b=γ0(a)=a，反對(duì)稱性可證.

3) 設(shè)集合γ*(s0)中有狀態(tài)a,b,c滿足a≤b且b≤c，設(shè)a=γi(s0),b=γj(s0),c=γk(s0).i,j,k∈N，根據(jù)二元關(guān)系≤的定義可知，i≤j,j≤k即i≤k，可得a≤c，傳遞性可證.綜上，二元關(guān)系≤為偏序關(guān)系可證.

4) 集合γ*(s0)中的任意元素均存在γi(s0),i≥0的表達(dá)形式，因此任意2個(gè)元素總是可比較的.

證畢.

狀態(tài)遷移函數(shù)定義了指令執(zhí)行前后機(jī)器狀態(tài)的一個(gè)二元關(guān)系.因此程序在機(jī)器上的執(zhí)行過程可以用全序集{γ*(s0),≤}來表示，其中s0為程序加載完后的機(jī)器初始狀態(tài).

2.3 模擬行為的抽象

模擬是二級(jí)制翻譯的核心本質(zhì)，抽象描述程序執(zhí)行過程后，就可以對(duì)模擬的概念加以闡述.

設(shè)源機(jī)器MR=(SR,γR)在初始狀態(tài)s0∈SR執(zhí)行程序p得到狀態(tài)有序集合

2.4 二進(jìn)制翻譯過程的抽象

二進(jìn)制翻譯最終實(shí)現(xiàn)了指令序列到指令序列的映射.根據(jù)宿主機(jī)器對(duì)源機(jī)器上程序模擬執(zhí)行的定義，可以定義二進(jìn)制翻譯：

3 二進(jìn)制翻譯的正確性

翻譯源機(jī)器平臺(tái)上的程序，是為了在宿主機(jī)器平臺(tái)上得到具有相同邏輯功能的程序.因此翻譯得到程序的邏輯功能相同與否決定了翻譯的正確性.然而當(dāng)討論翻譯正確性的時(shí)候，需要先統(tǒng)一描述程序的功能，繼而給出關(guān)于邏輯功能等價(jià)的定義，最終探討正確的二進(jìn)制翻譯過程具有的一般性質(zhì).

3.1 等價(jià)的一般性描述

程序邏輯功能的等價(jià)可以通過相同邏輯功能的正確性證明[13].即通過證明不同程序滿足相同邏輯功能的正確性，從而證明程序間在某種程度上具有等價(jià)性.

證明程序a,b等價(jià)，需要證明對(duì)于任意前置條件P和后置條件Q，{P}a{Q}可證當(dāng)且僅當(dāng){P}b{Q}可證.該描述方法借用了程序功能驗(yàn)證描述的一般形式——霍爾三元組，將程序的功能等價(jià)定義為功能相同.然而此處定義的前置條件和后置條件是不加限制的.因此，當(dāng)討論對(duì)象限制在源機(jī)器和宿主機(jī)器之間的指令序列執(zhí)行其指稱語義的等價(jià)，有效的二進(jìn)制翻譯具有如下性質(zhì).

性質(zhì)2.設(shè)機(jī)器MR到機(jī)器MH的正確翻譯是指對(duì)于MR上任意滿足關(guān)系(p≤q)∧(p≠q)的狀態(tài)p,q，在SH上總存在狀態(tài)滿足關(guān)系(p′≤q′)∧(p′≠q′)的狀態(tài)p′,q′與之相對(duì)應(yīng)，可表示為

trans(MR,MH)?(?p,q∈SR.(p≤q)∧(p≠q)? ?p′,q′∈SH.(p′≤q′)∧(p′≠q′)).

(6)

式(6)中，限制狀態(tài)p,q不相等，因?yàn)閷?duì)于不改變機(jī)器狀態(tài)的指令進(jìn)行翻譯是沒有意義的.性質(zhì)2和式(6)是對(duì)具體程序在不同機(jī)器上翻譯、模擬性質(zhì)的推廣.因而在此不予證明.通過將源機(jī)器和宿主機(jī)器抽象為2個(gè)偏序集合 {SR,≤}和{SH,≤}，翻譯過程和程序模擬執(zhí)行過程被有效區(qū)分，有利于二進(jìn)制翻譯正確性的深入分析.

3.2 狀態(tài)映射函數(shù)的性質(zhì)

在給出二進(jìn)制翻譯正確性的一般性質(zhì)之后，我們需要對(duì)翻譯過程所具有的性質(zhì)進(jìn)行分析.即為了實(shí)現(xiàn)源機(jī)器上程序的模擬執(zhí)行，如何在宿主機(jī)器上構(gòu)建與之相對(duì)應(yīng)的狀態(tài)序列.

性質(zhì)3.態(tài)映射函數(shù)φS是保序映射，單調(diào)且存在反函數(shù).

盡管狀態(tài)映射函數(shù)φS作用的對(duì)象是源機(jī)器的機(jī)器狀態(tài)，然而其本質(zhì)是對(duì)源機(jī)器狀態(tài)集合中的后繼關(guān)系到宿主機(jī)器狀態(tài)集合中的后記關(guān)系的再現(xiàn).

因此，翻譯的正確性體現(xiàn)在狀態(tài)映射函數(shù)φS能否構(gòu)建一個(gè)滿足模擬源機(jī)器程序執(zhí)行的狀態(tài)集在本地的一個(gè)模擬實(shí)現(xiàn).

3.3 狀態(tài)轉(zhuǎn)移函數(shù)的表達(dá)形式

綜合3.2節(jié)所述，映射φS描述了狀態(tài)轉(zhuǎn)移函數(shù)γR和γH執(zhí)行前后狀態(tài)之間的關(guān)系.

根據(jù)式(6)可知，滿足正確性的翻譯過程中所實(shí)現(xiàn)的二元關(guān)系的映射，是從γR到γH的映射，即從已知源平臺(tái)的指令序列到不確定的宿主平臺(tái)指令序列的映射.此時(shí)可以用描述機(jī)器狀態(tài)序列所蘊(yùn)含的指令序列指稱語義的函數(shù)來描述二進(jìn)制翻譯中映射關(guān)系的保持.

狀態(tài)轉(zhuǎn)移函數(shù)γH所描述的前后繼關(guān)系顯然是受γR的描述約束的.根據(jù)緊致性定理，若對(duì)狀態(tài)轉(zhuǎn)移函數(shù)γR作用域中每個(gè)子函數(shù)均有對(duì)應(yīng)的狀態(tài)轉(zhuǎn)移函數(shù)滿足有效翻譯間的映射關(guān)系，那么每個(gè)子函數(shù)映射得到函數(shù)的集合所構(gòu)建得到狀態(tài)轉(zhuǎn)移函數(shù)γH是滿足翻譯的有效性的.

因此，復(fù)雜機(jī)器指令的指稱語義函數(shù)可以使用其子函數(shù)指稱語義函數(shù)集合的形式描述[14].描述翻譯過程需要明確狀態(tài)轉(zhuǎn)移函數(shù)的表示形式.根據(jù)工程實(shí)踐中待翻譯指令的可確定性，本文將狀態(tài)轉(zhuǎn)移函數(shù)的描述劃分為基于子函數(shù)的描述和基于連通圖的描述2種.

3.3.1 基于子函數(shù)的描述

γ={fi(s)},s∈Ai給出了符合機(jī)器指令功能描述的狀態(tài)轉(zhuǎn)移函數(shù)表示形式.根據(jù)狀態(tài)轉(zhuǎn)移過程中所執(zhí)行的指令進(jìn)行分類，將狀態(tài)轉(zhuǎn)移函數(shù)劃分為若干個(gè)描述不同指令功能的子函數(shù).其中，{Ai|i∈I}表示對(duì)狀態(tài)轉(zhuǎn)移函數(shù)γ在狀態(tài)集合S上的1個(gè)劃分.當(dāng)劃分所得的子集數(shù)目有限時(shí)，根據(jù)緊致性定理，如果對(duì)于機(jī)器狀態(tài)集S劃分的每個(gè)子集，狀態(tài)轉(zhuǎn)移函數(shù)γ都有1個(gè)有效的子函數(shù)，那么狀態(tài)轉(zhuǎn)移函數(shù)γ對(duì)于機(jī)器狀態(tài)集S的狀態(tài)轉(zhuǎn)移關(guān)系定義是有效的.

然而這種劃分需要對(duì)作用的狀態(tài)先進(jìn)行關(guān)于定義域劃分的歸類，因此在使用狀態(tài)函數(shù)計(jì)算時(shí)需要先進(jìn)行歸類計(jì)算.

3.3.2 基于連通子圖的描述

使用基于子函數(shù)的描述方式通常能夠較為完備地描述狀態(tài)轉(zhuǎn)移函數(shù).然而當(dāng)研究范圍局限于部分機(jī)器狀態(tài)時(shí)，基于子函數(shù)的描述方式會(huì)構(gòu)建大量冗余的關(guān)系定義.并且當(dāng)需要對(duì)狀態(tài)轉(zhuǎn)移函數(shù)進(jìn)行修改且狀態(tài)后繼關(guān)系不確定的時(shí)候，使用子函數(shù)進(jìn)行描述所定義的狀態(tài)轉(zhuǎn)移函數(shù)更加復(fù)雜.

γ={{[γn(si),γn+1(si)]}},si∈Ai給出了符合特定指令執(zhí)行序列描述的狀態(tài)轉(zhuǎn)移函數(shù)表示形式,其中{[γn(s),γn(s)]},n∈N表示狀態(tài)s及其所有后繼狀態(tài)作為狀態(tài)轉(zhuǎn)移函數(shù)定義集所定義的后繼形成的集合.其現(xiàn)實(shí)意義即每個(gè)初始狀態(tài)對(duì)應(yīng)機(jī)器執(zhí)行過程中一個(gè)特定的執(zhí)行序列.

此時(shí)可以使用有向圖來描述二元后繼關(guān)系.對(duì)滿足(a≤b)∧(a≠b)的機(jī)器狀態(tài)a,b，以a為起點(diǎn)、b為終點(diǎn)作有向圖.因此，當(dāng)給定任意狀態(tài)s時(shí)，求解s所定義狀態(tài)轉(zhuǎn)移圖中所有的連通關(guān)系，通過求解以s為起點(diǎn)，依次求解每個(gè)后繼節(jié)點(diǎn)的后繼，得到1個(gè)后繼關(guān)系圖，該圖是狀態(tài)轉(zhuǎn)移狀態(tài)圖的1個(gè)連通子圖.這種描述則是將機(jī)器狀態(tài)根據(jù)后繼關(guān)系劃分成了若干個(gè)連通子圖.

狀態(tài)轉(zhuǎn)移函數(shù)適合描述待翻譯指令具有不確定性的動(dòng)態(tài)翻譯過程，因?yàn)榇g指令不確定，機(jī)器狀態(tài)序列間的前后繼關(guān)系較為復(fù)雜，使用子函數(shù)能夠較好地描述這種復(fù)雜的前后繼關(guān)系；而在可以靜態(tài)翻譯的程序中，分析得到確定的指令序列片段，因此每個(gè)指令序列執(zhí)行前后機(jī)器狀態(tài)的變化較為簡(jiǎn)單，使用狀態(tài)連同圖描述較為便捷，可以簡(jiǎn)化新構(gòu)建的狀態(tài)轉(zhuǎn)移函數(shù).

3.4 指稱語義等價(jià)狀態(tài)序列的構(gòu)建

Fig. 2 Construction of state transition function based on subfunction description圖2 基于子函數(shù)描述的狀態(tài)轉(zhuǎn)移函數(shù)構(gòu)建

通過這種描述，將狀態(tài)轉(zhuǎn)移函數(shù)γRH的構(gòu)建問題細(xì)化為對(duì)狀態(tài)轉(zhuǎn)移函數(shù)γR中子函數(shù)fRi(s),s∈Ai對(duì)應(yīng)的狀態(tài)轉(zhuǎn)移函數(shù)fRHi(s),s∈φS(Ai)的構(gòu)建.因?yàn)闋顟B(tài)轉(zhuǎn)移函數(shù)γR的作用域SR為有限域，其上的劃分{Ai|i∈I}也是有限的，選擇的劃分方式?jīng)Q定了i的值，從而決定了構(gòu)建狀態(tài)轉(zhuǎn)移函數(shù)γRH的復(fù)雜程度.

這種描述的現(xiàn)實(shí)意義即按照機(jī)器狀態(tài)轉(zhuǎn)移的方式進(jìn)行分類，從而可以對(duì)不同指令的處理過程進(jìn)行分類討論.如果γR是基于連通子圖描述的，γRH的構(gòu)建如圖3所示：

Fig. 3 Construction of state transition function based on connected subgraph description圖3 基于連通子圖描述的狀態(tài)轉(zhuǎn)移函數(shù)構(gòu)建

基于連通子圖描述的狀態(tài)轉(zhuǎn)移函數(shù)構(gòu)建過程如圖3所示.其中,si∈Ai,0

當(dāng)在宿主機(jī)上構(gòu)建具有語義等價(jià)的指稱函數(shù)之后，便可以使用代表宿主機(jī)指令指稱函數(shù)的狀態(tài)轉(zhuǎn)移函數(shù)γH去實(shí)現(xiàn)構(gòu)建的γRH，通過γH實(shí)現(xiàn)γRH所構(gòu)建的狀態(tài)序列若滿足和源機(jī)器序列語義等價(jià)，則滿足翻譯正確性[13].至此，二進(jìn)制翻譯的形式化模型可以描述如圖4所示：

Fig. 4 Formal model of binary translation圖4 二進(jìn)制翻譯的形式化模型

3.5 狀態(tài)轉(zhuǎn)移函數(shù)構(gòu)建的正確性驗(yàn)證

圖4構(gòu)建了二進(jìn)制翻譯統(tǒng)一的形式化模型，然而在工程實(shí)現(xiàn)中，宿主機(jī)器狀態(tài)轉(zhuǎn)移函數(shù)構(gòu)建的正確性驗(yàn)證與翻譯器使用的翻譯方式是相關(guān)的.

動(dòng)態(tài)二進(jìn)制翻譯中代碼發(fā)現(xiàn)過程與翻譯過程是交叉執(zhí)行的，因此可以處理執(zhí)行路徑較為復(fù)雜和不確定的指令序列.處理這種指令序列，使用基于子函數(shù)的形式描述源機(jī)器指令執(zhí)行前后機(jī)器狀態(tài)的變化是較為合適的.如翻譯器QEMU自帶的正確性驗(yàn)證程序test-i386，即通過x86處理器指令的翻譯測(cè)試驗(yàn)證翻譯系統(tǒng)的正確性.

靜態(tài)二進(jìn)制翻譯中代碼發(fā)現(xiàn)過程相對(duì)于翻譯過程是獨(dú)立的，可以構(gòu)建待翻譯程序的執(zhí)行路徑流圖.此時(shí)，使用基于聯(lián)通子圖的狀態(tài)轉(zhuǎn)移函數(shù)描述源機(jī)器上一段確定指令序列的狀態(tài)轉(zhuǎn)移函數(shù)是較為合適的.靜態(tài)二進(jìn)制翻譯通常以指令段為基本單位，在翻譯的過程中結(jié)合語義分析進(jìn)行優(yōu)化，最終翻譯得到的結(jié)果很難使用基于指令翻譯正確性的驗(yàn)證方法去驗(yàn)證翻譯的正確性.因此，靜態(tài)二進(jìn)制翻譯通常以翻譯后指令最終執(zhí)行結(jié)果作為正確性測(cè)試的結(jié)果.常用的測(cè)試集包括nbench，spec2006等.

4 優(yōu)化過程的形式化描述

本節(jié)從狀態(tài)轉(zhuǎn)移函數(shù)不同表述形式的使用、狀態(tài)轉(zhuǎn)移函數(shù)在宿主機(jī)器狀態(tài)序列的實(shí)現(xiàn)以及狀態(tài)轉(zhuǎn)移函數(shù)的修改3個(gè)方面，闡述各種實(shí)現(xiàn)方法對(duì)翻譯得到的狀態(tài)序列效率的影響.

4.1 狀態(tài)轉(zhuǎn)移函數(shù)表述形式對(duì)效率的影響

翻譯后得到的宿主機(jī)狀態(tài)序列，其目標(biāo)后繼狀態(tài)的計(jì)算過程越快，計(jì)算執(zhí)行的速度越好.即生成的指稱函數(shù)γRH在使用基于γH定義的子函數(shù)實(shí)現(xiàn)時(shí)，其實(shí)現(xiàn)的復(fù)雜程度越低越好.狀態(tài)轉(zhuǎn)移函數(shù)γ同時(shí)也是指令序列的指稱函數(shù)，具有2種描述形式.因此后續(xù)狀態(tài)的計(jì)算形式也有2種.

首先給出使用基于子函數(shù)描述的狀態(tài)轉(zhuǎn)移函數(shù)計(jì)算后繼狀態(tài)的計(jì)算過程.

設(shè)γ={fi(s),s∈Ai},0

γi(s)=fm(γi-1(s)),γi-1(s)∈Am.

若將對(duì)當(dāng)前狀態(tài)歸類的過程看作一個(gè)函數(shù)，該函數(shù)以當(dāng)前狀態(tài)為參數(shù)，查詢當(dāng)前狀態(tài)在狀態(tài)轉(zhuǎn)移函數(shù)定義域中所屬的子域，以該子域?qū)?yīng)的子函數(shù)為返回值.設(shè)δ為狀態(tài)歸類函數(shù)，δ(s)=fi,s∈Ai，則基于子函數(shù)表示的狀態(tài)轉(zhuǎn)移函數(shù)γ計(jì)算后繼狀態(tài)γ(s)的計(jì)算過程可表示為

(7)

式(7)中狀態(tài)歸類函數(shù)δ是一個(gè)關(guān)于γi-1(s)的二階函數(shù).該函數(shù)抽象描述了基于子函數(shù)表示的狀態(tài)轉(zhuǎn)移函數(shù)做后繼狀態(tài)計(jì)算的過程，忽略了狀態(tài)轉(zhuǎn)移函數(shù)的表示形式，可以將任意起始狀態(tài)s0的后繼狀態(tài)的計(jì)算遞歸地表示為

用δi=δ(γi-1(s))表示第i次后繼狀態(tài)計(jì)算的狀態(tài)轉(zhuǎn)移函數(shù)，則后繼遞歸計(jì)算遞歸地表示為

此時(shí)狀態(tài)轉(zhuǎn)移函數(shù)定義了由若干狀態(tài)子集劃分的后繼關(guān)系集合γ={δSi,δSj,…}，其中狀態(tài)集合Si,Sj是狀態(tài)全集S的1個(gè)有效劃分中的不同元素.

由此可見，在針對(duì)部分指定狀態(tài)的后繼計(jì)算過程中，使用基于子函數(shù)表示的狀態(tài)轉(zhuǎn)移函數(shù)與使用基于連通子圖表示的狀態(tài)轉(zhuǎn)移函數(shù)具有一致性.

性質(zhì)4.設(shè)有狀態(tài)集合Si，如果其在源機(jī)器狀態(tài)轉(zhuǎn)移函數(shù)中有基于連通子圖的定義，那么，在宿主機(jī)上構(gòu)建狀態(tài)轉(zhuǎn)移函數(shù)時(shí)，針對(duì)狀態(tài)集Si的映射狀態(tài)φS(Si) 構(gòu)建的狀態(tài)轉(zhuǎn)移函數(shù)，基于連通子圖構(gòu)建的狀態(tài)轉(zhuǎn)移函數(shù)效率會(huì)比基于子函數(shù)構(gòu)建的狀態(tài)映射函數(shù)效率高.

性質(zhì)4的證明需要通過分析圖5中使用2種不同狀態(tài)轉(zhuǎn)移函數(shù)計(jì)算后繼狀態(tài)的復(fù)雜程度.

Fig. 5 Subsequent state calculation progress (1)圖5 后繼狀態(tài)計(jì)算過程(1)

在實(shí)際應(yīng)用中，動(dòng)態(tài)翻譯在運(yùn)行時(shí)翻譯和維護(hù)代碼的過程實(shí)現(xiàn)了模擬狀態(tài)轉(zhuǎn)移指令序列的生成，但從功能上并沒有實(shí)現(xiàn)模擬源平臺(tái)狀態(tài)的轉(zhuǎn)移，所以執(zhí)行效率低于靜態(tài)翻譯.與此同時(shí)，也顯示出了靜態(tài)翻譯的局限性，因?yàn)樾枰A(yù)測(cè)源機(jī)器執(zhí)行的狀態(tài)序列.

將指令及其解釋函數(shù)抽象為狀態(tài)轉(zhuǎn)移函數(shù)，能夠?qū)ΧM(jìn)制翻譯過程進(jìn)行更系統(tǒng)的刻畫，主要是可以對(duì)機(jī)器模擬、動(dòng)態(tài)翻譯和靜態(tài)翻譯進(jìn)行統(tǒng)一描述.而這種形式化的統(tǒng)一描述對(duì)于構(gòu)建動(dòng)靜結(jié)合的二進(jìn)制翻譯模式是至關(guān)重要的.

4.2 狀態(tài)轉(zhuǎn)移函數(shù)在宿主機(jī)器狀態(tài)序列的實(shí)現(xiàn)

在二進(jìn)制翻譯模型中，基于偏序集{SH,γH}翻譯得到了偏序集合{φS(SR),γRH}.因此在實(shí)現(xiàn)γRH時(shí)，所使用的狀態(tài)序列是需要滿足γH所定義的后繼關(guān)系限制的.這種限制體現(xiàn)在宿主機(jī)器體系結(jié)構(gòu)特征對(duì)二進(jìn)制翻譯結(jié)果的限制.

這種限制形式化描述為：若γH={f1,f2,…,fn}，那么γRH=f…(…fj(fi(s))…),s∈SH.

現(xiàn)實(shí)中，任何機(jī)器平臺(tái)最終只能執(zhí)行該平臺(tái)所能識(shí)別的指令和操作.基于子函數(shù)描述的狀態(tài)轉(zhuǎn)移函數(shù)γH抽象了宿主機(jī)器的體系架構(gòu)，定義了一系列的功能(指令).由此可見，不同指令序列所對(duì)應(yīng)的狀態(tài)序列會(huì)影響γRH中后繼狀態(tài)計(jì)算的效率.這種影響和具體的機(jī)器架構(gòu)相關(guān)，不做過多討論.這種優(yōu)化方式在應(yīng)用中主要體現(xiàn)為寄存器映射一類的優(yōu)化方法中，將源平臺(tái)上使用頻繁的存儲(chǔ)單元(通常為寄存器)映射到宿主平臺(tái)的寄存器上.因?yàn)槭褂妙l繁，節(jié)省了映射在內(nèi)存中反復(fù)讀寫而占用的時(shí)間[17-18].

4.3 狀態(tài)轉(zhuǎn)移函數(shù)的修改

在二進(jìn)制翻譯中，有時(shí)為了獲取更高的效率，會(huì)忽略宿主機(jī)器翻譯執(zhí)行過程中的部分狀態(tài)是否與源機(jī)器的執(zhí)行狀態(tài)相互對(duì)應(yīng)、而只是關(guān)注在部分關(guān)心的狀態(tài)節(jié)點(diǎn)是否能夠相互對(duì)應(yīng).這種忽略源機(jī)器執(zhí)行序列過程，而只在意部分節(jié)點(diǎn)對(duì)應(yīng)的方法，是在具體問題中對(duì)源機(jī)器所定義的偏序集{SR,γR}進(jìn)行了修改、在刪減部分不關(guān)心的狀態(tài)之后，并使用其前驅(qū)元素和后繼元素構(gòu)建成新的狀態(tài)轉(zhuǎn)移函數(shù)，如此提高后繼狀態(tài)的計(jì)算速度.經(jīng)過這種修改后，在宿主機(jī)器得到的執(zhí)行狀態(tài)序列與源平臺(tái)的狀態(tài)序列其對(duì)應(yīng)關(guān)系不再嚴(yán)格滿足，此時(shí)式(6)中關(guān)于正確性的描述是不成立的.為了使得翻譯中正確性和優(yōu)化帶來的影響能夠有區(qū)別的討論，因此對(duì)二進(jìn)制翻譯的模型修改如圖6所示：

Fig. 6 The quadratic mapping process of binary translation圖6 二進(jìn)制翻譯雙映射過程

4.4 復(fù)合優(yōu)化翻譯模式

刪減狀態(tài)元素有利于降低問題的復(fù)雜程度，忽略一些不關(guān)注的機(jī)器狀態(tài)及其處理過程.在現(xiàn)實(shí)中，根據(jù)用戶的需求和關(guān)注的對(duì)象，如進(jìn)程級(jí)的翻譯系統(tǒng)在操作系統(tǒng)層及其以下做了本地虛擬化的處理，忽略了一些底層實(shí)現(xiàn)的翻譯，而在軟件無源移植的過程中相較于系統(tǒng)級(jí)的翻譯系統(tǒng)具有巨大優(yōu)勢(shì).

然而此類優(yōu)化是基于對(duì)具體問題的求解需求進(jìn)行分析的.處理方法是將不關(guān)心的過程的起始狀態(tài)及其終止?fàn)顟B(tài)進(jìn)行界定，為了保證問題討論的完備性，對(duì)起始狀態(tài)進(jìn)行劃分，劃分的依據(jù)即對(duì)于問題的具體討論，然后根據(jù)專業(yè)知識(shí)構(gòu)建起始狀態(tài)每個(gè)子類到終止?fàn)顟B(tài)的狀態(tài)轉(zhuǎn)移函數(shù).

圖7中使用優(yōu)化后的基于狀態(tài)集與狀態(tài)轉(zhuǎn)移函數(shù)描述了后繼狀態(tài)的計(jì)算過程，使用該方法形成的狀態(tài)轉(zhuǎn)移函數(shù)同時(shí)使用了基于子函數(shù)以及基于同構(gòu)圖2中狀態(tài)轉(zhuǎn)移函數(shù)的表示方法.

Fig. 7 Subsequent state calculation progress (2)圖7 后繼狀態(tài)計(jì)算過程(2)

不同于圖5中逐單條源指令后繼狀態(tài)的變換以及后繼轉(zhuǎn)移函數(shù)的推導(dǎo)，圖7中計(jì)算狀態(tài)Si的子集

在軟件移植的應(yīng)用中，對(duì)應(yīng)用程序的主體采用動(dòng)態(tài)的二進(jìn)制翻譯技術(shù)，對(duì)程序執(zhí)行所依賴的過程函數(shù)，根據(jù)函數(shù)的特性，可以不做任何處理，模仿源平臺(tái)調(diào)用過程的動(dòng)態(tài)翻譯；也可以根據(jù)函數(shù)說明，分析參數(shù)傳遞，做本地函數(shù)封裝調(diào)用的替換處理；也可以對(duì)依賴的自定義庫(kù)函數(shù)進(jìn)行靜態(tài)翻譯成本地庫(kù)函數(shù)，再封裝調(diào)用替換.在上述相關(guān)工作中，特別是庫(kù)函數(shù)的替換處理以及庫(kù)函數(shù)的靜態(tài)翻譯，對(duì)該模型的性質(zhì)進(jìn)行了驗(yàn)證.

5 總 結(jié)

二進(jìn)制翻譯技術(shù)在體系結(jié)構(gòu)優(yōu)化、程序性能優(yōu)化、安全性分析以及軟件移植的研究中具有重要作用.

本文首先分析了基于指令解釋的映射模型在二進(jìn)制翻譯關(guān)于正確性以及翻譯效率研究中的不足，給出了基于后繼關(guān)系的映射模型；繼而定義了正確翻譯并形式化地描述了正確翻譯的過程；最后就翻譯過程匯中翻譯效率的優(yōu)化方法分別進(jìn)行了討論.

在分析翻譯正確性和翻譯優(yōu)化方法的過程中，結(jié)合實(shí)際也對(duì)翻譯正確性的性質(zhì)以及翻譯優(yōu)化方法的效果進(jìn)行了論證.并在最后指出了二進(jìn)制翻譯研究中的熱點(diǎn)以及難點(diǎn)——?jiǎng)屿o結(jié)合的二進(jìn)制翻譯模式.

本文所論述的二進(jìn)制翻譯中的正確性以及優(yōu)化方法的形式化也是該翻譯模式研究的基礎(chǔ).針對(duì)如何通過動(dòng)靜結(jié)合的二進(jìn)制翻譯模式有效提高二進(jìn)制翻譯技術(shù)的實(shí)用性將作為下一步的研究目標(biāo).