Infer Introduction

verify C infer


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 は p のNULLデリファレンスが起きないことが分かるので、エラーは報告されなくなります。

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


外部ライブラリを含むプロジェクトの場合も上の方法で 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:実は細かいオプションの意味はよく分からない(^^;; 標準モデルのビルドスクリプトを写しただけなので。誰か教えて。

z3sml リリース！

AdC SML SMT

この記事は MLアドベントカレンダー 12日目の記事です。


SML# 向けに Z3 というライブラリのバインディングライブラリ z3sml をリリースしました。
Z3 は SMT*1ソルバ(もしくは単にSMT) と呼ばれる種類のソフトウェアで、ある種類の制約充足問題を自動で解くことが出来ます。
z3sml を使うと、SML#からZ3のC言語インターフェースにアクセスすることが出来るようになります。

SMTとは

SMTソルバは(原則)一階述語論理の制約充足問題を扱う様々な理論ソルバの寄せ集めです。
同じく制約充足問題を扱うSATソルバが命題論理(bool式)しか扱えないのと比べて、様々な理論が使えるため問題のエンコードが簡潔かつ直接的に行えます。

参考 SATソルバーの基礎

ユースケース
パズル
SMTのデモとしてよく引き合いに出されるのは数独やピクロスと始めとするパズルソルバの実装です。これらのパズルはルールが単純でSMTソルバの入力としてエンコードしやすく、また解が列挙出来るためSMTで扱えることも明らか[要出典]です。何かを線で繋いだり囲んだりする類のパズルでも制約の記述を工夫すると解けるようです。
自動定理証明
SMTソルバは自動定理証明器としても扱えます。そもそも最初から定理証明器として作られるSMTソルバもあります。どのように定理証明が出来るかというと、まず対象の命題(P)の否定(¬P)をSMTソルバに与えます。 するとSMTソルバは命題(P)の反例を探索することになります。ここで解が見つからない場合は命題(P)の反例が無いことになり、その命題(P)が常に成り立つ事が分かり、証明終了。…となります。
型推論器
我々(誰？)にとって重要なのはこれですよね。SMTソルバは型推論にも使うことが出来る…見込みです*2。型推論というのは、与えられたターム(型の付いてないプログラム)から得られた型についての方程式を解くことで型を決定する仕組みです。よく知られたMLやHaskell系の型推論では、高速に解ける範囲の問題に収まるように型の表現力を制限していますが、この制限を緩めて(一部を)SMTソルバに力業で解かせることでより詳細な(?)型を扱うことが出来るようになります。
その他
最近では最強のボジョレーを求めることも出来るようです :)

Z3とは

Z3はマイクロソフトの研究所(MSR)が作成している高速なSMTソルバです。
いきなりトップに

Z3 is a theorem prover from Microsoft Research.

と書いてあるので実際定理証明器ですね。

でもz3のスライドを見るとテストケースの生成に使ってるとか書いてあるし、F*にも使ってるし、いろいろ使える普通のSMTソルバです。

公式に C, C++, OCaml(!!), Pythonインターフェースが提供されています。が、公式的にはpython推しっぽい気がします。

z3smlとは

今回リリースした z3sml はSMLから z3 の機能を使用できるようにしたバインディングライブラリです。
このライブラリでは SML# から z3 の全機能(v4.3.2時点^^;;)を使用できるようにバインディングが提供されています。
エラー通知やプラグイン周りのAPIが関数ポインタを要求しますが、SML# のFFIでは任意の(型の合う)クロージャを関数ポインタに変換してC側に渡せるため、これらも含めてSMLのコードだけで Z3 の機能を使うことが出来ます。*3

ビルドして動かす

ビルドするには SML# と Z3 をインストールした上で z3sml のディレクトリで make するだけです。
sample ターゲットを指定するとサンプルが実行されます。
これは公式で提供されているC APIのサンプルをほとんどそのまま含んでいるので参考にしてください。

