[發明專利]一種基于線性規劃預測的符號執行優化方法及裝置

有效

• 申請號: 202011197098.6
• 申請日: 2020-10-30
• 公開（公告）號: CN112162932B
• 公開（公告）日: 2022-07-19
• 發明（設計）人: 陳振邦;王戟;毛曉光;董威;文艷軍;李姍姍;陳立前;尹良澤;帥子琦
• 申請（專利權）人: 中國人民解放軍國防科技大學
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 湖南兆弘專利事務所(普通合伙) 43008
• 代理人: 胡君

本發明公開一種基于線性規劃預測的符號執行優化方法及裝置，該方法步驟包括：S1.對待測源程序進行符號執行的過程中，收集分支條件信息，生成對應探索路徑上的位向量路徑約束；S2.在求解各探索路徑上的路徑約束前，預先掃描各位向量路徑約束；S3.判斷各位向量路徑約束中是否存在數組操作，如果不存在，則直接轉換為線性規劃模型；如果存在，則根據數組內容信息，轉換為對應的線性規劃模型；S4.求解得到的線性規劃模型并進行可滿足性判斷，如果判斷結果不是不可滿足的，則將對應的位向量約束傳遞給約束求解器以進行求解。本發明具有實現方法簡單、效率高，能夠快速檢測數組約束的不可滿足性，提高可達路徑探索能力等優點。

技術領域

本發明涉及軟件自動測試中符號執行技術領域，尤其涉及一種基于線性規劃預測的符號執行優化方法及裝置。

背景技術

在軟件開發流程中，測試是必不可少的一環。軟件測試通過構造不同的測試用例來執行軟件，期望盡早地發現軟件中的漏洞。目前，測試用例一般都是人工構造的，存在構造成本高、構造效率低的問題，難以達到理想的覆蓋率。測試用例自動生成技術旨在通過軟件手段實現測試用例的自動化生成，從而提高軟件測試的效率。符號執行是測試用例自動生成技術中的重要分支，可以有效生成高覆蓋率的測試用例。在符號執行過程中，程序的輸入被符號化。符號執行器通過符號輸入來執行程序，構建符號路徑條件并轉換成位向量形式的路徑約束加以求解，從而達到系統探索程序路徑的目的，在這個過程里，約束求解的作用至關重要。每當一條程序路徑被探索完時，符號執行器就調用約束求解器來求解該條路徑上的約束，只有當該條路徑上的約束是可滿足的，也即存在某個解使得路徑約束為真，符號執行器才能根據約束求解器返回的解構造測試用例。

約束求解是符號執行中最主要的性能瓶頸，也是影響符號執行高效生成測試用例的關鍵因素。目前符號執行時使用的約束求解器通常是基于可滿足性模理論(Satisfiability-Modulo Theory,SMT)的，即SMT求解器，符號執行中產生的約束被轉換成SMT公式后，再通過該SMT求解器檢查其可滿足性。SMT公式是一種結合了不同背景理論的一階邏輯公式，包括整數理論、位向量理論、數組理論等。而在符號執行場景下，通常是使用位向量理論和數組理論綜合的SMT公式，其可滿足性的判定問題是一個NPC(Non-deterministic Polynomial Complete)問題。在實際程序中，往往會存在大量不可達的路徑，因此對這些程序做符號執行會生成大量不可滿足的路徑約束，使得SMT求解器需要花費大量時間來判斷這些約束的不可滿足性。而且，由于這些路徑約束不存在解，符號執行器無法生成對應的測試用例，造成大量不必要的時間耗費。

發明內容

本發明要解決的技術問題就在于：針對現有技術存在的技術問題，本發明提供一種實現方法簡單、效率高的基于線性規劃預測的符號執行優化方法及裝置，能夠在符號執行過程中快速檢測數組約束的不可滿足性，提高符號執行過程中可達路徑的探索能力。

為解決上述技術問題，本發明提出的技術方案為：

一種基于線性規劃預測的符號執行優化方法，步驟包括：

S1.路徑約束生成：對待測源程序的中間碼進行符號執行的過程中，收集各分支指令處的分支條件信息，并生成對應探索路徑上的位向量路徑約束；

S2.掃描判斷：在求解各探索路徑上的路徑約束前，預先掃描各所述位向量路徑約束，若所述位向量路徑約束中不包含非線性操作且不包含無法線性化的操作，轉入步驟S3；

S3.模型構建：判斷所述位向量路徑約束中是否存在數組操作，如果不存在，則直接將所述位向量路徑約束轉換為線性規劃模型；如果存在，則根據所述位向量路徑約束中的數組內容信息對數組操作進行抽象處理，然后再轉換為對應的線性規劃模型；

S4.模型求解：求解得到的所述線性規劃模型并判斷可滿足性，如果判斷結果不是不可滿足的，則將對應的所述位向量約束傳遞給約束求解器以進行求解。