郭曦，王盼

（1. 華中農(nóng)業(yè)大學(xué)信息學(xué)院，湖北 武漢 430070；2. 武漢電力職業(yè)技術(shù)學(xué)院電力工程系，湖北 武漢 430079）

1 引言

對(duì)程序的屬性和行為進(jìn)行精確分析是研究人員的主要目標(biāo)，然而隨著程序規(guī)模的增大，往往導(dǎo)致程序狀態(tài)空間也在不斷增大，從而嚴(yán)重影響程序分析的效果。符號(hào)執(zhí)行作為廣泛使用的程序分析方法，在路徑覆蓋、分支覆蓋、測(cè)試用例生成等方面發(fā)揮著重要的作用，但是由于其長(zhǎng)期受制于路徑條件提取精度以及約束求解器性能，極大限制了它的分析效果。

為了提高路徑分析的精度，研究人員采用多種分析方法從不同角度進(jìn)行研究，其中，狀態(tài)優(yōu)化合并是常用的分析方法，它通過在程序中增加臨時(shí)變量[1]來區(qū)分不同路徑對(duì)應(yīng)的符號(hào)輸入，但是這種分析方法會(huì)增加約束求解器的計(jì)算開銷，并且可能導(dǎo)致約束求解器停止工作而產(chǎn)生誤報(bào)或漏報(bào)。目前，約束求解器能夠較好地求解線性邏輯表達(dá)式，但是對(duì)程序中常見的復(fù)雜變量類型和數(shù)據(jù)結(jié)構(gòu)則難以有較好的分析精度。另外，約束求解器本身的調(diào)用開銷較大，為了使其能夠較長(zhǎng)時(shí)間工作，往往會(huì)刪除一些難以求解的邏輯結(jié)構(gòu)，從而導(dǎo)致分析的結(jié)果不夠完備。

本文主要對(duì)程序中的符號(hào)變量狀態(tài)進(jìn)行研究，通過提取不同路徑中的公共邏輯表達(dá)式，構(gòu)建新的符號(hào)表示方法，另外，對(duì)于邏輯表達(dá)式產(chǎn)生過程中存在的條件合并而導(dǎo)致的條件丟失問題，采用改進(jìn)的路徑重構(gòu)算法，從而提高路徑條件求解的效率。本文的主要貢獻(xiàn)如下。

1) 把符號(hào)變量和路徑條件進(jìn)行合并分析，從而對(duì)符號(hào)的表示形式進(jìn)行優(yōu)化。

2) 對(duì)符號(hào)執(zhí)行過程中基本塊之間存在的關(guān)聯(lián)關(guān)系進(jìn)行分析，并對(duì)路徑條件進(jìn)行優(yōu)化重構(gòu)，從而減少路徑條件的丟失。

3) 量化分析程序數(shù)量的邊界，從而可以準(zhǔn)確地分析程序的復(fù)雜度。

本文首先介紹程序分析的相關(guān)研究現(xiàn)狀和基本概念，然后詳細(xì)分析狀態(tài)合并的不足以及采用的狀態(tài)合并方法和變量間的關(guān)聯(lián)分析方法，并分析路徑執(zhí)行數(shù)量的邊界，最后通過實(shí)驗(yàn)分析驗(yàn)證本文所提方法的有效性。

2 相關(guān)研究進(jìn)展

程序分析是驗(yàn)證程序性質(zhì)、提高程序可靠性等需求的必需工作，在程序分析過程中廣泛使用的符號(hào)執(zhí)行分析方法以其特有的工作過程，在路徑可達(dá)分析、測(cè)試用例生成等領(lǐng)域有重要的研究?jī)r(jià)值。其主要工作方式為將變量以符號(hào)的形式進(jìn)行輸入，來代替具體的輸入值，這種靜態(tài)的分析方法相對(duì)于動(dòng)態(tài)分析方法來說可以獲得更為底層的程序邏輯關(guān)系，從而可以更好地分析程序的性質(zhì)。但是程序規(guī)模的變化對(duì)于符號(hào)執(zhí)行的分析效果有直接的影響，主要體現(xiàn)在程序變量類型的多樣化和數(shù)據(jù)結(jié)構(gòu)的復(fù)雜化，這使符號(hào)執(zhí)行在提取路徑表達(dá)式的過程中難以精確地刻畫路徑條件，同時(shí)由于約束求解器本身性能的限制，其對(duì)函數(shù)調(diào)用、數(shù)組下標(biāo)等復(fù)雜數(shù)據(jù)結(jié)構(gòu)，可能因?yàn)殡y以準(zhǔn)確求解而刪除部分邏輯表達(dá)式，從而影響分析精度或產(chǎn)生誤報(bào)。

