蔣 剛,李兆鵬

1(中國(guó)科學(xué)技術(shù)大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,合肥 230026) 2(中國(guó)科學(xué)技術(shù)大學(xué) 先進(jìn)技術(shù)研究院 中國(guó)科大—國(guó)創(chuàng)高可信軟件工程中心,合肥 230027)

1 引 言

隨著當(dāng)今計(jì)算機(jī)技術(shù)的飛速發(fā)展,在航空航天、醫(yī)療等安全攸關(guān)領(lǐng)域高可信軟件的需求與日俱增,提高軟件的可靠性和安全性是軟件開(kāi)發(fā)中所追求的目標(biāo)之一,目前確保軟件安全質(zhì)量的方法有程序驗(yàn)證,動(dòng)態(tài)測(cè)試和靜態(tài)分析.程序驗(yàn)證作為保證程序正確性的嚴(yán)格手段,通過(guò)形式化方法如霍爾邏輯[1]、分離邏輯[2]等對(duì)程序中的各種性質(zhì)給出嚴(yán)格的數(shù)學(xué)證明,從而保證程序的高可靠性,程序驗(yàn)證目前還未實(shí)現(xiàn)完全的自動(dòng)化證明,需要大量的人工輔助證明,因此未能在工業(yè)界得到廣泛應(yīng)用.程序動(dòng)態(tài)測(cè)試在實(shí)踐中具有廣泛的應(yīng)用,它提供了程序運(yùn)行時(shí)的檢查,但是其精確性和覆蓋率依賴于給定的測(cè)試集,缺少良好的測(cè)試集,將導(dǎo)致高漏報(bào)率和低覆蓋率,而且運(yùn)行時(shí)的檢查成本和風(fēng)險(xiǎn)相對(duì)較高.靜態(tài)分析技術(shù)不需要運(yùn)行程序,是對(duì)代碼進(jìn)行分析,與形式化驗(yàn)證相比,靜態(tài)分析能自動(dòng)分析程序中的相關(guān)信息,與動(dòng)態(tài)測(cè)試相比,靜態(tài)分析可以以較低的成本更早地發(fā)現(xiàn)程序中的缺陷.

目前較為成熟的靜態(tài)分析技術(shù)有模型檢測(cè)[3]、抽象解釋[4]、數(shù)據(jù)流分析[5]和符號(hào)執(zhí)行[6].其中符號(hào)執(zhí)行被廣泛用于測(cè)試?yán)淖詣?dòng)生成[7],它的主要思想是對(duì)代碼中變量的取值進(jìn)行符號(hào)化,使用一定的執(zhí)行策略,以帶約束的符號(hào)值代替程序變量運(yùn)行時(shí)的具體值,較為精確地模擬程序的執(zhí)行過(guò)程,從而達(dá)到分析的高覆蓋率,得到較精確的分析結(jié)果.符號(hào)執(zhí)行技術(shù)對(duì)路徑敏感,模擬執(zhí)行程序時(shí)會(huì)嘗試所有可能的路徑,因此比動(dòng)態(tài)測(cè)試的覆蓋率高.另一方面,符號(hào)執(zhí)行隨著程序中控制結(jié)構(gòu)的增加,所需執(zhí)行的狀態(tài)數(shù)目呈指數(shù)級(jí)增長(zhǎng),會(huì)帶來(lái)路徑爆炸問(wèn)題,這嚴(yán)重制約了使用符號(hào)執(zhí)行技術(shù)的分析工具的可伸縮性.

隨著軟件的規(guī)模越來(lái)越大,要使符號(hào)執(zhí)行技術(shù)依然保持低漏報(bào)率、低誤報(bào)率并且具有良好的性能和可伸縮性成為一大挑戰(zhàn).目前筆者所在的課題組已實(shí)現(xiàn)一個(gè)基于開(kāi)源編譯框架LLVM[8]的符號(hào)執(zhí)行分析工具ShapeChecker[9],它的總體框架如圖1所示.

ShapeChecker是一個(gè)C程序靜態(tài)分析工具,首先源代碼經(jīng)由Clang編譯器翻譯成LLVM的中間表示(Intermediate Representation,簡(jiǎn)稱IR),ShapeChecker符號(hào)執(zhí)行引擎通過(guò)解析IR字節(jié)碼來(lái)分析程序,分析完畢后生成bug報(bào)告.

