Hatena::ブログ(Diary)

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

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

2015-12-11

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。型推論というのは、与えられたターム(型の付いてないプログラム)から得られた型についての方程式を解くことで型を決定する仕組みです。よく知られたMLHaskell系の型推論では、高速に解ける範囲の問題に収まるように型の表現力を制限していますが、この制限を緩めて(一部を)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:まじ移植タイヘン…