$ make (* ビルド *)
$ make sample (* サンプルを動かす *)

使い方

自分のコードから使うにはトップ階層の z3.smi を _require するだけです。
実行する際には libz3.so が動的にリンクできる必要があります。

(* sample.smi *)
_require "z3.smi"

(* sample.sml *)
open Z3
fun main () =
	...

$ smlsharp -Iz3sml/src -o sample sample.smi

コード例(数独ソルバ)

id:suer さんのSMT solver 入門の例をパク^H^H参考にした数独ソルバをz3smlで書いた例を以下に示します。
(コード全体はもう少し長いので省略…。全体は example/example3.sml としてリポジトリに入ってるのでそちらを参照。)

open Z3
(* いろいろ準備を省略 *)

fun solve () =
with_context (fn ctx =>
let
  fun Var id = int_var ctx id

  fun Int v =
	Z3_mk_int (ctx, v, Z3_mk_int_sort ctx)

  infix 4 == <> >= <=
  fun p == q = Z3_mk_eq (ctx, p, q)
  fun p <> q = Z3_mk_not (ctx, p == q)
  fun p <= q = Z3_mk_le (ctx, p, q)
  fun p >= q = Z3_mk_ge (ctx, p, q)

  fun && xs = Z3_mk_and (ctx, Vector.fromList xs)

  fun assert p = D.Z3_assert_cnstr (ctx, p)

  val x11 = Var "v11"
  val x12 = Var "v12"
  val x13 = Var "v13"
  val x14 = Var "v14"
  val x21 = Var "v21"
  val x22 = Var "v22"
  val x23 = Var "v23"
  val x24 = Var "v24"
  val x31 = Var "v31"
  val x32 = Var "v32"
  val x33 = Var "v33"
  val x34 = Var "v34"
  val x41 = Var "v41"
  val x42 = Var "v42"
  val x43 = Var "v43"
  val x44 = Var "v44"

in
  (* domain *)
  assert (&& [(Int 1 <= x11), (x11 <= Int 4)]);
  assert (&& [(Int 1 <= x12), (x12 <= Int 4)]);
  assert (&& [(Int 1 <= x13), (x13 <= Int 4)]);
  assert (&& [(Int 1 <= x14), (x14 <= Int 4)]);
  assert (&& [(Int 1 <= x21), (x21 <= Int 4)]);
  assert (&& [(Int 1 <= x22), (x22 <= Int 4)]);
  assert (&& [(Int 1 <= x23), (x23 <= Int 4)]);
  assert (&& [(Int 1 <= x24), (x24 <= Int 4)]);
  assert (&& [(Int 1 <= x31), (x31 <= Int 4)]);
  assert (&& [(Int 1 <= x32), (x32 <= Int 4)]);
  assert (&& [(Int 1 <= x33), (x33 <= Int 4)]);
  assert (&& [(Int 1 <= x34), (x34 <= Int 4)]);
  assert (&& [(Int 1 <= x41), (x41 <= Int 4)]);
  assert (&& [(Int 1 <= x42), (x42 <= Int 4)]);
  assert (&& [(Int 1 <= x43), (x43 <= Int 4)]);
  assert (&& [(Int 1 <= x44), (x44 <= Int 4)]);

  (* distinct row *)
  assert (&& [(x11 <> x21), (x11 <> x31), (x11 <> x41), (x21 <> x31), (x21 <> x41), (x31 <> x41)]);
  assert (&& [(x12 <> x22), (x12 <> x32), (x12 <> x42), (x22 <> x32), (x22 <> x42), (x32 <> x42)]);
  assert (&& [(x13 <> x23), (x13 <> x33), (x13 <> x43), (x23 <> x33), (x23 <> x43), (x33 <> x43)]);
  assert (&& [(x14 <> x24), (x14 <> x34), (x14 <> x44), (x24 <> x34), (x24 <> x44), (x34 <> x44)]);

  (* distinct column *)
  assert (&& [(x11 <> x12), (x11 <> x13), (x11 <> x14), (x12 <> x13), (x12 <> x14), (x13 <> x14)]);
  assert (&& [(x21 <> x22), (x21 <> x23), (x21 <> x24), (x22 <> x23), (x22 <> x24), (x23 <> x24)]);
  assert (&& [(x31 <> x32), (x31 <> x33), (x31 <> x34), (x32 <> x33), (x32 <> x34), (x33 <> x34)]);
  assert (&& [(x41 <> x42), (x41 <> x43), (x41 <> x44), (x42 <> x43), (x42 <> x44), (x43 <> x44)]);

  (* distinct 2x2 block *)
  assert (&& [(x11 <> x12), (x11 <> x21), (x11 <> x22), (x12 <> x21), (x12 <> x22), (x21 <> x22)]);
  assert (&& [(x13 <> x14), (x13 <> x23), (x13 <> x24), (x14 <> x23), (x14 <> x24), (x23 <> x24)]);
  assert (&& [(x31 <> x32), (x31 <> x41), (x31 <> x42), (x32 <> x41), (x32 <> x42), (x41 <> x42)]);
  assert (&& [(x33 <> x34), (x33 <> x43), (x33 <> x44), (x34 <> x43), (x34 <> x44), (x43 <> x44)]);

  (* pre assinged values *)

  (**
   *     1   2   3   4
   *   +---+---+---+---+
   * 1 |   |   |   | 4 |
   *   +---+---+---+---+
   * 2 |   |   | 1 | 2 |
   *   +---+---+---+---+
   * 3 |   | 1 | 4 | 3 |
   *   +---+---+---+---+
   * 4 | 4 | 3 | 2 | 1 |
   *   +---+---+---+---+
   *)
  assert (x14 == Int 4);
  assert (x23 == Int 1);
  assert (x24 == Int 2);
  assert (x32 == Int 1);
  assert (x33 == Int 4);
  assert (x34 == Int 3);
  assert (x41 == Int 4);
  assert (x42 == Int 3);
  assert (x43 == Int 2);
  assert (x44 == Int 1);

  check ctx Z3.Z3_lbool.Z3_L_TRUE
end)

