一種快速低內(nèi)存消耗的SMT 全解求解器*

白 楊，賈 悠

（1.中國電子科技集團(tuán)公司第三十研究所，四川 成都 610041；2.電子科技大學(xué) 計(jì)算機(jī)科學(xué)與工程學(xué)院（網(wǎng)絡(luò)空間安全學(xué)院），四川 成都 611731）

0 引言

可滿足性模理論（Satisfiability Modulo Theories，SMT）是用來檢查邏輯公式在一種或者多種理論下的可滿足性。已知一個(gè)邏輯公式φ，一個(gè)SMT 求解器將返回SAT、UNSAT 或UNKNOWN，并且在需要的時(shí)候嘗試構(gòu)建一個(gè)φ的模型m。一個(gè)SMT 全解求解器在給出的公式可滿足時(shí)，嘗試找出所有模型。本文假設(shè)已知公式有有限個(gè)模型，否則不可能找到所有模型。

一個(gè)SMT 全解求解器具有許多（潛在）應(yīng)用。例如，估計(jì)被分析軟件擁有某一屬性的可能性[1]；計(jì)算信息泄漏的不確定性和數(shù)量計(jì)算[2]；還有邊界模型檢查、自動(dòng)測試生成、可靠性分析以及安全性量化[3]。但是，現(xiàn)有的SMT 全解求解器在速度、內(nèi)存消耗以及支持理論類型方面都存在局限性[3-5]。

本文提出了4 個(gè)新的潛在應(yīng)用，并設(shè)計(jì)了一種快速、低內(nèi)存消耗的SMT 全解求解器，采用二分查找（Binary Search，BS）把搜索空間根據(jù)先前的模型動(dòng)態(tài)劃分為多個(gè)較小子空間，并嘗試在一個(gè)子空間中找到一個(gè)模型。當(dāng)所有模型都產(chǎn)生后，程序終止。BS 方法帶來兩個(gè)優(yōu)點(diǎn)：一是在原始公式后附加描述子空間邊界的子句，附加子句的數(shù)量受變量數(shù)量限制而傳統(tǒng)的BCM 方法在該方面有明顯的缺陷，子句會(huì)隨著生成模型的增加而增加；二分查找支持具有“來自不同模型的相同變量的分配可以互相比較”屬性的理論。由于許多理論如布爾、位向量、整數(shù)、實(shí)數(shù)、浮點(diǎn)數(shù)以及字符串等都符合此要求，所以提出的方法可以對(duì)這些理論的問題進(jìn)行求解。

此外，本文的方法應(yīng)用上下文感知（Context Aware，CA）機(jī)制加快求解速度，同時(shí)，通過應(yīng)用暫停恢復(fù)機(jī)制（Suspend Resume，SR）機(jī)制來降低內(nèi)存消耗。結(jié)果表明，BS、BS+CA、BS+SR 和本文提出的方法分別將BCM 方法的求解速度分別加速了4.6 倍、13.4 倍、7.3 倍以及32.4 倍。此外，與BCM 方法相比，本文提出的方法的內(nèi)存消耗只有其35.3%，并且還能通過并行化處理進(jìn)一步提升速度。

綜上所述，本文有3 個(gè)主要貢獻(xiàn)：

（1）介紹了SMT 全解求解器的4 種潛在應(yīng)用，這4 種應(yīng)用在現(xiàn)有的研究中未被提到；

（2）設(shè)計(jì)了基于BS 的SMT 全解求解器，該方法支持多種理論，并集成了CA 和SR。

（3）實(shí)驗(yàn)結(jié)果表明，本文的提出的方案有速度快、內(nèi)存消耗低、能夠通過并行方式加速等優(yōu)點(diǎn)。

1 新應(yīng)用研究

介紹提出的SMT 全解求解器的4 個(gè)潛在的新應(yīng)用，這些應(yīng)用在現(xiàn)有的研究中沒有被討論過，且現(xiàn)有的SMT 全解求解器[3-5]不支持這些應(yīng)用?，F(xiàn)有的SMT 全解求解器只能夠找到并返回邏輯公式φ關(guān)于布爾值的所有模型。3 個(gè)應(yīng)用與外部代碼有關(guān)，這些外部代碼只能作為黑盒進(jìn)行分析，如其他模塊、進(jìn)程、內(nèi)核甚至遠(yuǎn)程服務(wù)中的代碼。