為了提高程序分析的性能，目前主要采用狀態(tài)合并[2]的分析方法來處理不同路徑對(duì)應(yīng)的邏輯表達(dá)式，并采用多種分析策略來研究合并點(diǎn)處的邏輯符號(hào)[2-5]。文獻(xiàn)[2]使用傳統(tǒng)的輔助變量來分析程序在合并點(diǎn)的狀態(tài)，并采用函數(shù)摘要的分析方法產(chǎn)生測(cè)試集。文獻(xiàn)[3]使用狀態(tài)合并和符號(hào)執(zhí)行的分析方法研究程序的性質(zhì)，但是需要對(duì)程序進(jìn)行預(yù)處理，以消除函數(shù)調(diào)用和語句跳轉(zhuǎn)，才能進(jìn)行狀態(tài)合并操作。文獻(xiàn)[4]使用刪除冗余路徑的不可達(dá)分析方法對(duì)程序狀態(tài)進(jìn)行處理。這幾種分析方法的共同特點(diǎn)是都使用了臨時(shí)符號(hào)變量，從而進(jìn)一步影響約束求解器的分析效果。文獻(xiàn)[5]采用不引入臨時(shí)變量的分析方法，但是該方法的使用范圍只能局限于具有相同數(shù)據(jù)結(jié)構(gòu)的程序。對(duì)于程序分析過程中常見的冗余路徑和不可達(dá)路徑，目前的分析方法主要通過比較當(dāng)前狀態(tài)和歷史狀態(tài)，或?qū)顟B(tài)空間劃分為規(guī)模較小的子空間進(jìn)行單獨(dú)求解。常見的分析工具（如JPF[6]）通過狀態(tài)匹配的分析方法來減少狀態(tài)空間，文獻(xiàn)[7]則采用讀寫集的分析方法來優(yōu)化狀態(tài)匹配條件。函數(shù)摘要[8-9]可以對(duì)程序的函數(shù)調(diào)用接口進(jìn)行分析，作為一種靜態(tài)分析方法，它可以與其他程序優(yōu)化方法進(jìn)行協(xié)同工作，如可達(dá)分析、指向分析等，但是這些方法存在分析精度較低等問題。文獻(xiàn)[10]將變量符號(hào)轉(zhuǎn)換為守衛(wèi)條件表達(dá)式，從而分析程序的可達(dá)性，但是該方法沒有對(duì)路徑條件順序進(jìn)行優(yōu)化分析，存在漏報(bào)的情況。文獻(xiàn)[11]依據(jù)程序的輸出結(jié)果對(duì)程序的執(zhí)行路徑進(jìn)行分類，但是該方法存在路徑條件未用邏輯符號(hào)表達(dá)式的形式表示的問題，故約束求解器在處理過程中容易終止分析。對(duì)于程序上下文執(zhí)行語義中存在的惡意代碼，文獻(xiàn)[12]統(tǒng)計(jì)缺陷的種類和與之相關(guān)的路徑集合，從而生成能夠發(fā)掘惡意代碼的測(cè)試用例集。文獻(xiàn)[13]使用抽象精化的形式化方法對(duì)符號(hào)變量進(jìn)行分析，產(chǎn)生可以同時(shí)分析多個(gè)目標(biāo)狀態(tài)的序列。文獻(xiàn)[14]采用條件約束、最短路徑等分析方法，推遲程序變量的實(shí)例化操作從而減少路徑狀態(tài)的擴(kuò)大。