これを実行してみると、以下のように制約を満たすモデルを出力します。

z3sml.git$ make sample3
  SML# [sample/sample3.o]
./sample/sample3
sat
v43 -> 2
v24 -> 2
v34 -> 3
v12 -> 2
v14 -> 4
v21 -> 3
v41 -> 4
v33 -> 4
v42 -> 3
v23 -> 1
v32 -> 1
v31 -> 2
v22 -> 4
v11 -> 1
v44 -> 1
v13 -> 3

これを並べてみると以下のようになり、確かに解けていることが分かります。

    1   2   3   4
  +---+---+---+---+
1 | 1 | 2 | 3 | 4 |
  +---+---+---+---+
2 | 3 | 4 | 1 | 2 |
  +---+---+---+---+
3 | 2 | 1 | 4 | 3 |
  +---+---+---+---+
4 | 4 | 3 | 2 | 1 |
  +---+---+---+---+

コード例(定理証明)

次は定理証明の例です。サンプルコード(sample/sample2.sml)に全体があります。

(* 命題 f が成り立つことを証明する補助関数 *)
fun prove ctx f is_valid =
  local_ctx ctx (fn ctx =>
  let
    val not_f = Z3_mk_not (ctx, f)
    val () = D.Z3_assert_cnstr (ctx, not_f)
    val m : Z3_model ref = ref (Ptr.NULL())
    val ret = D.Z3_check_and_get_model (ctx, m)
    val ref m = m
  in
    case ret
      of Z3_lbool.Z3_L_FALSE => ...
       | Z3_lbool.Z3_L_UNDEF => ...
       | Z3_lbool.Z3_L_TRUE => ...
  end)

