方昭潭，蘇 亭，李 博，經(jīng)小川，張 偉

（1.華東師范大學(xué) 軟件學(xué)院，上海200062；2.中國航天系統(tǒng)科學(xué)與工程研究院，北京100080）

0 引 言

在計算機(jī)語言發(fā)展過程中，類型系統(tǒng)用于定義如何將編程語言中的數(shù)值和表達(dá)式歸類為許多不同的類型，如何操作這些類型，這些類型如何互相作用，類型系統(tǒng)的目的是防止在程序的執(zhí)行過程中有運行時錯誤的發(fā)生。最初，高級語言并沒有類型系統(tǒng)的概念，即語言中的變量x可以指向任何存儲位置，而被引用的位置可以保存任意類型的信息［1］。Ocaml就是這樣的高級語言，雖然它沒有類型系統(tǒng)，但是運行時，變量的意義就會知道，這就造成編譯器無法在編譯時事先安排存儲方案。所以，類型系統(tǒng)有助于提高編譯效率。

對于軟件開發(fā)過程，測試是一個非常重要的階段，而測試用例是測試過程中重要的輸出結(jié)果，在一定程度上檢測軟件程序的實現(xiàn)是否滿足規(guī)范的要求。為了方便軟件工程師的分析和調(diào)試，自動化測試已經(jīng)是當(dāng)前測試發(fā)展的前進(jìn)趨勢。工業(yè) 界工具，如 TESTBED和googletest［2－6］，可將測試用例作為這些工具的輸入，從而達(dá)到測試自動化。然而這些測試用例都需要測試人員的前期介入，并非真正的自動化［7，8］。本文基于類型理論背景講述C語言的類型系統(tǒng)的構(gòu)建過程，為真正的測試自動化解決前期工作問題。

本文有如下貢獻(xiàn)：①出工具前端用于處理類型的類型收集系統(tǒng)模型，輔助工具后端收集變量信息。②提出類型收集系統(tǒng)中每個類型所占的內(nèi)存塊模型相關(guān)的數(shù)據(jù)結(jié)構(gòu)。③實現(xiàn)關(guān)于程序中類型的收集，并完成對程序進(jìn)行類型接口插樁，用于工具后端的處理。

1 CAUT

CAUT （C analysis and unit testing toolkit）是一個基于動態(tài)符號執(zhí)行開發(fā)的，用于C程序單元測試的測試輸入數(shù)據(jù)生成工具，一個針對白盒測試標(biāo)準(zhǔn)的單元測試工具，可以生成測試輸入以達(dá)到預(yù)期的覆蓋標(biāo)準(zhǔn)。其主要功能包括兩大部分：C程序的分析和變換，主要包括對C程序進(jìn)行必要的簡化和變換，將C程序解析成抽象語法樹，從C函數(shù)單元中分析出控制流程圖等；C程序的單元測試，自動生成測試用例，并且遵循兩個測試覆蓋標(biāo)準(zhǔn) （分支覆蓋和MC／DC覆蓋）。從圖1CAUT總流程，可以看出CAUT工具在程序開始階段，首先完成各個數(shù)據(jù)結(jié)構(gòu)的初始化操作，隨后將一個路徑輸入前綴傳入執(zhí)行測試執(zhí)行相關(guān)任務(wù)模塊［9－11］。

圖1 CAUT總流程

測試完成后根據(jù)執(zhí)行次數(shù)決定程序流程：若執(zhí)行次數(shù)已經(jīng)達(dá)到預(yù)設(shè)的最大值，或已經(jīng)符合相關(guān)覆蓋標(biāo)準(zhǔn)，則完成本次測試并給出覆蓋報告；若尚未達(dá)到最大執(zhí)行次數(shù)，且尚未達(dá)到覆蓋標(biāo)準(zhǔn)，則從路徑選擇模塊中選擇一條路徑前綴，傳入執(zhí)行約束求解任務(wù)模塊，并將求解結(jié)果作為下次輸入，傳入測試執(zhí)行模塊，繼而循環(huán)執(zhí)行本過程。

從上述過程可知，CAUT工作主要含有3個重要子模塊：測試執(zhí)行模塊，主要負(fù)責(zé)運行時的數(shù)據(jù)收集工作；約束求解模塊，對傳入的路徑前綴進(jìn)行求解；路徑選擇模塊，主要負(fù)責(zé)從路徑池中挑選路徑前綴。

