基于區間向量抽象域的數值程序分析算法

吳世堂，李 寧，詹海潭

（中國航天科技集團公司第七一○研究所，北京100037）

0 引 言

程序中變量的值范圍信息有助于判斷程序中是否存在除零錯誤、數組越界、整數溢出等多種運行時錯誤。精確獲取變量值范圍是不可能的，必須在精度和效率之間進行折中。基于抽象解釋理論［1］的數值程序分析技術可以給出每個程序點的數值變量近似且可靠的值范圍信息。其中基于該理論的抽象域的設計是權衡分析精度和效率的關鍵。

在航天控制軟件中，往往需要進行大量矩陣運算，因此對矩陣的抽象直接影響該類軟件的分析。在已有的抽象域中，有許多對數組的抽象，為了降低分析的復雜性，提高分析效率，一般是將整個數組簡單抽象為單個數值變量，即不考慮數組元素之間的差異性；或者將數組元素抽象為固定數目的幾個數值變量［2］，每個部分用一個數值概要變量來抽象，有限考慮了元素之間的差異性，但是仍然極大損失數組元素精度；還有的提出數組區間集的方式來抽象數組元素［3］，通過在整型區間集的基礎上構造數組區間集記錄數組變量值范圍和數組長度信息，增加了空間開銷；侯蘇寧等提出將數組中的每個元素均抽象為一個數值變量［4］，雖然提高數組元素分析的精度，但是分析效率極低，并不適合實際航天控制軟件的分析［5］。

本文在充分考慮對航天控制軟件分析中矩陣運算的精度重要性，以及分析效率，提出了區間向量抽象域。通過將矩陣的各行各列分別抽象為一個區間，形成一個區間向量對，用區間向量對的對應元素交集表示矩陣元素。同時，設計了一系列域上的操作算子保證分析的精度和效率。本文方法與將矩陣抽象為單個變量方法和抽象為簡單幾個變量方法相比，精度有了很大的提高；與完全展開矩陣每個元素的方法相比，大大減少時間和空間開銷，增加了方法的實用性。

1 區間向量抽象域

1.1 區間向量抽象域的表示

區間向量抽象域是在經典的區間抽象域基礎上，針對程序中的數組變量的表示而進行的擴展。下面先回顧區間抽象域的定義。

區間抽象域是指用值區間來描繪程序變量值范圍的抽象狀態。其符號通常可以表示為Internal＝ ｛⊥｝∪｛［m1，m2］｜m1≤m2，m1∈M∪ ｛－∞｝，m2∈M∪ ｛＋∞｝｝。對任意m∈M，都可以將m 的大小擴展到 （－∞，＋∞）上，即－∞≤m≤＋∞。

基于區間抽象域［6］的靜態分析是在所有程序點為每個變量維護一個區間，用來刻畫變量在該程序點的值范圍信息。

為了更準確的描述變量的值范圍，很多研究提出區間集的概念［7］。但是仍然沒有區別數組元素之間的差異性，僅僅將數組變量作為單獨變量來處理相對應的區間集，對于分析數組元素運算所帶來的精度損失仍然很大。

矩陣元素是實數集的有序集合，而區間向量［8］是區間集的有序集合，能夠合理的表示矩陣元素的有序性，在程序靜態分析中就能夠體現元素之間的差異性，在提高分析的精度的同時，分析的效率也不會過于復雜，滿足實際軟件分析的需要。

對于給定的矩陣 （數值型二維數組）A 中假設包含m×n個元素，那么首先可以將實數矩陣轉化為區間矩陣，然后將矩陣中每一行的n 個區間元素由該n 個元素可能取到的最小值和最大值所構成的區間來近似表示。將矩陣中每一列的m 個區間元素由該m 個元素可能取到的最小值和最大值所構成的區間來近似表示。因此，一個矩陣可以由一個列區間向量＝［A1A2… Am］T和一個行區間向量＝［Ar1Ar2… Arn］所組成的區間向量對＜，＞來近似表示，其中向量中的元素Ai（i＝1，2，…，m）是矩陣A 的第i 行元素抽象后的形式化表示，Ajr（j ＝1，2，…，n）是矩陣A 第j 列元素抽象后的形式化表示。