fun main () =
  with_context (fn ctx =>
  let
    infix 4 ==
    fun p == q = Z3_mk_eq (ctx, p, q)

    infix 8 $
    fun f $ x = Z3_mk_app (ctx, f, Vector.fromList [x])

    (* create uninterpreted type *)
    val U = Z3_mk_uninterpreted_sort (ctx, Z3_mk_string_symbol (ctx, "U"))
    (* g : U -> U *)
    val g = Z3_mk_func_decl (ctx, Z3_mk_string_symbol (ctx, "g"), Vector.fromList[U], U)
    (* create x and y *)
    val x = Z3_mk_const (ctx, Z3_mk_string_symbol(ctx, "x"), U)
    val y = Z3_mk_const (ctx, Z3_mk_string_symbol(ctx, "y"), U)
  in
    D.Z3_assert_cnstr (ctx, x == y); (* x == y と仮定 *)

    (* g x == g y となることを証明 *)
    print "prove: x = y ==> g(x) = g(y)\n";
    prove ctx (g $ x == g $ y) Z3_TRUE;

    (* g (g x) == g y とは(一般には)ならないことを証明 *)
    print "disprove: x = y implies g(g(x)) = g(y)\n";
    prove ctx (g $ (g $ x) == g $ y) Z3_FALSE
  end)

内容はコメントから察してもらうとして重要なのは prove です。
prove 関数の冒頭部分に注目してみると、上で説明した定理証明の形がそのまま現れていることが分かります。

fun prove ... =
 ...
 val not_f = Z3_mk_not (ctx, f) (* 命題 f の否定を作る *)
 val () = D.Z3_assert_cnstr (ctx, not_f) (* (not f) が成り立つよ と仮定してみる *)
 val m : Z3_model ref = ref (Ptr.NULL())
 val ret = D.Z3_check_and_get_model (ctx, m) (* 否定した命題を満たすモデルがあるか検証 *)
 ...

その他の例

さらなる例としては冒頭紹介した、 sample ターゲットで使用する
sample/example.sml が z3/path/to/example.c(公式のC APIのサンプル) をSMLに移植したものとなっているので見てみるとよいでしょう。
広範囲のAPIを使用するサンプルコードが多く含まれて居ます*4。

binding/naming規則

以下でbindingと命名の規則を示します。
各APIの説明は公式のC APIドキュメントで確認してください。

関数

C APIと同名の関数が structure Z3 から提供される。
ただしdeprecatedなやつはstructure Z3.Deprecated の中にある。
例えばC言語で Z3_xxx という名前の関数はSMLでは Z3.Z3_xxx という名前になる。

Z3の型

ほぼ全てのopaqueポインタはstructure Z3から提供される。これらはSMLでもopaqueポインタ型になっている。

例えば Z3_ast 型は Z3.Z3_ast (= Z3.Tag.Z3_ast ptr) として表現される。
Z3.Tag.Z3_ast 型はopaqueなのでデリファレンスは出来ないが nullable になっている。(引数経由で受け取るAPIあるから仕方ないんや…)

Enum

全てのenum型はC APIと同名のstructureとして、バリアントは(当然)コンストラクタとして提供される。
またそれぞれのstructureには val fromInt : int -> t と val toInt : t -> int が提供され、int型の値と相互に変換できる。

例えば Z3_symbol_kind は以下のようなシグネチャを持つ。

structure Z3_symbol_kind = struct
  datatype t = Z3_INT_SYMBOL
             | Z3_STRING_SYMBOL

  val fromInt : int -> t
  val toInt : t -> int
end

以上！

SML#用の z3 バインディングを紹介しました！
現状ではCと同じインターフェースしか含んでいないのでSML的な便利インターフェースを提供していきたいです。