由于本流程中默認(rèn)輸入為已經(jīng)變形并插樁后的文件，所以在整體工作流程之前，本工程還涉及 “源代碼變形分析”重要過程，主要由 CIL （C intermediate language）工具前端處理流程完成。

1.1 Ocaml

OCAML （object CAML）是目前語言CAML中最流行的一種變種語言，它是種函數(shù)式編程語言。它在CAML語言的基礎(chǔ)上增加面向?qū)ο髮樱瑫r結(jié)合模塊化思想，帶有一個以類型推導(dǎo)為基礎(chǔ)的多態(tài)類型系統(tǒng)。OCAML有一個巨大并強(qiáng)悍的標(biāo)準(zhǔn)庫，可以很方便地開發(fā)應(yīng)用程序。本工具針對C語言的解析和處理工作都是基于OCAML語言，所以需要安裝該語言包。

1.2 CIL

CIL是C Intermediate Language的縮寫，它是一個支持對C語言程序進(jìn)行分析和變換的開源的工具包。CIL是由美國加利福尼亞伯克利大學(xué)設(shè)計和開發(fā)，CIL完整支持C99標(biāo)準(zhǔn)，另外也兼容GNU GCC擴(kuò)展和 Microsoft VC擴(kuò)展，實現(xiàn)語言為OCAML。它對C語言解析后的表示形式介于C語言本身和三地址代碼之前，消去原始C程序中的復(fù)雜結(jié)構(gòu)，但同時包含比三地址代碼更豐富的程序信息。另外它也提供一系列的工具，比如StackGuard用于檢查緩沖區(qū)溢出，Merger用于整個源代碼工程代碼合并為一個獨立的可編譯文件，便于進(jìn)行程序的整體分析。

2 類型和類型系統(tǒng)

CAUT工具用于C程序單元測試輸入數(shù)據(jù)自動生成，需要做到將測試用例可視化。在CAUT工具運行時階段，約束求解器針對程序中的約束進(jìn)行求解，返回約束中變量的值。但為了可視化測試用例，需要對程序中變量建立類型收集系統(tǒng)，以滿足約束求解器返回的值與程序變量之間的對應(yīng)關(guān)系。

在編譯程序的過程中，變量的類型包含有用的信息，如類型指定變量的取值范圍和對變量所進(jìn)行的操作。對類型的檢查可以大大提高程序的運行效率，例如類型檢查可省去變量是否為空的檢查。

基本上，類型可分為幾個大類：原始類型 （最簡單的類型種類，如整數(shù)和浮點數(shù)）；整數(shù)類型 （數(shù)字的類型，如整數(shù)和自然數(shù)）；浮點數(shù)類型；復(fù)合類型 （由基本類型組合成的類型，如數(shù)組或記錄單元）；子類型；派生類型 （如結(jié)構(gòu)和聯(lián)合）；對象類型；遞歸類型；函數(shù)類型；全稱量化類型；存在量化類型等等。其中，C的類型被分為3個主要組：對象類型、函數(shù)類型和不完整類型，對象類型基本上用來聲明變量，函數(shù)類型用于聲明函數(shù)，不完整類型是對象類型在一些重要信息，未被提供時的一種特殊情形。一個不完整類型通常需要在被補(bǔ)充上所需的信息后達(dá)到完整［12，13］。

類型系統(tǒng)在理論上主要的研究方向是把它作為研究語言的形式化工具和開發(fā)語言的形式化方法，建立研究的模型和實現(xiàn)語言的規(guī)范［14］。而在本項目中，注重類型系統(tǒng)關(guān)于收集類型的實現(xiàn)過程。

類型自身也有結(jié)構(gòu)，把這種結(jié)構(gòu)定義為類型表達(dá)式。它可以是基本類型，例如int等，也可以是通過把被稱為類型構(gòu)造算子的運算符作用于類型表達(dá)式而得到，例如struct、union等。

本項目基于Alfred V.Aho的Compilers中對類型表達(dá)式的遞歸定義，將其作為類型系統(tǒng)的理論框架，對待測程序中可能出現(xiàn)的類型進(jìn)行詳細(xì)分析和設(shè)計，包括基礎(chǔ)類型和用戶自定義類型。

3 CAUT編譯系統(tǒng)中的類型系統(tǒng)構(gòu)建

3.1 編譯前段類型系統(tǒng)構(gòu)建