由于區間抽象域［5］在實數R 上的區間集合構成了一個完全格，顯然，區間向量的集合也構成了一個完全格［Itvects，iv，∩iv，∪iv，⊥iv，┬iv］。基于抽象解釋理論，實數矩陣與區間向量對抽象域之間的關系可以通過下面Galois連接來表示

式中： （R）——實數集合，I——區間集合， ——矩陣。具體函數γiv是將區間向量抽象域向矩陣具體域進行具體化的過程，形式化表示為γiv＝［〈ItvectsT，Itvects〉→ （I（（R）））］，具體化過程是通過將行、列兩個區間向量對應的區間元素求交集獲得矩陣中的相對應的矩陣元素，形式化定義如下所示

抽象函數αiv是將矩陣具體域向區間向量抽象域進行抽象化 的 過 程。形 式 化 定 義 為αiv＝ ［ （I（ （R）））→〈ItvectsT，Itvects〉］，抽象化的過程是通過首先將實數矩陣轉化為區間矩陣，形式化表示為： （ （R））→ （I（（R）））。然后將區間矩陣的每一行的所有區間元素的可能取值的最小值和最大值作為一個區間，表示該行所有元素的可能取值的上界；每一列的所有區間元素的可能取值的最小值和最大值作為一個區間，表示該列所有元素的可能取值的上界。這樣就形成一個區間向量對來實現矩陣的抽象過程。形式化定義如下所示

1.2 區間向量抽象域的域操作

在基于抽象解釋理論框架下，抽象域是主要內容，而支撐抽象域的各種基本操作算子是抽象解釋框架中的抽象域應用于實際程序分析的關鍵。下面給出在上面定義的區間向量抽象域上基本操作算子的設計。

設任意給定兩個實數矩陣Am×n 和Bn×t，通過上面設計的抽象化函數αiv，可以獲得抽象區間向量對分別為

區間向量抽象域是對實數矩陣轉化為區間矩陣后進行的抽象，也就是對區間抽象域進行的擴展，因此，在區間向量抽象域上的操作算子也與區間抽象域操作算子密切相關。下面分別詳細給出該抽象域上的基本操作算子的設計。

（1）交操作 （Meet）

兩個區間向量之間的交運算是指兩個矩陣的相對應的兩個元素區間值范圍進行交運算。具體過程為，首先根據區間向量對進行具體化操作，分別獲得兩個區間矩陣，然后對獲得的兩個區間矩陣相對應的元素求交運算。那么矩陣Am×n和Bn×t單個元素Aij和Bhk交運算的形式化定義如下所示

式中：∩i運算是區間抽象域交操作，即兩個區間進行交操作。

（2）接合操作 （Join）

兩個區間向量進行接合是指兩個矩陣的相對應兩個元素區間值范圍作并運算，具體過程為，首先根據區間向量進行具體化操作，分別獲得兩個區間矩陣，然后對獲得的兩個區間矩陣相對應的元素求接合。那么矩陣Am×n 和Bn×t單個元素Aij和Bhk接合運算的形式化定義如下所示

式中：∪i運算是區間抽象域接合操作，即兩個區間進行接合操作。

（3）算術運算操作 （Arithmetic）

兩個區間向量的算術運算操作是指兩個矩陣的相對應的兩個元素區間值范圍作算術運算。具體過程為，首先根據區間向量對進行具體化操作，分別獲得兩個區間矩陣，然后對這兩個區間矩陣相對應的元素進行相應的算術運算。那么矩陣Am×n和Bn×t單個元素Aij和Bhk算術運算的形式化定義的四則運算如式 （6）所示