次は古参SML#er よんた(@keita44_f4) さんの番です期待しませう +(0ﾟ・∀・) +

*1:satisfiable module theories

*2:まだメジャーでは無いという意味で

*3:出来るはず。プラグインとかは動作確認してない…。

*4:まじ移植タイヘン…

PolyMLのpretty printerをユーザ定義する

SML PolyML

Poly/MLというStandardMLの処理系があります。
このPoly/MLの提供するREPLでは、入力した式の値をエコーバックする際に使用するプリンタ(REPLの'P')をSML自身のコード内で指定することができます。


この記事では Poly/ML のREPLのpretty printerを部分的に上書きして、ユーザ定義のデータ型の表示をカスタマイズする方法を紹介します。
Poly/ML(version 5.5.1 または 5.5.2)を使用します。古いバージョン(5.5系以前)から仕様が変更されているようなので注意して下さい。

モチベーション

デフォルトで用意されているプリンタは優秀なので通常困ることはあまりありませんが、
入り組んだユーザ定義型の値の場合、いちいちコンストラクタが表示に含まれると内容が把握しづらくなることがあります。

例えば典型的な定義のjson型の値は、以下のようにいちいちコンストラクタが表示され、読みづらくなっています。

> Json.sample;
val it =
   JArray
    [JBool true, JBool false, JNull, JInteger 31412341234,
     JObject
      [("foo", JString "foos foosss..."),
       ("bar", JString "bars barsssszzzz.."), ("bazz", JArray [...])],
     JString "aaaaaaabbbbbbdddeeeeeee"]: JSON.value
>

これを例えば、通常のjsonとして表示するようなプリンタに差し替えることが出来れば、以下のように

> Json.sample;
val it =
   [
     true,
     false,
     null,
     31412341234,
     {
       "foo":"foos foosss...",
       "bar":"bars barsssszzzz..",
       "bazz":[ "bazzs", null, 141421356 ]
     },
     "aaaaaaabbbbbbdddeeeeeee"
   ]: JSON.value
>

リテラルそのままの見易い表示にすることが出来るはずです。


Poly/MLは、以上のようなREPLのP(プリンタ)を差し替える機能を提供しています。
以降の章では、上で示したユーザ定義jsonプリンタの構築を例として使い方を解説します。

前提

以下のようなディレクトリレイアウトを前提として話を進めます。

$ ls Json/
JsonTy.sml ml_bind.ML

つまりカレントディレクトリで PolyML.make "Json"; とすると structure Json (+ JsonTy)がロードされます。
これから編集していくのは Json/ml_bind.ML (が公開する structure Json) です。*1

JsonTy.smlはjsonの型だけを提供するファイルで、以下のように型定義のみから成ります。

(* JsonTy.sml *)
structure JsonTy =
  struct
    datatype value
      = JObject of (string * value) list
      | JArray of value list
      | JNull
      | JBool of bool
      | JInteger of IntInf.int
      | JReal of real
      | JString of string
  end

始まりのプリンタ

最も簡単なプリンタの定義として以下の定義からはじめます。

(* ml_bind.ML *)
open PolyML JsonTy
structure Json = struct
  fun pretty _ _ _:t = PolyML.PrettyString "<json>"
end
val () = PolyML.addPrettyPrinter JsonTy.pretty;

これを使ってみると：

> PolyML.make "Json";
> JsonTy.JInteger 314;
val it = <json>: JsonTy.t
> JsonTy.JBool true;
val it = <json>: JsonTy.t
>

JsonTy.t型の値は全て という(ひどい)表記になりました。
ここで定義した JsonTy.pretty を有用な表示をするように改善していきます。

プリンタの登録

上のように、定義したプリンタをREPLが使用するようにするには、専用に提供されている関数 PolyML.addPrettyPrinter を使い、型とそれに対応するプリンタの組を登録します。

PolyML.addPrettyPrinter : (int -> 'a -> 'b -> pretty) -> unit