基于Compilers關(guān)于類型及類型表達(dá)式的定義，需要在編譯前端中，依靠CAUT前段工具CIL將C程序源碼合并為一個單獨的可編譯文件，CIL對C語言程序分析并得到源代碼的類型信息等相關(guān)信息，然后存儲到對應(yīng)的數(shù)據(jù)庫中。

其中，CIL分析源碼時，為了記錄當(dāng)前變量的相關(guān)信息，需要記錄每個類型的信息，所以在此提出一個類型收集系統(tǒng)的構(gòu)建方案。類型收集系統(tǒng)的一個直接應(yīng)用就是用于編譯程序的開發(fā)，本項目基于CIL編譯待測程序，CIL作為一個開源程序，提供一套近乎完全的編譯前端，也提供用戶在其編譯前端上做修改，以便用戶得到自己所需要的數(shù)據(jù)結(jié)構(gòu)。本項目欲編譯待測程序后，收集運行時數(shù)據(jù)類型和數(shù)據(jù)值，以便后續(xù)打印。

基于CIL的編譯前端中的C語言類型收集系統(tǒng)設(shè)計架構(gòu)主要分為3個模塊：Type Visitor、Record Type和Register Type模塊。

表1Record Type模塊是記錄類型的算法：輸入為一種類型，輸出為包含所有類型的數(shù)組。首先檢查傳入的類型名稱在數(shù)組中是否存在，如果當(dāng)前的類型數(shù)組中沒有，則將類型插入數(shù)組中，并分析類型種類，若為非函數(shù)類型的復(fù)雜類型，則分析當(dāng)前類型的子類型，若為函數(shù)類型，則獲取其返回值類型和參數(shù)類型。

表1 Record Type模塊

表2Type Visitor模塊是對待測程序中類型和全局對象分析算法：輸入為待測程序，輸出為程序中的類型集合。分析程序中的類型和全局對象，如果獲取程序中的是全局對象，包括復(fù)雜類型和枚舉類型，就記錄該類型；如果獲取的是類型，再分析是不是TNamed（用戶自定義類型），如果是，則展開該類型，獲取其子類型，如果不是，則直接記錄。

表2 Type Visitor模塊

表3Register Type模塊主要對待測程序進(jìn)行類型插樁，用于向編譯后端提供類型接口：輸入為待測程序類型集合，輸出為類型插樁函數(shù)。首先在待測程序中打印類型插樁函數(shù)頭，并打印臨時變量，然后對記錄好的類型數(shù)組進(jìn)行遍歷，打印其對應(yīng)的類型函數(shù)，具體如圖2所示。

表3 Register Type模塊

該類型系統(tǒng)中還有一個輔助模塊get＿type＿content，用以根據(jù)類型返回類型的名稱和其元類型。類型包括primitive type、數(shù)組、函數(shù)、指針、復(fù)雜、枚舉和unsigned long類型。

編譯前端關(guān)于類型分析和記錄的流程如圖2類型前端總流程所示：源代碼首先要經(jīng)過Type Visitor調(diào)用，該模塊會對程序中的類型和全局對象進(jìn)行遍歷，遍歷過程中會調(diào)用Record＿type模塊，用于記錄類型和全局對象。當(dāng)遍歷完待測程序后，模塊Register＿type會遍歷當(dāng)前的type＿list，每獲取其中的一個元素，就打印相對應(yīng)的類型函數(shù)。

3.2 編譯后端類型系統(tǒng)構(gòu)建

編譯前端收集到C程序單元的類型系統(tǒng)，記錄程序變量的數(shù)據(jù)類型，在CAUT約束求解模塊中，求解器可以求解出在本次迭代中變量的運行時值，但在下一次迭代中該運行時值會被刪除，故需要在編譯后端先在運行時通過前端插樁函數(shù)的響應(yīng)，完成對所有程序中出現(xiàn)的數(shù)據(jù)類型原型做記錄，方便記錄程序變量的每一次迭代所求解出的運行時值。

圖2 類型前端總流程

CAUT的類型系統(tǒng)將基礎(chǔ)類型、指針類型、結(jié)構(gòu)體、聯(lián)合體、數(shù)組、枚舉以及函數(shù)類型進(jìn)行封裝，對外表示的數(shù)據(jù)類型定義為datatype＿t（如圖3datatype＿t數(shù)據(jù)類型描述的類型信息所示），該數(shù)據(jù)類型的內(nèi)部表示為每種類型標(biāo)識Id，類型名稱Name，類型對象所占內(nèi)存大小Size，元類型Members和類型信息。其中，類型信息用于描述類型詳細(xì)信息，包括有無符號整型與浮點型。

