本文是對於北京大學熊英飛老師《軟件分析》課件以及南京大學李樾老師《軟件分析》課程視頻的總結。
1.哥德爾不完備定理及其在軟件分析中應用
1.1定理內容
對任意能表示自然數的系統，一定有定理不能 被證明
1.2定理應用
主流程序語言的語法+語義=能表示自然數的形式系統 。
哥德爾不完備定理在處理內存泄露判定問題時的應用
設有表達式T不能被證明
a=malloc()
if (T) free(a);
return;
若T為永真式，則沒有內存泄露，否則就可能有。
2.停機問題
2.1停機問題內容
停機問題的實質是判斷一個程序在給定輸入上是否會終止 ，不存在一個算法能回答停機問題。
2.2停機問題實例
假設存在停機問題判斷算法：bool Halt(p) ，p為特定程序，給定某邪惡程序
void Evil() {
if (!Halt(Evil)) return;
else while(1);
}
Halt(Evil)的返回值是什么？
• 如果為真，則Evil不停機，矛盾
• 如果為假，則Evil停機，矛盾
2.3一個檢查停機問題的算法
當前系統的狀態為內存和寄存器中所有Bit的值 ，給定任意狀態，系統的下一狀態是確定的 。令系統的所有可能的狀態為節點，狀態A可達狀態B 就添加一條A到B的邊，那么形成一個有向圖（有限 狀態自動機），如果從任意初始狀態出發的路徑都無環，那么系統 一定停機，否則可能會死機 ，給定起始狀態，遍歷執行路徑，同時記錄所有訪問過的狀 態。 如果有達到一個之前訪問過的狀態，則有環。如果達到終 態，則無環。 因為狀態數量有窮，所以該算法一定終止。
3.可判定問題
判定問題（Decision Problem）：回答是/否的問題
可判定問題（Decidable Problem）是一個判定問題，該問題存在一個算法，使得對於該問題的每 一個實例都能給出是/否的答案。
停機問題是不可判定問題
4.萊斯定理(Rice’s Theorem)
4.1定理內容
我們可以把任意程序看成一個從輸入到輸出上的 部分函數（Partial Function），該函數描述了程序的行為 。
關於程序行為的任何非平凡屬性，都不存在可以 檢查該屬性的通用算法
- 平凡屬性：要么對全體程序都為真，要么對全體程序 都為假
- 非平凡屬性：不是平凡的所有屬性
- 關於程序行為：即能定義在函數上的屬性
- 特別注意萊斯定理的適用條件是關於程序行為而不是結構，並且不適用萊斯定理的也未必可判定。例如程序使用了多少個變量，就是涉及程序結構的問題，所以像[確定程序使用的變量是否多於50個]這樣的問題無法用萊斯定義來說明它是不是不可判定的。
4.2萊斯定理的證明
反證法：給定函數上的性質P，因為P非平凡，所以一定存在程序使 得P滿足，記為ok_prog。假設檢測該性質P的算法為P_holds。
編寫如下函數來檢測程序p是否停機
Bool halt(Program p) {
void evil(Input n) {
Output v = ok_prog(n);
p();
return v;
}
return P_holds(evil);
}
如果P_holds存在，則我們有了檢測停機的算法
5.近似法
5.1定義
近似法：允許在得不到精確值的時候，給出不精確的答案。對於判斷問題，不精確的答案就是不知道。
近似求解判定問題：輸出“是”、“否”或者“不 知道”，我們的目標就是盡可能多的回答“是”、“否”，盡可能少的回答“不知道”。
5.2分類
假設正確答案是一個集合S
-
must分析：返回的集合總是S的子集
-
may分析：返回的集合總是S的超集
must和may的區分並不嚴格，可以互相轉換 ，可以將判定問題取反，或者隊友返回集合的問題，將返回值定義為原集合的補集。
6.軟件分析的評定標准
在編譯器優化中，我們需要保證決定不改變程序的語義 。安全性就是根據分析結果所做的優化絕對不會改變程序語義 。安全性的定義和具體應用場景有關，但往往對應於 must分析和may分析中的一個 。安全性有時也被成為健壯性(soundness)、正確性 (correctness) 。 健壯性的反面有時也被稱為完整性(completeness) ，如果健壯性對應must-analysis，則完整性對應may-analysis。
根據萊斯定理，現實中不存在既sound又complete（即下圖中的truth的分析）
如上圖，我們舉例來理解這幾個概念，假設一個程序中某錯誤有十個，分別是a、b、c、d...等等，這是個錯誤叫做truth，sound就是找到了不小於十個的錯誤，這其中包含了真實的這十個，我們稱之為overapproximate，也就是過近似。而complete就是找到錯誤的數量不大於十個，但是能保證所有找到的都是真實的錯誤，我們稱之為underapproximate。
軟件分析的目的並不是求完美解（也求不到），我們的目的是求最優解，因此會產生兩種情況：
- 妥協soundness(false negatives漏報)
- 妥協completeness(false positives誤報)
絕大多數軟件分析都是妥協completeness,所以從靜態分析角度只要滿足soundness就是正確的。
7.軟件分析求解過程
軟件分析求解過程分為兩步，分別是abstraction和safe-approximation.
- Abstraction:符號分析里的簡單例子，可以將變量值抽象為正負零以及未知和未定義
- Safe-approximation(Over-approximation)
- Transfer functions
- Control flows
8.控制流分析
控制流分析主要是通過控制流圖來實現的。控制流圖中的每個節點可以是一條單獨的三地址指令也可以（或者說大多數情況下）是一個基本塊（Basic Block,簡稱BB)。
8.1控制流圖中的基本塊
基本塊是連續的三地址指令的集合，它滿足以下條件：
- 每個BB只有一個入口，且必為該BB的第一條語句。
- 每個BB的出口必為該BB的最后一條語句。
下面是一個BB分析的實錄
方法：先將第一句和最后一句指令分別作為所在塊的入口及出口，接下來找出所有的跳轉語句，將它們作為所在BB的最后一句，再將這些跳轉語句的目標語句作為所在BB的第一句，以此切分出BB來。結果如下：
8.2控制流圖
控制流圖中的節點就是基本塊
從基本塊A到基本塊B中間右邊的條件是：
- 從塊A的出口到塊B的入口之間有條件性或者無條件性的跳轉。
- A的出口指令是一個無條件的goto（），這樣A到B之間就沒有邊。
- 條件Jump Block天然有兩個出口，這取決於條件值是否為真。
我們經常將指令間的跳轉轉化為基本塊間的跳轉，關於以上的內容的總結如下圖：