圖1 ShapeChecker的總體框架Fig.1 Framework of ShapeChecker

由于分析工具中的執(zhí)行引擎采用的是符號(hào)執(zhí)行的方法,在分析大規(guī)模程序時(shí),會(huì)降低工具的運(yùn)行效率.針對(duì)工具中符號(hào)執(zhí)行技術(shù)的不足,可采用程序切片的方法來(lái)提高工具的時(shí)間性能,即根據(jù)用戶的興趣點(diǎn)來(lái)專門檢測(cè)某一類或幾類缺陷,與關(guān)心的缺陷無(wú)關(guān)的代碼可被切除不分析,這樣在一定程度上緩解了狀態(tài)爆炸問(wèn)題.

本文的組織結(jié)構(gòu)如下:第2節(jié)介紹切片準(zhǔn)則生成模塊,根據(jù)各類缺陷分析IR生成切片準(zhǔn)則;第3節(jié)介紹切片模塊,分析IR得到程序依賴圖,再根據(jù)切片準(zhǔn)則進(jìn)行切片,得到切片后的程序,最后將切片后的程序交給符號(hào)執(zhí)行引擎分析;第4節(jié)介紹程序切片的實(shí)驗(yàn)結(jié)果;第5節(jié)是相關(guān)工作和總結(jié).

2 生成切片準(zhǔn)則

切片準(zhǔn)則生成模塊的輸入是LLVM IR,根據(jù)用戶指定的缺陷分析IR產(chǎn)生切片準(zhǔn)則,下面簡(jiǎn)要介紹LLVM IR的核心語(yǔ)法,如圖2所示.編譯過(guò)程中的每個(gè)翻譯單元對(duì)應(yīng)IR的一個(gè)模塊(module),包含函數(shù)聲明、函數(shù)定義和全局變量.

LLVM IR以函數(shù)為單位,每個(gè)函數(shù)包含若干基本塊b,每個(gè)基本塊包含若干條指令c,指令有函數(shù)調(diào)用指令,棧變量分配指令,算術(shù)運(yùn)算指令,load與store指令,getelementptr指令等.其中g(shù)etelementptr指令用于獲取聚合數(shù)據(jù)類型中子元素的地址,如獲取數(shù)組元素或結(jié)構(gòu)體成員.

本系統(tǒng)共設(shè)計(jì)了針對(duì)八類缺陷的切片準(zhǔn)則,分別是內(nèi)存泄漏、文件描述符未釋放、除零、整數(shù)溢出、懸空指針或空指針解引用、緩沖區(qū)溢出、使用未初始化的變量、返回棧變量的地址,下面是由各類缺陷生成切片準(zhǔn)則的設(shè)計(jì).

圖2 LLVM IR的核心語(yǔ)法
Fig.2 Core grammar of LLVM IR

1)內(nèi)存泄漏:檢測(cè)指令是否是malloc,realloc,calloc或free四種函數(shù)調(diào)用指令中的一種,如果是則將該條指令加入切片準(zhǔn)則.

2)文件描述符未釋放:檢測(cè)指令是否是fopen,freopen,fclose,open,openat,creat,close函數(shù)調(diào)用指令中的一種,如果是則將該條指令加入切片準(zhǔn)則.

3)除零:檢測(cè)指令是否是無(wú)符號(hào)除法,有符號(hào)除法,浮點(diǎn)數(shù)除法,無(wú)符號(hào)取模,有符號(hào)取模,浮點(diǎn)數(shù)取模運(yùn)算中的一種,如果是則將指令加入切片準(zhǔn)則.

4)整數(shù)溢出:將截?cái)嘀噶?加減乘除指令,取余指令,求絕對(duì)值的函數(shù)調(diào)用指令加入切片準(zhǔn)則,之所以加絕對(duì)值函數(shù)是為了檢測(cè)求最大負(fù)數(shù)的絕對(duì)值導(dǎo)致溢出的缺陷.

5)懸空指針或空指針解引用:在C語(yǔ)言上表現(xiàn)為對(duì)指針解引用和對(duì)數(shù)組作下標(biāo)訪問(wèn)操作,它們分別有取值和賦值兩種操作.比如對(duì)指針解引用的取值操作是*p,它的LLVM IR是

%1 = load i32*,i32** %p,align 8

