郭 曦 王 盼

1(華中農(nóng)業(yè)大學(xué)信息學(xué)院計(jì)算機(jī)科學(xué)系 武漢 430070)2(武漢電力職業(yè)技術(shù)學(xué)院電力工程系 武漢 430079)

程序分析的一個(gè)主要目標(biāo)是提高路徑的覆蓋率，從而對(duì)程序的行為、狀態(tài)和屬性等特征進(jìn)行分析.然而在實(shí)際操作過(guò)程中，窮盡地覆蓋分析往往導(dǎo)致過(guò)大的時(shí)空開銷，并且伴隨有極大的狀態(tài)冗余以及約束條件精度丟失.現(xiàn)有的程序分析方法通常采用符號(hào)執(zhí)行和約束求解的方法來(lái)開展各種分析，其中存在的問(wèn)題主要有狀態(tài)空間爆炸和約束求解器對(duì)于路徑約束求解能力的限制等.導(dǎo)致狀態(tài)空間爆炸的原因，除了程序本身的規(guī)模決定了搜索空間呈指數(shù)級(jí)增長(zhǎng)之外，程序狀態(tài)合并的效率、輸入集合的優(yōu)化程度以及約束求解器對(duì)于不同類型符號(hào)表達(dá)式的求解能力等，都會(huì)導(dǎo)致分析的時(shí)空開銷激增，從而極大地影響分析的效率.

狀態(tài)合并作為減少狀態(tài)空間爆炸的常見方法，其思路是對(duì)不同的執(zhí)行路徑進(jìn)行分析，在合并點(diǎn)通過(guò)引入輔助變量[1]來(lái)對(duì)目標(biāo)變量進(jìn)行表示，從而區(qū)分輸入的符號(hào)值.但是引入的輔助變量往往會(huì)極大影響后期的約束求解器的求解效果，因?yàn)槟壳暗募s束求解器對(duì)于線性約束有較好的處理效果，但當(dāng)約束條件中存在浮點(diǎn)類型數(shù)據(jù)、函數(shù)調(diào)用等結(jié)構(gòu)時(shí)，約束求解器為了能夠持續(xù)運(yùn)行，可能會(huì)刪除部分路徑條件或者停止工作從而導(dǎo)致分析結(jié)果不完備.同時(shí)在逆向符號(hào)執(zhí)行過(guò)程中，路徑條件在改變執(zhí)行路徑過(guò)程中，可能會(huì)導(dǎo)致部分路徑條件丟失的問(wèn)題，從而遺漏部分執(zhí)行分支使分析結(jié)果不夠精確.

本文針對(duì)符號(hào)執(zhí)行過(guò)程中通常使用的狀態(tài)合并方法進(jìn)行優(yōu)化研究，使用改進(jìn)符號(hào)表達(dá)式表示形式的方法，提高約束求解器的分析效果，從而減少狀態(tài)空間爆炸對(duì)于路徑分析效率的影響.在該過(guò)程中，針對(duì)路徑條件在迭代分析過(guò)程中存在條件丟失的問(wèn)題，提出改進(jìn)的路徑條件優(yōu)化組合方法，以提高路徑分析的精度.本文主要貢獻(xiàn)有2個(gè)方面：

1) 通過(guò)對(duì)狀態(tài)合并的符號(hào)表示方式進(jìn)行改進(jìn)，將路徑約束與目標(biāo)變量作為一個(gè)整體參與分析，從而精簡(jiǎn)符號(hào)執(zhí)行樹的表示形式；

2) 基于該符號(hào)執(zhí)行樹，根據(jù)基本塊的之間的依賴關(guān)系對(duì)路徑條件進(jìn)行優(yōu)化組合，減少路徑條件的丟失，提高逆向分析的精度.

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

符號(hào)執(zhí)行作為主流的程序分析方法在路徑覆蓋、測(cè)試用例生成等研究方向發(fā)揮了重要的作用.符號(hào)執(zhí)行的主要思路是使用符號(hào)替代具體的數(shù)值作為程序的輸入，模擬程序的執(zhí)行，通過(guò)收集、求解路徑中的條件表達(dá)式來(lái)研究程序的狀態(tài)和性質(zhì).隨著程序規(guī)模的增大，其狀態(tài)搜索空間呈指數(shù)增長(zhǎng)，同時(shí)大量冗余的執(zhí)行分支以及因?yàn)榧s束求解器的分析性能導(dǎo)致的路徑遺漏等問(wèn)題嚴(yán)重影響了分析的效果.為了緩解狀態(tài)空間爆炸帶來(lái)的影響，狀態(tài)合并[2]作為目前主要的分析方法得到了廣泛的應(yīng)用，它通過(guò)分析不同路徑的符號(hào)表達(dá)式在合并點(diǎn)的狀態(tài)來(lái)研究各種合并策略[2-5].SMART[2]通過(guò)計(jì)算程序的函數(shù)摘要的方法生成測(cè)試用例集，并使用輔助變量來(lái)對(duì)不同路徑的符號(hào)狀態(tài)進(jìn)行合并.MergePoint[3]采用符號(hào)執(zhí)行和狀態(tài)合并的搜索方法，狀態(tài)合并的操作只能在沒有函數(shù)調(diào)用、跳轉(zhuǎn)語(yǔ)句的程序中才能使用.SMASH[4]使用不可達(dá)分析的方法對(duì)程序狀態(tài)進(jìn)行分析，并刪除與需求不相關(guān)的執(zhí)行路徑.這幾種方法都在函數(shù)調(diào)用時(shí)引入了輔助變量，它會(huì)增加符號(hào)變量分析的難度，從而進(jìn)一步制約了約束求解器的求解性能[5].ROSSETTE[6]使用減少輔助變量引入的方法對(duì)狀態(tài)合并展開分析，但該方法只能適用于對(duì)等的數(shù)據(jù)結(jié)構(gòu).對(duì)于狀態(tài)空間中的冗余狀態(tài)以及不可達(dá)狀態(tài)，主要通過(guò)分析當(dāng)前狀態(tài)是否出現(xiàn)在之前的分析結(jié)果中，以及將狀態(tài)空間分解為若干獨(dú)立的子空間的方法進(jìn)行研究.JPF[7]使用狀態(tài)匹配的方法減少狀態(tài)規(guī)模，Boonstoppel等人[8]使用讀寫集的方法來(lái)簡(jiǎn)化狀態(tài)匹配條件.文獻(xiàn)[9-10]使用程序切片的方法對(duì)狀態(tài)空間進(jìn)行分組.函數(shù)摘要[11-12]作為一種靜態(tài)分析方法，主要對(duì)接口符號(hào)變量開展分析，該過(guò)程可以與別名分析、可達(dá)分析、指向分析等方法進(jìn)行協(xié)同工作.這些方法都存在對(duì)程序行為推理不夠精確的問(wèn)題.靜態(tài)單賦值(static single assignment, SSA)通過(guò)改變變量的下標(biāo)，獲得不同變量的定義，使得每個(gè)變量只有惟一的定義，同時(shí)每個(gè)變量只有一條定義-使用鏈，主要應(yīng)用于程序分析、編譯器優(yōu)化等領(lǐng)域[13].文獻(xiàn)[14]提出將變量轉(zhuǎn)換為守衛(wèi)符號(hào)表達(dá)式集合的符號(hào)執(zhí)行方法，但該方法并未分析路徑條件的順序?qū)s束求解的影響.文獻(xiàn)[15]基于程序輸出的符號(hào)將程序的執(zhí)行路徑進(jìn)行劃分，從而對(duì)回歸測(cè)試和程序版本進(jìn)行測(cè)試，該方法并沒有對(duì)路徑條件的表示形式進(jìn)行優(yōu)化，易導(dǎo)致約束求解器停止工作.文獻(xiàn)[16]通過(guò)分析缺陷的類型以及關(guān)聯(lián)的路徑，以計(jì)算不同上下文中危險(xiǎn)操作的覆蓋能力為目標(biāo)，使用符號(hào)執(zhí)行的分析方法來(lái)生成高效輸入.文獻(xiàn)[17]采用抽象引導(dǎo)的半形式化方法框架對(duì)候選狀態(tài)進(jìn)行評(píng)估，生成能夠覆蓋多個(gè)目標(biāo)狀態(tài)的狀態(tài)序列.文獻(xiàn)[18]從最短路徑、條件約束集概率和可達(dá)路徑數(shù)量的角度，通過(guò)推遲變量實(shí)例化的方法緩解路徑組合爆炸問(wèn)題.