圖3 datatype＿t數(shù)據(jù)類型描述的類型信息

內(nèi)核在運行時維護(hù)一張datatype＿table表，該表記錄每一個類型信息 （datatype＿t指針）和其對應(yīng)的id，有對應(yīng)的接口使用指定的標(biāo)識將類型注冊到類型系統(tǒng)中，如果表中存在同一個id的注冊，將采用覆蓋已存在的注冊類型機(jī)制。其它接口可以通過類型的標(biāo)識或者類型名稱就可以從該表中獲取到類型對象，類型對象就包括該類型的所有信息，在獲取結(jié)構(gòu)體、聯(lián)合體、數(shù)組及枚舉類型的成員類型時，可按成員序號獲取，結(jié)構(gòu)體還可以按偏移量來獲取成員類型。運行時結(jié)束時，需要釋放并回收該表所占內(nèi)存空間。

內(nèi)核為了完全滿足于可視化程序中變量的測試用例值，還需要存儲變量名稱以及其邏輯地址，這樣，內(nèi)核在可視化測試用例時候就可以用其邏輯地址在type model中查找運行時值。

類型系統(tǒng)定義了一個input＿var＿t結(jié)構(gòu)體對象，其數(shù)據(jù)類型內(nèi)部表示為變量名稱、變量的邏輯地址以及變量在類型系統(tǒng)中注冊的值。內(nèi)核從前端提供的store＿input＿var接口將待測程序中所出現(xiàn)的輸入變量名稱、邏輯地址和其類型記錄到一張g＿input＿var＿set表中。當(dāng)運行時結(jié)束時，需要清除并回收該表空間。

當(dāng)約束求解器計算出變量的運行時值時，內(nèi)核通過調(diào)用print＿testcase接口輸入變量的類型信息和地址值來將測試用例可視化，如表4測試用例可視化表所示，該可視化表顯示迭代次數(shù)，變量名稱，變量類型和變量的運行時值。該接口實現(xiàn)打印基礎(chǔ)類型、指針、數(shù)組、結(jié)構(gòu)體和聯(lián)合體等類型的功能。打印結(jié)構(gòu)體變量需要累加偏移，打印指針時，需要將其本身地址轉(zhuǎn)化成其指向成員的真實地址。

表4 測試用例可視化

4 應(yīng)用實例

本項目已經(jīng)在CAUT中實現(xiàn)類型系統(tǒng)，為了測試該類型系統(tǒng)設(shè)計的有效性，本文對一些開源程序進(jìn)行編譯測試，檢查是否對待測程序中出現(xiàn)的類型有完整的收集和表達(dá)。

本文以開源程序grep中的grep＿xrealloc＿1.c文件作為示例，表5grep＿xrealloc＿1.c文件是該文件的代碼。

表5 grep＿xrealloc＿1.c文件

在本項目下首先生成編譯文件 （.／configure），然后編譯CAUT項目 （make），然后輸入相應(yīng)的命令執(zhí)行，則該文件對應(yīng)的類型文件grep＿xrealloc＿1.cil.c就存在該路徑下，該文件詳細(xì)記錄待測程序中的變量類型，函數(shù)返回類型和函數(shù)參數(shù)類型以及類型插樁函數(shù)。表6待測程序類型表包括類型種類Type、類型名稱Type＿name和復(fù)雜類型的成員Member。

表6 待測程序類型

表7待測程序類型插樁函數(shù)包含類型插樁函數(shù)，其中＿＿CAUT＿ctype＿t為CAUT工具自定義的類型，用于定義類型插樁函數(shù)＿＿CAUT＿create＿primitive＿type的返回值，該函數(shù)有4個參數(shù)，第一個為類型名，第二個為類型名長度，第三個為類型所占字節(jié)大小，第四個為類型id號。＿＿CAUT＿reg＿ret為CAUT注冊數(shù)據(jù)類型函數(shù)＿＿CAUT＿register＿datatype的返回值，該函數(shù)有兩個形參，第一個為id號，第二個為對應(yīng)id號的類型插樁函數(shù)的返回值。

通過編譯前端記錄的這些類型信息，交給編譯后端，編譯后端通過接收前端傳入的類型插樁函數(shù)來建立一張datatype＿table表，這里只列出跟待測函數(shù)相關(guān)的變量類型datatype＿name、類型名稱var＿name和在內(nèi)存中所占的空間大小var＿size。具體如表8datatype＿table表所示。

