高級(jí)靜態(tài)分析工具正在成為許多專業(yè)程序員工具包的標(biāo)準(zhǔn)部分。同時(shí)，越來(lái)越重視基于契約的編程，其中明確的前置條件、后置條件和其他契約被添加到源代碼中，以幫助增強(qiáng)軟件安全性和安全性，因?yàn)?a target="_blank">嵌入式系統(tǒng)變得更加復(fù)雜和相互依賴。當(dāng)這兩種趨勢(shì)相遇時(shí)，就會(huì)出現(xiàn)一些有趣的機(jī)會(huì)。特別是，某些高級(jí)靜態(tài)分析工具開始直接識(shí)別合約，有些甚至通過(guò)從現(xiàn)有代碼中推斷出合約來(lái)幫助程序員創(chuàng)建合約。對(duì)高級(jí)靜態(tài)分析的回顧有助于為討論基于契約的編程奠定基礎(chǔ)。

回顧高級(jí)靜態(tài)分析

較新的靜態(tài)分析工具不再簡(jiǎn)單地執(zhí)行編碼指南，而是深入研究程序結(jié)構(gòu)的語(yǔ)義，有效地模擬運(yùn)行時(shí)可能發(fā)生的情況，以檢測(cè)邏輯不一致或安全漏洞。這些工具通常基于編譯器技術(shù)，使用高級(jí)數(shù)據(jù)流分析來(lái)確定程序可能出錯(cuò)的地方，方法是跟蹤變量在運(yùn)行時(shí)可能具有的值，然后檢查這些值是否都被程序正確處理以及是否可能被污染數(shù)據(jù)在被信任之前經(jīng)過(guò)適當(dāng)?shù)膶彶椤Ｔ诖a實(shí)際上安全可靠但工具的價(jià)值跟蹤或污點(diǎn)跟蹤不夠精確的地方，此類工具仍然存在產(chǎn)生誤報(bào)（實(shí)際上是誤報(bào)）的挑戰(zhàn)。盡管如此，

圖 1 說(shuō)明了靜態(tài)分析器如何使用數(shù)據(jù)流分析來(lái)跟蹤變量（例如Count ）的可能值，并確定這些值中的任何一個(gè)是否可能在以后的某個(gè)時(shí)間點(diǎn)導(dǎo)致問題。正在顯示表格的值，然后是平均值。這里的經(jīng)典“錯(cuò)誤”是忽略表為空的可能性，從而導(dǎo)致可能的被零除錯(cuò)誤。

圖 1：高級(jí)流量分析示例

在這個(gè)例子中，為了避免被零除，程序員已經(jīng)包含了一個(gè)表有至少一個(gè)元素的斷言（即“ Table‘Length 》= 1） ”。但是，需要進(jìn)行一些數(shù)據(jù)流分析來(lái)驗(yàn)證Float（Count）在除法“ Sum / Float（Count） ”中是否非零。這需要靜態(tài)分析器將Float（Count）的值鏈接到Count的值，將Count的最終值鏈接到由Table’Range確定的循環(huán)迭代次數(shù)，并將該數(shù)字鏈接到Table‘Length（X’Range 表示“X‘First 。. X’Last”，而 X‘Length 表示“（如果 X’First 》 X‘Last then 0 else X’Last – X‘First + 1）”）。對(duì)程序員來(lái)說(shuō)容易的事情可以為靜態(tài)分析器做更多的工作。

那么靜態(tài)分析器對(duì)“ pragma Assert（Table’Length 》= 1） ”做了什么？這就是分析器不同的地方，這取決于他們是采用自下而上還是自上而下的策略來(lái)發(fā)現(xiàn)跨越過(guò)程邊界的錯(cuò)誤，以及他們?nèi)绾螌⑦@一點(diǎn)與基于合同的編程概念相結(jié)合。

基于合同的編程適合的地方

基于契約的編程（除其他外）是使用前置條件和后置條件來(lái)表達(dá)對(duì)組成程序的功能和過(guò)程（即子程序）的輸入和輸出（分別）的期望。

在圖 1 的示例中，程序員的意圖顯然是“ Table‘Length 》= 1 ”作為該過(guò)程的先決條件。不幸的是，這個(gè)Assert隱藏在過(guò)程的代碼中，而不是很容易被調(diào)用者看到。在 Eiffel［1］ 或 Ada 2012［2］ 等語(yǔ)言中，前置條件和后置條件是語(yǔ)法的一部分，或者在 C# 或 Java 等語(yǔ)言中使用 Spec#［3］ 或 Java 建模語(yǔ)言 （JML）［4］ 等擴(kuò)展，程序員對(duì)Display_Table過(guò)程的表輸入的意圖可以使用顯式前置條件來(lái)表達(dá)。例如，在 Ada 2012 中，此過(guò)程的規(guī)范可以寫成：

過(guò)程 Display_Table（Table： Float_Array） 與 Pre =》 Table’Length 》= 1;