Fig. 1 Symbolic execution tree圖1 符號(hào)執(zhí)行樹

針對(duì)狀態(tài)合并分析過(guò)程中由于輔助變量的引入帶來(lái)的約束求解困難問(wèn)題，以及路徑約束條件在求解過(guò)程中存在條件遺漏的問(wèn)題，本文以傳統(tǒng)的符號(hào)執(zhí)行樹為起點(diǎn)，以基本塊為單位對(duì)符號(hào)執(zhí)行樹進(jìn)行優(yōu)化表示，將相同的基本塊進(jìn)行合并，從形式上約簡(jiǎn)符號(hào)執(zhí)行樹的規(guī)模.在狀態(tài)合并過(guò)程中，將約束條件和目標(biāo)變量作為整體向目標(biāo)變量提供反饋信息，從而避免輔助變量的引入.在路徑條件的約束求解階段，本文以程序輸出語(yǔ)句為起點(diǎn)，采用逆向符號(hào)執(zhí)行和流敏感的數(shù)據(jù)流的分析方法，提取能夠改變輸出變量值的隱式語(yǔ)句集合，再通過(guò)對(duì)路徑約束條件的重新組合，使得約束條件在新的路徑分析過(guò)程中得以完整地保留，避免因約束條件丟失帶來(lái)的路徑搜索不完備的問(wèn)題.與傳統(tǒng)基于狀態(tài)合并的符號(hào)執(zhí)行方法相比，本文方法可以減少符號(hào)表達(dá)式和路徑約束條件的數(shù)量，同時(shí)在約束條件求解過(guò)程中有更高的分析精度.

2 符號(hào)執(zhí)行和狀態(tài)合并

符號(hào)執(zhí)行的基本思想是使用變量符號(hào)來(lái)代替具體的輸入值，模擬程序的執(zhí)行.這種抽象的分析方法相對(duì)于具體的執(zhí)行可以獲得更多的路徑信息，從而可以更加高效地生成測(cè)試用例，以及挖掘未執(zhí)行的路徑.

定義1. 路徑條件(path condition).對(duì)于一個(gè)程序P、一個(gè)測(cè)試輸入t，設(shè)π為P在t作用下的執(zhí)行路徑，其對(duì)應(yīng)的路徑條件φ是由π中的分支條件等信息組成的一階邏輯公式.

路徑條件的生成是符號(hào)執(zhí)行中的一個(gè)重要步驟，在程序的一次執(zhí)行過(guò)程中，當(dāng)遇到條件分支時(shí)，符號(hào)執(zhí)行工具會(huì)收集當(dāng)前的分支條件，并計(jì)算在t作用下的約束公式，該約束公式由該路徑中所有分支條件進(jìn)行連接得出.任何輸入只要符合t所對(duì)應(yīng)的路徑約束條件都會(huì)產(chǎn)生與t一致的執(zhí)行路徑.

對(duì)于圖1(a)所示的程序，傳統(tǒng)符號(hào)執(zhí)行所生成的符號(hào)執(zhí)行樹如圖1(b)所示.符號(hào)執(zhí)行在執(zhí)行過(guò)程中需要保存當(dāng)前的符號(hào)狀態(tài)：由符號(hào)表達(dá)式組成的變量，以及當(dāng)前路徑條件φ.當(dāng)執(zhí)行過(guò)程中遇到分支條件時(shí)，符號(hào)執(zhí)行工具使用可達(dá)的分支對(duì)應(yīng)的當(dāng)前路徑條件φ更新當(dāng)前的符號(hào)狀態(tài).

