Metaは、コードがユーザーに到達する前に静的解析ツールが捉えた10万件以上のバグ修正をリリースしてきた。そのツールはInferと呼ばれ、オープンソースであり、コードを実行しない。コードを読み込み、コードが可能な動作の数学モデルを構築し、特定の有害な事象が起こりえないことを証明する。あるいは、それが起こりうる経路を発見する。

この技法は抽象解釈（abstract interpretation）である。学術的に聞こえるのは、そうだからだ。パトリック・クーソとラディア・クーソは1970年代に、プログラムを実行せずに推論する方法としてこれを発明した。ピーター・オハーン率いるMetaのチームは、この理論を取り入れ、数百万行のモバイルおよびサーバーコードを数分で解析できるほど高速化した。結果として生まれたツールは、差分適用時点でヌルポインタ参照、メモリリーク、リソースリーク、および競合状態を検出する。

問題：動的テストは実行しようと思わなかった経路をカバーできない

単体テストはコード内の一つの経路を検証する。結合テストはさらにいくつかの経路を検証する。しかし、条件分岐が五つ、ループが二つある関数は数百の経路を持ち、そのほとんどはテストスイートで実行されることはない。

動的テスト、つまりコードを実行して検証する手法は、実際に実行した経路上のバグしか発見できない。静的解析は、想像もしなかった経路上のバグを発見する。これは、懐中電灯を持って部屋を歩き回って侵入者を確認するのと、すべてのドアと窓が施錠されていることを証明して確認するのとの違いに似ている。

課題は、実際のプログラムについて何かを証明することは難しいという点にある。実際のプログラムにはループ、再帰、ヒープ割り当て、並行処理がある。すべての状態を列挙することはできない。抽象解釈は、この問題を近似によって解決する。

抽象解釈の実際の意味

抽象解釈は、具体的な値の代わりに抽象的な値を使ってプログラムを実行することで機能する。

通常の実行では、変数 x は整数 42 を保持しているかもしれない。抽象解釈では、x は「正の数」という抽象値を保持しているかもしれない。解析器は x が 42 であることを知らない。x がゼロより大きいことを知っている。これで、y も正の数であれば x / y がゼロ除算にならないことを証明するには十分だ。しかし、x == 42 を証明するには不十分だ。抽象解釈は、計算可能性を得るために精度を犠牲にする。

抽象的な値の集合を抽象ドメイン（abstract domain）と呼ぶ。最も単純なドメインは符号ドメインであり、各変数は負、ゼロ、正、または不明のいずれかだ。より複雑なドメインは範囲、ポインタ、またはメモリ位置が解放されたかどうかを追跡する。解析器はプログラムを反復処理し、各操作の抽象バージョンを適用し、抽象的な状態が変化しなくなるまで続ける。その時点で、固定点（fixed point）が見つかり、各プログラム地点で可能なすべての具体的な状態の近似値が得られる。

ループが難しい部分だ。ループはゼロ回、一回、あるいは十億回実行される可能性がある。解析器は十億回も展開することはできない。代わりに、過近似に飛ぶ拡大演算子（widening operator）を適用する。変数が反復ごとに一ずつ増加する場合、解析器はその抽象値を「正の数」から「非負の数」に拡大し、そこで停止するかもしれない。正確な上限は失われるが、証明に必要な性質は保持される。

Inferが双方向誘導を使って手続きをモジュール的に解析する仕組み

従来の抽象解釈は、プログラム全体を一つの塊として解析する。これは数百万行のモバイルアプリにはスケールしない。Inferは双方向誘導（bi-abduction）という技法でこの問題を解決する。

双方向誘導により、Inferは一度に一つの関数を解析できる。Inferが関数を解析するとき、二つのことを発見する：関数が安全であるために満たさなければならない事前条件（precondition）、および関数が保証する事後条件（postcondition）だ。これらは自動的に推論され、プログラマーが記述するものではない。

具体的な例を挙げよう。Inferが次のC関数を見たとする：

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

Inferは、greet が p がヌルでないことを要求すると推論する。これが事前条件だ。また、greet が p を解放したり、可視状態を変更したりしないことも推論する。これが事後条件だ。別の関数が greet を呼び出すとき、Inferは呼び出し元を推論された事前条件に対して検証する。呼び出し元がヌルを渡す可能性がある場合、Inferはバグを報告する。

