Meta已經發布了超過10萬個由靜態分析器在程式碼到達使用者之前捕獲的缺陷修復。這個工具名為Infer，它是開源的，並且不會執行您的程式碼。它讀取程式碼，建構程式碼可能執行的數學模型，並證明某些壞事不可能發生。或者它會找到一條可能發生的路徑。

這項技術是抽象詮釋。它聽起來很學術，因為它確實是。派屈克·庫索和拉迪亞·庫索在1970年代發明了它，作為不執行程式就能推理程式的方法。彼得·奧漢恩領導的Meta團隊採用了這個理論，並將其速度提升到足以在幾分鐘內分析數百萬行行動和伺服器程式碼。結果是一個在差異提交時就發現空指標解引用、記憶體洩漏、資源洩漏和競態條件的工具。

問題：動態測試無法覆蓋您沒想到要執行的路徑

單元測試檢查程式碼中的一條路徑。整合測試再多檢查幾條。但一個包含五個條件陳述式和兩個迴圈的函式有數百條路徑，其中大多數在測試套件中從未被執行。

動態測試，即執行程式碼，只能在您實際執行的路徑上發現缺陷。靜態分析在您從未想到過的路徑上發現缺陷。這就像是用手電筒逐個房間檢查入侵者，與證明所有門窗都已上鎖之間的區別。

挑戰在於，證明真實程式中的事情是困難的。真實程式有迴圈、遞迴、堆積配置和並行處理。您無法列舉每個狀態。抽象詮釋透過近似來解決這個問題。

抽象詮釋的實際含義

抽象詮釋透過用抽象值而不是具體值來執行程式。

在正常執行中，變數 x 可能儲存整數 42。在抽象詮釋中，x 可能儲存抽象值「正數」。分析器不知道 x 是42。它知道 x 大於零。這足以證明如果 y 也是正數，x / y 不會除以零。但這不足以證明 x == 42。抽象詮釋用精確性換取可計算性。

抽象值的集合稱為抽象領域。最簡單的領域是符號領域：每個變數為負、零、正或未知。更複雜的領域追蹤範圍、指標或記憶體位置是否已被釋放。分析器遍歷程式，套用每次操作的抽象版本，直到抽象狀態停止變化。此時，它找到了一個不動點，即每個程式點處每個可能具體狀態的近似值。

迴圈是難點。一個迴圈可能執行零次、一次或十億次。分析器無法將其展開十億次。相反，它套用一個擴展運算子，跳轉到過度近似。如果一個變數每次迭代增加一，分析器可能將其抽象值從「正數」擴展為「非負數」並在那裡停止。它失去了確切的界限，但保留了證明所需的關鍵屬性。

Infer如何利用雙向推理模組化地分析程序

傳統的抽象詮釋將整個程式作為一個整體來分析。這對於有百萬行程式碼的行動應用來說無法擴展。Infer透過一種稱為雙向推理的技術解決了這個問題。

雙向推理讓Infer一次分析一個函式。當Infer分析一個函式時，它會發現兩件事：函式安全所必須滿足的前置條件，以及函式保證的後置條件。這些是自動推論的，而不是由程式設計師編寫的。

下面是一個具體範例。假設Infer看到這個C函式：

void greet(struct Person* p) {
    printf("Hello, %s\n", p->name);
}

Infer推論 greet 要求 p 非空。這就是前置條件。它還推論 greet 不會釋放 p 或修改任何可見狀態。這就是後置條件。當另一個函式呼叫 greet 時，Infer會根據推論的前置條件檢查呼叫者。如果呼叫者可能傳遞空值，Infer就會報告一個缺陷。

雙向推理引擎透過分離邏輯上的符號執行來運作。分離邏輯讓Infer能夠推理堆積所有權：哪個函式擁有哪個記憶體，以及該記憶體是否已被釋放。這就是Infer擅長在C、C++、Objective-C和Java中發現空指標解引用和記憶體洩漏的原因。

Infer能捕獲什麼以及遺漏什麼

Infer不是通用的程式碼檢查工具。它針對的是動態發現成本高且在投產中危險的特定缺陷類別。

空指標解引用。 Infer追蹤每個指標是確定為空、確定為非空，還是可能為空。對可能為空的指標進行解引用會觸發報告。在Java和Objective-C中，這捕獲了最常見的當機類型。

記憶體洩漏。 Infer使用分離邏輯來追蹤堆積所有權。如果一個函式配置了記憶體，卻沒有釋放它或將其返回給呼叫者，Infer就會報告洩漏。這在C和C++程式碼庫中特別有價值，因為洩漏會在數週的執行時間內累積。

資源洩漏。 檔案描述子、通訊端和鎖也以類似方式被追蹤。如果一個函式開啟了一個檔案，卻在每條路徑上都沒有關閉它就返回，Infer就會報告洩漏。

競態條件。 Infer的RacerD模組分析Java並行性。它追蹤哪些執行緒存取哪些欄位，以及這些存取是否受到鎖的保護。兩個執行緒在沒有同步的情況下存取同一個欄位就是一種競態。