對(duì)于圖1(a)所示的程序，傳統(tǒng)的符號(hào)執(zhí)行采用符號(hào)值x0,y0,z0分別替代輸入變量x,y,z.對(duì)于圖1(b)所示的每條執(zhí)行路徑，符號(hào)執(zhí)行會(huì)記錄該路徑所對(duì)應(yīng)的狀態(tài)，圖1(b)所對(duì)應(yīng)的狀態(tài)集合如表1所示.同時(shí)將圖1(b)轉(zhuǎn)換為圖1(c)所示的形式，即將相同的結(jié)點(diǎn)進(jìn)行合并，可以有效減少執(zhí)行路徑集合中結(jié)點(diǎn)存儲(chǔ)的次數(shù)，第3節(jié)的分析也是基于轉(zhuǎn)換后的符號(hào)執(zhí)行樹.

Table 1 State Set of Symbolic Execution表1 符號(hào)執(zhí)行狀態(tài)集合

Fig. 2 Potential dependent analysis圖2 隱式依賴分析

符號(hào)執(zhí)行在遇到新的路徑分支時(shí)，會(huì)將該路徑條件加入到狀態(tài)集合中，并依據(jù)路徑的可達(dá)性對(duì)各符號(hào)變量的值進(jìn)行更新.路徑條件φ可以表示為φ=φ1∨φ2∨φ3∨φ4∨φ5.由于符號(hào)執(zhí)行對(duì)于路徑的搜索依賴于路徑條件φ，即通過(guò)反轉(zhuǎn)最近新增的路徑條件符號(hào)的值來(lái)進(jìn)行，例如對(duì)于程序ifkthena=0.3 elsea=fun(b)，其符號(hào)執(zhí)行狀態(tài)可以表示為(k=k0)∧((k∧a=0.3)∨(k∧a=fun(b))).圖1(a)中的程序具有嵌套分支條件，可以產(chǎn)生類似的執(zhí)行狀態(tài).注意到表1中φ5所在的行對(duì)應(yīng)的輸入變量存在浮點(diǎn)數(shù)，在現(xiàn)實(shí)程序中除了浮點(diǎn)數(shù)以外，存在函數(shù)返回以及庫(kù)函數(shù)調(diào)用等方式對(duì)變量的賦值，目前的約束求解器在處理浮點(diǎn)數(shù)以及函數(shù)調(diào)用等類型的約束條件時(shí)，其分析性能受到很大限制.故這種符號(hào)執(zhí)行狀態(tài)表示方法在實(shí)際分析過(guò)程中，存在較高的概率使得約束求解器丟棄不能求解的約束條件，從而影響分析的精度.本文使用一種新的狀態(tài)表示方法，將狀態(tài)表達(dá)式中的路徑條件φ和輸入變量符號(hào)作為2個(gè)獨(dú)立的部分進(jìn)行表示，從而緩解因約束求解器性能而導(dǎo)致的求解不完備或中斷問(wèn)題，第3節(jié)將詳細(xì)分析該方法的工作過(guò)程.

逆向符號(hào)分析由于具有明確的分析目標(biāo)，故在路徑挖掘、程序調(diào)試等方向有廣泛的應(yīng)用.在逆向分析過(guò)程中，目標(biāo)語(yǔ)句一般選取最后一條表達(dá)式語(yǔ)句，也可以通過(guò)設(shè)置斷言的方法將某一可疑語(yǔ)句設(shè)為目標(biāo)語(yǔ)句.從目標(biāo)語(yǔ)句開始，對(duì)程序進(jìn)行逆向分析直到程序的入口語(yǔ)句，該過(guò)程中目標(biāo)語(yǔ)句可以表示為程序輸入的符號(hào)表達(dá)式，從而枚舉出與目標(biāo)語(yǔ)句相關(guān)的路徑條件表達(dá)式集合.

與目標(biāo)語(yǔ)句相關(guān)的符號(hào)分析方法可以精簡(jiǎn)地表示程序全部執(zhí)行路徑，該處用與目標(biāo)語(yǔ)句中變量b相關(guān)的3個(gè)符號(hào)表達(dá)式就可以概括圖2(a)的全部8條執(zhí)行路徑.依據(jù)程序輸出，將程序執(zhí)行路徑集合進(jìn)行分組，即2條執(zhí)行路徑π1，π2對(duì)應(yīng)的輸出符號(hào)有相同的表達(dá)式形式，則π1和π2有相同的關(guān)聯(lián)切片[19].關(guān)聯(lián)切片對(duì)數(shù)據(jù)依賴、控制依賴進(jìn)行傳遞閉包運(yùn)算.數(shù)據(jù)依賴和控制依賴依據(jù)執(zhí)行路徑π中修改目標(biāo)語(yǔ)句中變量值的語(yǔ)句集合進(jìn)行分析.

定義2. 直接依賴.設(shè)b1和b2為符號(hào)執(zhí)行樹中的2個(gè)結(jié)點(diǎn)，v為目標(biāo)語(yǔ)句中的變量，如果：

1)b1重新定義了變量v的值；

2)b2中的語(yǔ)句使用了變量v的值；

3)b1和b2之間存在一條可達(dá)路徑π，同時(shí)在π中的所有語(yǔ)句均沒有重定義變量v的值；

則稱b2直接依賴于b1.直接依賴是符號(hào)執(zhí)行樹中最常見的依賴形式，圖2(b)中實(shí)線表示2個(gè)結(jié)點(diǎn)存在直接依賴關(guān)系，但是在逆向符號(hào)執(zhí)行分析過(guò)程中，目標(biāo)語(yǔ)句中的變量在不同的執(zhí)行路徑π中會(huì)有不同的語(yǔ)句對(duì)其符號(hào)值進(jìn)行重定義，故存在如下定義:

定義3. 隱式依賴.對(duì)于程序P中的一條執(zhí)行路徑π，目標(biāo)語(yǔ)句為s，π中某條語(yǔ)句s′對(duì)應(yīng)的路徑條件為φ，稱s隱式依賴于s′，當(dāng)且僅當(dāng)以下條件成立:

1)s具有與φ一致的路徑條件sφ；

2)s中的變量v在π中的語(yǔ)句集合中都沒有被重新定義，但v在s與s′之間另一條路徑π′中被重定義了；

3) 通過(guò)反轉(zhuǎn)φ中某個(gè)邏輯公式的值，可以觸發(fā)新路徑π′的執(zhí)行.