由于變量符號(hào)狀態(tài)在合并操作過程中普遍存在臨時(shí)變量，從而加重求解器的性能開銷，同時(shí)約束求解器在求解過程中對(duì)于路徑條件表達(dá)式的處理性能不夠強(qiáng)大而導(dǎo)致分析精度下降，對(duì)于這些問題，本文在符號(hào)執(zhí)行的分析基礎(chǔ)上，將目標(biāo)符號(hào)和對(duì)應(yīng)的約束條件作為整體進(jìn)行協(xié)同表示，從而不引入臨時(shí)變量。在約束求解器的工作階段，采用流敏感的上下文分析方法，提取對(duì)目標(biāo)變量有重定義操作的語句集合，然后逆向分析到程序的入口，對(duì)于該過程收集到的邏輯表達(dá)式，本文提出路徑條件重構(gòu)的分析方法，減少因求解器刪除邏輯表達(dá)式而產(chǎn)生的誤報(bào)和漏報(bào)。本文方法相對(duì)于傳統(tǒng)的程序分析方法，可以避免臨時(shí)變量的引入，同時(shí)可以提高約束求解器的分析性能。

3 路徑條件和關(guān)聯(lián)分析

符號(hào)執(zhí)行作為主要的程序分析工具，已經(jīng)在可達(dá)分析、路徑覆蓋、分支覆蓋等方向有了廣泛的應(yīng)用。其核心思想是將變量符號(hào)作為程序的輸入，符號(hào)化地執(zhí)行程序，從而驗(yàn)證程序的性質(zhì)。

定義1 路徑條件。記程序P和一組對(duì)應(yīng)的輸入t，t對(duì)應(yīng)的程序路徑記為π，路徑條件φ為π中所有分支語句對(duì)應(yīng)的判定條件組成的邏輯表達(dá)式。

符號(hào)執(zhí)行在工作過程中，會(huì)沿著當(dāng)前執(zhí)行路徑記錄分支語句對(duì)應(yīng)的判定條件，將其作為當(dāng)前輸入對(duì)應(yīng)的路徑條件。后續(xù)新的程序輸入如果能夠滿足該路徑條件對(duì)應(yīng)的邏輯表達(dá)式，則該新的輸入也會(huì)驅(qū)使程序運(yùn)行到相同的語句位置。路徑條件φ可以表示為 φ=φ1∨φ2∨φ3∨φ4∨φ5，其中，φi為一個(gè)分支語句對(duì)應(yīng)的邏輯表達(dá)式。

符號(hào)執(zhí)行樹如圖1所示。符號(hào)執(zhí)行在工作過程中需要記錄并更新變量的符號(hào)狀態(tài)，主要包括變量對(duì)應(yīng)的符號(hào)以及對(duì)應(yīng)的路徑條件φ。對(duì)于圖1(a)中的程序，符號(hào)執(zhí)行將 x0、y0、z0作為程序的輸入。表1列舉了圖1(a)中的程序?qū)?yīng)的所有狀態(tài)。

圖1 程序片段及對(duì)應(yīng)的符號(hào)執(zhí)行樹

在程序當(dāng)前執(zhí)行路徑中，新加入的路徑分支條件會(huì)更新當(dāng)前的符號(hào)狀態(tài)，同時(shí)也會(huì)更新變量的符號(hào)值。為了發(fā)掘新的執(zhí)行路徑，常用的方法是將某一個(gè)路徑條件對(duì)應(yīng)的邏輯表達(dá)式進(jìn)行取反，從而獲得不同的路徑條件邏輯值，以驅(qū)使程序沿著另外的分支運(yùn)行。由于程序中變量類型的多樣化和復(fù)雜化，表1中φ5所對(duì)應(yīng)的示例程序中的語句包含浮點(diǎn)類型的變量，對(duì)于該類型的變量，目前的約束求解器的分析效果難以滿足程序性質(zhì)研究的需要，故一般的約束求解器在工作過程中，會(huì)采取近似值或刪除對(duì)應(yīng)的邏輯條件表達(dá)式來確保盡可能長(zhǎng)的求解過程，這樣的結(jié)果必然會(huì)影響程序分析的精度，類似的情況還包括函數(shù)調(diào)用和數(shù)組下標(biāo)等情形。為了應(yīng)對(duì)這種問題，本文將輸入變量的符號(hào)和對(duì)應(yīng)的路徑條件進(jìn)行協(xié)同處理，從而能夠減少因邏輯表達(dá)式刪除而產(chǎn)生的約束求解器中斷或誤報(bào)等情形。