Infer並不能捕獲所有缺陷。它會遺漏需要對數值精度、字串內容或複雜別名模式進行推理的缺陷。它在設計上也是不健全的：為了保持低誤報率，它可能會遺漏缺陷。一個在每次差異提交時都喊狼來了的靜態分析器會被停用。Meta的內部部署將Infer的誤報率控制在10%以下，這就是開發人員真正會對其報告採取行動的原因。

在您的程式碼上執行Infer

Infer是開源的，支援C、C++、Objective-C、Java，以及（實驗性地）Rust和Swift。最簡單的嘗試方式是在Java或C專案上。

透過Homebrew或Docker安裝Infer：

# macOS
brew install infer

# Or via Docker
docker run --rm -v $(pwd):/repo infer/infer infer run -- make -C /repo

對於使用Maven的Java專案：

infer run -- mvn compile

對於使用Make的C專案：

infer run -- make

Infer會編譯您的程式碼，建構控制流程圖，並執行分析。輸出是一組帶有檔案名稱、行號和被違反的推論前置條件的缺陷報告。

下面是一個Infer會標記的最小C範例：

// leak.c
#include <stdlib.h>

int* allocate_but_leak(void) {
    int* p = malloc(sizeof(int));
    *p = 42;
    // forgot to return p or free it
    return NULL;
}

執行 infer run -- cc leak.c 會產生：

leak.c:5: error: MEMORY_LEAK
  memory dynamically allocated by call to `malloc()` at line 5 is not reachable after line 7

Infer還會捕獲下面這個範例中的空指標解引用：

// null.c
#include <stdio.h>

void print_length(const char* s) {
    if (s != NULL) {
        printf("%zu\n", strlen(s));
    }
}

void unsafe_call(void) {
    print_length(NULL);  // Infer reports this
}

等等，實際上Infer不會報告上面的情況。print_length 函式安全地處理了空引數。Infer只在可能為空的指標在沒有檢查的情況下被解引用時才會報告。下面是一個會觸發的情況：

// null_bad.c
#include <stdio.h>

void unsafe_print(const char* s) {
    // No null check before dereference
    printf("first char: %c\n", s[0]);
}

void call_unsafe(void) {
    unsafe_print(NULL);  // Infer reports this
}

Infer追蹤從 call_unsafe 經過 unsafe_print 的路徑，並報告在計算 s[0] 時 s 為空。

權衡：速度與精度

Infer的模組化設計使其快到足以在Meta的每次拉取請求上執行。但模組化會引入近似。當Infer分析一個函式時，它不知道確切的呼叫上下文。它推論的前置條件是保守的，意味著它們可能比必要的更強。更強的前置條件意味著在呼叫點報告的缺陷更少，但誤報也更少。

這是靜態分析中的核心張力。一個健全的分析器會報告每個缺陷，但會讓您淹沒在誤報中。像Infer這樣的不健全分析器透過只報告它有把握的缺陷來讓開發人員滿意。它遺漏的缺陷就是採用的代價。

Infer的雙向推理引擎也難以處理全域狀態和複雜的callback。如果您的Java程式碼將匿名內部類別傳遞給執行器，Infer可能會遺失哪個執行緒執行哪個方法的追蹤。RacerD處理常見模式，但會遺漏涉及條件變數或原子欄位的微妙競態。

何時採用靜態分析，何時跳過

如果您發布的是原生程式碼、行動應用或C族語言或Java的伺服器程式碼，您應該考慮使用Infer。它發現的缺陷——空指標解引用、洩漏、競態——正是導致投產當機和安全漏洞的那些。

您不應該期望Infer取代您的測試套件。靜態分析和動態測試是互補的。測試驗證您的程式碼在您選擇的輸入上做了您打算做的事情。靜態分析驗證您的程式碼在任何輸入上都沒有做您禁止的事情。

如果您的程式碼庫是Python、Ruby或JavaScript，Infer不是合適的工具。這些語言缺乏Infer用來建構其抽象模型的靜態型別資訊。對於動態語言，像mypy或pyright這樣的型別檢查器會捕獲不同類別的錯誤。

結論

Meta的10萬個缺陷修復不是一個行銷數字。它是一個在每次差異提交時執行、在不執行程式碼的情況下分析程式碼、並報告任何測試都無法捕獲的缺陷的工具的產出。底層技術抽象詮釋已有數十年的歷史。工程成就在於讓它快到足夠精確，以至於開發人員不會關掉它。

您不需要Meta的基礎設施就能受益。安裝Infer，指向您的建置系統，然後在一個讓您擔心的模組上執行它。記憶體管理模組、並行層、C互操作邊界。修復它發現的洩漏和空指標解引用。然後將其新增到CI中，防止缺陷數量成長。

抽象詮釋不是魔法。它是應用於程式碼的數學，帶有所有隨之而來的近似和權衡。但它是能在真實程式碼庫中發現真實缺陷的數學，這使它值得了解。