定義4. 依賴條件(dependency condition).對(duì)于程序P中的一條執(zhí)行路徑π，目標(biāo)語(yǔ)句為s，π中某條語(yǔ)句s′對(duì)應(yīng)的路徑條件為φ，若s隱式依賴于s′，同時(shí)經(jīng)修改φ中若干分支謂詞表達(dá)式的真值，得到φ′，使得s與s′之間另一條路徑π′可達(dá)，則該分支謂詞φ′表達(dá)式構(gòu)成路徑π的依賴條件.

以圖2(a)所示的程序?yàn)槔?，?duì)比傳統(tǒng)符號(hào)執(zhí)行、傳統(tǒng)逆向分析和依賴條件分析在路徑條件φ表達(dá)方面的區(qū)別.設(shè)圖2(a)所示的程序的一組輸入為{x=6,y=2,z=2}，記語(yǔ)句④，⑧，⑩對(duì)應(yīng)的謂詞表達(dá)式分別為p1,p2,p3，它們?cè)诋?dāng)前輸入下的真值分別為true,false,true，對(duì)應(yīng)的執(zhí)行路徑π可以標(biāo)記為[p1,t,p2,f,p3,t].在當(dāng)前輸入值的作用下，傳統(tǒng)符號(hào)執(zhí)行的路徑條件為(x-y>0)∧(x+y>10)∧(z×z>3).對(duì)于傳統(tǒng)逆向分析，以語(yǔ)句為目標(biāo)語(yǔ)句進(jìn)行逆向分析，由于p2的真值為false，故語(yǔ)句⑨沒有對(duì)目標(biāo)語(yǔ)句中的符號(hào)變量b進(jìn)行重定義操作，此時(shí)與符號(hào)變量b相關(guān)的路徑為[,②]，p1,p2,p3均不出現(xiàn)在該路徑條件中，故逆向分析的路徑條件為true.依賴條件分析在收集路徑條件的過(guò)程中，加入了流敏感的數(shù)據(jù)流分析方法，故可以通過(guò)“定義-使用鏈”分析來(lái)提取對(duì)變量b有重定義操作的符號(hào)語(yǔ)句位置，這些對(duì)目標(biāo)變量有隱式作用的語(yǔ)句集合S′成為隱式依賴分析的依據(jù)，在p1,p2,p3的取值過(guò)程中，通過(guò)修改部分謂詞表達(dá)式的真值能夠?qū)崿F(xiàn)對(duì)S′可達(dá)，則這些謂詞表達(dá)式構(gòu)成目標(biāo)語(yǔ)句的依賴條件.本例中若p2的當(dāng)前真值經(jīng)修改為true，則語(yǔ)句⑨對(duì)目標(biāo)語(yǔ)句中的符號(hào)變量b有重定義操作，從而改變程序的輸出結(jié)果，此時(shí)逆向分析的路徑為[,⑧,②]，對(duì)應(yīng)的依賴條件為(x+y>10).只要輸入符合該依賴條件，則可以使目標(biāo)語(yǔ)句中的符號(hào)變量b有相同的符號(hào)表達(dá)式.

基于路徑條件的程序分析主要用來(lái)提高語(yǔ)句或者分支的覆蓋率.隱式依賴分析可以將程序的輸入符號(hào)以及依賴條件與目標(biāo)語(yǔ)句中的變量符號(hào)進(jìn)行關(guān)聯(lián)，對(duì)于依賴條件φ1∧φ2∧…∧φn,每次路徑分析時(shí)通過(guò)取反最近加入的條件表達(dá)式來(lái)獲取不同的路徑，即通過(guò)約束求解器對(duì)集合{φ1∧φ2∧…∧φi|1≤i≤n}的可滿足性進(jìn)行分析，若某個(gè)路徑條件可解，則將其從集合中刪除，當(dāng)集合為空時(shí)分析結(jié)束.對(duì)于程序2(a)以及一組輸入{x=6,y=2,z=2}，其路徑分析過(guò)程如表2所示：

Table 2 Paths Analysis Based on Dependent Condition表2 基于依賴條件的路徑分析

3 符號(hào)簽名與依賴條件重構(gòu)

經(jīng)過(guò)第2節(jié)的分析可以將一段程序生成精簡(jiǎn)的符號(hào)執(zhí)行樹，并在其基礎(chǔ)上進(jìn)行路徑條件的生成以及路徑搜索操作，從而提高語(yǔ)句和分支覆蓋率.但在上述分析過(guò)程中存在2個(gè)問(wèn)題：

1) 現(xiàn)有的路徑條件中常包含較為復(fù)雜的數(shù)據(jù)結(jié)構(gòu)和方法調(diào)用，這種表示形式對(duì)于主流的約束求解器難以求解，故約束求解器需要?jiǎng)h除某些不能求解的邏輯公式從而保持求解過(guò)程的連續(xù)性，但這種直接刪除的邏輯公式往往包含關(guān)鍵的路徑信息，從而使得求解的結(jié)果不完備.

2) 新路徑的生成需要對(duì)依賴分析后的路徑條件進(jìn)行增量修改，但在增量修改過(guò)程中存在部分約束表達(dá)式丟失的現(xiàn)象.其原因是約束求解器在增量求解過(guò)程中，對(duì)依賴條件產(chǎn)生的輸入符號(hào)可能與之前增量過(guò)程所產(chǎn)生的輸入符號(hào)相同，導(dǎo)致該依賴條件在下一步的增量分析中被刪除，這種間接刪除的邏輯公式會(huì)屏蔽部分新路徑的發(fā)掘，從而對(duì)約束求解器的分析精度產(chǎn)生影響.

對(duì)于第1個(gè)問(wèn)題，本文使用符號(hào)簽名的方法，使用新的路徑條件表示形式，將路徑條件中目標(biāo)語(yǔ)句包含的符號(hào)表達(dá)式抽出，從而避免狀態(tài)合并中輔助變量對(duì)于約束求解器的干擾，提高約束求解器的執(zhí)行效率.對(duì)于第2個(gè)問(wèn)題，本文提出依賴條件的優(yōu)化表示算法，減少因間接刪除邏輯公式所產(chǎn)生的影響.