這為Display_Table過(guò)程指定了方面Pre（“前提條件”的縮寫），因此它對(duì)調(diào)用者可見并有效地成為Display_Table上的合同，這表明只要Table的長(zhǎng)度至少為 1，Display_Table就可以執(zhí)行它的正確工作。

靜態(tài)分析：檢查和推斷合約

現(xiàn)在回到圖 1 中的 pragma Assert。如果沒有明確的合同要求調(diào)用者確保Table‘Length 》= 1，靜態(tài)分析器可能會(huì)正確地抱怨，因?yàn)闆]有什么可以阻止調(diào)用者傳入零長(zhǎng)度表。但是，許多靜態(tài)分析器使用不同的策略。他們不是立即抱怨Assert，而是依靠更多的全局檢查來(lái)確定是否存在真正的問題，并且僅在有一個(gè)通過(guò)零長(zhǎng)度表的調(diào)用時(shí)才抱怨。如前所述，這些全局的、過(guò)程間的檢查可以主要是自下而上的，也可以主要是自上而下的，如圖 2 所示。

圖 2：自上而下與自下而上的過(guò)程間靜態(tài)分析

在自上而下的策略中，分析器從程序的入口點(diǎn)向下走，在每次調(diào)用時(shí)用實(shí)際參數(shù)代替形式，直到識(shí)別出每個(gè)子程序的每次調(diào)用，累積一組可能的實(shí)際值傳入對(duì)于每個(gè)正式的。然后使用該值集來(lái)確定是否可能通過(guò)某些特定的調(diào)用鏈違反Assert 。

在自下而上的策略中，分析從程序的葉子（不進(jìn)行調(diào)用的子程序）開始，分析每個(gè)子程序以確定它對(duì)其輸入施加的要求。在此示例中，Assert（Table’Length 》= 1）被有效地轉(zhuǎn)換為過(guò)程的隱式前提條件。靜態(tài)分析器本質(zhì)上是在為每個(gè)子程序推斷未聲明的合約，然后將其傳播到每個(gè)調(diào)用點(diǎn)，其中前提條件成為調(diào)用點(diǎn)實(shí)際參數(shù)的隱式斷言。這個(gè)過(guò)程一直持續(xù)到更高級(jí)別的子程序，直到最終整個(gè)程序都被分析完。

隨著程序變得越來(lái)越大，自下而上的方法可以比自上而下的方法更好地?cái)U(kuò)展，但它取決于推斷潛在的復(fù)雜合同，包括條件先決條件，其中一個(gè)輸入的先決條件可能取決于另一個(gè)輸入的值。例如，對(duì)于以“ if X 》 0 then Assert（Y 》 0） ”開頭的過(guò)程，推斷的前提條件應(yīng)該是“ X 》 0 ==》 Y 》 0 ”。兩種通過(guò)自下而上分析推斷合約的高級(jí)靜態(tài)分析工具是 AdaCore［5］ 的 CodePeer 工具，它分析 Ada 源代碼，以及 Microsoft Research［6］ 的 Clousot 工具，它分析 .NET 程序。

隨著明確的前置條件和后置條件開始出現(xiàn)在程序中，使用像 Ada 2012 這樣的語(yǔ)言，這些合同和高級(jí)靜態(tài)分析工具的功能之間出現(xiàn)了新的協(xié)同作用。顯式契約可以簡(jiǎn)化程序間分析，因?yàn)槌绦騿T已經(jīng)完成了艱苦的工作。該工具可以簡(jiǎn)單地檢查顯式前提條件，而不必在調(diào)用中傳播。在子程序中，該工具可以使用前置條件作為可能輸入值的精確描述，而無(wú)需猜測(cè)程序員的意圖。

顯式契約還可以幫助其他希望利用子程序的程序員，因?yàn)樗鼈兂洚?dāng)機(jī)器可檢查的注釋和直接嵌入代碼中的低級(jí)需求。但它們只有在程序員編寫它們時(shí)才有幫助。由于一些高級(jí)靜態(tài)分析工具可以從源代碼中推斷出合約，它們可以提供自動(dòng)將它們插入源代碼。Clousot［6］ 之類的工具允許程序員“祝福”推斷的合約，使其成為源代碼的永久部分。

未來(lái)：一邊編程一邊證明

靜態(tài)分析和基于合同的編程之間的協(xié)同作用可能允許更快地采用這兩種技術(shù)。隨著這兩者的集成，一種新的編程方法可能會(huì)出現(xiàn)，程序員的助手會(huì)在創(chuàng)建源代碼時(shí)幫助推斷和檢查合同。隨著程序的編寫，安全性得到了證明，就像文本編輯器中的拼寫檢查器可以確保不會(huì)出現(xiàn)拼寫錯(cuò)誤的單詞一樣。隨著這些技術(shù)的成熟，我們可以希望不安全、不安全的程序?qū)⒉辉偈浅B(tài)，而是從一開始就內(nèi)置安全性和安全性，并附帶代碼的機(jī)器可檢查、人類可讀的合約。書面。CodePeer［5］ 和 Clousot［6］ 等工具展示了一些可能性。

審核編輯：郭婷