吳世堂，李 寧，詹海潭

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

0 引 言

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

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

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

1 區(qū)間向量抽象域

1.1 區(qū)間向量抽象域的表示

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

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

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

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

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

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

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

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

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

1.2 區(qū)間向量抽象域的域操作

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

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

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

（1）交操作 （Meet）

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

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

（2）接合操作 （Join）

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

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

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

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

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

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

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

（4）比較操作 （Compare）

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

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

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

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

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

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

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

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

賦值遷移函數(shù) （assignment transfer function）

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

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

測試遷移函數(shù) （test transfer function）

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

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

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

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

圖1 區(qū)間關系

2 實驗與實驗結果分析

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

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

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

本文實驗基于的環(huán)境是：Ubuntu 10Linux操作系統(tǒng)，2G 物理內(nèi)存，1.70GHZ雙核CPU 處理器。本文抽象域的實現(xiàn)及與已有方法的對比實驗均是基于該環(huán)境。

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

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

圖2 矩陣加法程序片段

單變量法

完全展開法

區(qū)間向量法

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

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

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

表1 3種方法數(shù)據(jù)比較

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

3 結束語

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

［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）.［張仕金，尚趙偉.基于區(qū)間集的Cppcheck數(shù)組邊界缺陷檢測 ［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）.［侯蘇寧.基于抽象解釋的數(shù)值程序分析技術研究 ［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數(shù)值程序的靜態(tài)分析工具 ［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）.［姜加紅，陳立前.基于浮點區(qū)間冪集抽象域的浮點程序分析 ［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）.［王雅文，宮云戰(zhàn).基于抽象解釋的變量值范圍分析及應用 ［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）.［張建華.基于區(qū)間數(shù)學的全局優(yōu)化算法及其應用研究 ［D］.合肥：合肥工業(yè)大學，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.