3.1 符號(hào)簽名

符號(hào)執(zhí)行的方法在一次計(jì)算過(guò)程中，對(duì)每個(gè)變量只保存一個(gè)符號(hào)表達(dá)式，故在狀態(tài)合并時(shí)，對(duì)于在多次執(zhí)行過(guò)程中有多個(gè)符號(hào)表達(dá)式的變量，需要引入輔助變量來(lái)代替該變量的符號(hào)表達(dá)式.例如對(duì)于圖1(a)中語(yǔ)句⑥，對(duì)應(yīng)的符號(hào)執(zhí)行狀態(tài)如表3所示，由于變量z在3條路中有不同的符號(hào)表達(dá)式(z0,2.5)，則在狀態(tài)合并時(shí)，需要引入輔助變量z′來(lái)表示[14]，如表4所示，狀態(tài)合并后的路徑條件φ為每條路徑對(duì)應(yīng)的路徑條件與當(dāng)前變量z的符號(hào)值的合取操作進(jìn)行析取.

若基于表4的結(jié)果進(jìn)行約束求解，由于路徑條件中存在諸如z′=2.5這樣帶有浮點(diǎn)數(shù)運(yùn)算的表達(dá)式，則約束求解器在計(jì)算過(guò)程中可能受制于求解能力而導(dǎo)致狀態(tài)合并失敗，故下面給出在不影響路徑條件邏輯含義的基礎(chǔ)上刪除輔助變量的方法.對(duì)于圖1(a)的程序，其符號(hào)執(zhí)行的最終狀態(tài)如表1所示.這種表示方法難以直觀地獲得每個(gè)變量對(duì)應(yīng)的符號(hào)值集合以及每個(gè)符號(hào)值對(duì)應(yīng)的約束條件.

Table 3 Example of Intermediate State (Statement ⑥ in

Table 4 Example of State Merging表4 狀態(tài)合并示例

對(duì)于一個(gè)程序P，其輸入變量集合為T(t1,t2,…,tm)，P的路徑條件集合記為Φ(Φ=φ1∨φ2∨…∨φn)，設(shè)某個(gè)輸入變量t(t∈T)在狀態(tài)合并點(diǎn)對(duì)應(yīng)的符號(hào)值集合為V(V=v1∨v2∨…∨vi)，則有如下定義.

定義5[14]. 符號(hào)簽名(symbol signature).令某個(gè)符號(hào)表達(dá)式vk對(duì)應(yīng)的路徑條件Φv k為：

{φx∨φy∨…∨φz|1

例如對(duì)于圖1(a)的程序，依據(jù)表1所示的狀態(tài)表和符號(hào)簽名的定義，可以將其轉(zhuǎn)換為符號(hào)簽名視圖[14]，該視圖反映了圖1(a)中語(yǔ)句⑧位置經(jīng)狀態(tài)合并后程序的最終狀態(tài)：

(1)

注意式(1)中沒有輔助變量，且邏輯上與含有輔助變量的狀態(tài)一致.下面分析式(1)的產(chǎn)生過(guò)程.首先對(duì)于圖1(a)中的狀態(tài)合并點(diǎn)語(yǔ)句⑥，語(yǔ)句①～⑥對(duì)應(yīng)的符號(hào)執(zhí)行狀態(tài)如表3所示.

對(duì)于即將執(zhí)行的語(yǔ)句⑥，其邏輯表達(dá)式z>2需要進(jìn)行運(yùn)算以求出下一個(gè)合并點(diǎn)，即語(yǔ)句⑧處的符號(hào)簽名視圖.對(duì)于變量z對(duì)應(yīng)的符號(hào)表達(dá)式z0和2.5，進(jìn)行z>2的運(yùn)算，即此時(shí)語(yǔ)句⑥對(duì)應(yīng)的符號(hào)簽名為{(φ5,z0>2),(φ5,2.5>2)}，由于 (2.5>2)恒為真，故可以表示為{(φ5,z0>2),(φ5,true)}.此時(shí)語(yǔ)句⑥對(duì)應(yīng)的路徑條件為φ6=(φ5∧z0>2)∨(φ5∧true).

當(dāng)φ6可滿足時(shí)語(yǔ)句⑦可達(dá)，此時(shí)的y=z-1運(yùn)算存在對(duì)變量y的重定義，變量y在目標(biāo)語(yǔ)句⑧處對(duì)應(yīng)的符號(hào)簽名為：y={(φ6,y0),(φ5∧φ6,z0-1),(φ5∧φ6,1.5)}，這和式(1)中的y的符號(hào)簽名在邏輯上是等價(jià)的.此時(shí)依據(jù)前一個(gè)狀態(tài)合并點(diǎn)的符號(hào)執(zhí)行狀態(tài)信息和符號(hào)簽名信息，計(jì)算出程序最終狀態(tài)的符號(hào)簽名信息，這與依據(jù)程序最終狀態(tài)的符號(hào)執(zhí)行狀態(tài)獲得的簽名信息在邏輯上是一致的.

這種符號(hào)簽名視圖可以直觀地獲得每個(gè)輸入變量在合并點(diǎn)處的符號(hào)值以及對(duì)應(yīng)的路徑條件，對(duì)于表2中不同的符號(hào)值，采用灰色背景進(jìn)行標(biāo)記.符號(hào)簽名的特點(diǎn)如下.

1) 對(duì)于某個(gè)符號(hào)表達(dá)式的符號(hào)簽名vs，設(shè)(φ1,v1)和(φ2,v2)是vs中的2個(gè)不同元素，若v1=v2，則這2個(gè)元素可以合并為(φ1∨φ2,v1)，且此時(shí)的符號(hào)簽名等價(jià)于vs{(φ1,v1),(φ2,v2)}∪{φ1∨φ2,v1}；

2) 如果vs中存在形如(false,v)的元素，則可以將其從vs中刪除.