其中，運算符⊙i∈｛＋i，－i，×i，÷i｝，均為區間抽象域上進行加、減、乘、除四則運算。

如式 （7）為對矩陣Am×n 單個元素Aij取反運算的形式化表示

其中，運算符－i為區間抽象域上的取反操作。

（4）比較操作 （Compare）

比較是指格上的兩個數之間偏序關系的比較。兩個區間向量之間的比較操作是指兩個矩陣相對應的元素區間值范圍的比較。具體比較過程為，首先根據區間向量抽象域進行具體化操作，分別獲得相應區間矩陣，然后對區間矩陣對應的元素進行區間抽象域上的比較操作，形式化表示如下

其中，i是區間抽象域上的比較操作。（5）拓寬操作 （Widening）

在基于抽象解釋理論進行程序靜態分析過程中，為了加速程序分析的收斂速度，需要對抽象域進行拓寬操作。而對表示矩陣的變量進行拓寬操作可以表示為對區間向量對的拓寬操作也就是分別對行區間向量和列區間向量進行拓寬操作。區間向量的拓寬操作則是將兩個區間向量對應元素之間分別進行區間拓寬操作，區間向量對拓寬操作的形式化表示如下

其中，運算 i 是區間抽象域上的標準拓寬操作。（6）遷移函數 （transfer function）

在基于抽象解釋的程序靜態分析過程中，遷移函數是指，程序在執行完一條語句之后，程序狀態發生的變化在抽象域上所表示的狀態遷移動作。

基于抽象解釋的程序靜態分析，會在每個程序點創建一個抽象環境，用X＃表示，即把所有程序變量映射到抽象域。對于C語言中的基本類型的變量都可以映射到區間抽象域，但是對于表示矩陣的變量，在實際程序中并不存在直接矩陣類型，而往往是使用數組表示。矩陣運算操作的完成也是通過若干次的數組元素運算來完成。下面討論使用二維數組表示矩陣，且程序中采用數組下標訪問方式對數組元素進行操作情況下的區間向量抽象域上的遷移函數的操作。

在程序分析過程中，數組的下標需要映射為區間抽象域，對程序中訪問矩陣某個元素操作采用如下的方式作為該元素的穩定上近似，即取下標區間內的所有區間元素的最小上界。假設數組行下標變量，列下標變量，那么有

在程序分析過程中，訪問二維數組的單個元素時取A［i］［j］＝Ai∩iAjr。如果i⊥i或者j⊥i，則Ai，Ajr⊥i，使用前必須先判斷交集是否為⊥i。下面給出針對C語言程序分析過程中需要使用到的各種遷移函數的詳細設計。

賦值遷移函數 （assignment transfer function）

對于程序中矩陣元素的賦值語句A［i］［j］＝expr在抽象環境X＃下，程序的狀態發生變化，矩陣元素值需要更新，反應在區間向量抽象域中則需要更新區間向量對中相應的元素，賦值遷移函數形式化定義如下

其中，［expr］＃X＃表示程序在某程序點對應的抽象環境X＃下計算表達式expr所得到的區間抽象值。

測試遷移函數 （test transfer function）

對于程序中矩陣元素相關的測試語句A［i］［j］ test，（其中 ｛≤，≥｝）在不同的測試分支中，相關矩陣的狀態不同，因此，在不同分支中矩陣元素的值范圍需要進行相應的更新，在抽象域中表現為更新區間向量對中相應元素的值。

由于抽象環境X＃中存放該程序點中所有變量的抽象域，因此，此時的抽象環境中對應矩陣元素的抽象域表示有X＃（A［i］［j］）＝〈Ai，Ajr〉，其中假設區間向量抽象域中相應的元素表示為，且有Ai是矩陣相應元素值范圍的上近似，test表達式計算出的區間假設表示為test［c，d］。

那么針對程序中測試語句≤和≥分別有式 （12）、式（13）實現區間向量抽象域元素狀態的遷移

