[發明專利]一種基于共享不可行路徑池的代碼并行驗證方法和裝置

在審

• 申請號: 202010344638.2
• 申請日: 2020-04-27
• 公開（公告）號: CN111444112A
• 公開（公告）日: 2020-07-24
• 發明（設計）人: 卜磊;閭樂成;謝準一;郭育鯤;趙建華;李宣東
• 申請（專利權）人: 南京大學
• 主分類號: G06F11/36
• 分類號: G06F11/36;G06F8/41
• 代理公司: 江蘇銀創律師事務所 32242
• 代理人: 孫計良

1.一種基于共享不可行路徑池的代碼并行驗證方法，其特征在于，包括如下步驟：

S1：獲取用戶輸入的源代碼和驗證目標，所述驗證目標為用戶所輸入的源代碼中指定位置在所指定的步數內是否可達；

S2：將用戶輸入的源代碼轉換成流程控制狀態圖，并初始化并行任務池T為空，共享不可行路徑池I為空以及所述并行任務池T的最大路徑數K；

S3：根據流程控制狀態圖和驗證目標構建SAT約束編碼G；

S4：將所述共享不可行路徑池I中的各個路徑片段取反編碼后與所述SAT約束編碼G輸入至SAT求解器進行求解；若SAT求解器有解，則將SAT求解器所求的解對應至程序路徑生成相應的潛在程序路徑加入至所述并行任務池T，并將該組解取反加入所述SAT約束編碼G以避免重復路徑；若SAT求解器無解，則說明用戶所輸入的源代碼指定位置在所指定的步數內不可達，結束代碼驗證；

S5：持續步驟S4直到所述并行任務池T中的潛在程序路徑數達到最大路徑數K；

S6：根據并行任務池T的最大路徑數K構建包含K個線程的線程組，然后將所述并行任務池T中的每個潛在程序路徑分別輸入至線程組的各個線程中，由對應的線程進行SMT求解；所述SMT求解包括如下步驟：

S61：根據所輸入的潛在程序路徑和所述流程控制狀態圖構建SMT約束編碼W；

S62：將所構建的SMT約束編碼W輸入至SMT約束求解器；若SMT約束求解器不可解，則抽取其中不可滿足的最小集合X，根據最小集合X生成對應的不可行程序路徑片段，將該不可行程序路徑片段放入所述共享不可行路徑池I中；若SMT約束求解器可解，則說明該潛在程序路徑為能夠到達用戶所輸入代碼指定位置的可達路徑，結束代碼驗證；

S7：轉步驟S4進行迭代。

2.如權利要求1所述的基于共享不可行路徑池的代碼并行驗證方法，其特征在于，所述步驟S6還包括不可行路徑剪枝步驟；

所述不可行路徑剪枝步驟，用于：檢測共享不可行路徑池I中的不可行程序路徑片段是否得到更新，若存在更新，則判斷當前潛在程序路徑是否包含新增的不可行程序路徑片段；若當前潛在程序路徑包含新增的不可行程序路徑片段，則結束該潛在程序路徑所對應的SMT求解線程。

3.如權利要求2所述的基于共享不可行路徑池的代碼并行驗證方法，其特征在于，檢測共享不可行路徑池I中的不可行程序路徑片段是否得到更新采用版本號的方法，具體如下：共享不可行路徑池I設有版本號，每個潛在程序路徑也設有版本號；共享不可行路徑池I的版本號在步驟S2中初始化為0；步驟S4中，每次將潛在程序路徑加入至所述并行任務池T時，該潛在程序路徑的版本號為所述共享不可行路徑池I的版本號；步驟S62中，將不可行程序路徑片段放入共享不可行路徑池I時，遞增共享不可行路徑池I的版本號；檢測共享不可行路徑池I中的不可行程序路徑片段是否得到更新則判斷當前潛在程序路徑的版本號是否與當前共享不可行路徑池I的版本號是否相同即可。

4.如權利要求2所述的基于共享不可行路徑池的代碼并行驗證方法，其特征在于，判斷當前潛在程序路徑是否包含新增的不可行程序路徑片段采用如下方法：獲取所述共享不可行路徑池I中新增的不可行程序路徑片段，將其取反編碼后與當前潛在程序路徑對應的SAT編碼輸入SAT求解器，若此時SAT求解器無解，則表示當前潛在程序路徑包含新增的不可行程序路徑片段。

5.如權利要求2所述的基于共享不可行路徑池的代碼并行驗證方法，其特征在于，所述不可行路徑剪枝步驟被配置于獨立的線程中。