一種基于執(zhí)行路徑狀態(tài)比對的科學(xué)計算程序等效性判定方法?

曲海鵬， 張敏媛， 韓慶迪， 林喜軍

(中國海洋大學(xué)信息科學(xué)與工程學(xué)院， 山東 青島 266100)

科學(xué)計算程序通常使用Fortran和C/C++編寫。其中，F(xiàn)ortran是科學(xué)計算的特定領(lǐng)域語言，廣泛用于氣候科學(xué)，天氣預(yù)報，化學(xué)循環(huán)反應(yīng)器，等離子物理等領(lǐng)域[1]，在科學(xué)計算程序中占有很高的比例。在20世紀(jì)中后期，幾乎所有科學(xué)計算代碼都用Fortran實(shí)現(xiàn)。與其他語言相比，F(xiàn)ortran的語言特點(diǎn)使其更適用于科學(xué)計算，F(xiàn)ortran在數(shù)值計算中的性能優(yōu)于C ++，這也是Fortran被廣泛用于科學(xué)計算的原因。迄今，科學(xué)計算領(lǐng)域已經(jīng)積累了許多高度優(yōu)化的數(shù)值計算代碼，這些程序隨著計算方法的改進(jìn)和計算架構(gòu)的更新，需要不斷進(jìn)行算法改進(jìn)、程序優(yōu)化、架構(gòu)遷移、版本迭代等維護(hù)和更新活動。但是，作為一種面向過程的編程語言，F(xiàn)ortran的后續(xù)維護(hù)比較困難，維護(hù)周期甚至?xí)^開發(fā)新代碼的周期，這導(dǎo)致了Fortran代碼維護(hù)和更新是一項(xiàng)艱巨的任務(wù)。而對修改前后的代碼能否進(jìn)行可靠完備的自動化等效性判定，則是阻礙Fortran代碼維護(hù)和更新的主要困難之一。

對于程序的等效性判定問題，研究者主要在編譯器正確性檢查、軟件偽造鑒定以及回歸驗(yàn)證等多個領(lǐng)域進(jìn)行了研究，并開發(fā)了一些工具。但這些工具多是針對特定用途的代碼等效性檢測，對Fortran程序的研究成果更為少見，因此難以直接用于科學(xué)計算程序的等效性判定。目前常用的基于用例測試的判定方法，因其無法覆蓋所有程序分支和全部輸入條件，判定結(jié)果不具有完備性。而基于人工審查的代碼等效性檢查缺乏嚴(yán)格性，在大規(guī)模程序檢查中由于復(fù)雜度增大更缺乏可行性。

近年來，隨著C/C ++使用范圍的擴(kuò)大及其在操作系統(tǒng)功能調(diào)用和底層硬件操作等方面的優(yōu)勢，經(jīng)常需要在C/C++和Fortran程序之間進(jìn)行函數(shù)調(diào)用操作。在大規(guī)模代碼的開發(fā)過程中，混合調(diào)用會降低程序的性能，混合調(diào)用還因其編譯、鏈接的環(huán)境依賴性顯著降低代碼的可移植性。因此，研究者將一些Fortran科學(xué)計算程序向C/C++進(jìn)行轉(zhuǎn)換，轉(zhuǎn)換通常由程序員人工完成，并借助于目前已存在的一些自動轉(zhuǎn)換工具，如F2C[2]，F(xiàn)2CPP，F(xiàn)ABLE[3]等，但這些轉(zhuǎn)換工具存在較大局限性，實(shí)際應(yīng)用并不廣泛。無論是人工轉(zhuǎn)換還是自動轉(zhuǎn)換，轉(zhuǎn)換前后的程序都需要進(jìn)行等效性判定，而對于Fortran到C/C++的等效性判定問題，目前更是缺乏實(shí)用的技術(shù)和工具。