表1 符號(hào)執(zhí)行狀態(tài)集合

本文采用的分析策略包含后向分析方法，由于后向分析通常以程序的出口語句或指定語句為起點(diǎn)，逆向分析到程序的入口語句，在該過程中可以提取與出口語句或指定語句中符號(hào)變量相關(guān)的邏輯表達(dá)式集合。

由于程序中的條件嵌套語句可以轉(zhuǎn)化為不帶嵌套的形式，為了描述方便，采用圖2(a)所示的不帶條件嵌套的程序進(jìn)行說明。圖2(a)所示程序的目標(biāo)語句中變量b在不同路徑條件φ的作用下有不同的符號(hào)值。

1)(x ? y ＞ 0) ∧ (x + y ＞ 10) ? (b = =x)。

2)?(x ? y ＞ 0) ∧ (x + y ＞ 10) ? (b = =y)。

3)?(x + y ＞ 10) ? (b ==2)。

這種符號(hào)化的表示方法在一定程度上可以簡(jiǎn)化程序的可達(dá)路徑集合，對(duì)于圖2(a)中程序的目標(biāo)語句14)中的變量b，與b相關(guān)的符號(hào)表達(dá)式可以表示該程序所有的8條可達(dá)路徑，如圖3所示。根據(jù)程序的輸出符號(hào)，可以將可達(dá)路徑進(jìn)行劃分，這樣就可以進(jìn)一步分析符號(hào)變量在不同可達(dá)路徑之間的關(guān)聯(lián)關(guān)系。

圖2 隱式依賴分析

圖3 基于依賴條件的路徑劃分

對(duì)于程序的執(zhí)行路徑中的2個(gè)節(jié)點(diǎn)b1和b2，設(shè)目標(biāo)語句中的變量符號(hào)為v，若b2與b1之間是直接依賴關(guān)系，則存在如下可能：b1對(duì)v進(jìn)行了賦值運(yùn)算等操作；b2中存在使用v的語句。這種依賴關(guān)系是程序分析過程中較普遍的關(guān)系，但是在實(shí)際分析過程中，還存在間接依賴關(guān)系，下面給出其定義。

定義2 間接依賴。設(shè)s為程序P中的目標(biāo)語句，P存在一條可達(dá)路徑π，s′為π中的一條語句，φ為其對(duì)應(yīng)的路徑條件，若s與s′存在間接依賴關(guān)系，則有如下條件成立。

1) s和φ有相同的路徑條件。

2) s中的某個(gè)變量v在當(dāng)前執(zhí)行路徑π中不存在賦值操作，但該變量在s與s′之間的其他路徑中被重新賦值。

依據(jù)定義2，圖2(b)中語句8)和語句14)之間存在間接依賴[12]關(guān)系，即語句14)中的變量b在當(dāng)前可達(dá)路徑[8,10,11,12,13,14]里無賦值操作，而在另一條可達(dá)路徑[8,9,10,11,12,13,14]里存在賦值操作。

由于依賴條件分析同時(shí)具備目標(biāo)語句與程序輸入的符號(hào)信息，故可以根據(jù)目標(biāo)語句的符號(hào)值將優(yōu)化后的符號(hào)執(zhí)行樹的路徑劃分為若干組。圖2(a)所示程序經(jīng)路徑劃分后的結(jié)果如圖3所示，程序所有的8條執(zhí)行路徑被劃分為3組，每組具有不同的符號(hào)輸出表達(dá)式。

在路徑條件分析過程中，通過修改最新加入的路徑條件表達(dá)式的邏輯值來發(fā)掘新的路徑集合，間接依賴分析可以把程序的依賴條件和輸入符號(hào)與目標(biāo)語句中的變量進(jìn)行關(guān)聯(lián)分析，若存在可解的路徑條件，則可以從路徑集合中刪除該路徑條件。對(duì)于圖2(a)中的程序，表2為程序輸入x=6, y=2, z=2時(shí)的路徑分析過程。