上式中各變量在區間抽象域上的關系如圖1所示。

圖1 區間關系

2 實驗與實驗結果分析

本文實驗基于開源的編譯器前端goto－cc［9］（支持嵌入式C）及開源的數值抽象域庫Apron［10］，開發了面向嵌入式C數值程序分析原型工具。

goto－cc是由牛津大學Daniel等開發的編譯器，用于將嵌入式C程序編譯成控制流圖。本文實驗是在該編譯器生成的控制流圖上利用抽象解釋理論框架求不動點實現對程序的靜態分析。

Apron 是由法國INRIA 開發的一個開源數值抽象域庫。為程序分析工具開發者提供一個通用的抽象域獨立的接口，可以通過接口直接使用其中已有的抽象域，還為新抽象域的開發提供通用的設計接口。本文的區間向量抽象域就是基于Apron 庫提供的接口設計和實現的。

本文實驗基于的環境是：Ubuntu 10Linux操作系統，2G 物理內存，1.70GHZ雙核CPU 處理器。本文抽象域的實現及與已有方法的對比實驗均是基于該環境。

圖2給出一個從實際嵌入式C 程序抽取出一個簡單的有代表性的矩陣加法的程序片段，為方便精度比較，給二維數組賦值為簡單的數值。并且，在不動點迭代時為了不讓拓寬操作影響各方法分析精度，這里循環展開次數設為3次，拓寬延遲1次。

下面對各主流對矩陣抽象方法的實驗結果進行比較。Blanche提出將矩陣所有元素抽象為一個變量方法 （下文簡稱單變量法），無法刻畫元素之間的區別，無法描述矩陣元素的有序性，計算結果雖是矩陣所有元素的上近似，精度損失很大。侯蘇寧提出將矩陣每個元素均抽象為一個變量（下文簡稱完全展開法），精度損失最小，計算結果與具體域最接近，但是在實際程序分析過程中效率極低，該方法并不實用。本文區間向量抽象域能夠較好刻畫元素之間區別，在精度損失較小的情況下增加實用性。上述3種方法對數組c實驗結果如下所示：

圖2 矩陣加法程序片段

單變量法

完全展開法

區間向量法

該程序片段中矩陣加法實際求解結果為：｛｛3，9，6，8｝，｛10，7，14，16｝，｛4，6，10，10｝，｛7，14，11，18｝｝根 據 上 面 的 實驗結果，可以看出本文的方法能夠穩定且較精確的表示矩陣各元素的值范圍。

在空間開銷上，單變量法抽象方法簡單，對于每個表示矩陣變量的數組變量，無論數組的長度是多大均抽象為單個數值變量，因此，對于一個數組變量僅需要的一個抽象值，空間開銷復雜度是一個常數O（1）級。而完全展開法對一個矩陣中的每個元素都用一個抽象值 （區間）表示，抽象值的空間開銷是依據數組的元素個數而定的。因此，對一個有m×n個數組元素的矩陣需要的抽象值個數為m×n個，對每個抽象值的表示采用的是區間抽象域那么，空間復雜度是O（m×n）級。本文的區間向量抽象域依據矩陣的各行、各列分別進行區間抽象，即m 行抽象出一個含m個區間元素的區間向量，n列抽象出一個含n 個區間元素的區間向量，需要抽象區間的開銷為m＋n個，因此空間開銷復雜度為O（m＋n）級。

在時間開銷上，單變量法在抽象域對矩陣進行操作時只需要對一個抽象值進行交、接合、拓寬等操作，也不會因為矩陣元素的多少而變化，完成一次對矩陣的操作，只需要執行域上操作一次。需要時間自然最少。完全展開法則在每次進行交、接合、拓寬等操作時都需要對m×n個抽象值（區間）均進行操作，因此，完成一次對矩陣的操作時需要進行m×n次的域上的操作操作，消耗時間最大。本文提出的區間向量抽象域在進行交、接合、拓寬等操作時，僅需要對m＋n個區間抽象值進行操作，即完成一次對矩陣的操作時需要執行域上的操作m＋n次。表1為3種方法比較。