前人已提出的等效性判定方法主要應(yīng)用于編譯器正確性檢查等場景，通常建立在待比較的程序控制流高度相似的前提下，但在科學(xué)計算程序的版本更新和語言轉(zhuǎn)換中，待比較程序通常具有控制流不具備高度相似性的特點(diǎn)。本文面向這一問題，研究控制流相似性較低前提下的等效性判別問題，主要解決以下三個方面的挑戰(zhàn)：被比較的兩個分支條件的約束可能在形式上有所不同，并且在大多數(shù)情況下，無法通過SMT(Satisfiability Modulo Theories)約束求解器獲取所有可滿足的解，這為匹配相同的路徑帶來了難度。在本文中，利用兩條路徑的約束表達(dá)式構(gòu)造出新的約束表達(dá)式，然后根據(jù)求解器對新約束的求解結(jié)果確定路徑是否匹配；程序中的迭代為路徑匹配帶來了難度，當(dāng)?shù)拇螖?shù)與程序輸入相關(guān)時，程序中的路徑條數(shù)也無法確定。本文采用添加“循環(huán)上限”的方法來處理這個問題；程序調(diào)用也是等效性判定過程中的困難問題。當(dāng)被調(diào)函數(shù)的源碼已知時，使用本文的SCEP方法能夠進(jìn)行等效性驗(yàn)證，而當(dāng)程序包含源碼未知的庫函數(shù)調(diào)用時，此種情況下的等效性判別問題尚待解決。

本文的創(chuàng)新點(diǎn)包括：提出基于執(zhí)行路徑狀態(tài)比對的等價性驗(yàn)證方法，對科學(xué)計算程序進(jìn)行自動化的語義等價性驗(yàn)證；采用Matching-Constraint求解的方式進(jìn)行執(zhí)行路徑條件約束的等價性判定；基于Horn范式約束求解進(jìn)行執(zhí)行路徑的狀態(tài)等價性判別。

1 相關(guān)研究

程序等效性檢查在代碼轉(zhuǎn)換驗(yàn)證[4-7]、軟件剽竊檢測[8-15]以及回歸驗(yàn)證[16-19]等領(lǐng)域具有廣泛的應(yīng)用。代碼轉(zhuǎn)換驗(yàn)證是證明源碼和轉(zhuǎn)換后的代碼具備語義等價性的過程，主要應(yīng)用于編譯器正確性檢測領(lǐng)域。編譯器正確性檢測的重要思想是將編譯器優(yōu)化的代碼與原始代碼進(jìn)行比較，并確定這兩個代碼在語義上是否相等，主要通過構(gòu)造關(guān)聯(lián)兩個程序的中間狀態(tài)的不變式[6]，以比較中間狀態(tài)的等效性，這種檢測方法要求被比較的程序控制流高度相似，而編譯器優(yōu)化前后的程序基本都滿足此條件，因此該方法在編譯器正確性檢測中有著較為廣泛的應(yīng)用；軟件剽竊是指通過非法復(fù)制他人軟件的代碼，并利用代碼混淆技術(shù)使代碼在文本上發(fā)生變化，違反軟件原始許可條款的行為，軟件剽竊檢測中同樣采用了程序等效性檢查的方法；回歸驗(yàn)證是由Godlin和Strichman[18]最先提出的，它用于相似程序的等效性檢查，其目標(biāo)是建立兩個不同版本程序等效的形式證明。

Invariant-sketching[6]是一種通過不變式初稿和查詢降解進(jìn)行編譯前后程序等效性檢測的算法，它將待比較的程序的位置點(diǎn)抽象成節(jié)點(diǎn)，將兩程序中由兩個節(jié)點(diǎn)確定的路徑抽象成邊，并設(shè)計算法構(gòu)造描述兩個函數(shù)關(guān)系的JTFG(關(guān)聯(lián)傳遞函數(shù)圖，joint transfer function graph)。在構(gòu)造JTFG的過程中，使用“不變式初稿”來表示兩條邊中變量的線性關(guān)系，從而進(jìn)行“邊”的關(guān)聯(lián)；如果存在無法關(guān)聯(lián)的邊，則判定兩程序不等價。SamaTulyataII[5]提出針對循環(huán)的代碼轉(zhuǎn)換驗(yàn)證。該方法將轉(zhuǎn)換前后的代碼抽象成基于Petri Net的模型，在帶有循環(huán)的程序中，循環(huán)執(zhí)行的次數(shù)未知，路徑構(gòu)造器將CPN(Colour Petri Net)模型表示成有限路徑的形式，再使用基于路徑的等價性檢查器進(jìn)行等價性驗(yàn)證。

