傅立國 龐建民 王 軍 張家豪 岳 峰

(數(shù)學工程與先進計算國家重點實驗室(戰(zhàn)略支援部隊信息工程大學) 鄭州 450002)

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

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

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

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

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

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

文獻[8]借鑒文獻[9]中可計算代數(shù)系統(tǒng)中同構的性質，構建了機器模擬過程和動態(tài)二進制翻譯過程的形式化模型.該模型將機器模擬的過程定義為由源機器狀態(tài)和指令解釋函數(shù)組成的有序對到由宿主機器狀態(tài)和指令解釋函數(shù)組成的有序對的映射；繼而在此基礎上，將動態(tài)二進制翻譯過程歸約為機器模擬過程的動態(tài)優(yōu)化方法，從而描述了動態(tài)二進制翻譯過程相較于機器模擬過程所優(yōu)化的對象和方法.

1.1 機器模擬的形式化描述

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

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

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

1.2 機器模擬的性質

Fig. 1 The mapping relation in machine simulation圖1 機器模擬中的映射關系

(1)

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

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

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

1.3.1 確定的指令路徑

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

1.3.2 指令路徑的映射

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

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

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

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

2 二進制翻譯過程的抽象及其形式化

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

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

2.1 機器的抽象描述

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

i,s→s′.

(2)

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

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

γ(s)=s′.

(3)

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

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

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

(4)

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

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

綜合以上分析，對機器定義如下：

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

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

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

重新定義機器描述后，程序執(zhí)行的過程也可以得到進一步的抽象.設加載完可執(zhí)行文件后的機器狀態(tài)為s0∈S，程序執(zhí)行的過程可以用機器指令的迭代執(zhí)行過程表示，而程序執(zhí)行過程狀態(tài)和程序執(zhí)行結果的求解問題則被歸約為狀態(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í)行的性質，需要對該集合中元素間的關系進一步討論.

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

性質1.當集合γ*(s0)中不存在2個相等的元素時，集合γ*(s0)上的二元關系≤為全序關系.

證明.

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

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

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

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

證畢.

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

2.3 模擬行為的抽象

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

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

2.4 二進制翻譯過程的抽象

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

3 二進制翻譯的正確性

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

3.1 等價的一般性描述

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

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

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

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

(6)

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

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

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

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

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

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

3.3 狀態(tài)轉移函數(shù)的表達形式

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

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

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

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

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

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

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

3.3.2 基于連通子圖的描述

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

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

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

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

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

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

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

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

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

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

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

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

3.5 狀態(tài)轉移函數(shù)構建的正確性驗證

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

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

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

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

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

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

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

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

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

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

若將對當前狀態(tài)歸類的過程看作一個函數(shù)，該函數(shù)以當前狀態(tài)為參數(shù)，查詢當前狀態(tài)在狀態(tài)轉移函數(shù)定義域中所屬的子域，以該子域對應的子函數(shù)為返回值.設δ為狀態(tài)歸類函數(shù)，δ(s)=fi,s∈Ai，則基于子函數(shù)表示的狀態(tài)轉移函數(shù)γ計算后繼狀態(tài)γ(s)的計算過程可表示為

(7)

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

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

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

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

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

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

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

在實際應用中，動態(tài)翻譯在運行時翻譯和維護代碼的過程實現(xiàn)了模擬狀態(tài)轉移指令序列的生成，但從功能上并沒有實現(xiàn)模擬源平臺狀態(tài)的轉移，所以執(zhí)行效率低于靜態(tài)翻譯.與此同時，也顯示出了靜態(tài)翻譯的局限性，因為需要預測源機器執(zhí)行的狀態(tài)序列.

將指令及其解釋函數(shù)抽象為狀態(tài)轉移函數(shù)，能夠對二進制翻譯過程進行更系統(tǒng)的刻畫，主要是可以對機器模擬、動態(tài)翻譯和靜態(tài)翻譯進行統(tǒng)一描述.而這種形式化的統(tǒng)一描述對于構建動靜結合的二進制翻譯模式是至關重要的.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

5 總 結

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

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

在分析翻譯正確性和翻譯優(yōu)化方法的過程中，結合實際也對翻譯正確性的性質以及翻譯優(yōu)化方法的效果進行了論證.并在最后指出了二進制翻譯研究中的熱點以及難點——動靜結合的二進制翻譯模式.

本文所論述的二進制翻譯中的正確性以及優(yōu)化方法的形式化也是該翻譯模式研究的基礎.針對如何通過動靜結合的二進制翻譯模式有效提高二進制翻譯技術的實用性將作為下一步的研究目標.