基于變量符號關聯(lián)分析的程序狀態(tài)優(yōu)化方法

郭曦，王盼

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

1 引言

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

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

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

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

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

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

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

2 相關研究進展

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

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

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

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

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

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

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

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

圖1 程序片段及對應的符號執(zhí)行樹

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

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

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

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

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

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

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

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

圖2 隱式依賴分析

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

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

定義2 間接依賴。設s為程序P中的目標語句，P存在一條可達路徑π，s′為π中的一條語句，φ為其對應的路徑條件，若s與s′存在間接依賴關系，則有如下條件成立。

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

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

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

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

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

表2 當程序輸入為x=6, y=2, z=2時的路徑分析過程

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

4 符號條件重構算法

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

4.1 符號簽名

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

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

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

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

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

4.2 依賴條件重構

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

算法1 依賴條件重構算法

輸入 程序P，測試集t，目標語句C

輸出 重構后的依賴條件

1) 棧Stack為空;

2) Procedure Execute(t, n)

3) 計算關于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的長度為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(…)的作用是對依賴條件分析順序進行重構，它通過加入最新的路徑條件從而將當前的路徑序列seq劃分為seq1和seq2這2個子序列，seq與最新加入的路徑條件之間有間接依賴關系，依據(jù)seq中條件的順序?qū)eq與最新加入的路徑條件進行重構并存儲在seq1中，類似地，將seq與最新加入的路徑條件之間沒有間接依賴關系的放在 seq2中。然后對 seq1和 seq2分別再次進行該操作，當原路徑條件集合為空時，算法停止工作并得到重構后的路徑表達式。通過依賴條件重構分析，可以提高路徑條件分析的精度。

5 實驗及分析

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

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

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

圖4 實驗流程

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

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

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

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

所以可以通過泰勒級數(shù)的系數(shù)來決定與指定長度n相關的路徑數(shù)量，例如，該處g(z)的系數(shù)構成了圖5中path(n)對應的數(shù)值。對于給定的CFG，可以

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

其中，(I ?zT ):|N |,1表示從行列式I?zT中刪除第|N |行和第1列，函數(shù)det(…)用來計算參數(shù)的行列式。圖5程序?qū)木仃嚍?/p>

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

因此有

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

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

表4 復雜度表示形式對比

6 結(jié)束語

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