%2 = load i32,i32* %1,align 4

檢測(cè)load指令的操作數(shù)是否來(lái)自上一條load指令,是則將其加入切片準(zhǔn)則,此例中第二條load指令的操作數(shù)%1來(lái)自上一條load指令,故將第二條load指令加入切片準(zhǔn)則;對(duì)數(shù)組取元素的取值操作,比如p[0],它的IR是

%0 = load i32*,i32** %p,align 8

%arrayidx = getelementptr inbounds i32,i32* %0,i64 0

%1 = load i32,i32* %arrayidx,align 4

檢測(cè)load指令的操作數(shù)是否來(lái)自getelementptr指令,滿足則加入切片準(zhǔn)則;同理,賦值操作如*p = 2,它的IR是

%1 = load i32*,i32** %p,align 8

store i32 2,i32* %1,align 4

檢測(cè)store指令的操作數(shù)是否來(lái)自load,滿足則加入切片準(zhǔn)則;對(duì)數(shù)組元素賦值,如p[0] = 2的IR是

%0 = load i32*,i32** %p,align 8

%arrayidx = getelementptr inbounds i32,i32* %0,i64 0

store i32 2,i32* %arrayidx,align 4

檢測(cè)store指令的操作數(shù)是否來(lái)自getelementptr指令,是則加入切片準(zhǔn)則.

6)緩沖區(qū)溢出:緩沖區(qū)溢出的缺陷在C上表現(xiàn)為數(shù)組解引用,如arr[1],它的IR是

%arrayidx3 = getelementptr inbounds [3 x i32],[3 x i32]* %arr,i64 0,i64 1

%2 = load i32,i32* %arrayidx3,align 4

檢測(cè)load指令的操作數(shù)是否來(lái)自getelementptr指令,是則加入切片準(zhǔn)則;同理,arr[1] = 0這樣的對(duì)數(shù)組元素賦值則檢測(cè)store指令是否來(lái)自getelementptr指令;最后,對(duì)C庫(kù)函數(shù)中與操作緩沖區(qū)相關(guān)的函數(shù)調(diào)用也加入切片準(zhǔn)則,有memset、memcpy、memmove、strcpy、strncpy、strcat、strncat、wmemset、wmemcpy、wmemmove、wcscpy、wcsncpy、wcscat和wcsncat.

7)使用未初始化的變量:第一種情況是使用未初始化變量的值本身,如int a;printf(“%d ”,a);它的IR是

%a = alloca i32,align 4

%0 = load i32,i32* %a,align 4

%call = call i32(i8*,...)@printf(i8* getelementptr inbounds([4 x i8],[4 x i8]* @.str,i32 0,i32 0),i32 %0)

如果load指令的操作數(shù)來(lái)自alloca,則將load指令加入切片準(zhǔn)則;第二種情況是將未初始化的變量的地址賦給指針,如int a;int *p = &a;它的IR是

%a = alloca i32,align 4

%p = alloca i32*,align 8

store i32* %a,i32** %p,align 8

因此若store指令的值操作數(shù)來(lái)自alloca,則將store指令加入切片準(zhǔn)則.

8)返回棧變量的地址:這類缺陷分三種情況.第一種是將棧變量的地址賦值給指針類型的全局變量;第二種情況是將棧變量的地址賦值給二級(jí)指針的形參指向的區(qū)域,可通過(guò)形參傳回主調(diào)函數(shù),這兩種情況都是將棧變量的地址賦給某變量,如store i32* %a,i32** %p,align 8,檢測(cè)store指令的值操作數(shù)的類型是否是指針,是則將store指令加入切片準(zhǔn)則;第三種情況是在被調(diào)函數(shù)中返回指針或變量的地址,如ret i32* %p,所以檢測(cè)return指令的類型是否是指針,是則將它加入切片準(zhǔn)則.

以上缺陷模式的檢測(cè)均是作保守分析,只要指令符合缺陷的特征,就將它加入切片準(zhǔn)則,這樣保證了分析過(guò)程中與所關(guān)注的缺陷相關(guān)的程序語(yǔ)義的完備性.用戶可以指定多種缺陷,根據(jù)每一種缺陷獲取相應(yīng)的切片準(zhǔn)則,最后合并再交給切片模塊.

3 程序切片模塊

