Hatena::ブログ(Diary)

::Eldesh a b = LEFT a | RIGHT b このページをアンテナに追加 RSSフィード Twitter

2016-11-21

静的コード解析の会 第0回 でVeriFastについて発表してきた

#静的コード解析の会 第0回C言語(とJava)の検証器であるVeriFastについて発表してきました。

資料は公開してあるので興味ある人は見てください。動画もあります。

> https://metasepi.connpass.com/event/42141/presentation/

D

結構(私の理解が)きわどい質問も出ましたが、大体伝えたかった内容は伝わったんじゃないかと思います。

個人的には手ぶらで(ぐだぐだ)発表したProofSummit2016のリベンジでもあったので資料はかなり頑張って作りました。(内容は全然違いますが


本当に詳しく知りたい人は公式チュートリアル読むべきなのですが、これは結構ヘビーな量と内容です。これに対して私の発表は「忙しい人向けの入門」といった感じなのでお気軽にどうぞ(^^)

他の発表について

CSPというのを初めて知りました。プロセス代数というのは(多分大学生の時に)聞いたことはあったんですが、通信するプリミティブがあるなぁ、くらいのことしか分かりませんでした。

今になって説明を聞くと、多少理論的な話や記号が出てもビビらなくなったし、なんとなく理解できる部分も増えていたので嬉しみがありました(なお、日本語力は低下したもよう…)

あとCMLに似てますね(これは多分関係が逆だけど)。


自分がここ数年多少なりとも理論的な話として勉強してきた内容は、主に(型付き)ラムダ計算とその意味論だったので、実装でも仕様でもない(あるいはどちらにもなる?)ものと意味論を扱うというのは新鮮でした。


他には具体的に気になったものとしてトレース意味論というのが紹介されていました。これはプログラム副作用を形式的に扱う方面でも出てきてよく分からなかったんですが、CSPでの扱いはかなり明快だなという感じを受けました。(プロセス間の作用が初めから限定されているから当たり前か?

あとは「coinductive」という単語も出ていたので、それを持ち出す気持ちくらいは知りたいなという感じです。

気になるワードは他にも幾つか出ていたので忘れないうちにフォローしておきたいですね。


最後にInferですが、やはり残念だという結論のようです…。

個人的には少なくともFalse Positiveは出てほしくないですねぇ。

ヒューリスティクスでなく理論的基礎がしっかりしているということに期待出来る/したいのはそこだと思うので。

次回

来年(2017)の2月に第1回を開催するみたいです。

私もネタはあるので体力があれば発表するかも知れません。

2016-06-24

古の商用SML処理系MLWorksを動かす

2016年現在SMLの処理系はいくつもありますが、昔はMLWorksという商用の処理系がありました。

MLWorksは開発元のHarlequinが潰れて2000年くらいに姿を消していたのですが、突然2013年にオープンソースになりgithub上に公開されました。


実働していた頃は様々な環境で動作していたようですが、githubに公開当初は想定している動作環境自体が古すぎてビルド自体が困難な状態でした。現在ではellerhさんのおかげでLinux(x86)上でビルド;動作するようになっています。

ちょっとした修正を取り込んでもらってCentOS上での動作が確認できたので紹介します*1


ちなみにこのHarlequinという会社、90年代後半の時点でMLで仕事してたのに加えてバージョン管理に内製のDVCSを使ったりしてたそうで楽しそうですね。(もう無いけど

ビルド

現在ではLinux上でsmlnjからbootstrapできます*2

(大抵の人には)面倒な事にビルドにはlibXtとMotifが必要です。

$ git clone https://github.com/ellerh/mlworks.git
$ cd mlworks
mlworks$ git checkout --track origin/mono-array-slices    # commit:75393c4
mlworks$ cd src
mlworks/src$ make ARCH=I386 OS=Linux bootstrap

起動

今のところinstallターゲットはありません。

起動するには以下のようにします。

mlworks/src$ XUSERFILESEARCHPATH=app-defaults/MLWorks-mono LD_LIBRARY_PATH=rts/bin/I386/Linux/ rts/bin/I386/Linux/main-g -MLWpass xx -load images/I386/Linux/guib.img xx [-tty]

mainてファイル名はどうかと思う…。

`-tty` をつけて起動するとCUIREPLが、付けずに起動するとMotifを使った対話環境が起動します。

ttyb.img を直接指定してもターミナル上で起動できます。

mlworks/src$ LD_LIBRARY_PATH=rts/bin/I386/Linux/ rts/bin/I386/Linux/main-g -MLWpass xx -load images/I386/Linux/ttyb.img xx
MLWorks 2.1 Professional Edition
Copyright (C) 1999 Harlequin Group plc.  All rights reserved.
MLWorks is a trademark of Harlequin Group plc.

MLWorks> print "Hello, MLWorks!\n";
Hello, MLWorks!
val it : unit = ()

以上

意外とあっさりREPLが動くので気が向いた人は触ってみましょう。

*1:特にこれといった面白機能があるわけでは無さそうなんですが、まぁSML freakとしては動かさないわけにはいかないですよね

*2:手元ではsml/nj110.79で確認

2016-06-03

MLKitの謎のバグを修正してaobenchが動くようにした

AObench-SMLがSMLの処理系の一つであるMLKitに対応しました。

これまではMLKitにバグがあり、実数の指数表現リテラルのうち小文字の'e'を使ったもの(e.g. 2e3 10e~5 など)が使えませんでした。

単にレキサの規則が足りてなかっただけなんですが(基本的過ぎて)謎ですね。だれも気付かなかった…?


ま、ともかくこれの修正がマージされたのでmlkitでaobenchが動くようになりました!

自分で動かしてみたい方は、現時点でのMLKitの開発ヘッド(commit:1365653)以降でお試しください。


私の手元での実行結果を張っておきます。

動作環境は32bit Linuxです。

処理系realusersys
gcc 0m3.846s 0m3.846s 0m0.006s
smlnj 0m9.545s 0m9.384s 0m0.041s
mlton 0m6.029s 0m5.927s 0m0.029s
mlkit 0m26.194s 0m25.850s0m0.037s
smlsharp2.0.0 0m31.322s 0m30.846s0m0.089s
polyml 0m12.467s 0m12.062s0m0.261s

注) SML#は更新できてないので2.0.0を使ってますがSML#の最新版は3.0.1です。

polymlが意外と健闘してるという印象ですが、mlkitはちょっと振るわないですねぇ。

配列を持ちまわってヘビーループで書き換えるベンチマークなのでメモリアロケート周りを工夫しているmlkitには不利なのかも知れません。

2016-05-25

QCheckをSML#に対応させた

以前紹介したSML版QuickCheckであるところの QCheck

SML#3.0.1で動作できるようにしてマージされましたヽ(゚ー゚*ヽ)(ノ*゚ー゚)ノ*1!!


そのマージに続いていくつか変更があって現在バージョンが v1.2 に上がっていますので今後はこれを使いましょう。

#どうでもいいけどREADMEにtravisバッジとか付いたら途端にそれらしく見えますよね


セットアップ

まずビルド方法ですが、これは make するだけです。

$ make -f Makefile.smlsharp

付属のBasisのテストも移植しました。

$ make -f Makefile.smlsharp test

恐らくString/from-toがいくつかfailしますが、これはBasisの仕様です(゚∀゚)。*2

使い方

QCheck のトップレベルのインターフェースファイル(qcheck.smi)を require します。

(* test.smi *)
_require "basis.smi"
_require "/path/to/qcheck.smi"

QCheck.checkGenを呼ぶコードを書きます。(コード例は前回と同じ)

(* test.sml *)
structure Test =
struct
  open QCheck

  (* 実装した(テストしたい)関数 *)
  fun succ x = x + 1
  fun even x = x mod 2 = 0
  fun  odd x = x mod 2 = 1

  (* 満たすべき性質 *)
  fun even_xor_odd x = even x <> odd x

  val int = (Gen.Int.int, SOME Int.toString)
  (* Check *)
  val _ = checkGen int ("even<>odd", pred even_xor_odd)
end

後はリンクして実行するだけ。

$ smlsharp -I /path/to/qcheck.smi -o test test.smi
$ ./test
even<>odd..............ok      (100 passed)

終わり

SML#を書くときはQCheckでテスト書きましょう!

*1:実はSML#1系列の時からずーーーっと処理系の都合でビルドできなくて手元に抱え込んでいました…

*2:非printableな文字が来るとstringのパースはそこで打ち切られるので toString o fromString = id にならない…。

2016-05-06

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