表2 當(dāng)程序輸入為x=6, y=2, z=2時(shí)的路徑分析過程

注意到表2中的間接依賴分析，路徑列中缺乏路徑條件?(x?y＞0)∧(x+y＞10)對(duì)應(yīng)的程序執(zhí)行路徑。若該路徑表達(dá)式可解，則當(dāng)前的路徑可達(dá)。但是目前的約束求解器在工作過程中為了保持工作的持續(xù)性，可能會(huì)刪除或合并某些邏輯表達(dá)式，這將會(huì)產(chǎn)生誤報(bào)或漏報(bào)現(xiàn)象。這種自行刪除的邏輯表達(dá)式往往蘊(yùn)含豐富的邏輯關(guān)系，故第4節(jié)將詳細(xì)分析路徑條件優(yōu)化的方法。

4 符號(hào)條件重構(gòu)算法

在第3節(jié)的程序分析過程中，常見的約束求解器對(duì)于線性邏輯表達(dá)式有較好的分析效果，但是對(duì)于較為復(fù)雜的數(shù)據(jù)結(jié)構(gòu)，為了減少約束求解器的調(diào)用次數(shù)，求解器會(huì)刪除難以分析的表達(dá)式，而刪掉的表達(dá)式可能包含關(guān)鍵的路徑信息，導(dǎo)致路徑分析的結(jié)果不夠精確。另外，在路徑發(fā)掘過程中，新增的路徑條件可能導(dǎo)致約束表達(dá)式隱式刪除，原因是在依賴條件分析過程中產(chǎn)生的變量符號(hào)與已有的變量符號(hào)一致，則這種新增的符號(hào)會(huì)被刪除，而被刪除的符號(hào)與新增的路徑有關(guān)聯(lián)關(guān)系，這樣會(huì)影響求解器的分析精度。本文采用改進(jìn)的路徑表達(dá)式分析方法，提取不同路徑在目標(biāo)語句處的符號(hào)表達(dá)式，這樣可以不引入輔助變量；對(duì)于已有的邏輯表達(dá)式集合，本文使用優(yōu)化算法進(jìn)行處理，從而減少因邏輯表達(dá)式的刪除而帶來精度上的損失。

4.1 符號(hào)簽名

采用符號(hào)執(zhí)行的程序分析方法在收集變量邏輯表達(dá)式的過程中會(huì)保存變量的符號(hào)表達(dá)式，新執(zhí)行路徑的生成會(huì)導(dǎo)致目標(biāo)語句中的變量符號(hào)有多個(gè)表達(dá)式，故通常使用輔助變量來進(jìn)行分析。圖1(a)語句6)中的變量z在不同路徑中對(duì)應(yīng)的符號(hào)表達(dá)式為(z0, 2.5)，故常規(guī)的符號(hào)分析方法會(huì)引入臨時(shí)變量z′來進(jìn)行分析，在該處狀態(tài)合并過程中，變量 z對(duì)應(yīng)的路徑條件為(2x0≤3∧z′=z0)∨(2x0＞3∧y0≠2∧z′=z0)∨(2x0＞3∧y0=2∧z′=2.5)。

定義3 符號(hào)簽名。設(shè)程序P對(duì)應(yīng)的輸入集合為T，P在每個(gè)輸入作用下對(duì)應(yīng)的路徑條件集合為Φ(Φ=φ1∨φ2∨…∨φn)，且在狀態(tài)合并點(diǎn)處變量 t的符號(hào)值集合為V(V=v1∨v2∨…∨vi)，對(duì)于任意一個(gè)vk，其對(duì)應(yīng)的路徑條件為 Φvk={φx∨φy∨…∨φz|1＜x,y,z＜n, x≠y≠z}，其中，φx、φy、φz為 3 條不同的執(zhí)行路徑對(duì)應(yīng)的路徑條件，此時(shí)變量t的符號(hào)簽名[12]為{(φ, vk)| φ∈Φvk}。

在符號(hào)簽名定義的基礎(chǔ)上，可以在程序某個(gè)待分析的語句位置將程序的輸入變量映射到其對(duì)應(yīng)的值簽名，將該過程的結(jié)果定義為“符號(hào)簽名視圖”。