Xu等人[11]總結(jié)了軟件剽竊檢測五個方面的需求，并根據(jù)這五個方面的需求評估了現(xiàn)存的軟件剽竊檢測方法。目前軟件剽竊檢測中采用最廣泛的是是動態(tài)軟件胎記技術(shù)。早期一些基于源碼的技術(shù)中，也通過程序等價性檢查的方式進(jìn)行剽竊檢測。GPLAG[12]是基于靜態(tài)源碼比對的檢測方法，通過構(gòu)造程序依賴圖(PDG, program dependence graph)并使用圖同構(gòu)檢測算法，能夠檢測經(jīng)過FA、IR、SR、CR、CI[12]這幾種混淆方式混淆的代碼的等價性，但對于不透明謂詞和循環(huán)展開這兩種方式的代碼混淆則無法進(jìn)行軟件剽竊鑒別。Myles和Collberg[13]提出基于動態(tài)控制流的方法WPPB(Whole Program Path Birthmark)進(jìn)行剽竊鑒別。這種方法利用WPP(Whole Program Path)[20]能夠標(biāo)記程序動態(tài)行為中的固有規(guī)律的特點(diǎn)，識別出保留語義的代碼轉(zhuǎn)換。LoPD[10]是一種動態(tài)和靜態(tài)相結(jié)合的軟件剽竊檢測技術(shù)，利用動態(tài)符號執(zhí)行來獲得執(zhí)行路徑的語義并尋找路徑偏移，再檢測兩條偏移的路徑是否在語義上等價。這種技術(shù)能夠針對多種代碼混淆方式進(jìn)行整個程序的剽竊檢測以及局部的剽竊檢測。

LLRêVE-DYNAMIC[16]是針對回歸驗(yàn)證的等效性判定技術(shù)，采用插入同步點(diǎn)的方式打破程序中的循環(huán)控制流，在同步點(diǎn)處構(gòu)造霍恩約束來表示兩個被比較的程序中間狀態(tài)間的關(guān)系，再使用約束求解器進(jìn)行求解，根據(jù)求解結(jié)果判斷程序的中間狀態(tài)是否等效。這種方法對程序控制流的相似度有較高的要求，當(dāng)程序中存在循環(huán)結(jié)構(gòu)并且迭代次數(shù)不相同時，需要對程序在源碼級別上進(jìn)行“循環(huán)展開(Loop Unrolling)”和“循環(huán)剝離(Loop Unpeeling)”操作，將程序轉(zhuǎn)換為控制流相似的程序才能進(jìn)行等效性判定。

這些針對特定領(lǐng)域的等效性判定技術(shù)都難以直接應(yīng)用于科學(xué)計算程序的等效性判定，SCEP方法的提出有助于解決該問題。

2 方法

2.1 SCEP介紹

本文將程序等效性判別技術(shù)應(yīng)用于科學(xué)計算程序的等效關(guān)系證明，提出基于C/C++源碼和Fortran源碼的程序等價性判別方法SCEP。與之前專門針對C/C ++語言的代碼驗(yàn)證工具不同， SCEP方法在工作過程中不需要用戶理解程序并對程序進(jìn)行人工干預(yù)，此外，它也可以在控制流相似度較小的程序上進(jìn)行判定工作。