程序切片模塊根據(jù)切片準(zhǔn)則,對(duì)LLVM IR做切片,由于C代碼的結(jié)構(gòu)與IR等價(jià),為便于圖示,下面的分析基于C代碼.本模塊分兩步,先構(gòu)建程序依賴圖,然后根據(jù)程序切片準(zhǔn)則在程序依賴圖上標(biāo)記節(jié)點(diǎn),計(jì)算反向可達(dá)性,所有可達(dá)的語(yǔ)句即是程序切片.

3.1 構(gòu)建程序依賴圖

程序依賴圖表示程序中各語(yǔ)句間的依賴關(guān)系,包括數(shù)據(jù)依賴和控制依賴,程序依賴圖由數(shù)據(jù)依賴圖和控制依賴圖構(gòu)成,依賴圖中的每個(gè)節(jié)點(diǎn)是一條語(yǔ)句.

3.1.1 構(gòu)建數(shù)據(jù)依賴圖

定義1.數(shù)據(jù)依賴.語(yǔ)句p中定值的變量可能會(huì)在語(yǔ)句q中被使用,稱語(yǔ)句q數(shù)據(jù)依賴于語(yǔ)句p.

如圖3的示例程序所示,用戶在循環(huán)后動(dòng)態(tài)分配了i個(gè)字節(jié)的內(nèi)存,后續(xù)程序未釋放堆內(nèi)存.

1 intmain(){2 void?p；3 intsum=0；4 inti=1；5 while(i<11){6 sum=sum+i；7 i=i+1；8 }9 p=malloc(i)；10 printf(″%d ″，sum)；11 }

圖3 示例程序
Fig.3 Sample program

第4條語(yǔ)句int i=1定義了變量i,在循環(huán)的判斷語(yǔ)句while(i< 11)中使用了i,所以while(i< 11)這條語(yǔ)句數(shù)據(jù)依賴于int i=1.LLVM在IR級(jí)別上提供了變量的DEF-USE信息,可得到語(yǔ)句間的定值和使用的關(guān)系,由此構(gòu)建出圖3程序的數(shù)據(jù)依賴圖,如圖4所示,其中entry節(jié)點(diǎn)表示程序的入口,語(yǔ)句間的指向表示數(shù)據(jù)依賴.

圖4 圖3程序的數(shù)據(jù)依賴圖Fig.4 Data dependence graph of program in Fig.3

3.1.2 構(gòu)建控制依賴圖

定義2.控制依賴.語(yǔ)句p的直接后繼至少有兩個(gè),從其中一條路徑出發(fā)可到達(dá)語(yǔ)句q,從另外的一條路徑出發(fā)可能不會(huì)到達(dá)q,則稱語(yǔ)句q控制依賴于語(yǔ)句p.

通俗地說(shuō),語(yǔ)句p能決定語(yǔ)句q能否被執(zhí)行,如圖3中的第6條語(yǔ)句sum = sum + i控制依賴于判斷條件while(i< 11).一定會(huì)被執(zhí)行的語(yǔ)句控制依賴于程序的入口點(diǎn)entry.圖3示例程序的控制依賴圖如圖5所示,其中的虛線箭頭表示語(yǔ)句間的控制依賴關(guān)系.

最后,將數(shù)據(jù)依賴圖與控制依賴圖合并,構(gòu)成程序依賴圖,圖6是圖3示例程序的程序依賴圖.

3.2 計(jì)算反向可達(dá)性

假設(shè)用戶關(guān)心內(nèi)存泄漏的缺陷,由切片準(zhǔn)則生成模塊分析圖3得到切片準(zhǔn)則是malloc函數(shù)調(diào)用語(yǔ)句,如圖7中的深灰色節(jié)點(diǎn)所示,以它為起始點(diǎn),對(duì)程序依賴圖反向遍歷,所能到達(dá)的所有節(jié)點(diǎn)即為程序切片,如灰色節(jié)點(diǎn)所示.

圖5 圖3程序的控制依賴圖Fig.5 Control dependence graph of program in Fig.3

圖6 圖3程序的程序依賴圖Fig.6 Program dependence graph of program in Fig.3

圖7 圖3程序的反向可達(dá)性Fig.7 Inverse reachability of program in Fig.3

由此得到源程序中與內(nèi)存泄漏缺陷相關(guān)的語(yǔ)句,圖8是程序切片的源代碼表示,它的規(guī)模較原有程序要小,最后將切片交給分析工具ShapeChecker檢測(cè).

