高級靜態(tài)分析工具不再是新鮮事物，而是成為標準專業(yè)開發(fā)人員工具包中真正的戰(zhàn)略元素。

一些早期的靜態(tài)分析工具嚴格按照逐個函數(shù)或逐個模塊的方式運行，很少或根本沒有跨模塊分析。接下來是“整個程序”分析，工具可以在其中找到可能的運行時故障，但前提是給出感興趣程序的所有源代碼。今天，我們看到的工具可以對程序的某些部分有效，例如軟件庫或軟件子系統(tǒng)，而無需人工“驅動程序”代碼來激活庫或子系統(tǒng)中的代碼。

靜態(tài)分析正在成為專業(yè)開發(fā)人員工具集的標準部分。美國國防部已經(jīng)認識到靜態(tài)分析在幫助識別軟件密集型系統(tǒng)中的安全漏洞和弱點方面的重要性。 許多非國防組織也開始將靜態(tài)分析作為其日常軟件衛(wèi)生的一部分，因為靜態(tài)分析在早期識別使用更傳統(tǒng)的測試不易檢測到的問題方面提供了獨特的優(yōu)勢。但是現(xiàn)在已經(jīng)確定了它們的好處，我們需要更仔細地研究各種工具的功能，并了解如何在現(xiàn)代開發(fā)環(huán)境中最有效地部署它們。

幾乎所有軟件開發(fā)組織都提倡代碼庫或代碼子系統(tǒng)的重用，至少在組織內是這樣。不幸的是，許多靜態(tài)分析工具不能很好地適應分析完整可執(zhí)行程序以外的任何內容。這是因為許多靜態(tài)分析工具首先找到給定例程的所有調用者，然后有效地替換在任何這些調用中傳遞的參數(shù)值集，以確定感興趣的例程是否可能在給定輸入上失敗。因此，要對庫執(zhí)行靜態(tài)分析，程序員必須首先創(chuàng)建范圍廣泛的單元測試集，然后將靜態(tài)分析應用于這些測試。這在一定程度上降低了靜態(tài)分析工具的潛在優(yōu)勢，

通過一種基于從代碼本身推斷構建的前置條件和后置條件（通常稱為“合同”）的軟件庫靜態(tài)分析方法，同時還適應程序員提供的斷言和前置條件和后置條件合同，分析工具非常有效地分析了庫中的所有代碼，并且作為一個附帶好處，生成了人類可讀的合同，總結了每個庫例程的要求和效果。

分析可重用庫

一種新型的靜態(tài)分析工具正在出現(xiàn)，它擺脫了為正在分析的代碼提供驅動程序或線束的需求（圖 1）。這些工具可以自下而上地工作，從程序的葉例程或庫開始，并朝著更高級別的例程工作。此類工具從代碼本身推斷例程的契約（前置條件和后置條件），確定例程的算法可以處理哪些值范圍或值組合，以及哪些值集或組合將導致運行時問題，例如在數(shù)組外部建立索引、溢出數(shù)值計算或取消引用可能為空的指針。這種自下而上、基于契約的方法允許這些高級靜態(tài)分析工具提供對程序片段的寶貴見解，從單個模塊到庫和子系統(tǒng)。推斷的合同被設計成人類可讀的，它提供了有用的竣工文檔，以幫助促進手動代碼審查，以及識別原始需求和當前現(xiàn)實之間的不匹配。此類工具的示例包括 AdaCore 的 CodePeer 分析器和 Microsoft Research 的 CC-Check 工具 。

圖 1：可重用庫的靜態(tài)分析。

推斷前置條件和后置條件

在手動代碼審查期間，由高級靜態(tài)分析工具推斷的合同可以幫助識別代碼的直接問題。這是一個例程的示例，其中例程的名稱顯然與其功能不匹配，如分析工具生成的推斷后置條件所示（圖 2）。

圖 2：推斷后置條件的示例。

推斷的后置條件（由 --#postcondition 注釋標識）表明例程返回給定月份自年初以來的天數(shù)，而例程的名稱暗示它應該返回在月。顯然，無論是程序員還是命名例程的人都感到困惑。這只是分析器推斷竣工合同的好處的一個例子。許多其他情況發(fā)生，其中推斷的前置條件或推斷的后置條件表明程序員選擇的算法顯然是錯誤的，給定例程的要求。