在方法設(shè)計中，SCEP是基于程序路徑的等效性驗(yàn)證。通過比較兩個程序中的分支條件，構(gòu)造Matching-Constraint，根據(jù)SMT求解器的求解結(jié)果，可以構(gòu)造兩個程序中相匹配的路徑。此外，已有的方法是通過構(gòu)造兩個程序的中間狀態(tài)的等價關(guān)系來驗(yàn)證整個程序的等效性，這種方法能夠處理的情況是有限的，SCEP不考慮程序中間狀態(tài)是否等價，只關(guān)注程序的出口狀態(tài)，這使得SCEP在已有方法的基礎(chǔ)上能夠應(yīng)對更多類型的程序轉(zhuǎn)換方式。

本文收集C/C++和Fortran編程語言實(shí)現(xiàn)的函數(shù)，針對采用不同方式進(jìn)行的語義不變的函數(shù)轉(zhuǎn)換，構(gòu)造“spcLib”數(shù)據(jù)集，分別使用前人的方法和SCEP對數(shù)據(jù)集中的函數(shù)轉(zhuǎn)換進(jìn)行等效性驗(yàn)證實(shí)驗(yàn)，我們發(fā)現(xiàn)SCEP能夠針對更多的函數(shù)轉(zhuǎn)換方式得到驗(yàn)證結(jié)果，并且能夠在Fortran代碼上工作。

2.2 框架概述

SCEP的主要架構(gòu)包括預(yù)處理、路徑采集與匹配、狀態(tài)比較三個模塊，如圖1所示。如果輸入的兩個待比較的源代碼在功能上等效，則將輸出“true”作為處理結(jié)果；對于其他任何無法判定為等效的程序?qū)?，輸出結(jié)果“undecidable”。

圖1 SCEP整體架構(gòu)

在預(yù)處理階段，LLVM框架將源代碼編譯成LLVM中間表示的形式。待分析的代碼使用的編程語言是C/C ++或Fortran，在將Clang和Flang[21]。安裝為LLVM的前端之后，可以使用LLVM框架將C/C++和Fortran編譯為中間語言。除了安裝上的差異，使用Clang和Flang進(jìn)行源碼到中間語言的轉(zhuǎn)換在操作非常相似。

路徑匹配階段會將待分析的程序中具有等效約束的兩條路徑匹配為一組路徑對。根據(jù)兩程序的分支條件構(gòu)造Matching-Constraint，再使用SMT求解器(例如Z3[22])對它進(jìn)行求解。如果轉(zhuǎn)換前后的程序中所有路徑的約束都相同，則可以匹配這兩個程序中的所有路徑；否則，將認(rèn)為這兩個程序的等效性無法判定。

最后一步是比較所有路徑對的路徑狀態(tài)。通過兩程序中的變量構(gòu)造Horn范式約束，再次使用求解器進(jìn)行約束求解，根據(jù)求解情況，判定兩程序在語義上是否等效。

2.3 預(yù)處理

在預(yù)處理階段，程序源碼將被轉(zhuǎn)換為LLVM中間表示(Intermediate Representation, IR)，接著會在IR級別上進(jìn)行等效性判別。在LLVM IR上進(jìn)行等效性判別的優(yōu)勢主要體現(xiàn)在以下三個方面：

(1)屏蔽不同編程語言語法上的差異性。

本文的主要工作是判定C/C ++代碼與Fortran代碼或Fortran代碼與Fortran代碼之間的等效性，然而，F(xiàn)ortran和C/C ++語法完全不同，這將導(dǎo)致在具體的判別工作之前需要對源代碼進(jìn)行復(fù)雜的分析工作，LLVM + Clang/Flang可以將C/C ++源代碼和Fortran源代碼分別編譯為中間語言。 LLVM IR將指令、函數(shù)和程序抽象為相應(yīng)的類，用戶只需要使用LLVM框架提供的接口來對程序進(jìn)行分析和處理。

(2)減少程序分析過程中的工作量。

采用LLVM框架便于在中間語言上生成控制流圖。在SCEP方法中，程序的每條路徑都由約束表達(dá)式表示，為了獲得所有路徑的約束，必須對程序的控制流進(jìn)行分析，通過遍歷LLVM生成的控制流圖上的基本塊來獲得路徑約束，為整個處理過程減少了很多冗余的工作。