表1 3種方法數據比較

實驗結果表明本文提出的區間向量抽象域對矩陣變量進行抽象，在時空效率以及分析精度作了很好的權衡。

3 結束語

本文在經典區間抽象域的基礎上，提出針對矩陣運算的區間向量抽象域，綜合考慮數組元素運算的精確性以及計算的效率。將一個矩陣 （二維數組）抽象為兩個區間向量，將矩陣每一行元素抽象為一個區間獲得一個區間向量，將矩陣每一列元素也抽象為一個區間獲得另一個區間向量。在程序中訪問某個元素時，根據數組下標，由行號索引該元素所在行的抽象區間，由列號索引該元素所在列的抽象區間，那么兩個區間的交集作為該元素的近似。能夠體現元素之間的差異性且較精確的表示數組元素，同時，在時間和空間消耗上取得合理的權衡。實驗分析結果證實區間向量抽象域對矩陣運算的精確性以及實用性。

［1］Cousot P.Formal verification by abstract interpretation ［G］.LNCS 7226： NASA Formal Methods. Norfolk， USA：Springer Berlin Heidelberg，2012：3－7.

［2］Gopan D.Numeric program analysis techniques with applications to array analysis and library summarization ［D］.Madison：University of Wisconsin，2007：64－93.

［3］ZHANG Shijin，SHANG Zhaowei.Detection of array bound overflow by interval set based on Cppcheck ［J］.Journal of Computer Applications，2013，33 （11）：3257－3261 （in Chinese）.［張仕金，尚趙偉.基于區間集的Cppcheck數組邊界缺陷檢測 ［J］.計算機應用，2013，33 （11）：3257－3261.］

［4］HOU Suning.Research on value range analysis based on abstract interpretation ［D］.Changsha：National University of Defense Technology，2009 （in Chinese）.［侯蘇寧.基于抽象解釋的數值程序分析技術研究 ［D］.長沙：國防科學技術大學，2009.］

［5］HOU Suning，CHEN Liqian.A static analyzer for numerical programs in C and Fortran ［J］.Computer Engineering ＆Science，2011，33 （3）：94－102 （in Chinese）.［侯蘇寧，陳立前.一個面向C和Fortran數值程序的靜態分析工具 ［J］.計算機工程與科學，2011，33 （3）：94－102.］

［6］JIANG Jiahong，CHEN Liqian.Floating－point program analysis based on floating－point power set of intervals abstract domain［J］.Journal of Frontiers of Computer Science and Technology，2013，7 （3）：209－217 （in Chinese）.［姜加紅，陳立前.基于浮點區間冪集抽象域的浮點程序分析 ［J］.計算機科學與探索，2013，7 （3）：209－217.］

［7］WANG Yawen，GONG Yunzhan.A method of variable range analysis based on abstract interpretation and its applications［J］.Chinese of Journal Electronics，2011，39 （2）：296－303（in Chinese）.［王雅文，宮云戰.基于抽象解釋的變量值范圍分析及應用 ［J］.電子學報，2011，39 （2）：296－303.］

［8］ZHANG Jianhua.The global optimization algorithm using interval mathematics and its application research ［D］.Hefei：Hefei University of Technology，2012 （in Chinese）.［張建華.基于區間數學的全局優化算法及其應用研究 ［D］.合肥：合肥工業大學，2012.］

［9］University of Oxford.Goto－cc－a C／C＋＋front－end for Verification ［EB／OL］. ［2014－03－19］.http：／／www.cprover.org／goto－cc.HTM.

［10］Jeannet B，Mine A.The APRON library for numerical abstract domains ［C］／／Proceedings of the 21st International Conference on Computer Aided Verification，2009：661－667.