1.1 上下文感知外部代碼探索器

為動(dòng)態(tài)程序分析提供有效的測試輸入極具挑戰(zhàn)，尤其是在被分析的軟件調(diào)用外部代碼時(shí)。如果分析人員能找到外部代碼路徑并收集路徑條件，則外部代碼的所有行為可以通過本文提出的方法產(chǎn)生的模型運(yùn)行外部代碼來探索。此外，使用本文方法，分析者可以對(duì)外部代碼在不同情況下的行為進(jìn)行比較。

1.2 增強(qiáng)型靜態(tài)程序分析

由于實(shí)際程序中通常會(huì)大量使用外部代碼，因此會(huì)阻止進(jìn)行徹底的靜態(tài)程序分析。傳統(tǒng)的方法如手工編寫外部代碼模型既麻煩又容易出錯(cuò)。通過本文提出的方法可以使用生成的測試輸出來探索外部代碼，因此執(zhí)行外部代碼的有效性可以被包含在靜態(tài)分析中。為了找到外部代碼所有可能行為，需到達(dá)外部代碼的所有可行路徑（即所有有效上下文）。

1.3 外部感知混合執(zhí)行

混合執(zhí)行是一種多路徑程序分析技術(shù)。但是，在分析實(shí)際程序時(shí)，如何處理外部代碼是一項(xiàng)有難度的工作。通過本文提出的方法，分析人員可理解外部代碼在特定上下文中的行為。因此，本文的方法通過引入描述執(zhí)行外部代碼產(chǎn)生影響的新約束來執(zhí)行外部代碼（如代表外部函數(shù)的所有可能返回值的約束）。

1.4 診斷路徑分歧

路徑分歧表示預(yù)期程序路徑和實(shí)際執(zhí)行的程序路徑不匹配。路徑分歧的根本原因很難定位和診斷，因?yàn)樗赡軙?huì)在很寬的范圍內(nèi)在入口和分支之間發(fā)生分歧。本文提出的方法有助于通過產(chǎn)生多個(gè)測試輸入來縮小檢查范圍。由于分歧可能會(huì)發(fā)生在當(dāng)前分歧分支前，因此引入本文方法做路徑分歧診斷能夠輔助分析員節(jié)省分析開銷。

2 動(dòng)機(jī)闡述

下面闡述使用本文提出的方法采用二分搜索來求解公式。

式（1）共 有100 萬（100×100×100）個(gè) 模型。其中第一個(gè)模型m0通過求解φ得到{x=50,y=50,z=50}。

傳統(tǒng)BCM 方法獲取下一個(gè)模型m1，新公式φ1是φ和子句(x≠50)∨(y≠50)∨(z≠50)的析取，可表示為：

隨后通過求解φ1得到m1。一直迭代上述流程，直到找不到模型為止。BCM 會(huì)導(dǎo)致子句隨著模型的增加而增加。極致情況下，找到最后一個(gè)模型m1000000，對(duì)應(yīng)的公式φ1000000包含了1 000 000 個(gè)子句。大量子句會(huì)花費(fèi)過多內(nèi)存，并在很大程度上減慢了求解過程。

提出的BS 方法和上述方法一樣，通過求解φ產(chǎn)生與上述方法相同的第一個(gè)模型m0。隨后產(chǎn)生6個(gè)公式φ1～φ6對(duì)應(yīng)6 個(gè)任務(wù)動(dòng)態(tài)劃分搜素空間，如圖1 所示，如φ6=φ∧((x==50)∧(y==50)∧(z＞50))。

圖1 一個(gè)例子闡述二分查找

增量子句來描述子空間邊界，如x＜50 表示子空間：

-INF和+INF表示可以由變量獲取的最小值和最大值。如果在原始子空間找到模型，則這個(gè)子空間可以被分為更小的子空間。例如，可以通過求解φ6找到一個(gè)模型{x=50,y=50,z=80}，隨之產(chǎn)生兩個(gè)新公式：

