BT

InfoQ ホームページ ニュース Facebook、静的解析ツールInferをオープンソース化

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

ブックマーク

原文(投稿日:2015/06/11)へのリンク

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で入手できる。

この記事に星をつける

おすすめ度
スタイル

こんにちは

コメントするには InfoQアカウントの登録 または が必要です。InfoQ に登録するとさまざまなことができます。

アカウント登録をしてInfoQをお楽しみください。

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

コミュニティコメント

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

HTML: a,b,br,blockquote,i,li,pre,u,ul,p

BT

あなたのプロファイルは最新ですか?プロフィールを確認してアップデートしてください。

Eメールを変更すると確認のメールが配信されます。

会社名:
役職:
組織規模:
国:
都道府県:
新しいメールアドレスに確認用のメールを送信します。このポップアップ画面は自動的に閉じられます。