BT

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

| 作者: Abel Avram フォローする 7 人のフォロワー , 翻訳者 笹井 崇司 フォローする 0 人のフォロワー 投稿日 2015年6月21日. 推定読書時間: 2 分 |

原文(投稿日: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

このスレッドのメッセージについてEmailでリプライする
コミュニティコメント

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

このスレッドのメッセージについてEmailでリプライする

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

このスレッドのメッセージについてEmailでリプライする

ディスカッション

InfoQにログインし新機能を利用する


パスワードを忘れた方はこちらへ

Follow

お気に入りのトピックや著者をフォローする

業界やサイト内で一番重要な見出しを閲覧する

Like

より多いシグナル、より少ないノイズ

お気に入りのトピックと著者を選択して自分のフィードを作る

Notifications

最新情報をすぐ手に入れるようにしよう

通知設定をして、お気に入りコンテンツを見逃さないようにしよう!

BT