この関数が要求する関数が登録するプリンタで、定義は以下のようになってい(るものとして説明し)ます。

fun printer
	depth         (* 深さ *)
	printArgTypes (* 引数のプリンタ *)
	value         (* 表示する値 *)
= ...
  • 第1引数は表示する深さです。データ構造のどこまで深い階層まで表示するのかを表します。この値が0以下の場合は PrettyString "..." を返してください。
  • 第2引数は扱おうとしているデータ型に型変数があった場合、その型用のプリンタが渡されます。今回は型変数を扱いませんので、この値は単に捨てます。
  • 第3引数は表示しようとしている値です。

プリンタの実装

プリンタは、表示を指定したい型に対応する pretty 型の値を構築して実装します。

datatype PolyML.pretty =
    PrettyBlock of int * bool * context list * pretty list
  | PrettyBreak of int * int
  | PrettyString of string

PrettyString

まず最も簡単なものから。
PrettyString はその場で(単一の行内に)表示するための文字列を表します。 "true" とか "()" などの改行を挟む余地のない要素の表現に使います。

fun pretty value =
  case value
    of Ty.JInteger x => PrettyString (LargeInt.toString x)
     | Ty.JString  s => PrettyString ("\"" ^ s ^ "\"")
     | Ty.JReal    r => PrettyString (Real.toString r)
     | Ty.JNull      => PrettyString "null"
     | Ty.JBool    b => PrettyString (Bool.toString b)
     | _ => raise Fail "undefined"

これを使うと以下のようになります。

> JReal 3.14;
val it = 3.14: T.value
> JString "hoge";
val it = "hoge": T.value
> JInteger 4242;
val it = 4242: T.value

ちゃんと(?)コンストラクタが表示されなくなりました。

PrettyBlock

PrettyBlock は他のプリンタの集合を一つのまとまったプリンタにするコンストラクタです。

PrettyBlock of int * bool * context list * pretty list
  • 第1引数はこのブロックの表示全体のインデント増加数を指定します。
  • 第2引数は改行の一貫性指定です。true を指定すると、このプリンタの扱う要素のいずれかの表示が1行に収まらない場合、すべての「改行するかも知れない場所」で改行します。
  • context listはユーザが任意に持ち回れる値ですがここでは割愛します。常に空リストで問題ありません。
  • pretty listはそのブロックを構成する子要素のプリンタの集合です。
fun interleave []      _ = []
  | interleave [x]     _ = [x]
  | interleave (x::xs) s = x::s::interleave xs s

fun pretty value =
case value
  of ... => ...
   | ... => ...
   | Ty.ARRAY  xs => 
      P.PrettyBlock (2, true, [],
                          [P.PrettyString "["]
                        @ interleave
                             (map pretty xs)
                             (P.PrettyString ",") (* コンマで区切る *)
                        @ [P.PrettyString "]"])

これを使ってみると:

> JArray [JInteger 314, JString "hoge", JArray [JReal 1.4, JNull]];
val it = [314,"hoge",[1.4,null]]: value

カンマで区切られて大分すっきりした表示になりましたが、スペースが全く無いので多少窮屈ですね。

PrettyBreak

残ったコンストラクタ PrettyBreak は要素間のスペースと改行時のインデント増加数を指定します。

datatype PolyML.pretty =
    ...
  | PrettyBreak of int * int (* スペース, インデント *)
  | ...

これを使って json array の表示を改良します。

fun pretty value =
case value
  of ... => ...
   | ... => ...
   | JArray xs =>
    let
      val pxs = map pretty xs (* Arrayの各要素のプリンタ *)
      fun split xs = foldr (fn (x,[]) => [x]
	                         | (x,xs) => [x, comma, PrettyBreak(1,0)] @ xs)
	                       [] xs
    in
      P.PrettyBlock (indent, consistent, []
			   (* 括弧 '[' + スペース *)
			 , [bracket_open , P.PrettyBreak(1, 0)]
			 @ (split pxs)
			   (* インデント浅く + 括弧 ']' *)
			 @ [P.PrettyBreak(1,~indent), bracket_close])
    end