表7 待測程序類型插樁函數(shù)

表8 datatype＿table表

編譯后端通過約束求解器根據(jù)不同的分支返回變量的值，類型系統(tǒng)通過獲取內(nèi)存中的值和對應(yīng)的類型將值可視化。在dfs策略 （depth－first search）下，grep＿xrealloc＿1的測試用例如表9grep＿xrealloc＿1.c在dfs策略下的測試用例所示：該圖可視化迭代次數(shù)，其中每行顯示3個域，第一個是變量名稱，第二個是變量類型，第三個是變量值。

表9 grep＿xrealloc＿1.c在dfs策略下的測試用例

5 結(jié)束語

目前對于類型系統(tǒng)的研究很廣泛，本文首先介紹關(guān)于類型和類型系統(tǒng)的基本概念，并提出用CIL構(gòu)建C語言程序的類型系統(tǒng)。解決當(dāng)下測試自動化工具中測試用例可視化的問題，幫助測試工作完全的自動化，節(jié)省測試工作的投入。

對于研究和設(shè)計程序設(shè)計語言，類型系統(tǒng)為其提供形式化的工具和方法，對軟件工程具有重要的意義。我們用實驗驗證該類型系統(tǒng)的有效性，將來我們的工作是有關(guān)于類型檢查的研究。

［1］Boonstoppel P，Cadar C，Engler D.Rwset：Attacking path explosion in constraint－based test generation ［C］／／Proceedings of the Theory and Practice of Software，14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems，2008：351－366.

［2］Atif M Memon，Myra B Cohen.Automated testing of GUI applications：Models，tools and controlling flakiness ［C］／／Proceedings of the International Conference on Software Engineering，2013.

［3］Inderveer Chana，Priyanka Chawla.Testing perspectives for cloud－based applications ［J］.Software Engineering Frameworks for the Cloud Computing Paradigm Computer Communications and Networks，2013：145－164.

［4］Nguyen，CD，Marchetto A，Tonella P.Test Case prioritization for audit testing of evolving Web services using information retrieval techniques ［C］／／IEEE International Conference on Web Services，2011.

［5］Ho Cheng－Yuan，Wang Fu－Yu，Tseng Chien－Chao，et al.NAT－compatibility testbed：An environment to automatically verify direct connection rate ［J］.IEEE Communications Letters，2011，15 （1）：4－6.

［6］Huang W Y，Hu J W，Lin S C，et al.Design and implementation of automatic network topology discovery system for international multi－domain future internet testbed ［J］.Journal of Internet Technology，2013，14 （2）：181－188.

［7］Tarik Nahhal.A formal framework of hybrid test cases generation applied to embedded systems ［J］.IJCSI International Journal of Computer Science Issues，2013，10 （2）：337－345.

［8］Burnim J，Sen K.Heuristics for scalable dynamic test generation ［C］／／Washington，DC，USA：Proceedings of the 23rd IEEE／ACM International Confere－nce on Automated Software Engineering.IEEE Computer Society，2008：443－446.

［9］Yu Xiao，Sun Shuai，Pu Geguang，et al.A parallel approach to concolic testing with low－cost synchronization ［C］／／Shanghai，China：Proc the 4th International Wokshop on Harnessing Theories for Tool Support in Software，2010.

［10］Wang Zheng，Yu Xiao，Sun Tao，et al.Test data generation for derived types in C program ［C］／／Tianjin，China：Proc the Third IEEE International Symposium on Theoretical Aspects of Software Engineering，2009.

［11］Anand S，Godefroid P，Tillmann N.Demand－driven compositional symbolic execution ［C］／／Procee－dings of the Theory and Practice of Software.14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems，2008：367－381.

［12］Indrdeep Ghosh，Nastaran Shafiei，Li Guodong，et al.JST：An automatic test generation tool for industrial Java applications with strings ［C］／／Proceedings of the International Conference on Software Engineering，2013.

［13］Tillmann N，De Halleux J.Pex：White box test generation for.Net ［C］／／Proceedings of the 2nd International Conference on Tests and Proofs，2008：134－153.

［14］Li Guodong，Li Peng，Geof Sawaya，et al.GKLEE：Concolic verification and test generation for GPUs ［J］.Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming.2012，47 （8）：215－224.