1 intmain(){2 void?p；3 inti=1；4 while(i<11){5 i=i+1；6 }7 p=malloc(i)；8 }

圖8 圖3程序的切片結(jié)果
Fig.8 Result of slicing program in Fig.3

4 實(shí)驗(yàn)結(jié)果

實(shí)驗(yàn)的硬件平臺(tái)是Intel(R)Core(TM)i7-4790 CPU @ 3.60GHz 4核8線程,20G內(nèi)存;操作系統(tǒng)是Ubuntu 16.04.1 LTS64位.被測(cè)程序采用美國(guó)國(guó)家安全局的Common Weakness Enumeration(CWE)公共測(cè)試集*The MITRE Corporation.Common Weakness Enumeration [EB/OL].http://cwe.mitre.org/data/definitions/1000.html, 2017.,選取其中八類缺陷目錄,分別是內(nèi)存泄漏(CWE401)、文件描述符未釋放(CWE773、775)、除零(CWE369)、整數(shù)溢出(CWE190、191)、懸空指針或空指針解引用(CWE476、690)、緩沖區(qū)溢出(CWE121、122、124、126、127)、使用未初始化的變量(CWE457)、返回棧變量的地址(CWE562),用靜態(tài)分析工具ShapeChecker檢測(cè)缺陷,加程序切片功能前后的時(shí)間對(duì)比如表1所示,其中切片后的分析時(shí)間包括切片本身的耗時(shí).

表1 程序切片前后的分析時(shí)間比較
Table 1 Analysis time of before and after slicing

分析時(shí)間(s)切片前切片后時(shí)間減少的百分比內(nèi)存泄漏603．87253．0558．10%文件描述符泄漏71．0539．5444．35%除零625．27363．2741．90%整數(shù)溢出3565．41911．2346．40%空指針解引用432．54172．9560．02%緩沖區(qū)溢出17036．1212915．6824．19%用未初始化變量2622．662403．798．35%返回棧變量地址0．890．4153．93%

從測(cè)試結(jié)果來(lái)看,程序切片減少了分析工具的運(yùn)行時(shí)間,平均減少了27.64%.CWE的每種測(cè)試目錄專門針對(duì)某種缺陷,在用戶指定檢測(cè)相應(yīng)缺陷時(shí),程序切片可將無(wú)關(guān)的控制結(jié)構(gòu)刪除,減少了程序的規(guī)模和符號(hào)執(zhí)行中的狀態(tài)數(shù)目,在一定程度上提高了靜態(tài)分析的性能.表2是加程序切片功能前后的平均漏報(bào)率和誤報(bào)率.

表2 程序切片前后的精度比較
Table 2 Precision of before and after slicing

切片前切片后漏報(bào)率1．86%3．73%誤報(bào)率15．75%18．77%

加程序切片之后,分析工具的漏報(bào)率和誤報(bào)率有略微的上升,這是由于靜態(tài)分析本身是不完備的,將切片后的程序交給符號(hào)執(zhí)行引擎執(zhí)行時(shí)可能會(huì)影響它的分析策略.程序切片剔除的是與所關(guān)心的缺陷無(wú)關(guān)的代碼,不會(huì)改變與缺陷相關(guān)的程序語(yǔ)義,因此漏報(bào)率和誤報(bào)率只是有略微上升,相比工具在時(shí)間性能上的提升,精度損失在可接受的范圍之內(nèi).

5 相關(guān)工作和總結(jié)

程序切片的思想由Weiser[10]提出,最初用于調(diào)試程序[11],程序中某一條語(yǔ)句出錯(cuò)后,為了找到影響該語(yǔ)句的所有前面的語(yǔ)句,只關(guān)注出錯(cuò)部分,方便程序員的調(diào)試.這一思想也可用于程序分析領(lǐng)域,用戶想專門檢測(cè)某種缺陷,這種缺陷關(guān)聯(lián)的語(yǔ)句即是興趣點(diǎn).

Swarup等[12]用一組自動(dòng)生成的近似滿足程序不變量的輸入來(lái)檢測(cè)軟件缺陷,之后用動(dòng)態(tài)后向切片技術(shù)逐步過(guò)濾輸入集以提高分析精度.