反復(fù)執(zhí)行該操作，直到所有生成的公式都完成求解。與BCM 相比，所有的BS 生成的公式添加一個(gè)或多個(gè)子句來描述子空間的邊界。增加的子句數(shù)量由變量個(gè)數(shù)決定，而不是由模型數(shù)量來決定的。因此，這個(gè)例子中，由BS 產(chǎn)生的公式包含不超過4 個(gè)子句，而同樣的問題傳統(tǒng)BCM 方法的φ1000000包含1 000 000 個(gè)子句。

3 一種快速低內(nèi)存消耗的SMT 全解求解器

本文設(shè)計(jì)了一款快速低內(nèi)存消耗的SMT 全解求解器，基于Z3[6]求解器實(shí)現(xiàn)。下面將介紹這種方法用到的多種優(yōu)化方法的設(shè)計(jì)，包括CA、SR 以及并行優(yōu)化。

3.1 基于上下文感知（CA）機(jī)制的優(yōu)化

CA 適用于連續(xù)求解過程，因?yàn)镾MT 求解器在求解當(dāng)前方程的過程中需要學(xué)習(xí)大量知識(shí)。為了構(gòu)造上下文感知機(jī)制，利用現(xiàn)代SMT 求解器（如Z3）支持的push/pop 命令來實(shí)現(xiàn)。提出的方法能夠通過push 命令在求解原始公式后迅速記住上下文信息。求解任務(wù)基于已經(jīng)記住的上下文內(nèi)容，通過添加子句來描述變量子空間。求解完畢后，上下文內(nèi)容通過pop 命令進(jìn)行恢復(fù)。

3.2 并行化優(yōu)化

由于求解器具有多任務(wù)模式且易于并行化處理，為了更好地利用硬件資源，本文提出的求解器創(chuàng)建了多個(gè)并行運(yùn)行工作程序。每個(gè)工作程序首先從任務(wù)隊(duì)列中獲取任務(wù)（即該位置記錄未執(zhí)行的任務(wù)），然后運(yùn)行任務(wù)生成新任務(wù)，最后將生成的任務(wù)附加到任務(wù)隊(duì)列。該過程反復(fù)進(jìn)行，直到任務(wù)隊(duì)列為空。

將上述兩種方法結(jié)合存在挑戰(zhàn)。具體描述為要了解上下文情況，每個(gè)工作程序應(yīng)該獲取一個(gè)上下文對(duì)象。為此，本文創(chuàng)建了多個(gè)上下文對(duì)象，并使用每個(gè)上下文對(duì)象求解原始公式，然后將所有上下文對(duì)象存儲(chǔ)在池中。上下文對(duì)象的數(shù)量和工作程序數(shù)量相等。因此，任務(wù)的解決過程變?yōu)椋海╝）至少有一個(gè)閑置工作程序；（b）工作程序從池中獲取上下文對(duì)象；（c）工作程序從任務(wù)任務(wù)隊(duì)列中選取一個(gè)任務(wù)；（d）工作程序執(zhí)行任務(wù)；（e）工作程序恢復(fù)上下文并將其釋放回池中；（f）工作程序閑置。

3.3 基于暫停-恢復(fù)（SR）機(jī)制的優(yōu)化

SR 可以暫停求解過程，然后從斷點(diǎn)準(zhǔn)確恢復(fù)它。在掛起過程中，所有未執(zhí)行的任務(wù)內(nèi)存將轉(zhuǎn)存儲(chǔ)到磁盤。本文設(shè)計(jì)了磁盤任務(wù)隊(duì)列，并通過求解原始方程來恢復(fù)上下文內(nèi)容。本文引入緩存隊(duì)列來更好地實(shí)施本優(yōu)化設(shè)計(jì)方案，即本方法使用任務(wù)緩存隊(duì)列和磁盤中的緩存文件一起維持任務(wù)，新生成的任務(wù)將被添加到緩存隊(duì)列中，所有的工作程序從任務(wù)隊(duì)列中選取任務(wù)。如果任務(wù)隊(duì)列為空，工作程序通過從緩存文件中加載任務(wù)來填充任務(wù)隊(duì)列；如果緩存文件為空，求解器用緩存隊(duì)列里的任務(wù)填充任務(wù)隊(duì)列，并清空緩存隊(duì)列。