括弧開く '[' の時点でインデントが入っているので、閉じる ']' 時にのみ符号を反転してマイナスのインデントを指定します。
では実際に大きめのJson Arrayで確認してみます。

> JArray [JInteger 314, JString "hogehogehoge", JArray [JReal 1.4, JArray [JNull, JBool true, JBool false, JNull, JString "foo bar bazz"]]];
val it =
   [
     314,
     "hogehogehoge",
     [ 1.4, [ null, true, false, null, "foo bar bazz" ] ]
   ]: value

要素間のスペース、ブラケットの内側で必要に応じた改行と必要に応じたインデントが追加され、より大きい構造を持つ値も見やすく表示されるようになりました。

まとめ

Poly/MLのREPLを使う際、処理系の提供する関数 addPrettyPrinter を使って JSON型 のプリンタを上書きすることが出来ました。
これは型の定義とは独立して(ml_bind.MLで)定義;設定するため、既存のコードを変更せず導入できます。

もちろん同様の方法で任意のユーザ定義型についてプリンタが設定可能なので、デフォルトの表示で不満がある場合は、適宜プリンタを変更して快適にREPLを使いましょう。


ここで紹介した実装(を元にしたprinter)全体はgitに置いてあります。

*1:PolyML.makeするとml_bind.MLというファイルを探して自動的に読み込んでくれます

Cygwin/X 1.17に繋げない

Cygwin x_window_system

新たにCygwinをインストールしたマシン(win7 64bit)上で、Cygwinの提供するXサーバが使えなかった。
より正確には、XWin.exeは起動しているのにxterm等のクライアントが接続できない。

$ xterm
xterm: Xt erorr: Can't open display: 192.168. ...

またこのエラーかよ !!(｀Д´)

解決

デフォルトでのXの挙動が変更され、tcp接続を受け付けなくなったのが原因らしい。
以下のように -listen tcp オプションをつけて起動すればよい。

// 変更前のX起動コマンド
$ run xwin -multiwindow

// 変更後X起動コマンド
$ run xwin -multiwindow -listen tcp

$DISPLAY を localhost:0.0 とか指定していると(= tcpを使うようになってると)、ローカルのクライアントも起動できなくなるので注意。

参考

改訂新版C++ポケットリファレンスレビュー

C++ review

前回のBoost.勉強会でいただいた 改訂新版C++ポケットリファレンス を一通りさらったのでレビュー(というか紹介)を書いておきます。

どんな本？

この本は、目的から探せる形式でC++の(主に)標準ライブラリを解説した逆引きリファレンスです。
今回私が読んだ第2版(「改訂新版」が付いてる方)では、現在最新の規格であるC++14に対応していて、新たにconstexpr指定が追加された箇所等に解説が加えられています。

各項目には、関連するライブラリのシグネチャと簡単な利用例が完結したコードとして載っていて、もっとも単純な類のユースケースと機能が簡単に把握できます。
コア言語に関連した内容もトピックとしてはだいたい網羅的に紹介されていますので、構文の詳細や特定のライブラリがあることは知っているんだけど、'そら'では出て来ない。といった場合に便利です。

どんな人向け？

古いC++を知っている人、あるいはぼんやりとC++を知っている人が、C++11や14で新たに加えられたライブラリや機能を一通り頭に入れるのに適していると思います。

簡単な使用例が併記されているのも、使い込んでいない機能を手っ取り早く理解するにはポイントが高いところです。
載っているサンプルコード自体も一貫してモダンなスタイルで書かれているので、眺めてみると気付くことがあるかも知れません。