定義 4 符號(hào)簽名視圖。對(duì)于一個(gè)程序 P，其輸入變量集合為T，程序中某個(gè)位置的變量t(t∈T)的值簽名為 vst，則該處程序的符號(hào)簽名視圖為{t ? vst|t∈T}。

符號(hào)簽名視圖可以直觀地展示出該位置變量所有的路徑條件和符號(hào)值。依據(jù)該定義，圖1(a)所示的程序?qū)?yīng)的符號(hào)簽名視圖為 x ?{(true,2 x0)}，y?{(?1∨?3, y0) ,(?2∨ ?4, z0?1),(?5,1.5)}，z?{(?1∨?2∨ ?3∨ ?4, z0) ,(?5,2.5)}。此種路徑條件的邏輯表示形式中沒有引入其他的臨時(shí)變量且語義上保持不變，從而有利于減少約束求解器的開銷。故符號(hào)簽名的主要操作過程為：對(duì)于符號(hào)簽名 vs中的 2個(gè)不同元素(φ1,v1)和(φ2,v2)，若 v1=v2，符號(hào)簽名最后 的 結(jié) 果 為(φ1∨ φ2,v1)， 即 等 價(jià) 于 vs{(φ1,v1),(φ2,v2)}?{φ1∨φ2,v1}，若 φ 為空，則可以將該符號(hào)簽名刪除。其優(yōu)點(diǎn)在于可以共享不同執(zhí)行路徑中的路徑條件表達(dá)式，減少約束求解器的調(diào)用次數(shù)。

4.2 依賴條件重構(gòu)

在第2節(jié)中，圖2(a)所示的程序?qū)?yīng)的8條可達(dá)路徑中，存在?(x?y＞0)∧(x+y＞10)的路徑條件，但在表2所示的路徑分析中，并沒有發(fā)掘該路徑，這樣會(huì)導(dǎo)致程序分析的不完備。導(dǎo)致這種路徑條件丟失的原因是表 2中步驟 3)在步驟 2)的基礎(chǔ)上加入x+y＞10并對(duì)其邏輯結(jié)果取反，得到步驟3)中的依賴條件(x?y＞0)∧?(x+y＞10)，滿足該條件的輸入設(shè)為x=6, y=2, z=2，而該組輸入對(duì)應(yīng)的依賴條件是?(x+y＞10)，這樣導(dǎo)致步驟 3)中的條件 x?y＞0 在表 2結(jié)果中丟失，本文采用依賴條件重構(gòu)的算法來處理這種條件丟失的問題，該算法通過對(duì)依賴條件處理的順序進(jìn)行優(yōu)化，從而保留關(guān)鍵的路徑邏輯表達(dá)式，依賴條件重構(gòu)的算法[13]如算法1所示。

算法1 依賴條件重構(gòu)算法

輸入 程序P，測(cè)試集t，目標(biāo)語句C

輸出 重構(gòu)后的依賴條件

1) 棧Stack為空;

2) Procedure Execute(t, n)

3) 計(jì)算關(guān)于C的依賴條件;

4) 將 φ1∧φ2∧…∧φm賦值給 dc;

5) 將 Reorder(dc) 賦值給 dc′;

7) for all 從n+1到m中的變量i

8) k =?1′ ∧?2′ ∧ … ∧ ??i′ ;

9) 將函數(shù)值(k,j)壓入棧Stack中;

10) end for

11) return

12) end Procedure

13)

14) Procedure Reorder(seq)

15) if seq的長(zhǎng)度為0

16) return seq;

17) end if

18) 將 φ1∧φ2∧…∧φk賦值給 seq;

19) 將seq1和seq2的值都賦值為true;

20) for all 從1到k1中的變量i

21) if br(φi)是 br(φk)的子集

22) 將 seq1∧φi的值賦給 seq1;

23) else

24) 將 seq1∧φi的值賦給 seq2;

25) end if

26) end for

27) return Reorder(seq1)∧Reorder(seq2)∧φk;

28) end Procedure

