基于時序邏輯的編譯優化測試用例生成方法

摘要：提出一種基于時序邏輯公式的關鍵節點控制圖生成方法，生成的測試用例針對性強，容易擴展；并以該方法改進了一種編譯優化自動化測試工具，在很大程度上消除了其測試冗余，提高了測試效率。

關鍵詞：編譯優化； 測試用例； 時序邏輯； 基本塊； 關鍵節點控制圖

中圖分類號：TP301文獻標志碼：A

文章編號：1001－3695(2007)07－0046－03

0引言

編譯器是軟件開發的基礎支撐工具，其正確性直接影響到應用軟件的可靠性。它需要通過充分測試以保證其質量。編譯器測試用例生成方法可以分為針對前端語法語義的用例生成方法和針對后端優化算法的用例生成方法兩大類[1]。

針對前端語法語義的測試用例生成方法的基本思想是基于語言文法生成測試用例，用于編譯器前端翻譯功能的測試[2，3]。隨著編譯技術的發展，優化技術逐漸成為編譯技術研究的核心內容，出現了一些針對后端優化的測試用例生成方法，文獻[4]介紹一種針對編譯后端優化的基于文法生成代碼的優化測試用例生成方法。首先基于文法生成標準的源程序，再根據具體的優化技術特點加入新的語句以滿足特定優化條件。該方法仍屬于基于文法的用例生成方法，針對性較弱，具有較大局限性。文獻[5，6]對不同的優化類型進行建模，再將模型映射到程序文本作為測試用例。此方法有較好的針對性，但其建模過程和模型映射過程需要對不同的優化進行不同的定制，實現較為復雜。由中國科學院軟件所研制的JTT是一個面向編譯優化的自動化測試工具，它用于嵌入式環境下的C++優化編譯器的系統測試和回歸測試[7]。JTT在自動生成程序控制結構的基礎上，通過某些特定的隨機策略添加計算賦值語句，從而生成完整的測試用例。它缺乏對特定優化精確的形式化描述，難以生成有針對性的優化測試用例，存在大量測試冗余。文獻[8]使用基于時序邏輯的條件重寫規則LHS→RHS ifΦ精確刻畫了編譯優化。其中條件Φ用時序邏輯公式描述。

1基于時序邏輯的編譯優化描述

典型的優化變換能采用基于時序邏輯的條件重寫規則LHS→RHS ifΦ來作精確刻畫[9]。變換由兩部分組成，即變換的一系列動作和保證變換正確性的條件。變換動作通過程序控制流圖中節點和連接邊的變化表示；有四種基本動作，即節點替代(Replace)、邊刪除(Remove_edge)、邊添加(Add_edge)和邊分裂(Split_edge)。如圖1所示，節點替代是用一系列的節點替代控制流圖中的某個節點；刪除邊和添加邊分別是移除和添加控制流圖中的連接邊；分裂邊是在相連接的兩節點間插入中間節點。

3討論及應用

上述算法分為兩個階段：公式規整化和節點生成。其中公式規整化階段將每個條件的公式轉換為標準形式，以便節點生成階段的處理；節點生成階段則生成關鍵節點及關鍵節點之間的控制流。該算法需要的內存空間與公式中所涉及到的節點數量成正比，需要的時間與條件數目以及節點數目成正比。因此，算法一定可以在有限時間內結束。

構造出一個基本塊的關鍵節點控制圖后，可以此為模板很方便地生成大量有針對性的測試用例；可以使用隨機策略或啟發式策略，在關鍵節點控制圖的節點之間插入新的節點。插入的新節點需要滿足插入點之前緊鄰關鍵節點的前向屬性，也需要滿足插入點之后緊鄰關鍵節點的后向屬性。

本文基于前面介紹的方法對JTT工具作了改進，用腳本描述了基于CTL的編譯優化刻畫公式，并在此基礎上利用關鍵節點控制圖生成算法生成了一個基本塊的關鍵控制結構。對于圖中的每一條虛邊，使用隨機策略（可以指定生成代碼的并行程度及嵌套程度）生成實際路徑來代替[7]，插入賦值語句、表達式、變量和常量定義等語句，生成完整的源程序文件。通過改進后，使得JTT測試用例更具針對性，縮短了測試時間，提高了測試效率。在工業界的實踐表明，改進后的JTT能夠取得良好的測試質量。圖5為JTT截圖。

4結束語

傳統的編譯優化測試方法使用基于文法的方法生成測試用例，其針對性差、測試冗余較多。本文在文獻[8]使用時序邏輯公式精確刻畫編譯優化方法的基礎上，提出一種面向編譯優化的測試用例自動生成方法，利用時序邏輯公式中出現的關鍵節點以及節點間的時序關系，構造一個或多個滿足優化條件的基本塊的關鍵節點及節點間的控制關系，并結合實例詳細描述了該方法。該方法生成的測試用例針對性強，適用于多種編譯優化的測試。本文由此改進了JTT，很大程度上消除了測試冗余，提高了測試效率。下一步工作將集中在生成更為豐富的控制結構和數據流信息上。

參考文獻：

[1]BOUJARWAH A S， SALEH K. Compiler test case generation me－thods: a survey and assessment[J]. Information and Software Technology， 1997，39(9):617－625.

[2]PURDOM P. A sentence generator for testing parsers[J]. BIT Numerical Mathematics， 1972，12(3):366－375.

[3]JIANG Liyuan， HUANG Guangjun. An automatic system of generating test cases for compiler[J]. Journal of Northwestern Polytechnical University， 1992，10(2):153－158.

[4]BURGESS C J， SAIDI M. The automatic generation of test cases for optimizing Fortran compilers[J]. Information and Software Technology， 1996，38(2):111－119.

[5]KULIAMIN V V， PETRENKO A K. Applying model based testing in different contexts[EB/OL].2002(2004－12－28).http://www.ispras.ru/groups/rv/downloads/Dagstuhl2004_Kuliamin.pdf.

[6]KOSSATCHEV A， PETRENKO A， ZELENOV S， et al.Using model－based approach for automated testing of optimizing compilers: proc.of the International Workshop on Program Understanding[C]. Novosi－birsk， Russia:[s.n.]， 2003:81－88.

[7]朱丹楓.一種用于測試編譯優化的程序控制結構生成算法[D].北京:中國科學院軟件研究所，2005.

[8]LACEY D. Program transformation using temporal logic specification[D]. Oxford: Oxford University Computing Laboratory， 2003.

[9]CLARKE E M， EMERSON E A， SISTLA A P. Automatic verification of finite－state concurrent systems using temporal logic specifications[J]. ACM Transactions on Programming Languages and Systems， 1986，8(2):244－263.

[10]EMERSON E A， HALPERN J Y. Decision procedures and expressiveness in the temporal logic of branching time[J]. Journal of Computer and System Sciences， 1985，30(1):1－24.

[11]BEN ARI M， MANNA Z， PNUELI A. The temporal logic of bran－ching time[J]. Acta Information， 1983，20:207－226.

[12]KATOEN J P. Principles of model checking[EB/OL]. http://www.cs.auc.dk/~kgl/DAT4F02/KatoenIntro.ps.

注：“本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文”