Marek[13]等開(kāi)發(fā)的Symbiotic靜態(tài)分析工具將指令制導(dǎo)、程序切片和符號(hào)執(zhí)行工具KLEE[7]組合起來(lái),其中切片部分使用數(shù)據(jù)流方程迭代方式計(jì)算.

趙云山等[14]使用有限狀態(tài)自動(dòng)機(jī)描述的缺陷模式和路徑條件來(lái)生成切片準(zhǔn)則,并有選擇地對(duì)控制流圖中的匯合點(diǎn)進(jìn)行缺陷狀態(tài)合并以減少誤報(bào)率及提高分析效率.

本文在LLVM中間語(yǔ)言上提出針對(duì)缺陷的程序切片方法,筆者所在的課題組目前仍在改進(jìn)靜態(tài)分析工具ShapeChecker,下一步是支持C++的分析,C++有繼承、多態(tài)和異常等獨(dú)有的特性,在LLVM中間語(yǔ)言級(jí)別上會(huì)生成新的指令,可以將程序切片擴(kuò)展成對(duì)C++中異常安全、線程安全等缺陷的處理.程序切片技術(shù)也可用于逆向分析中,逆向分析關(guān)心軟件的基本原理和算法,可通過(guò)切片技術(shù)去除GUI和輸入輸出等部分,這樣減少了我們理解程序的負(fù)擔(dān).

[1] Hoare Charles Antony Richard.An axiomatic basis for computer programming [J].Communications of the ACM,1969,12(10):576-580.

[2] Reynolds John C.Separation logic:a logic for shared mutable data structures[C].Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science,IEEE,2002.

[3] Clarke Edmund,Allen Emerson.Design and synthesis of synchronization skeletons using branching time temporal logic[M].Workshop on Logic of Programs,Springer Berlin Heidelberg,1981.

[4] Cousot Patrick,RadhiaCousot.Abstract interpretation:a unified lattice model for static analysis of programs by construction or approximation of fixpoints [C].Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages,ACM,1977.

[5] Kildall Gary.A unified approach to global program optimization[C].Proceedings of the 1st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages,ACM,1973.

[6] King James C.Symbolic execution and program testing [J].Communications of the ACM,1976,19(7):385-394.

[7] Cristian Cadar,Daniel Dunbar,Dawson Engler.KLEE:unassisted and automatic generation of high-coverage tests for complex systems programs[C].Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation,2008:209-224.

[8] Lattner Chris,VikramAdve.LLVM:a compilation framework for lifelong program analysis & transformation [C].Proceedings of the International Symposium on Code Generation and Optimization:Feedback-directed and Runtime Optimization,IEEE Computer Society,2004.

[9] Liang Jia-biao,Li Zhao-peng,Zhu Ling,et al.Symbolic execution engine with shape analysis [J].Computer Science,2016,43(3):193-198.

[10] Weiser Mark.Program slicing [C].Proceedings of the 5th International Conference on Software Engineering,IEEE Press,1981:439-449.

[11] Weiser Mark.Programmers use slices when debugging [J].Communications of the ACM,1982,25(7):446-452.

[12] Swarup Kumar Sahoo,John Criswell,Chase Geigle,et al.Using likely invariants for automated software fault localization[J].ACM SIGARCH Computer Architecture News,2013,41(1):139-152.

[13] Marek Chalupa,Martin Joná?,Jiri Slaby,et al.Symbiotic 3:new slicer and error-witness generation[R].International Conference on Tools and Algorithms for the Construction and Analysis of Systems,Springer Berlin Heidelberg,2016.

[14] Zhao Yun-shan,Gong Yun-zhan,Liu Li,et al.Improving the efficiency and accuracy of path-sensitive defect detecting [J].Chinese Journal of Computers,2011,34(6):1100-1113.

附中文參考文獻(xiàn)：

[9] 梁家彪,李兆鵬,朱 玲,等.支持形狀分析的符號(hào)執(zhí)行引擎的設(shè)計(jì)與實(shí)現(xiàn) [J].計(jì)算機(jī)科學(xué),2016,43(3):193-198.

[14] 趙云山,宮云戰(zhàn),劉 莉,等.提高路徑敏感缺陷檢測(cè)方法的效率及精度研究 [J].計(jì)算機(jī)學(xué)報(bào),2011,34(6):1100-1113.