ただし、とっかかりとしてはともかく、この本でC++を勉強しようというのは本書の目的からは外れていると思います。
あくまでリファレンスですので、知っていることを手っ取り早く思い出す記憶の2次キャッシュとして、あるいは目的の機能を実現する手段に辿り着くためのインデックスとしての使い方がオススメです。
本棚ではなく手元に置いておくとよさげ。

その他

ほぼ修正が自明なものばかりではありますが、サンプルコードを中心にいくつか誤植があり、私もいくつか報告しました。
エラッタは 著者によるサポートサイト にまとまっているので怪しいと思ったら確認＆報告しましょう。


改訂新版　C++ポケットリファレンス

改訂新版　C++ポケットリファレンス

Boost.勉強会 #17 東京に参加

C++ 勉強会 event

先日(2015/05/30)行われたBoost.勉強会 #17 東京に久々に参加してきました。
IIJ新社屋がめっちゃ綺麗でビビりつつ滑り込みセーフ(アウト)で会場着。


セッション資料は以下にまとまってます。
Boost.勉強会 #17 東京 タイムテーブル


C++は適用ドメインがまったく絞られないので、数値計算(?)からブラウザゲームまで相変わらずバリエーションに富んだ発表内容でした。

印象的だったセッションについて

まず id:redboltz さん の「MessagePackとAPIバージョニング」を聴いてinline namespaceの存在を思い出しました(^^;;
これを知った時はデバッグ版とリリース版を切り替えるというユースケースで紹介されていた気がしますが、バージョニングにも使えそうですね。
ただ名前探索についてかなり詳細に理解している必要がありそうなので、もうすこし設計指針がこなれて来ればいいなぁ…という気がします。


他には [twitter:@Reputeless] さんのSiv3Dの発表が見てて楽しかったですね。
processingより型がかなりまともそうなので、次に可視化したいものがあったらSiv3Dを使うのも良さそうです。
あとウィジェットが標準装備なのもかなりポイント高いと思います。


最後に、kou_yeung, paosidufygthrj*1 さんの「C++11やEmscriptenと付き合って１年間の振り返り」。
つまり、emscriptenマジヤバイ。
何度か説明聞いて理屈は分かるんだけど、でも何言ってるのか意味分からない。

その他

個人的な目的でもあったのでDirectShowとMF(MediaFoundation)の話を[twitter:@yohhoy]さんに聴く。
薄々気付いてはいたものの、教えてもらったことをまとめると、DirectShow is 闇。だれか教えてください。


あと[twitter:@egtra]さんにCOMの勉強方法について教えてもらおうとするも、特に良い資料は無いらしい。つらい。
ATL/COMの本(多分コレ)はとりあえず持っておけとのこと。



最後に、じゃんけん大会で勝って、ポケットに入らないと評判のC++ポケットリファレンス第2版(C++14対応)を頂きました！！ →
貰ってから知ったんですが本当に出来立てらしく、レビュー書かないといけない流れ(^^;;
個人的にもC++14にはキャッチアップ出来てないことですし、読んでレビュー書くつもりです。

*1:どういう読みなんだろう

firefoxの更新をキャンセルする

browser


firefoxというブラウザでは [ソフトウェアの更新を確認] すると手元のソフトウェアが最新バージョンに更新される。
中断は(少なくとも素の状態では)出来ない。*1
何を言っているのか分からないと思うが事実だ。
ちなみにこの「ソフトウェアの更新」ボタンは「ヘルプ」メニューの中*2にある。意味が分からない。


ダウンロード自体の中断はどうやるのか分からなかったが、更新ファイルのダウンロードが終わってから以下のフォルダを削除すると更新せずに済んだ(ようだ)。


任意のバージョンが欲しい場合は以下のサイトからダウンロードできる。
> ftp://ftp.mozilla.org/pub/mozilla.org/firefox/releases/

*1:アプリケーション自体を終了しても次回の起動時に再開する

*2:孫要素