算法中的 Reorder(…)的作用是對(duì)依賴條件分析順序進(jìn)行重構(gòu)，它通過加入最新的路徑條件從而將當(dāng)前的路徑序列seq劃分為seq1和seq2這2個(gè)子序列，seq與最新加入的路徑條件之間有間接依賴關(guān)系，依據(jù)seq中條件的順序?qū)eq與最新加入的路徑條件進(jìn)行重構(gòu)并存儲(chǔ)在seq1中，類似地，將seq與最新加入的路徑條件之間沒有間接依賴關(guān)系的放在 seq2中。然后對(duì) seq1和 seq2分別再次進(jìn)行該操作，當(dāng)原路徑條件集合為空時(shí)，算法停止工作并得到重構(gòu)后的路徑表達(dá)式。通過依賴條件重構(gòu)分析，可以提高路徑條件分析的精度。

5 實(shí)驗(yàn)及分析

為了驗(yàn)證本文方法的有效性，實(shí)驗(yàn)以符號(hào)執(zhí)行為基礎(chǔ)并進(jìn)行狀態(tài)合并分析，來對(duì)比本文方法和傳統(tǒng)符號(hào)執(zhí)行方法在狀態(tài)合并效率以及程序分析精度上的提高。實(shí)驗(yàn)步驟為：通過構(gòu)建程序的控制流圖，以流敏感的方式對(duì)程序進(jìn)行分析，同時(shí)采用Z3工具作為約束求解器。實(shí)驗(yàn)流程如圖4所示。

為了對(duì)比本文方法和傳統(tǒng)程序分析方法在狀態(tài)合并等方面的效率，從合并數(shù)量、約束求解器調(diào)用次數(shù)等方面進(jìn)行分析，實(shí)驗(yàn)結(jié)果如表3所示。其中，符號(hào)簽名均值為程序出口語句中變量在不同執(zhí)行路徑中符號(hào)表達(dá)式的數(shù)量，其數(shù)值可以體現(xiàn)程序不同符號(hào)之間的關(guān)聯(lián)關(guān)系緊密程度。若路徑表達(dá)式和符號(hào)表達(dá)式在不同路徑中存在相同前綴，則在新路徑發(fā)掘過程中，可以利用已有的分析結(jié)果而減少計(jì)算開銷；符號(hào)簽名共享度用來衡量這種開銷的比例，其值為到達(dá)目標(biāo)語句位置的路徑數(shù)量與符號(hào)個(gè)數(shù)的比值。從表3可以看出，本文方法較傳統(tǒng)的分析方法有更好的狀態(tài)合并效果，本文使用的分析方法可以較好地緩解因路徑條件刪除而帶來的分析效率上的降低。

實(shí)驗(yàn)的另一個(gè)目的是分析路徑的復(fù)雜度。現(xiàn)有的程序路徑復(fù)雜度分析方法主要是分析程序輸入數(shù)量與路徑數(shù)量之間的關(guān)系。圈復(fù)雜度分析方法使用基本點(diǎn)測(cè)試的方法來計(jì)算復(fù)雜度，但是該方法的主要問題在于難以處理一條路徑中的節(jié)點(diǎn)都?xì)w屬于另一條路徑的程序。NPATH復(fù)雜度通過將循環(huán)次數(shù)限制在零次或一次的前提下進(jìn)行分析，其分析結(jié)果對(duì)復(fù)雜度的計(jì)算有較大干擾。

圖4 實(shí)驗(yàn)流程

表3 狀態(tài)合并和符號(hào)執(zhí)行的對(duì)比

由于循環(huán)語句的存在，導(dǎo)致路徑分析和約束求解難以精確衡量程序路徑的復(fù)雜程度。本文提出的路徑復(fù)雜度分析方法以程序的執(zhí)行深度為輸入，從而獲得程序執(zhí)行路徑的上界。該方法以控制流圖（CFG，control flow graph）為研究對(duì)象并采用深度優(yōu)先的搜索策略（DFS），當(dāng)程序中沒有循環(huán)結(jié)構(gòu)時(shí)，該方法與圈復(fù)雜度和NPATH方法的分析結(jié)果一致；當(dāng)存在循環(huán)結(jié)構(gòu)時(shí)，復(fù)雜度為關(guān)于程序執(zhí)行深度 n的表達(dá)式。記path(n)為長(zhǎng)度不超過n的路徑集合，同時(shí)定義路徑統(tǒng)計(jì)序列(a0,a1,…,ai,…)，其中，ai=path(n)，圖5所示的程序?qū)?yīng)的路徑統(tǒng)計(jì)序列為(0,0,1,1,1,2,2,2,3,…)。