符號(hào)簽名的表示形式相對(duì)于傳統(tǒng)符號(hào)執(zhí)行的狀態(tài)表示形式，其最大優(yōu)點(diǎn)在于不同執(zhí)行路徑的路徑條件表達(dá)式和變量的符號(hào)表達(dá)式，在符號(hào)簽名中的表達(dá)形式中可以共享，例如在圖1(a)中語(yǔ)句⑥處，傳統(tǒng)符號(hào)執(zhí)行依據(jù)路徑條件有3條不同的執(zhí)行路徑，但通過(guò)符號(hào)簽名分析，可以獲得在此處變量z的2個(gè)不同符號(hào)值(r0,2.5)，從而減少對(duì)約束求解器的調(diào)用次數(shù).

本文將變量符號(hào)與符號(hào)簽名之間建立起關(guān)聯(lián)，使用符號(hào)簽名的常用符號(hào)執(zhí)行語(yǔ)義[14]表示如圖3所示：

Binary Operation:

Condition Operation:

Fig. 3 Symbol execution semantic
圖3 符號(hào)執(zhí)行語(yǔ)義

其中v1⊙v2表示對(duì)2個(gè)符號(hào)簽名v1和v2進(jìn)行合并操作，但與普通的合并運(yùn)算的區(qū)別于v1⊙v2還進(jìn)行重復(fù)的路徑條件和約束表達(dá)式的共享，從而減少對(duì)求解器的調(diào)用.更新操作主要使用⊙運(yùn)算符進(jìn)行運(yùn)算，其中當(dāng)路徑條件φ可滿足時(shí)，則將符號(hào)簽名v1作用于后續(xù)路徑中的符號(hào)簽名，當(dāng)φ可滿足時(shí)，將v2作用于后續(xù)路徑中的符號(hào)簽名.當(dāng)存在對(duì)變量符號(hào)進(jìn)行賦值操作時(shí)，常量操作和符號(hào)輸入操作對(duì)該變量符號(hào)值進(jìn)行更新，該過(guò)程中⊙運(yùn)算只對(duì)滿足路徑條件φ的執(zhí)行路徑中的賦值操作進(jìn)行運(yùn)算.二元運(yùn)算主要對(duì)2個(gè)符號(hào)變量(a,b)間存在二元運(yùn)算符時(shí)進(jìn)行操作，運(yùn)算結(jié)果為變量a的符號(hào)表達(dá)式與變量b的符號(hào)表達(dá)式的笛卡兒積.在條件運(yùn)算中，當(dāng)條件表達(dá)式e可滿足時(shí)，則對(duì)e和后續(xù)可達(dá)語(yǔ)句s的各自符號(hào)簽名進(jìn)行笛卡兒積運(yùn)算，并將e對(duì)應(yīng)的符號(hào)表達(dá)式并入到當(dāng)前的路徑條件中，當(dāng)e不可滿足時(shí)，則需要對(duì)x的每個(gè)符號(hào)簽名中的符號(hào)變量進(jìn)行分析.

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

對(duì)于程序的一次執(zhí)行，傳統(tǒng)的路徑發(fā)掘方法具有如下性質(zhì)：如果φ1∧φ2∧…∧φn為該執(zhí)行對(duì)應(yīng)路徑條件的一個(gè)前綴，則滿足條件φ1∧φ2∧…∧φn的輸入，其對(duì)應(yīng)的路徑條件均以φ1∧φ2∧…∧φn為前綴.通過(guò)第2節(jié)分析，該性質(zhì)對(duì)于依賴條件不成立.由于依賴條件dc在邏輯上要弱于路徑條件pc，即φ?dc，故對(duì)于依賴條件所具有的性質(zhì)：如果φ1∧φ2∧…∧φn為程序一次執(zhí)行對(duì)應(yīng)依賴條件的一個(gè)前綴，則滿足條件φ1∧φ2∧…∧φn的輸入，其對(duì)應(yīng)的依賴條件均以φ1∧φ2∧…∧φn為前綴，由于φ?dc，此時(shí)該性質(zhì)也適用于路徑條件.

導(dǎo)致依賴信息丟失的原因是依賴條件的表示方法，為了能夠獲得遺漏路徑的依賴條件，需要將現(xiàn)有的依賴條件表示方法進(jìn)行修改，即采用依賴條件重構(gòu)的方法對(duì)目前的依賴條件進(jìn)行重新排序.依賴條件重構(gòu)的算法[15]如下所示.

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

輸入:程序P、測(cè)試集t、目標(biāo)語(yǔ)句C;

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

①Stack=?;

② 執(zhí)行函數(shù)Execute(t,0);

③ whileStack≠?

④ 將pop(Stack)的值賦給(f,j);

⑤ iff不能被滿足

⑥a是一個(gè)可以滿足f的輸入;

⑦ 將a賦值給T;

⑧ 執(zhí)行函數(shù)Execute(a,j);

⑨ end if

⑩ end while

其中函數(shù)Reorder( )用來(lái)對(duì)現(xiàn)有的依賴條件序列進(jìn)行重構(gòu)，其工作過(guò)程類似于快速排序算法.對(duì)于由多個(gè)邏輯表達(dá)式序列seq組成的待重組的依賴條件dc，該算法依據(jù)最近加入的條件表達(dá)式e將待重組的序列seq分解為2個(gè)子序列seq1和seq2，seq中與e存在隱式依賴的邏輯表達(dá)式依據(jù)seq中的相對(duì)順序存放到seq1中，對(duì)應(yīng)地將seq中與e不存在隱式依賴的邏輯表達(dá)式依據(jù)seq中的相對(duì)順序存放到seq2中，并將e存入到一個(gè)棧Stack中.然后分別對(duì)seq1和seq2重復(fù)上述過(guò)程，直到棧Stack=?，最后程序輸出為重組后的路徑分支表達(dá)式.圖4表示該算法的執(zhí)行過(guò)程[15].其中圖4(a)表示待重組的序列seq中邏輯表達(dá)式之間的隱式依賴關(guān)系，其中每個(gè)邏輯表達(dá)式用一個(gè)結(jié)點(diǎn)表示，例如e6→e1，則表示e6隱式依賴于e1.初始時(shí)，由于e6與其他結(jié)點(diǎn)存在隱式依賴關(guān)系，故將e6存入棧Stack中，并以e6為中心結(jié)點(diǎn)，將其余結(jié)點(diǎn)依據(jù)是否存在依賴關(guān)系依據(jù)原始相對(duì)順序移到e6兩側(cè).由于e1和e3均與e6存在隱式依賴，故將e1和e3依據(jù)原始序列seq中的順序存放到e6左側(cè)，記為seq1，e2，e5，e6則存放到e6右側(cè)，記為seq2.然后分別對(duì)seq1和seq2重復(fù)上述過(guò)程，直到棧Stack=?，此時(shí)重構(gòu)后的依賴條件序列.當(dāng)每次從棧Stack中彈出一個(gè)依賴條件，函數(shù)Execute( )需要對(duì)該依賴條件的可滿足性進(jìn)行分析，若該依賴條件可解，則可以計(jì)算出對(duì)應(yīng)的輸入i，該輸入i可以生成新的依賴條件，并對(duì)該依賴條件進(jìn)行分析.為了提高分析速度，在函數(shù)Execute( )的參數(shù)中加入了一個(gè)參數(shù)n，該參數(shù)用以指示分析從當(dāng)前序列第n個(gè)結(jié)點(diǎn)開始，如該節(jié)開頭分析，前n個(gè)結(jié)點(diǎn)的作為前綴時(shí)，分析結(jié)果能夠得以傳遞到下一次迭代分析中，從而提高分析的速度.在表2的分析結(jié)果基礎(chǔ)上，算法1的執(zhí)行步驟如表5所示，其中第3個(gè)函數(shù)中生成了表2中未能發(fā)掘的路徑[p1,f,p2,t,p3,t]，如表5中灰色背景標(biāo)記所示.

