Infer Introduction


C言語の静的自動検証器である Infer の使い方がある程度分かってきたので紹介します。

Infer

Infer は、C言語(or [C++, Obj-C, Java])の検証器で、
自動で特定の種類のバグを発見してくれます。発見できるバグとして分かり易い例ではリソースリークを発見できます。
元々Inferを開発した会社をFacebookが買収してオープンソースになりました。(https://github.com/facebook/infer)
スマートフォン向けアプリの検証に使っているようです。

追記: 勘違いしてましたが C++サポートはこれからのようです。> https://github.com/facebook/infer/issues/24

Separation Logic(分離論理)

InferはSeparation logicという意味論に沿って静的検証を実行します。Separation logicというのは、Hoare logicを拡張した意味論で、共有された変更可能なデータやアドレスに対する算術演算を意味論で(うまく)扱うために考案されました。
適当に言えば「ポインタが扱える意味論」だと理解しています。(ものすごくいい加減な理解なので鵜呑みにしてはイケナイ)

適用例

実際的といえるかはかなり怪しいですが、aobench.c をそのままInferに渡してみたところ、2箇所のリークを見つけ修正しました。> aobench.cの修正
かなり簡単な例ですが、これくらいは全自動で見つかります。

Inferの使い方

Inferを使う最も単純な方法は、コンパイルのコマンドをそのまま infer コマンドに引き渡す方法です。

$ infer -- clang -c <input.c>

Makeを使っている場合は make コマンドごと引き渡すだけでよいです。

$ infer -- make
使用例

最も簡単な部類の使用例を示します。

// simple.c
#include <stdlib.h>

int main () {
	int * p = malloc(4);
	return 0;
}

このコードをinferに渡す。

$ infer -- gcc simple.c
Starting analysis (Infer version v0.8.0-44a6bf7)
F.
Analyzed 1 file

Found 1 issue

simple.c:4: error: MEMORY_LEAK
   memory dynamically allocated to p by call to malloc() at line 4, column 12 is not reachable after line 4, column 12
  2.
  3.   int main () {
  4. >  int * p = malloc(4);
  5.    return 0;
  6.   }
  7.

Summary of the reports

  MEMORY_LEAK: 1

自明なバグですが、メモリリークが見つかってますね。

アノテーションの記述

以下のコードについて考えます。

// pass.c
#include <stdio.h>
#include <stdlib.h>

int * new_int (int x) {
	int * p = malloc(sizeof(int));
	if (p == NULL) exit(1); // (1)
	*p = x; // (2)
	return p;
}

int main () {
	int * p = new_int(42);
	printf("%d\n", *p);
	free(p);
	return 0;
}

このコードには(Inferが報告する)バグはありません。
Inferが(1)のexitでプログラムが終了することを知っているため、(2)のデリファレンスが常に安全だと分かるからです。


しかし次のコードを見てください。
アロケーションに失敗した場合にライブラリ関数を呼び出して終了するコードです。

// ext.h
// exit(3)のラッパー
void lib_exit(int c); // ライブラリの提供する関数のシグネチャ

// fail.c
#include <stdio.h>
#include <stdlib.h>
#include "ext.h"

int * new_int (int x) {
	int * p = malloc(sizeof(int));
	if (p == NULL) lib_exit(1); // 終了することが分からない
	*p = x;
	return p;
}

int main () {
	int * p = new_int(42);
	printf("%d\n", *p);
	free(p);
	return 0;
}

これを検証しようとすると…

$ infer -- gcc -c fail.c
Starting analysis (Infer version v0.8.0-44a6bf7)
F..
Analyzed 1 file

Found 1 issue

fail.c:9: error: NULL_DEREFERENCE
  pointer p last assigned on line 7 could be null and is dereferenced at line 9, column 2
  7.    int * p = malloc(sizeof(int));
  8.    if (p == NULL) lib_exit(1);
  9. >  *p = x;
  10.           return p;
  11.   }
  12.

Summary of the reports

  NULL_DEREFERENCE: 1

NULL_DEREFERENCE バグが報告されました。
Inferには lib_exit の実装が見えないため、該当箇所のデリファレンスが安全だということが分かりません。


そこで以下のようにします。

// fail2pass.c
#include <stdio.h>
#include <stdlib.h>
#include "ext.h"
#include "infer_builtins.h" // (1)

int * new_int (int x) {
	int * p = malloc(sizeof(int));
	if (p == NULL) lib_exit(1);
	INFER_EXCLUDE_CONDITION(p == NULL); // (2)
	*p = x;
	return p;
}

int main () {
	int * p = new_int(42);
	printf("%d\n", *p);
	free(p);
	return 0;
}

検証してみると…?

$ infer -- gcc -I ../../infer/models/c/src -c fail2pass.c
Starting analysis (Infer version v0.8.0-44a6bf7)
F..
Analyzed 1 file

  No issues found

エラーが無くなりました。
(1) で導入されるマクロ INFER_EXCLUDE_CONDITION を (2) で使用しています。
これは読んで字のごとく、指定した条件は「起きるはず無い(ので考えなくていいよ)」*1という指定です。

この指定によって Infer は pNULLデリファレンスが起きないことが分かるので、エラーは報告されなくなります。

外部ライブラリを含むコードの検証