(3)便于實(shí)現(xiàn)程序向邏輯公式的轉(zhuǎn)換。

為了將程序的等效性判定問題轉(zhuǎn)化成邏輯公式的求解問題，首先需要將程序轉(zhuǎn)化為SSA形式(Static single assignment form)，以便能夠利用自動化的方式將SSA形式的代碼表示轉(zhuǎn)化成邏輯公式。LLVM IR是SSA形式的中間表示，能夠滿足我們的需求。

2.4 路徑采集與匹配

程序的執(zhí)行路徑指的是在一個回合執(zhí)行期間執(zhí)行的所有指令的序列。 執(zhí)行路徑的語義可以通過符號執(zhí)行來獲取。更確切地說，執(zhí)行路徑的語義可以表示為輸出變量對應(yīng)于輸入變量的符號表達(dá)式以及路徑約束表示。

在檢查程序狀態(tài)的等效性之前，SCEP方法會將兩個目標(biāo)程序中的對應(yīng)路徑組合起來。如果兩個程序中某兩條路徑的約束等效，則它們將構(gòu)成一對路徑組合，在后續(xù)過程中將基于這兩條路徑進(jìn)行狀態(tài)等效性驗(yàn)證。要找到兩條路徑所對應(yīng)的約束的所有解，然后判斷它們在無限解的情況下是否都相同顯然是不切實(shí)際的。本文提出一種新的方法進(jìn)行路徑等效性判別：分別根據(jù)兩個程序所有分支處的謂詞構(gòu)造每條路徑的約束，再利用不同程序的兩條路徑的約束構(gòu)造Matching-Constraint。如果SMT求解器對Matching-Constraint求解的結(jié)果為“unsatisfiable”，則兩條路徑不等價；如果求解結(jié)果為“satisfiable”則路徑等價。 假設(shè)使用“ condA”和“ condB”表示兩條路徑的約束， “ condnew”表示構(gòu)造出的Matching-Constraint，則，

condnew=(condA∧┐condB)∨(┐condA∧condB)

如果滿足條件“condnew”的集合為空，則得出結(jié)論condA和condB是等效的，否則得出相反的結(jié)論。上述結(jié)論很容易得到證明：

(“ setA”和“ setB”分別表示滿足condA和condB的集合。)

2.5 狀態(tài)比較

狀態(tài)轉(zhuǎn)換謂詞用來抽象程序從入口處到出口處狀態(tài)的轉(zhuǎn)換過程，具體來說，狀態(tài)轉(zhuǎn)換謂詞指的是程序入口處變量集合和出口處變量集合的關(guān)系表達(dá)式。耦合不變式指的是兩條路徑約束相匹配的執(zhí)行路徑的不變式，利用耦合不變式和狀態(tài)轉(zhuǎn)換謂詞構(gòu)成Horn范式約束可以進(jìn)行狀態(tài)的等價性判別。

在路徑匹配完成后，SCEP不考慮兩程序中間值的大小關(guān)系，而僅對函數(shù)每條路徑的出口處的變量的值進(jìn)行比較。假設(shè)兩個待比較的程序分別為P和Q，P與Q入口處的變量分別表示為Xp和Xq，出口處的變量分別表示為Xp′和Xq′。針對這些變量，在函數(shù)的入口和出口處構(gòu)造耦合不變式b(Xp,Xq)和e(Xp′,Xq′)，再根據(jù)程序P和Q的指令構(gòu)造Xp和Xq的狀態(tài)轉(zhuǎn)換謂詞，分別用φ(Xp,Xp′)和π(Xq,Xq′)來表示。據(jù)此可以生成Horn范式約束，其形式為：

最后，將生成的約束提供給可用于Horn子句求解的求解器Z3，Z3將嘗試尋找一個滿足上述約束公式的實(shí)例。如果求解器能找到解，那么這條路徑的程序狀態(tài)等效；如果求解器顯示解不存在或者求解超時，則兩程序的等效性判定結(jié)果為“undecidable”。

