Facebook、静的解析ツールInferをオープンソース化

FacebookがC、Java、Objective-Cのための静的解析ツール、Inferをオープンソース化した。

Facebook Inferは静的解析ツールだ。チームによるレビューのためにコードを提出すると即座に実行され、コードがコードベースにコミットされたり、デバイスにデプロイされる前に、バグを発見することができる。現在のところ、Nullポインタアクセス、リソースおよびメモリリークを教えてくれる。InferはC、Java、Objective-Cで書かれたコードに対して実行できるが、それ自体はOCamlで書かれている。Facebookによると、iOSおよびAndroidモバイルアプリのコードを自動検証するのにInferを使っており、その80%で正しくバグを報告しているという。

Inferはコンパイル命令をキャッチし、ファイルを中間言語にコンパイルして、起こり得るエラーを分析する。このプロセスはインクリメンタルだ。つまり通常は、修正や追加がなされたファイルのみ、分析されるということだ。InferはGradle、Maven、Buck、Xcodebuild、clang、make、javacといった多くのコンパイルツールと統合されている。

Inferが検出するエラーの種類については、このページに詳しく書かれている。配列境界エラー、キャスト例外、汚染されたデータのリークなども検出できるよう取り組んでいるが、それらの機能はまだ含まれていない。

その他のエラーを検出できるようツールを強化すること、そして他の言語をサポートすることについて質問したところ、Facebookのスポークスマンは、コミュニティと協力するつもりであることを表明しつつ、「これはまだ道のりの1%にすぎず、プログラマの価値を最大限に引き出すため、引き続き取り組んでいくつもりです」と答えた。

Inferはうまくやっていますが、エンジニアリング組織を越えて解決すべき問題が、まだたくさんあります。Inferを公開することで、Facebookはたくさんのエンジニアリング組織、研究およびアカデミックなグループと協業できます。そうしたコミュニティから、やがて新しい機能追加や、新しいバグのチェック、新しい言語への対応が登場するかもしれません。

Facebookによると、Inferは2つの基本理論、ホーア論理(コンピュータプログラムの正当性に関する推論のための形式体系)と抽象解釈(プログラムの意味論の健全な近似の理論)、そしてSeparation LogicBi-abductionなどの研究に基づいているそうだ。

InferのソースコードはGitHubで入手できる。