抽象解釈は、エンジニアがタブを閉じてしまうような言葉だ。束理論を一学期学ばなければ理解できないようなものに聞こえる。ほとんどの開発者は、それが研究論文の世界のもので、プルリクエストの世界のものではないと思い込んでいる。
その思い込みは高くつく。抽象解釈は、コードを実行せずにコードについて何かを証明する方法に過ぎない。これを基盤に構築されたツールは、型チェッカーやリンターが見逃すヌル参照、メモリリーク、競合状態を捉えることができる。良い知らせは、それを使うためにガロア接続を理解する必要はないということだ。動作するCI設定と約20分があれば十分だ。
抽象解釈が実際に行うこと
その核心において、抽象解釈は自動化された証明技法である。プログラムを実行するが、実際の値ではなく近似値を使用する。
変数xを考えてみよう。通常の実行では、xは42を保持しているかもしれない。抽象解釈では、xは「正の整数」を保持しているかもしれない。解析はこれらの抽象値をすべての可能なコードパスを通じて追跡する。ヌル参照に至るパスが存在しないことを証明できれば安全だ。逆に、xが参照サイトでヌルになりうるパスを発見した場合、潜在的なバグを報告する。
魔法は、これがループや条件分岐でも機能することだ。解析器は抽象状態上で不動点を計算するため、実際に永遠に反復することなく、無限反復について推論できる。これが、ループで苦労するより単純な記号的実行ツールと抽象解釈を区別するものだ。
FacebookのInferは、この技法を使用する最もアクセスしやすいプロダクションツールだ。Java、C、C++、Objective-Cを解析するために、コードを中間表現にコンパイルし、各関数に対して構成論的抽象解釈を実行する。Inferは関数ごとに結果をキャッシュするため、インクリメンタルビルドは高速だ。これがCIで実行可能にする秘訣だ。
なぜリンターだけでは足りないのか
リンターは構文を見る。型チェッカーは型を見る。抽象解釈はパスを横断する動作を見る。
リンターはヌルチェックを忘れたことを指摘できる。型チェッカーは関数がOptional<T>を返すことを強制できる。しかし、複雑な分岐の後に、あるパスで未初期化のままになったポインタを47行目で参照することは、どちらも確実に捉えることができない。抽象解釈は、そのポインタの可能な状態をすべての分岐点とマージポイントを通じて追跡する。
トレードオフはノイズだ。抽象解釈は偽陽性を生み出す。ビジネスロジックが決して起こらないと保証しているヌル参照を報告する可能性がある。解析器は不変条件を知らない。コードが文字通り許可することだけを知っている。
Inferのデフォルトチェッカーは、ほとんどのコードベースで偽陽性率を10〜15%程度に抑えるよう調整されている。型チェッカーより高いが、見つけるバグはしばしばコードレビューやテストを抜け落ちるものだ。
CIパイプラインへのInfer追加
Inferをソースからビルドする必要はない。FacebookはDockerイメージを公開している。以下はJavaプロジェクトを解析する動作するGitHub Actionsワークフローだ：
# .github/workflows/infer.yml
name: Abstract Interpretation
on: [pull_request]
jobs:
infer:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Run Infer
uses: docker://ghcr.io/facebook/infer:main
with:
args: >
infer run
--make-command "mvn compile"
--
mvn compile
- name: Upload report
uses: actions/upload-artifact@v4
with:
name: infer-report
path: infer-out/report.jsonNode.jsやPythonプロジェクトの場合はビルドコマンドを入れ替える。InferはネイティブにJavaScriptやPythonを解析しないが、これらのプロジェクトがしばしば依存するC/C++拡張機能に対して実行できる。純粋なマネージド言語環境にいる場合でも、CodeQLやSonarQubeのようなツールから同様のパスに敏感な解析を得ることができるが、基盤となるエンジンは異なる。
CまたはC++プロジェクトの場合、設定はさらに簡単だ：
# .github/workflows/infer-cpp.yml
name: Infer C++ Analysis
on: [pull_request]
jobs:
infer:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Build with Infer
uses: docker://ghcr.io/facebook/infer:main
with:
args: >
infer run
--make-command "make"
--
makeinfer run --make-commandパターンは、通常のビルドプロセス中にコンパイラ呼び出しを傍受する。Inferは中間表現を抽出し、解析し、結果をinfer-out/に書き込む。実際のビルド成果物には影響を与えない。
出力の読み取りと偽陽性の調整
Inferは結果をinfer-out/report.jsonと人間が読めるinfer-out/report.txtに出力する。典型的な発見は次のようになる：
src/parser.c:142: error: NULL_DEREFERENCE
pointer `node` last assigned on line 138 could be null and is dereferenced at line 142, column 5メッセージは変数、代入された場所、参照が発生した場所を教えてくれる。エディタでパスをたどることができる。
Inferが騒がしすぎる場合は、特定のチェッカーを抑制したり、解析をスキップするためにコードに注釈を付けたりできる：
// src/parser.c
// infer-ignore: the parent check guarantees node is non-null here
node->value = parsed;または、特定のチェッカーをグローバルに無効にする：
infer run --make-command "make" --no-bufferoverrun --バッファオーバーランチェッカーは、複雑なポインタ演算を含むコードで特に偽陽性を起こしやすい。私は通常、レガシーCコードベースではこれを無効にし、ヌル参照チェッカーとメモリリークチェッカーをアクティブにしたままにする。この2つはレビュー時間を正当化する率で実際のバグを発見する。
ビルド時間のトレードオフ
抽象解釈はタダではない。中規模のC++プロジェクトでのInferのフル実行は、通常のビルドの2〜4倍の時間がかかることがある。増分解析は役立つ：後続の実行では、Inferは変更された関数とその依存関係のみを再解析する。実際には、これは10分のビルドがクリーンなCI実行では15〜20分になるかもしれないが、増分実行では3〜5分になることを意味する。
CI予算が厳しい場合、プルリクエストではInferを実行するが、mainへのすべてのプッシュでは実行しない。または毎晩実行する。発見するバグは通常遅延に見合う価値があるが、適切な頻度はチームのCI時間に対する許容度に依存する。
もう1つの選択肢は、プッシュ前にローカルでInferを実行することだ。同じDockerイメージは、Dockerがインストールされた任意のマシンで機能する：
docker run --rm -v $(pwd):/workspace -w /workspace \
ghcr.io/facebook/infer:main \
infer run --make-command "make" --Inferが捉えないもの
Inferは構成論的だ。関数を分離して解析し、要約を使用して呼び出し元と呼び出し先をモデル化する。これによりスケーラビリティが得られるが、完全なコールグラフの解析を必要とするクロスファンクション、パスに敏感なバグが抜ける可能性があることを意味する。
また、ロジックバグも見つけられない。コードがポインタを安全に参照するが、間違った値を使用する場合、Inferは黙っている。これは安全性チェッカーであり、正確性のオラクルではない。
並行性バグは限定的だ。Inferには競合状態チェッカーがあるが、これは実験的であり、ほとんどのチームがオフにしておくほどの偽陽性を生み出す。
次にすべきこと
小さく始めろ。コンパイル言語のプロジェクトを1つ選び、上記のGitHub Actionsワークフローを追加する。次の数回のプルリクエストで実行させる。チームと一緒に発見事項をレビューし、ノイズに対する抑制リストを構築する。
1週間後には、シグナルがCI時間に見合う価値があるかどうかの感覚がつかめるだろう。私の経験では、既存のCまたはJavaコードベースでの最初の実行は、コードレビューが見逃した少なくとも1つのヌル参照を常に発見する。通常、それを維持するのに十分な理由になる。
さらに深く入りたい場合、InferのドキュメントにはOCamlでのカスタムチェッカーの作成が記載されている。そこで博士学位が役立つ。それ以外のすべてには、デフォルトのチェッカーとDockerイメージで十分だ。
FAQ
簡単に言うと抽象解釈とは何ですか？ コードを実際に実行せずに「このポインタは決してヌルではない」などの性質を証明するために、プログラムの動作を近似する静的解析技法です。
Inferは無料で使用できますか？ はい。InferはMITライセンスの下でオープンソースであり、Metaがメンテナンスしています。
InferとSonarQubeを比較するとどうですか？ SonarQubeは、パターンマッチング、汚染分析、言語によってはより深い分析の組み合わせを使用します。Inferは具体的に抽象解釈に基づいて構築されており、SonarQubeが通常C、C++、Java、Objective-Cで行わない方法でパスに敏感です。
InferをJavaScriptやPythonで実行できますか？ 直接はできません。Inferはコンパイル言語を解析します。JavaScriptとPythonについては、CodeQLや、厳密なルールを持つESLintやPyrightのような型を意識したリンターを検討してください。
InferはCIを大幅に遅らせますか？ 完全な解析はビルド時間の2〜4倍かかります。プルリクエストでの増分解析ははるかに高速で、通常数分追加されます。