2.6 程序示例

圖2中函數(shù)的功能是計算非負(fù)十進(jìn)制數(shù)n(n≥ 0)的位數(shù)，很容易看出函數(shù)(a)和函數(shù)(b)在功能上是等價的。由于循環(huán)次數(shù)由n的大小來決定，路徑匹配的過程中函數(shù)路徑的條數(shù)將是一個非常大的數(shù)字，這會導(dǎo)致路徑爆炸問題，因此在分析過程中，需要為兩個程序的路徑約束添加“循環(huán)上限”，這種方法提高了驗(yàn)證錯誤率，但能有效解決路徑爆炸問題。假設(shè)添加的循環(huán)上限是n<108，那么對于函數(shù)(a)，有：

圖2 計算非負(fù)十進(jìn)制數(shù)的位數(shù)

path1:(na1>0)∧(na1/10≤0);

path2:(na2/10>0)∧(na2/100≤0);

path3:(na3/10>0)∧(na3/1 000≤0);

……

path8:(na8/10>0)∧(na8/100 000 000≤0);

對于函數(shù)(b)，有：

path1:(nb1>0)∧(nb1<10);

path2:(nb2>0)∧(nb2≥10)∧(nb2<100);

path3:(nb3>0)∧(nb3≥10)∧(nb3≥100)∧(nb3<1 000);

path4:(nb4>0)∧(nb4≥10)∧(nb4≥100)∧(nb4≥1 000)∧(nb4<10 000);

……

path8:(nb8>0)∧(nb8≥10)∧(nb8≥100)∧……∧(nb8<100 000 000)。使用2.4節(jié)中提到的路徑匹配方法能構(gòu)造這兩個函數(shù)路徑一一對應(yīng)的關(guān)系，例如，對于函數(shù)(a)的path2和函數(shù)(b)的path2，可以構(gòu)造出函數(shù)入口處的耦合不變式：

na2=nb2；

函數(shù)(a)的狀態(tài)轉(zhuǎn)換謂詞為：

函數(shù)(b)的狀態(tài)轉(zhuǎn)換謂詞為：

(result2=1)∧(result2′=result2+1)；

如果函數(shù)(a)和函數(shù)(b)等效，函數(shù)出口處的變量關(guān)系滿足：

result1′=result2′。

如果在Horn范式約束的前件有效的條件下，能夠推測出其后件有效，則該約束是可滿足的。據(jù)此，可以判定兩函數(shù)在(na2/10>0)∧(na2/100≤0)和(nb2′>0)∧(nb2′≥10)∧(nb2′<100)這兩條等價的路徑下狀態(tài)等效。按照這種方法，同樣可以對其他路徑下的狀態(tài)進(jìn)行比較，如果每條路徑的狀態(tài)都是相同的，那么判定這兩個函數(shù)等效。

3 實(shí)驗(yàn)與評估

3.1 實(shí)驗(yàn)測試程序集

本文的實(shí)驗(yàn)測試程序集spcLib通過兩種途徑進(jìn)行獲?。阂皇腔诔Ｒ姷拇a混淆方法以及程序優(yōu)化方法構(gòu)造的不同功能的函數(shù)集合(以下稱該類函數(shù)集合為一類函數(shù)集合，包括相同數(shù)量的C++和Fortran兩個版本)；二是從三種不同的libc實(shí)現(xiàn)中提取的程序樣例(以下稱該類函數(shù)集合為二類函數(shù)集合)。三種不同的libc實(shí)現(xiàn)分別為：dietlibc[22]、glibc[23]和OpenBSD[24]。

其中，一類函數(shù)集合通過本文總結(jié)的六種常見的代碼混淆或程序優(yōu)化方式進(jìn)行構(gòu)造，這六種語義等價轉(zhuǎn)換的方式包括：

(1)格式變更。