求解器可以基于SR 通過監(jiān)視內(nèi)存狀態(tài)來控制內(nèi)存消耗。當(dāng)內(nèi)存消耗超過閾值時(shí)掛起，隨后恢復(fù)求解過程。求解器經(jīng)過優(yōu)化I/O 消耗將變小。首先，求解器將寫操作延遲到求解過程被暫停時(shí)來完成，而不是通用的寫操作在產(chǎn)生的時(shí)候就執(zhí)行；其次，求解器將數(shù)百個(gè)任務(wù)添加到內(nèi)存中，而不是直接運(yùn)行任務(wù)；再次，所有未執(zhí)行的任務(wù)被存放到一個(gè)文件，而不是每個(gè)任務(wù)一個(gè)文件，因?yàn)樵L問大量小文件可能會(huì)凍結(jié)文件系統(tǒng)；最后，為了減少磁盤開銷，僅記錄必要信息，如任務(wù)ID 和邊界。

SR 機(jī)制可以設(shè)置求解器在指定條件下運(yùn)行，如可以要求求解器在工作日晚上9 點(diǎn)到早上7 點(diǎn)運(yùn)行，或者可以暫停求解過程，并在另一臺(tái)計(jì)算機(jī)上繼續(xù)執(zhí)行。

4 方法評(píng)估

實(shí)驗(yàn)執(zhí)行環(huán)境說明：4 核Intel i7 CPU，8 GB 主內(nèi)存和250 GB 固態(tài)硬盤電腦。使用本文提出的求解器解決SMT 庫[7]的工業(yè)類別中的8 個(gè)基準(zhǔn)，表明所有公式都是由實(shí)際應(yīng)用生成的。表1 列出了每個(gè)測試公式的名稱、文件大小和變量數(shù)量。將求解每個(gè)公式的時(shí)間預(yù)算設(shè)置為3 h，因此測試時(shí)間為168 h（即120=5×8×3 h），以獲得如表1 所示的結(jié)果。

表1 實(shí)際公式為基礎(chǔ)的實(shí)驗(yàn)結(jié)果

實(shí)驗(yàn)結(jié)果表明，與BCM 相比，本文提出的方法能夠加速求解并降低內(nèi)存消耗。在求解figld.phx時(shí)，本文提出的求解器在3 h 內(nèi)產(chǎn)生的模型數(shù)是BCM 求解器的4.7 倍，使用的內(nèi)存開銷為BCM 求解器的41.8%。

表1 中展示了每個(gè)算法的模型數(shù)量和內(nèi)存消耗、BS+SR 和本文求解器的暫停恢復(fù)次數(shù)。由表1 數(shù)據(jù)可知：本文的方法是最快的方法（比BCM快32.4 倍），且消耗最少內(nèi)存（僅為BCM 方法的35.3%）；BS 的性能比BCM 在求解速度上快，是其4.6 倍；CA 能夠明顯提升BS 優(yōu)化效果，達(dá)到13.4 倍。采用SR 后，比僅有BS 機(jī)制下的求解器消耗更少的內(nèi)存。究其原因，可以理解為降低內(nèi)存消耗的同時(shí)提升求解速度，是以SR 開銷為代價(jià)的（如將未執(zhí)行的任務(wù)轉(zhuǎn)存儲(chǔ)到磁盤中，還原上下文）。

圖3 表明，本文提出的求解器和BS+SR 機(jī)制的求解器保持恒定的求解速度，其他3 個(gè)則從長遠(yuǎn)來看會(huì)變慢，表明SR 對(duì)于解決無法在短期內(nèi)完成的復(fù)雜公式是必須的。這一結(jié)論是合理的，因?yàn)镾R 會(huì)定期重新啟動(dòng)約束求解。

圖3 表明基于BS 和BD+CA 求解器隨著時(shí)間增加持續(xù)增加內(nèi)存開銷，BCM 沒有明顯增加內(nèi)存開銷，這是由于BCM 求解器會(huì)變得很慢導(dǎo)致的，如圖2所示。

