古の商用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` をつけて起動するとCUIのREPLが、付けずに起動すると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が動くので気が向いた人は触ってみましょう。
MLKitの謎のバグを修正してaobenchが動くようにした
AObench-SMLがSMLの処理系の一つであるMLKitに対応しました。
これまではMLKitにバグがあり、実数の指数表現リテラルのうち小文字の'e'を使ったもの(e.g. 2e3 10e~5 など)が使えませんでした。
単にレキサの規則が足りてなかっただけなんですが(基本的過ぎて)謎ですね。だれも気付かなかった…？
ま、ともかくこれの修正がマージされたのでmlkitでaobenchが動くようになりました！
自分で動かしてみたい方は、現時点でのMLKitの開発ヘッド(commit:1365653)以降でお試しください。
私の手元での実行結果を張っておきます。
動作環境は32bit Linuxです。
| 処理系 | real | user | sys |
|---|---|---|---|
| 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.850s | 0m0.037s |
| smlsharp2.0.0 | 0m31.322s | 0m30.846s | 0m0.089s |
| polyml | 0m12.467s | 0m12.062s | 0m0.261s |
注) SML#は更新できてないので2.0.0を使ってますがSML#の最新版は3.0.1です。
polymlが意外と健闘してるという印象ですが、mlkitはちょっと振るわないですねぇ。
配列を持ちまわってヘビーループで書き換えるベンチマークなのでメモリアロケート周りを工夫しているmlkitには不利なのかも知れません。
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)
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 は 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？)(なのでその分岐は何も考えなくてよい)を体現してます。
ちなみに自分で同じマクロを書いてもちゃんと動作します。
z3sml リリース！
この記事は 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ﾟ・∀・) +
PolyMLのpretty printerをユーザ定義する
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に置いてあります。
- 実装全体@github https://github.com/eldesh/ppjson_polyml
- PolyML.PrettyPrint http://www.polyml.org/documentation/PrettyPrint.html
*1:PolyML.makeするとml_bind.MLというファイルを探して自動的に読み込んでくれます
Cygwin/X 1.17に繋げない
新たにCygwinをインストールしたマシン(win7 64bit)上で、Cygwinの提供するXサーバが使えなかった。
より正確には、XWin.exeは起動しているのにxterm等のクライアントが接続できない。
$ xterm xterm: Xt erorr: Can't open display: 192.168. ...
またこのエラーかよ !!(｀Д´)