Fig. 4 Example of dependent condition reconstruction圖4 依賴條件重組示例

StepInputPathDependency ConditionDependency Condition After Reconstruction1{x=6,y=2,z=2}[p1,t,p2,f,p3,t](x+y>10)(x+y>10)2{x=6,y=5,z=2}[p1,t,p2,t,p3,t](x-y>0)∧(x+y>10)(x+y>10)∧(x-y>0)3{x=5,y=6,z=2}[p1,f,p2,t,p3,t](x-y>0)∧(x+y>10)(x+y>10)∧(x-y>0)

通過(guò)符號(hào)簽名的分析方法對(duì)路徑條件的表示形式進(jìn)行修改，并在此基礎(chǔ)上使用依賴條件重組算法對(duì)路徑中的依賴關(guān)系進(jìn)行分析，可以有效減少傳統(tǒng)符號(hào)執(zhí)行方法和狀態(tài)合并方法因直接刪除或間接刪除路徑條件所帶來(lái)的分析精度上的損失.

定理1. 對(duì)于程序P對(duì)應(yīng)的2個(gè)輸入t1和t2，ti(i=1,2)對(duì)應(yīng)的執(zhí)行路徑為π(ti)，設(shè)s是π(t1)中的一條語(yǔ)句，但s不在π(t2)中.設(shè)b為π(t1)中的最后一個(gè)分支條件，且有sb，同時(shí)b也在π(t2)中，此時(shí)b在π(t1)和π(t2)中有不同的表達(dá)形式.

證明. 采用反證法.依據(jù)已有條件sb，設(shè)b′→b為π(t1)中從s到b的路徑中的最后一個(gè)連接，此時(shí)有sb′→b.此時(shí)假設(shè)b在π(t1)和π(t2)中有相同的表達(dá)形式，則b同樣也在路徑π(t2)中，故在π(t2)中b也滿足sb，即b也出現(xiàn)在路徑π(t2)中，這與定理中b為π(t1)中的最后一個(gè)滿足sb分支條件的條件相矛盾，故b在π(t1)和π(t2)中有不同的表達(dá)形式.

證畢.

定理2. 對(duì)于程序P對(duì)應(yīng)的2個(gè)輸入t1和t2，ti(i=1,2)對(duì)應(yīng)的執(zhí)行路徑為π(ti)，設(shè)s是π(t1)中的一條語(yǔ)句，若t2=dc(s,π(t1))，則s是路徑π(t2)中一條語(yǔ)句.

證明. 設(shè)si和sj是2條有先后順序的語(yǔ)句，即si→sj，則由sj和π(t1)共同決定的路徑π(sj,π(t1))中的語(yǔ)句都會(huì)包含在由si和π(t1)共同決定的路徑π(sj,π(t1))中，故dc(si,π(t1))?dc(sj,π(t1)).因t2dc(si,π(t1))，故t2dc(sj,π(t1))，從而sj將包含在π(t1)和π(t2)中，即任意的si是路徑π(t2)中一條語(yǔ)句.

證畢.

定理1使得依賴條件可以確保在目標(biāo)語(yǔ)句中，每個(gè)符號(hào)變量只有惟一的符號(hào)值.定理2使得對(duì)于一個(gè)可達(dá)路徑π，本文方法可以發(fā)掘一條路徑π′，使得π′和π有相同的依賴條件.

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

本文在WALA平臺(tái)上構(gòu)建實(shí)驗(yàn)原型系統(tǒng)，該平臺(tái)可以讀取待分析的程序，構(gòu)建程序調(diào)用圖和控制流圖，同時(shí)采用Z3作為約束求解器，對(duì)線性約束表達(dá)式和字符串進(jìn)行求解操作.Java語(yǔ)言由于具有動(dòng)態(tài)類型，使得變量在分析過(guò)程中可以方便地替換為符號(hào)表達(dá)式或者具體的數(shù)值，故本文以Java程序?yàn)闇y(cè)試集.實(shí)驗(yàn)方案如圖5所示:

Fig. 5 Experimental setup圖5 實(shí)驗(yàn)方案

依賴條件是在逆向符號(hào)執(zhí)行過(guò)程中生成的.對(duì)于目標(biāo)語(yǔ)句中的符號(hào)變量，主要分析與其有重定義操作的語(yǔ)句集合.實(shí)驗(yàn)以狀態(tài)合并和符號(hào)執(zhí)行作為分析工具，主要實(shí)驗(yàn)內(nèi)容包括：對(duì)比傳統(tǒng)狀態(tài)合并方法和本文方法在狀態(tài)合并上的數(shù)量，以及相對(duì)于傳統(tǒng)符號(hào)執(zhí)行方法，本文方法在發(fā)掘可行的隱式路徑數(shù)量上性能的提升.同時(shí)驗(yàn)證了路徑條件和符號(hào)表達(dá)式的共享在符號(hào)簽名的分析方法中的有效性.