圖2 式（3）的模型數(shù)量

表1 和圖3 表明，基于BS+CA 的求解器比基于BS 的求解器需要消耗更多的內(nèi)存（BS+CA 的為4.4 倍，BS 的為2.2 倍）。本文提出的求解器比基于BS+SR 的求解器在給定相同內(nèi)存閾值的情況下暫?；謴?fù)需要更多時(shí)間，前者41.4，后者8.5。導(dǎo)致這一結(jié)果是因?yàn)榛贑A 的求解器需要記住上下文信息。利用SR 機(jī)制的優(yōu)點(diǎn)，可以降低CA 機(jī)制導(dǎo)致的高內(nèi)存開銷。

圖4 表明本文提出的求解器能夠通過并行處理進(jìn)行加速。兩個(gè)工作程序能夠?qū)⑵骄俣忍岣叩?.62 倍，4 個(gè)工作程序能夠?qū)⑵骄俣忍岣叩?.4 倍。下一步可以考慮解決以下實(shí)現(xiàn)限制提升并發(fā)性。所有的工作程序從一個(gè)共享的任務(wù)隊(duì)列中獲取任務(wù)；所有的工作程序添加他們產(chǎn)生的任務(wù)到一個(gè)共享隊(duì)列；如果當(dāng)任務(wù)隊(duì)列為空時(shí)，工作程序嘗試從磁盤獲取任務(wù)，此時(shí)其他工作程序需要等待。

5 相關(guān)工作

MathSat[4]和Z3[3,5]方法嘗試找到關(guān)于布爾變量的所有模型。Lahiri 提出一個(gè)SMT 全解求解器基于DPLL（T）框架[8]來找到SAT 問題下的所有模型。盡管如此，構(gòu)建一個(gè)SMT 全解求解器也不容易，因?yàn)镾AT 內(nèi)核返回一個(gè)單SAT 模型可能表明了多個(gè)SMT 模型。因此，理論上構(gòu)建一個(gè)SAT 全解核需要增強(qiáng)從一個(gè)SAT 模型的多個(gè)SMT 模型派生能力。

LattE[9]計(jì)算了整數(shù)和實(shí)數(shù)上的線性模型，并被廣泛應(yīng)用于文獻(xiàn)[10-12]中。Sankaranarayanan 等[13]提到找通過區(qū)間約束傳播來找到區(qū)間邊界，其中區(qū)間約束傳播比精確模型技術(shù)快，僅限于整數(shù)和實(shí)數(shù)上的線性約束。qCORAL[1]使用區(qū)間約束傳播[14]來將解空間分解成為更小的區(qū)域，然后將采樣應(yīng)用到概率估計(jì)中，但qCORAL 僅支持邊界浮點(diǎn)數(shù)。本文提出的求解器和現(xiàn)有方法不同之處在于于支持多種理論類型，且公式的形式?jīng)]有限制。

6 結(jié)語

全解求解器可以為多種研究領(lǐng)域提供輔助計(jì)算，如軟件測試中的符號(hào)執(zhí)行等?，F(xiàn)有的全解求解器在速度、內(nèi)存消耗或者支持求解的理論類型存在局限性，因此設(shè)計(jì)了一種結(jié)合二分查找（BS）、上下文感知（CA）以及暫?；謴?fù)（SR）等機(jī)制的SMT 全解求解器。實(shí)驗(yàn)結(jié)果證明，該方法比傳統(tǒng)的BCM 求解速度更快，內(nèi)存消耗更小。此外，通過嘗試并行處理方法來優(yōu)化本文的求解器可以發(fā)現(xiàn)并行條件下求解速度能得到進(jìn)一步提升。同時(shí)，本文探討了求解器的4 種潛在應(yīng)用——外部代碼探索、靜態(tài)程序分析、外部感知混合執(zhí)行、診斷發(fā)散?？梢?，本文提出的快速低內(nèi)存開銷的SMT 全解求解器在軟件工程領(lǐng)域有重要的實(shí)踐意義。