圖5 路徑統(tǒng)計(jì)序列示例

路徑統(tǒng)計(jì)序列可以通過產(chǎn)生函數(shù)表示為一個(gè)有限多項(xiàng)式的形式：，進(jìn)一步可以使用泰勒級(jí)數(shù)的形式來表示：，其中，p(z)和 q(z)為有限多項(xiàng)式，此時(shí)統(tǒng)計(jì)序列中每一個(gè)元素可以通過計(jì)算得出，其中，gi(n)表示g(z)的第i次迭代。此時(shí)g(z)可以表示為

所以可以通過泰勒級(jí)數(shù)的系數(shù)來決定與指定長(zhǎng)度n相關(guān)的路徑數(shù)量，例如，該處g(z)的系數(shù)構(gòu)成了圖5中path(n)對(duì)應(yīng)的數(shù)值。對(duì)于給定的CFG，可以

通過構(gòu)建轉(zhuǎn)換矩陣 T[15]來計(jì)算產(chǎn)生函數(shù)：如果 CFG中2個(gè)節(jié)點(diǎn)vi和vj存在連接的邊，則Tij=1，否則Tij=0。同時(shí)有T|N|,|N|=1，則path(n)的產(chǎn)生函數(shù)可以表示為

其中，(I ?zT ):|N |,1表示從行列式I?zT中刪除第|N |行和第1列，函數(shù)det(…)用來計(jì)算參數(shù)的行列式。圖5程序?qū)?yīng)的矩陣為

其中，ci為多項(xiàng)式中的系數(shù)。對(duì)于圖 5所示程序，q(z)=1–z+z3–z4有 4個(gè)根，由于根 r=1有 2個(gè)，故r1=r2=1，且m3=m4=1。

因此有

由于q(z)存在共軛復(fù)根r和r，且rn+ rn為實(shí)數(shù)，故有。從而得到了在指定路徑長(zhǎng)度的情況下，程序執(zhí)行路徑數(shù)量的上界。為了分析該方法的復(fù)雜度，依據(jù)path(n)的上界進(jìn)行逼近分析。若則 f (n) = Θ( g(n))。

表4對(duì)比了圈復(fù)雜度、NPATH復(fù)雜度和本文方法在處理分支語句和循環(huán)語句時(shí)的時(shí)間復(fù)雜度。由表 4可以看出，圈復(fù)雜度的表示形式單一，NPATH復(fù)雜度在處理嵌套分支條件和嵌套循環(huán)時(shí)的表示形式相同，故這2種表示方法不適合用來分析復(fù)雜程序的復(fù)雜度，而本文方法對(duì)于不同的語句形式有不同的復(fù)雜度表示形式，故可以作為程序復(fù)雜度的分析依據(jù)。其中，K為條件語句數(shù)量，b為嵌套的層數(shù)，n為程序當(dāng)前路徑長(zhǎng)度。

表4 復(fù)雜度表示形式對(duì)比

6 結(jié)束語

目前的程序分析方法存在路徑條件提取不夠精確以及約束求解器難以處理復(fù)雜的數(shù)據(jù)結(jié)構(gòu)的情況，本文提出新的路徑條件表示方法，通過將路徑條件和符號(hào)表達(dá)式進(jìn)行協(xié)同分析，可以減少臨時(shí)符號(hào)變量的引入，另外本文還提出了依賴條件的重構(gòu)算法，可以減少因路徑條件刪除而帶來分析結(jié)果精度上的損失。實(shí)驗(yàn)結(jié)果表明，本文方法可以有效地進(jìn)行變量狀態(tài)的合并，并且可以提高程序分析的性能。將來的工作可以針對(duì)函數(shù)調(diào)用、數(shù)組下標(biāo)等復(fù)雜數(shù)據(jù)結(jié)構(gòu)進(jìn)行精確建模，從而使本文方法有更廣的使用范圍。