外部ライブラリを含むプロジェクトの場合も上の方法で Infer は正常に実行できますが、
コンパイラから実装が見えない(i.e. ヘッダしか見えない)関数が使用されている場合、それらの関数について必要な情報が得られないので、自明なバグでも発見できないことがあります。


ライブラリ関数を呼び出す箇所に INFER_EXCLUDE_CONDITION 等のアノテーションを書いてまわってもいいですが、冗長ですし、アノテーションの大半は通常の関数呼び出しとして提供されているため、実装コードと共存出来ない可能性があります。

これらの関数(e.g. 外部ライブラリの提供する関数)を使用するコードを検証するためには、
Infer が必要な性質が導出できるような関数の実装を(本物の実装とは)別に与える必要があります。この実装のことをモデルと呼びます。


標準(あるいは標準的な)ライブラリで提供される関数のモデルは Infer の一部として提供されており、/path/to/infer/infer/models/c/src/ 以下にあります。(これらは明示的な指定無しでもデフォルトで参照されます)



以下のようなコードを考えます。(ヘンな例ですいません…)

// extlib.h
int getStatus (void);

// uselib.c
#include <stdio.h>
#include <stdlib.h>
#include "extlib.h"

char const * stName (void) {
	switch (getStatus()) {
	case 0: return "St 0";
	case 1: return "St 1";
	case 2: return "St 2";
	}
	return NULL;
}

int main () {
	char const * s = stName();
	printf("%c\n", s[3]);
	return 0;
}
$ infer -- gcc -c uselib.c
Starting analysis (Infer version v0.8.0-44a6bf7)
F..
Analyzed 1 file

Found 1 issue

uselib.c:17: error: NULL_DEREFERENCE
  pointer s last assigned on line 16 could be null and is dereferenced at line 17, column 17
  15.   int main () {
  16.           char * s = stName();
  17. >         printf("%c\n", s[3]);
  18.           return 0;
  19. }
  20.

Summary of the reports

  NULL_DEREFERENCE: 1

extlib で提供される getStatus 関数からは 0, 1, 2 のどれかの値しか戻りませんが、Infer には実装が見えないのでそれが分かりません。


そこで以下のようにモデルを与えます。

// mylib.c
#include "extlib.h" // 本物のヘッダ
#include "infer_builtins.h"

int getStatus (void) {
	// 何が返って来るか知らない
	int s = __infer_nondet_int();
	// けどとにかく !(s < 0 || 3 <= s) が成り立つよ
	INFER_EXCLUDE_CONDITION(s < 0 || 3 <= s);
	return s;
}

モデルを解析。(infer/ 以下に解析結果が出力されます)*2

$ INFER_ANALYZE_MODELS=1 infer -o infer --models_mode --no_failures_allowed -- gcc -I ../../infer/models/c/src -c mylib.c

モデルの解析結果を参照して検証。

$ infer --specs-dir infer/specs -- gcc -c uselib.c
Starting analysis (Infer version v0.8.0-44a6bf7)
F..
Analyzed 1 file

  No issues found

エラーが出なくなりました(`・ω・´)


このようにライブラリの提供する関数の性質を現すモデルを記述することで、より精度の高い静的解析が出来ます。

所感


Inferを使用するためには、対象とするコードにアノテーションの類を追加する必要がほぼ無いので簡単に利用できるように見えました。
が、外部ライブラリに依存しようとすると(つまり普通の開発として想定される状況だと)検証用のモデル(関数)を別ファイルで記述する必要があって、これが全く簡単ではないです((命題を直接書くわけではないから自明でもないし、ドキュメントも無い(#・∀・)))。


モデルはC言語で書く必要がありますが、
これは命題を直接書くわけではなくて、Inferが必要な命題を導出できるようなコードを書かないとイケナイ。これはとても迂遠に感じます。


ただし良さもあって、標準ライブラリの範囲(mallocとかfopen)か、あるいはモデルを記述してあれば単純なリソースリークを全自動で見つけてくれるのでお手軽ではあります。
他に、make に渡せばまともな規模のコードのビルド手順にも手を入れる必要が無いというのは良い点ですね。



まとめると、とりあえずmakefileだけ書いてあれば使用出来るので導入してみても良さそうです。
ただし外部ライブラリまで含めてまじめに検証したい場合は頑張ってモデルを記述する必要があるので、多少手間が掛かる。頑張れ。

インストール

LLVMプラグイン(facebook-clang-plugins)を使用するので自分でビルドするのは時間が掛かりますが、
LLVMのバージョンに強く依存するので既存の環境を使わず、素直に全部ビルドした方がよさげです。

私は CentOS7 (x86_64) で動作を確認しています。
というか、おとなしく公式バイナリ http://fbinfer.com/docs/getting-started.html 使いましょう。

おまけ

文中で使用している INFER_EXCLUDE_CONDITION マクロですが、実装がちょっと面白いです。

#define INFER_EXCLUDE_CONDITION(cond) \
  if (cond)                           \
    while (1)

なるほどねー、という感じですよね。
無限ループはボトム(False?)(なのでその分岐は何も考えなくてよい)を体現してます。
ちなみに自分で同じマクロを書いてもちゃんと動作します。

*1:つまり !cond が成り立つという表明

*2:実は細かいオプションの意味はよく分からない(^^;; 標準モデルのビルドスクリプトを写しただけなので。誰か教えて。