插入或刪除程序中的空格或注釋。這種混淆方式僅對基于文本的檢測技術(shù)產(chǎn)生效果。

(2)標(biāo)識符重命名。

可以在不影響程序正確性的情況下不斷地更改程序中的標(biāo)識符名稱。本文的方法將源碼轉(zhuǎn)換成中間語言，當(dāng)程序僅有標(biāo)識符被改變時，改變前后的代碼會被轉(zhuǎn)換成相同的LLVM IR。

(3)插入噪聲指令。

插入的代碼不干擾原始程序邏輯。在進(jìn)行路徑探索的過程中，沒有任何一個基本塊會跳轉(zhuǎn)到噪聲指令所在塊進(jìn)行執(zhí)行，因此本文的方法可針對添加噪聲指令前后的等價程序進(jìn)行程序的等價性驗(yàn)證。

(4)語句重新排序。

某些語句可以重新排序而不會導(dǎo)致程序錯誤，例如變量的聲明語句，這種語句重新排序并不會改變LLVM中間語言中基本塊的跳轉(zhuǎn)順序。

(5)控制語句替換。

例如將for循環(huán)由while循環(huán)進(jìn)行等價替換，或者將有害的goto語句等價轉(zhuǎn)換成其他控制語句。這種代碼混淆方法同上一條一樣，并不會改變程序的控制流，程序的執(zhí)行路徑不會發(fā)生改變。

(6)循環(huán)語句展開。這是一種循環(huán)轉(zhuǎn)換技術(shù)，這種轉(zhuǎn)換方法基于“以空間換時間” 的思想，用于優(yōu)化程序的執(zhí)行速度。轉(zhuǎn)換可以由程序員手動執(zhí)行，也可以由優(yōu)化編譯器手動執(zhí)行。

3.2 實(shí)驗(yàn)結(jié)果統(tǒng)計

使用SCEP驗(yàn)證spcLib測試集中所有函數(shù)的等價性，通過驗(yàn)證結(jié)果來證明SCEP方法的可靠性。目前發(fā)現(xiàn)的與本工作最為接近的方法是Kiefer等人提出的LLRêVE-DYNAMIC[16]，因此實(shí)驗(yàn)中選擇該工具對spcLib測試集合中C++語言實(shí)現(xiàn)的一類函數(shù)以及所有二類函數(shù)進(jìn)行語義等價性驗(yàn)證，統(tǒng)計出兩種方法下的驗(yàn)證結(jié)果數(shù)據(jù)，并將它們進(jìn)行比較，據(jù)此評估SCEP的優(yōu)勢。

實(shí)驗(yàn)使用SCEP和LLRêVE-DYNAMIC分別對spcLib中的函數(shù)進(jìn)行程序等價性驗(yàn)證，統(tǒng)計的實(shí)驗(yàn)結(jié)果數(shù)據(jù)如表1所示。一類函數(shù)集合中包括等數(shù)量的Fortran函數(shù)和C++函數(shù)，SCEP對所有一類函數(shù)的驗(yàn)證結(jié)果為等價；二類函數(shù)集合中有150對函數(shù)，其中，判定結(jié)果為等價的有132對。由于LLRêVE-DYNAMIC不支持Fortran程序的等價性驗(yàn)證，因此使用該工具對一類函數(shù)集合中的C++函數(shù)和二類函數(shù)集合中的函數(shù)進(jìn)行等價性驗(yàn)證，統(tǒng)計結(jié)果表明，對于一類函數(shù)集合中的函數(shù)對，判定結(jié)果為等價的有126對，對于二類函數(shù)集合中的函數(shù)對，判定結(jié)果為等價的有123對。

表1 兩種方法的驗(yàn)證結(jié)果

3.3 評估