靜態(tài)分析器可以通過使用一種巧妙的技術來推斷例程的前置條件和后置條件，該技術首先假設例程的輸入可以采用任何可能的值，然后通過消除可能導致的輸入值或輸入組合繼續(xù)進行執(zhí)行期間的運行時故障。一旦分析器到達例程的末尾，剩余的不會導致運行時失敗的值代表了唯一可以始終安全地傳遞給例程的值，因此代表了例程的有效前提條件。后置條件是通過獲取滿足前置條件的輸入值集并計算它們?yōu)槔痰妮敵錾傻闹导瘉泶_定的。

有條件的先決條件

這種推斷合同的技術對于簡單的直線例程非常有效，但不能捕獲具有在某些但不是所有調用上執(zhí)行的代碼的例程的完整故事。對于這些，我們需要考慮條件前置條件，即僅適用于通過例程的某些路徑的前置條件。這是一個示例，說明了條件前置條件的必要性（圖 3）。

圖 3：條件前置條件示例。

此處分析器已推斷出在計算 Y +/- 1 時防止數(shù)值溢出的先決條件，但它需要為通過例程的兩條路徑提供不同的先決條件。它通過發(fā)出條件前置條件來處理這個問題，其形式為“不或者。“這相當于蘊涵” ? 。” 在分析典型的可重用庫時，條件前置條件非常重要，因此能夠捕獲適用前置條件的條件對于對庫或其他可重用子系統(tǒng)進行精確的自下而上靜態(tài)分析至關重要。

記錄關于未分析代碼的假設

分析庫或子系統(tǒng)時出現(xiàn)的另一個問題是它們通常依賴于其他較低級別的庫或子系統(tǒng)，并且希望相對獨立于它可能依賴的庫來分析一個庫。這為高級靜態(tài)分析器帶來了不同的挑戰(zhàn)，即處理從正在分析的代碼到當前分析中未包含的代碼的調用。當調用發(fā)生在當前分析中包含的較低級別的例程上時，自下而上的分析方法為被調用的例程提供推斷的前置條件和后置條件，從而能夠對較高級別的例程進行進一步分析。當被調用的例程不在當前分析中時，一種不同的方法是合適的——即，靜態(tài)分析工具可以跟蹤這個未經(jīng)分析的例程返回的值是如何使用的，并指出正在分析的例程中對這個未經(jīng)分析的代碼進行了哪些假設。例如，如果對返回指針的例程進行調用，并且調用例程立即取消引用該指針而沒有首先檢查它是否為空，則顯然假定此未經(jīng)分析的例程返回的指針是非空的（在例如，調用發(fā)生在第 12 行，由 @12 表示，圖 4）。

圖 4：調用未分析代碼的假設示例。

類似地，調用代碼可能會對數(shù)字返回值的值范圍或更復雜的返回對象的初始化狀態(tài)做出假設。通過顯式記錄調用代碼的所有此類假設，分析器可以讓庫實現(xiàn)者更深入地了解對較低級別庫的期望。然后可以將這些假設與低級庫的實際行為進行比較，以驗證低級庫是否被正確使用。

靜態(tài)分析工具的重要性

隨著靜態(tài)分析工具的使用成為軟件開發(fā)過程中不可或缺的一部分，這些工具的功能可以決定獲得的整體價值。成熟的軟件組織一直致力于以庫或子系統(tǒng)的形式創(chuàng)建可重用的軟件，因為眾所周知，整體生產(chǎn)力的關鍵在于為每個應用程序編寫更少的新代碼。高級靜態(tài)分析工具可以通過直接分析庫或子系統(tǒng)來幫助測試可重用組件的可重用性和穩(wěn)健性這一具有挑戰(zhàn)性的任務，而無需創(chuàng)建完整的可執(zhí)行程序可能需要的驅動程序、線束或存根。這些工具可以通過自下而上的方式實現(xiàn)這一目標，首先從可重用組件的葉例程開始，然后以前提條件、后置條件和假設的形式推斷人類可讀的信息。通過這樣做，它們使庫或子系統(tǒng)開發(fā)人員能夠準確了解組件的構建行為，而無需開發(fā)擴展的動態(tài)測試套件。

審核編輯：郭婷