双方向誘導エンジンは、分離論理（separation logic）上の記号的実行（symbolic execution）によって動作する。分離論理により、Inferはヒープの所有権について推論できる：どの関数がどのメモリを所有し、そのメモリが解放されたかどうか。これが、InferがC、C++、Objective-C、およびJavaでヌル参照やメモリリークを見つけるのに長けている理由だ。

Inferが捉えるものと見落とすもの

Inferは汎用のリンターではない。動的に発見するのが高く、本番環境で危険な特定のバグクラスを対象とする。

ヌルポインタ参照。 Inferは各ポインタが確実にヌル、確実に非ヌル、あるいはヌルの可能性があるかを追跡する。ヌルの可能性があるポインタの参照は報告を引き起こす。JavaとObjective-Cでは、これが最も一般的なクラッシュタイプを捉える。

メモリリーク。 Inferは分離論理を使ってヒープの所有権を追跡する。関数がメモリを割り当てて解放せず、呼び出し元にも返さない場合、Inferはリークを報告する。これは、稼働時間が長くなるにつれてリークが蓄積するCおよびC++のコードベースで特に価値がある。

リソースリーク。 ファイル記述子、ソケット、ロックも同様に追跡される。関数がファイルを開いて、すべての経路で閉じずに復帰した場合、Inferはリークを報告する。

競合状態。 InferのRacerDモジュールはJavaの並行処理を解析する。どのスレッドがどのフィールドにアクセスし、そのアクセスがロックによって保護されているかを追跡する。同期なしに同じフィールドにアクセスする二つのスレッドは競合だ。

Inferはすべてを捉えるわけではない。数値精度、文字列の内容、または複雑なエイリアシングパターンについての推論を必要とするバグは見落とす。設計上、unsound（完全ではない）でもある：誤検出を低く保つためにバグを見落とすことがある。差分ごとに狼少年を叫ぶ静的解析ツールは無効化される。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は保守的な事前条件を推論するが、これは必要以上に強い場合がある。より強い事前条件は、呼び出しサイトでの報告バグ数を減らすが、誤検出も減らす。

これが静的解析における核心的な緊張関係だ。sound（完全）な解析器はすべてのバグを報告するが、誤検出に溺れる。Inferのようなunsoundな解析器は、確信を持てるバグのみを報告することで開発者を満足させる。見落とされるバグは、導入の代償だ。

Inferの双方向誘導エンジンは、グローバル状態や複雑なコールバックにも苦労する。Javaコードが匿名内部クラスをエグゼキュータに渡す場合、Inferはどのスレッドがどのメソッドを実行するかを見失う可能性がある。RacerDは一般的なパターンを処理するが、条件変数やアトミックフィールドを含む微妙な競合は見落とす。

静的解析を導入すべきタイミングと避けるべきタイミング

ネイティブコード、モバイルアプリ、またはC系言語やJavaによるサーバーコードをリリースしている場合、Inferを検討すべきだ。Inferが発見するバグ、すなわちヌル参照、リーク、競合は、まさに本番環境のクラッシュやセキュリティ脆弱性を引き起こすものだ。

Inferがテストスイートを代替することを期待すべきではない。静的解析と動的テストは相補的だ。テストは、選んだ入力に対してコードが意図した動作をすることを検証する。静的解析は、あらゆる入力に対してコードが禁止された動作をしないことを検証する。

コードベースがPython、Ruby、またはJavaScriptの場合、Inferは適切なツールではない。これらの言語には、Inferが抽象モデルを構築するために使用する静的型情報が欠けている。動的言語の場合、mypyやpyrightのような型チェッカーが異なるクラスのエラーを捉える。

まとめ

Metaの10万件のバグ修正は、マーケティングの数字ではない。これは、差分ごとに実行され、コードを実行せずに解析し、テストでは捉えられなかったバグを報告するツールの成果だ。根底にある技法である抽象解釈は数十年の歴史がある。技術的な成果は、開発者が無効化しないほど高速かつ正確にしたことだ。

Metaのインフラストラクチャがなくても恩恵を受けられる。Inferをインストールし、ビルドシステムに向けて、恐ろしいモジュールで実行する。メモリ管理モジュール、並行処理レイヤー、C相互運用境界。発見されたリークとヌル参照を修正する。そしてCIに追加し、バグ数の増加を防ぐ。

抽象解釈は魔法ではない。それは近似とトレードオフを伴う、コードに適用された数学だ。しかし、それは実際のコードベースで実際のバグを発見する数学であり、そのことを知る価値がある。