LLRêVE-DYNAMIC[16]在進(jìn)行程序的等價性驗(yàn)證時，要求待驗(yàn)證的程序控制流高度相似，與LLRêVE-DYNAMIC不同，SCEP不要求被驗(yàn)證的兩程序的控制流相似；另外，LLRêVE-DYNAMIC在工作工程中，如果系統(tǒng)無法自動生成同步點(diǎn)(Synchronization Point)，需要用戶對源碼進(jìn)行理解，并在源碼的適當(dāng)位置手工插入同步點(diǎn)，從而進(jìn)行同步點(diǎn)之間的等價性驗(yàn)證，而SCEP不需要預(yù)先對源碼進(jìn)行理解基礎(chǔ)上的處理。從這兩個方面來看，SCEP方法比LLRêVE-DYNAMIC在使用過程中的限制更少，并且更加自動化。

SCEP和LLRêVE-DYNAMIC對spcLib中二類函數(shù)的驗(yàn)證情況對比如圖3所示，該圖顯示了兩種方法分別對兩類函數(shù)集合進(jìn)行驗(yàn)證，得到等價的結(jié)果所占的比例。在一類函數(shù)的驗(yàn)證中，LLRêVE-DYNAMIC能對84%左右的函數(shù)進(jìn)行等價性判別，而SCEP方法能夠達(dá)到100%的等價驗(yàn)證率；在驗(yàn)證的150對二類函數(shù)中，LLRêVE-DYNAMIC能對82%左右的函數(shù)進(jìn)行等價性判別，而SCEP方法能夠驗(yàn)證84%左右的函數(shù)對的語義等價性。

圖3 兩種方法在兩類函數(shù)集合上的驗(yàn)證情況

從條形圖的高度可以看出，在兩類函數(shù)集的實(shí)驗(yàn)中，本文的SCEP方法驗(yàn)證成功率略高于LLRêVE-DYNAMIC方法。SCEP在對第一類函數(shù)集合的驗(yàn)證上可以達(dá)到100%的成功率，遠(yuǎn)高于LLRêVE-DYNAMIC方法，但在第二類函數(shù)集合上，兩種方法的成功率十分接近。

從檢測程序的源碼上進(jìn)行分析，推測產(chǎn)生上述實(shí)驗(yàn)結(jié)果的原因可能是第一類函數(shù)集合是通過本文的六種變換方式進(jìn)行構(gòu)造的，而我們的驗(yàn)證方法在設(shè)計過程中專門考慮到了這六種類型的語義等價轉(zhuǎn)換，因此針對這類函數(shù)的等價性驗(yàn)證成功的概率更大。而二類函數(shù)包含更多種類別的語義等價的轉(zhuǎn)換方法，某些轉(zhuǎn)換方式在本文方法下無法成功驗(yàn)證函數(shù)語義的等價性。函數(shù)等價變換的方式十分復(fù)雜，要對該方法進(jìn)行更準(zhǔn)確的評估，還需要在更大的測試程序集上設(shè)計實(shí)驗(yàn)進(jìn)行驗(yàn)證，以便完善本文的SCEP，使其能夠?qū)Ω囝悇e的等價轉(zhuǎn)換方式下的語義等價函數(shù)進(jìn)行等價性驗(yàn)證。但總的來說，本文的SCEP成功進(jìn)行程序語義等價性驗(yàn)證的幾率比LLRêVE-DYNAMIC更高。

4 結(jié)語

SCEP是一種基于路徑的狀態(tài)等價性檢測方法。針對手工的程序轉(zhuǎn)化比自動化程序轉(zhuǎn)化具有更大的差異性，SCEP對轉(zhuǎn)化前后控制流差異較大的代碼采用構(gòu)造狀態(tài)不變式的方式進(jìn)行驗(yàn)證，基于對函數(shù)的結(jié)果狀態(tài)驗(yàn)證，來構(gòu)造對程序整體的等效性判定，可作為科學(xué)計算程序版本更新和平臺遷移的正確性驗(yàn)證工具。在下一步工作中，我們將完善spcLib數(shù)據(jù)集，并對方法進(jìn)行改進(jìn)，提高方法的計算效率和適用性，使其能更為高效地處理大規(guī)?？茖W(xué)計算程序轉(zhuǎn)換的等效性判定。