表6中“符號(hào)簽名均值”表示程序中各符號(hào)變量在不同路徑中對(duì)應(yīng)的不同符號(hào)表達(dá)式個(gè)數(shù)的平均值，符號(hào)簽名的平均值不超過(guò)6.該值越小，表明程序變量間的隱式依賴數(shù)量越少.“符號(hào)簽名共享比率”表示達(dá)到目標(biāo)位置的不同路徑的數(shù)量與該目標(biāo)位置的符號(hào)簽名個(gè)數(shù)的比值，表明路徑表達(dá)式和符號(hào)表達(dá)式在不同路徑中存在相同的前綴，故在新路徑發(fā)掘過(guò)程中，可以有效利用相同的前綴從而減少重復(fù)分析帶來(lái)的額外計(jì)算開銷.“傳統(tǒng)合并方法合并程度”表示對(duì)當(dāng)前程序進(jìn)行傳統(tǒng)合并方式與本文方法在狀態(tài)合并數(shù)量上的比值.從表6中可以看出除了3個(gè)程序，本文方法在其余程序中均可以較傳統(tǒng)方法有更多的狀態(tài)合并.在進(jìn)行符號(hào)執(zhí)行過(guò)程中，本文方法相對(duì)于傳統(tǒng)的符號(hào)執(zhí)行方法DART，均可以減少時(shí)間開銷.其中“有效路徑對(duì)比”表示傳統(tǒng)符號(hào)執(zhí)行方法所生成的路徑數(shù)量與本文方法所生成的路徑數(shù)量的比值，由于本文方法采用了符號(hào)簽名和依賴條件重組的分析方法，能夠有效減少因直接刪除和間接刪除依賴條件所導(dǎo)致的路徑分析精度上的損失.約束求解器在程序分支條件處需要對(duì)當(dāng)前的分支條件表達(dá)式進(jìn)行求解，由于約束求解器在計(jì)算過(guò)程中有較大的時(shí)間開銷，故在實(shí)際分析過(guò)程中需要盡可能減少約束求解器的調(diào)用次數(shù).“求解次數(shù)比率”表示傳統(tǒng)符號(hào)執(zhí)行方法與本文方法在調(diào)用約束求解器時(shí)數(shù)量的對(duì)比.由于采用了共享路徑條件和符號(hào)表達(dá)式的分析方法，故本文方法能夠較少地調(diào)用約束求解器.

Table 6 Comparison of State Merging and Symbolic Execution表6 狀態(tài)合并和符號(hào)執(zhí)行的對(duì)比

Fig. 6 Comparison of path coverage圖6 路徑覆蓋率對(duì)比

為了對(duì)比在路徑發(fā)掘方面的效率，本文以表6中規(guī)模最大的3個(gè)程序?yàn)槔?，?shí)驗(yàn)結(jié)果如圖6所示:

本文方法使用了基于依賴條件重組的路徑分析方法，相對(duì)于傳統(tǒng)符號(hào)執(zhí)行方法可以發(fā)掘更多的可達(dá)路徑.本文方法較傳統(tǒng)符號(hào)執(zhí)行方法在路徑覆蓋率方面有較大提高，但沒有達(dá)到100%，其原因是對(duì)于程序執(zhí)行語(yǔ)義的建模精度還有待提高，尤其是對(duì)于數(shù)組下表、內(nèi)存地址訪問(wèn)、循環(huán)終止條件等符號(hào)表達(dá)式的處理還有待進(jìn)一步完善.另一個(gè)原因是約束求解器的性能對(duì)于依賴條件的求解有直接的影響，雖然本文采用路徑條件和變量符號(hào)分離的表示方法來(lái)提高約束求解器的求解性能，但同樣由于數(shù)組下表等復(fù)雜數(shù)據(jù)結(jié)構(gòu)的影響，在一定程度上影響了路徑的覆蓋率，這是本文將來(lái)主要的研究工作.對(duì)于程序中一條具有n個(gè)分支條件的執(zhí)行路徑，本文的方法需要約束求解器對(duì)該路徑對(duì)應(yīng)的依賴條件進(jìn)行n次分析，另外不同執(zhí)行路徑的依賴條件之間有相似性，將來(lái)工作中可以采用并行符號(hào)執(zhí)行的方法以提高這2個(gè)過(guò)程的分析效率.

5 結(jié)束語(yǔ)

符號(hào)執(zhí)行是路徑分析中的傳統(tǒng)方法，但狀態(tài)空間爆炸和約束求解器性能嚴(yán)重制約了其性能的發(fā)揮.狀態(tài)合并作為一種有效的狀態(tài)約簡(jiǎn)方法得到了廣泛的應(yīng)用，但因路徑條件的表示形式影響了約束求解器求解的性能.本文采用一種基于改進(jìn)符號(hào)執(zhí)行樹的分析方法，在其基礎(chǔ)上通過(guò)分離路徑條件和符號(hào)表達(dá)式，從而可以提高約束求解器的求解性能而提高狀態(tài)合并的效率.在約束求解器的求解過(guò)程中，本文還提出了基于依賴條件的重構(gòu)算法，從而避免因路徑條件的直接刪除和間接刪除所導(dǎo)致的路徑分析不夠完備的問(wèn)題.如實(shí)驗(yàn)部分所述，本文方法在路徑分析的性能方面較傳統(tǒng)方法有較大提高，但由于對(duì)程序中數(shù)組下標(biāo)、地址解析等復(fù)雜結(jié)構(gòu)執(zhí)行語(yǔ)義建模還不夠精確，故影響了路徑覆蓋率的進(jìn)一步提升.將來(lái)的工作中主要是復(fù)雜數(shù)據(jù)結(jié)構(gòu)語(yǔ)義建模，例如可以加入靜態(tài)單賦值(SSA)的分析方法，減少路徑條件分析時(shí)引入臨時(shí)變量的數(shù)量及變量間命名的沖突，從而可以構(gòu)建更為精確的路徑條件.