うらぶろぐ @urasandesu: 7月 2016

フロー解析したい。フロー解析したくない？
— Akira Sugiura (@urasandesu) September 29, 2014

C# で作られた既存のシステムを改修する際、安全のため、現在の仕様を自動化された単体テストで囲ってから手を加えるっていうのはよくやるんですが、全ての振る舞いを通すよう、パラメータのバリエーションを考えるのは結構大変だったりします。

対象の機能が、時間が無かったなどの理由で急いで作ったのであれば、整理されていない幾重にもなる && や || が条件分岐として立ちはだかることも少なくなく、心が折れること必至。かと言って、「うーん、あっちがそっちで、ここがこうで……まあいっか！」などと勢いに任せてやってしまえば、さらなる複雑化や不具合の混入を招くこと必至です。冒頭のつぶやきのように、「コンピュータが、うまいこと処理の流れ解析してくれて、全てのパス通すパラメータのバリエーション作ってくれないもんかなー」と誰しもが思い始めるでしょう。

こんな時、Visual Studio（以下、VS）2010 世代であれば、Pex というフレームワークが無料で使えました。先ほどの、全ての振る舞いを通すパラメータのバリエーションを求め、テストコードを自動生成してくれたのです。使われていた方の評価を見ると、「バグったコードは基本として書けません、仕組み的に。」という素晴らしいもの。しかし、VS2013 世代になると、Code Digger という、機能を大幅に削られたものになりました。テストはもはや生成されず、無理やり作らせるにはハックが必要になってしまいました。VS2015 世代になり、再び Pex と同等のテストを生成できる機能を持つ IntelliTest が搭載されましたが、残念ながら Enterprise エディション以上でしか利用できません。頼む！Pex と同じように全てのエディションで使えるようにしてくれー！ってリクエストは結構前から上がっているのですが、今のところ放置されてる状態。まあ、競合製品もほとんどないので（Parasoft の dotTEST が近いぐらい？）、なんでもかんでも利用可能にするのは難しいのでしょうね。

というわけで、Pex が使えなくなってしまった VS2013 世代以降でも使える、仕様化テストを自動生成する何かを作り始めました。名を Fayle（ふぇいる）と言います：

まだ試作段階ということで、master ブランチには何も入れてません。しばらくはキリの良いところ毎に spike ブランチを切り、情報共有ができればと考えています（今回は ja_spike-01）。まずは基本のキ、基礎となっている技術や基本的な方針などを解説していきましょう。それでは、ごゆっくりどうぞ～。

以下の記事、論文およびライブラリを使用/参考にさせていただいてます！いつもありがとうございます！！ m(_ _)m
Pex and Moles - Isolation and White box Unit Testing for .NET - Microsoft Research
kazuk の開発環境晒し | kazuk は null に触れてしまった
Microsoft Code Digger extension
Microsoft Code Digger をさっそくハックした | kazuk は null に触れてしまった
Generate unit tests for your code with IntelliTest
Midnight Researcher Notes: The Z3 Constraint Solver, a developer perspective
Z3Prover/z3: The Z3 Theorem Prover
SMT@Microsoft
Z3 @ rise4fun from Microsoft
Pex for fun - from Microsoft Research
業績一覧 - 大阪大学大学院情報科学研究科コンピュータサイエンス専攻ソフトウェア設計学講座楠本研究室
SAT/SMTソルバの仕組み
SMT solver 入門 - すえひろがりっっっっ!
シンボリック実行に入門しようとした | 一生あとで読んでろ
converting IR to Z3 formula? - Stack Overflow
Equivalent of define-fun in Z3 API - Stack Overflow
Z3 4.3: get complete model - Stack Overflow

目次

やりたいこと
Z3
Flow Analysis
実装
終わりに

やりたいこと
Pex for fun で解説されているサンプルそのもので恐縮ですが、対象のプログラムとして、以下のようなものを考えてみます：

	using System;

	namespace HowDoesPexWork
	{
	class HiddenBug
	{
	public static void Puzzle(int[] v)
	{
	if (v != null &&
	v.Length > 0 &&
	v[0] == 1234567890)
	throw new Exception("hidden bug!");
	}
	}
	}

view raw 661425685-01.cs hosted with ❤ by GitHub

int 型の配列 v を 1 つ引数に取る単純なメソッドです。問題があるケースは、

v が null ではない。
かつ、v の長さが 0 より大きい。
かつ、v の要素 0 が 1234567890 になっている。

場合に発生するとのこと・・・まあ、このレベルであればパッと見でわかるのですががが (^_^;)

冒頭にあった通り、まずはこのメソッドの仕様を囲いたいと思います。パスを考えると・・・以下の 4 パターンがありますね（括弧内は C# で表した制約）：

v が null（v == null）
v が null でないかつ、v の長さが 0 以下（!(v == null) && !(v.Length > 0)）
v が null でないかつ、v の長さが 0 より大きいかつ、v の要素 0 が 1234567890 になっている（!(v == null) && v.Length > 0 && v[0] == 1234567890）
v が null でないかつ、v の長さが 0 より大きいかつ、v の要素 0 が 1234567890 以外（!(v == null) && v.Length > 0 && !(v[0] == 1234567890)）

そうすると、やりたいことは、①この 4 パターンのパスを通す引数を自動的に求め、②それを使ったパラメタライズドテストを自動生成すること、になります。①さえできれば、②は単なるソースコード生成ですので、①をメインに考えていきましょう。例えば、上記それぞれのパターンに対して、

null
new int[0]
new[] { 1234567890 }
new[] { 1234567890 以外の整数 }

を出力する機能が欲しいわけです。テストコードで表すとこんな感じになるでしょうか：

	using Mono.Cecil;
	using NUnit.Framework;
	using System.Linq;
	using Urasandesu.Fayle;

	namespace Test.Urasandesu.Fayle
	{
	[TestFixture]
	public class FayTest
	{
	[Test]
	public void GetInterestingInputs_can_get_inputs_that_cover_all_execution_path()
	{
	// Arrange
	var sampleName = "HiddenBug";
	var asmDef = AssemblyDefinition.ReadAssembly("HowDoesPexWork.dll");
	var modDef = asmDef.MainModule;
	var typeDef = modDef.Types.First(_ => _.Name == sampleName);
	var methDef = typeDef.Methods.First(_ => _.Name == "Puzzle");

	// Act
	var results = new Fay().GetInterestingInputs(methDef).Select(_ => _.Value).ToArray();

	// Assert
	Assert.That(results.Length, Is.EqualTo(4));
	Assert.That(results[0], Is.Null);
	Assert.That(results[1], Is.EqualTo(new int[0]));
	Assert.That(results[2], Is.EqualTo(new[] { 1234567890 }));
	Assert.That(results[3], Has.Length.GreaterThanOrEqualTo(1).And.Not.EqualTo(new[] { 1234567890 }));
	}
	}
	}

view raw 661425685-02.cs hosted with ❤ by GitHub

対象のプログラムのメソッド定義情報を取得し（methDef）、それを①の機能（Fay.GetInterestingInputs）に与えると、各実行パス向けの引数のバリエーションを全て求めてくれる寸法です。メソッド定義情報の取得については、後述のライブラリの仕様の関係で Mono.Cecil を使っていますが、こちらはすでに色々なところで紹介されていると思いますので、ここでは特に解説はしません。①の実現方法についてのみ考えていきたいと思います。

Z3
Pex はどうやって値のバリエーションを生成していたの？と調べ始めると、すぐ Z3 という定理証明器を使っていることがわかります。当初はテイリショウメイキ？なにそれ？おいしいの？という感じでしたが、ライブラリの公式ガイドを見る限り、今回のような用途で使う分にはそこまで難しいことはありませんでした。要は「与えた制約を全て満たす解を求めてくれる」ものです。ムズカシイ言葉だと「充足可能性を調べる」と言うそうですが、今のところ「連立方程式みたいなのが解けるのかー」ぐらいの理解デ大丈夫デス（棒読み）。

制約に当たる部分はもうありますね（上記 4 パターン）。Z3 が解釈できる SMT-LIB 標準形式で書き下してみましょう（Z3 は v2.0 を大体サポート、v2.5 は実装中）：

	(push)
	(echo "#1. v == null -----------------------------------------------")
	(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
	(declare-const v SystemInt32Array)
	(assert (= v null))
	(check-sat)
	(get-model)
	(pop)

	(push)
	(echo "#2. !(v == null) && !(v.Length > 0) -------------------------")
	(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
	(declare-const v SystemInt32Array)
	(assert (not (= v null)))
	(assert (not (> (seq.len (value v)) 0)))
	(check-sat)
	(get-model)
	(pop)

	(push)
	(echo "#3. !(v == null) && v.Length > 0 && v[0] == 1234567890 ------")
	(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
	(declare-const v SystemInt32Array)
	(assert (not (= v null)))
	(assert (> (seq.len (value v)) 0))
	(assert (= (seq.at (value v) 0) (seq.unit 1234567890)))
	(check-sat)
	(get-model)
	(pop)

	(push)
	(echo "#4. !(v == null) && v.Length > 0 && !(v[0] == 1234567890) ---")
	(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
	(declare-const v SystemInt32Array)
	(assert (not (= v null)))
	(assert (> (seq.len (value v)) 0))
	(assert (not (= (seq.at (value v) 0) (seq.unit 1234567890))))
	(check-sat)
	(get-model)
	(pop)

	; #1. v == null -----------------------------------------------
	; sat
	; (model
	; (define-fun v () SystemInt32Array
	; null)
	; )
	; #2. !(v == null) && !(v.Length > 0) -------------------------
	; sat
	; (model
	; (define-fun v () SystemInt32Array
	; (SystemInt32Array 1 (as seq.empty (Seq Int))))
	; )
	; #3. !(v == null) && v.Length > 0 && v[0] == 1234567890 ------
	; sat
	; (model
	; (define-fun v () SystemInt32Array
	; (SystemInt32Array 4 (seq.unit 1234567890)))
	; )
	; #4. !(v == null) && v.Length > 0 && !(v[0] == 1234567890) ---
	; sat
	; (model
	; (define-fun v () SystemInt32Array
	; (SystemInt32Array 3 (seq.unit 5)))
	; )

view raw 661425685-03.lisp hosted with ❤ by GitHub

Web 上の REPL で動かした結果はこちら。.NET のクラスは、先人の知恵を参考に Datatypes にエンコードしています。配列のような、長さと要素を持つものは、シーケンスにエンコードすると扱いやすかったですね（Z3 にも配列があるが、無限長なので長さに対する制約が書きにくい）。

さて、結果を確認すると、

null
new int[0]
new[] { 1234567890 }
new[] { 5 }

とデコードできそうな情報が出力されているのがわかります。つまり、各実行パス向けの制約全てを SMT-LIB 標準形式にエンコードすることさえできれば、関心がある入力値のバリエーションが求められそうですね！

Flow Analysis
各実行パス向けの制約を求めるには、IL の並びから処理の流れを解析する必要があります。この辺りも、調べるとすぐ ILSpy がそういう機能を持っている風の情報が見つかりますので、ありがたく使わせていただきましょう。ちなみに、ILSpy は、エンジン部分が分離されて Nupkg 化されていますので、今回のように UI を必要とせず、ライブラリとして使いたい場合は、こちらを使うと何かと捗ります。

中を見ると、その名もズバリ FlowAnalysis っていう名前空間がありますので、迷うことはないと思います。エントリーポイントは SsaFormBuilder。SSA 形式もこの時はまだ？？？だったのですが、@linerlock さんから静的単一代入形式なるものだということを教えていただけました。静的単一代入形式にしておくことで、同じ変数に値が代入されるようなコードが書かれていたとしても、無理なく制約にエンコードできるようになります。

SsaFormBuilder から出力される SsaForm には、自身を dot 言語に変換可能な機能があります。処理の流れを確認するには、以下のようなコードでこの情報を出力し・・・（※Mono.Cecil を使ったのは、ここの機能が依存していたからでした）：

	var sampleName = "HiddenBug";
	var asmDef = AssemblyDefinition.ReadAssembly(@"...dll へのフルパス...");
	var modDef = asmDef.MainModule;
	var typeDef = modDef.Types.First(_ => _.Name == sampleName);
	var methDef = typeDef.Methods.First(_ => _.Name == "Puzzle");
	var ssa = SsaFormBuilder.Build(methDef);
	var graph = ssa.ExportBlockGraph();
	graph.Save("hoge.gv");

view raw 661425685-04.cs hosted with ❤ by GitHub

Graphviz を使ってグラフ化するとわかりやすいでしょう：

CMD C:\> dot hoge.gv -Tpng -o hoge.png

view raw 661425685-05.bat hosted with ❤ by GitHub

これを眺めると、SSA 形式上の変数（tempXX）に値が割り当てられる度に制約を積み、ブランチ命令や例外を発生させる命令毎にそれらをグルーピングすることさえできれば、各実行パスを通す全ての条件を考慮できそうですね！

実装
ここまでで、処理は、大きく分けて 2 つのことを行えば良さそうなことがわかってきました：

SMT-LIB 標準形式へのエンコード
対象メソッド定義情報→SSA 形式→SMT-LIB 標準形式へと順にエンコード。SSA 形式→SMT-LIB 標準形式は、SSA 形式上の変数に値が割り当てられる度に制約を積み、ブランチ命令や例外を発生させる命令毎にそれらをグルーピングする。
関心がある入力値の検索
各実行パス向けの制約の SMT-LIB 標準形式を Z3 に与え、各々を満たす解を取得する。取得した解を解析し、.NET のオブジェクトにデコードする。

1. は、TranspilingToSmtService が担います。対象メソッド定義情報を SSA 形式に変換後、その構成要素（SsaForm, SsaBlock, SsaInstruction, SsaVariable）を、SMT-LIB 標準形式を表す構成要素（SmtForm, SmtBlock, SmtInstruction）にエンコードしていきます：

brfalse.s や ble.s、bne.un_s といったブランチ命令は、「条件を満たしブランチするパターン」と「条件を満たさずそのまま進むパターン」の制約を積む。
ldlen や ldelem.i4 といった例外を発生させる可能性がある命令も同様、「条件を満たし例外を発生させるパターン」と「条件を満たさずそのまま進むパターン」の制約を積む。
ブランチ命令と異なるのは、例外は、1 つの命令で複数のものが発生する可能性があること。例えば、ldelem.i4 は「必要とするオブジェクト参照が null のパターン」「そのオブジェクト参照とされた配列の型が違うパターン」「インデックスが配列の範囲外（負の方向）のパターン」「インデックスが配列の範囲外（正の方向）のパターン」の計 4 パターンが発生する可能性があることに注意し、全てのパターンの制約を積むようにする。
それ以外は、SSA 形式上の変数に値が割り当てられる毎に制約を積んで行く。

最後に SMT-LIB 標準形式にエンコードし、重複する制約を除去します。ここまでの結果はこんな感じになります：

	;#(2, Branch, (SomethingBranch:1), 4)
	(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
	(declare-const temp1 SystemInt32Array)
	(declare-const v SystemInt32Array)
	(declare-const temp2 SystemInt32Array)
	(assert (= temp1 v))
	(assert (not (= temp1 null)))
	(assert (= temp2 v))
	(assert (= temp2 null))
	;#(2, Branch, (SomethingBranch:1), 6)
	(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
	(declare-const temp1 SystemInt32Array)
	(declare-const v SystemInt32Array)
	(declare-const temp2 SystemInt32Array)
	(declare-const temp3 Int)
	(declare-const temp4 Int)
	(declare-const temp5 Int)
	(declare-const temp6 SystemInt32Array)
	(declare-const temp7 Int)
	(assert (= temp1 v))
	(assert (not (= temp1 null)))
	(assert (= temp2 v))
	(assert (not (= temp2 null)))
	(assert (= temp2 v))
	(assert (= temp3 (seq.len (value temp2))))
	(assert (= temp4 temp3))
	(assert (= temp5 0))
	(assert (not (<= temp4 temp5)))
	(assert (= temp6 v))
	(assert (= temp7 0))
	(assert (= temp6 null))
	;#(2, Branch, (SomethingBranch:2), 6)
	(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
	(declare-const temp1 SystemInt32Array)
	(declare-const v SystemInt32Array)
	(declare-const temp2 SystemInt32Array)
	(declare-const temp3 Int)
	(declare-const temp4 Int)
	(declare-const temp5 Int)
	(declare-const temp6 SystemInt32Array)
	(declare-const temp7 Int)
	(assert (= temp1 v))
	(assert (not (= temp1 null)))
	(assert (= temp2 v))
	(assert (not (= temp2 null)))
	(assert (= temp2 v))
	(assert (= temp3 (seq.len (value temp2))))
	(assert (= temp4 temp3))
	(assert (= temp5 0))
	(assert (not (<= temp4 temp5)))
	(assert (= temp6 v))
	(assert (= temp7 0))
	(assert (not (= temp6 null)))
	(assert (< temp7 0))
	;#(2, Branch, (SomethingBranch:3), 6)
	(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
	(declare-const temp1 SystemInt32Array)
	(declare-const v SystemInt32Array)
	(declare-const temp2 SystemInt32Array)
	(declare-const temp3 Int)
	(declare-const temp4 Int)
	(declare-const temp5 Int)
	(declare-const temp6 SystemInt32Array)
	(declare-const temp7 Int)
	(assert (= temp1 v))
	(assert (not (= temp1 null)))
	(assert (= temp2 v))
	(assert (not (= temp2 null)))
	(assert (= temp2 v))
	(assert (= temp3 (seq.len (value temp2))))
	(assert (= temp4 temp3))
	(assert (= temp5 0))
	(assert (not (<= temp4 temp5)))
	(assert (= temp6 v))
	(assert (= temp7 0))
	(assert (not (= temp6 null)))
	(assert (not (< temp7 0)))
	(assert (<= (seq.len (value temp6)) temp7))
	;#(3, Branch, NotApplicable, -1)
	(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
	(declare-const temp1 SystemInt32Array)
	(declare-const v SystemInt32Array)
	(assert (= temp1 v))
	(assert (= temp1 null))
	;#(5, Branch, NotApplicable, -1)
	(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
	(declare-const temp1 SystemInt32Array)
	(declare-const v SystemInt32Array)
	(declare-const temp2 SystemInt32Array)
	(declare-const temp3 Int)
	(declare-const temp4 Int)
	(declare-const temp5 Int)
	(assert (= temp1 v))
	(assert (not (= temp1 null)))
	(assert (= temp2 v))
	(assert (not (= temp2 null)))
	(assert (= temp2 v))
	(assert (= temp3 (seq.len (value temp2))))
	(assert (= temp4 temp3))
	(assert (= temp5 0))
	(assert (<= temp4 temp5))
	;#(7, Normal, NotApplicable, -1)
	(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
	(declare-const temp1 SystemInt32Array)
	(declare-const v SystemInt32Array)
	(declare-const temp2 SystemInt32Array)
	(declare-const temp3 Int)
	(declare-const temp4 Int)
	(declare-const temp5 Int)
	(declare-const temp6 SystemInt32Array)
	(declare-const temp7 Int)
	(declare-const temp8 Int)
	(declare-const temp9 Int)
	(assert (= temp1 v))
	(assert (not (= temp1 null)))
	(assert (= temp2 v))
	(assert (not (= temp2 null)))
	(assert (= temp2 v))
	(assert (= temp3 (seq.len (value temp2))))
	(assert (= temp4 temp3))
	(assert (= temp5 0))
	(assert (not (<= temp4 temp5)))
	(assert (= temp6 v))
	(assert (= temp7 0))
	(assert (not (= temp6 null)))
	(assert (not (< temp7 0)))
	(assert (not (<= (seq.len (value temp6)) temp7)))
	(assert (= temp6 v))
	(assert (= temp7 0))
	(assert (= (seq.unit temp8) (seq.at (value temp6) temp7)))
	(assert (= temp9 1234567890))
	(assert (not (not (= temp8 temp9))))
	;#(7, Branch, NotApplicable, -1)
	(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
	(declare-const temp1 SystemInt32Array)
	(declare-const v SystemInt32Array)
	(declare-const temp2 SystemInt32Array)
	(declare-const temp3 Int)
	(declare-const temp4 Int)
	(declare-const temp5 Int)
	(declare-const temp6 SystemInt32Array)
	(declare-const temp7 Int)
	(declare-const temp8 Int)
	(declare-const temp9 Int)
	(assert (= temp1 v))
	(assert (not (= temp1 null)))
	(assert (= temp2 v))
	(assert (not (= temp2 null)))
	(assert (= temp2 v))
	(assert (= temp3 (seq.len (value temp2))))
	(assert (= temp4 temp3))
	(assert (= temp5 0))
	(assert (not (<= temp4 temp5)))
	(assert (= temp6 v))
	(assert (= temp7 0))
	(assert (not (= temp6 null)))
	(assert (not (< temp7 0)))
	(assert (not (<= (seq.len (value temp6)) temp7)))
	(assert (= temp6 v))
	(assert (= temp7 0))
	(assert (= (seq.unit temp8) (seq.at (value temp6) temp7)))
	(assert (= temp9 1234567890))
	(assert (not (= temp8 temp9)))

view raw 661425685-06.lisp hosted with ❤ by GitHub

各グループの #(xx… が、それを導出する元となった SSA 形式の Block #xx に対応しています。#(2… であれば例外を発生させる可能性がある命令を含む Block のグループ、#(3… であれば最初のブランチ命令（brfalse.s）を含む Block のグループ、という感じですね。

ところでこの結果、全部で 8 グループもありますので、「あれ？多くね？？」と思われる方もいらっしゃるかもしれませんが・・・安心してください。次の手順でちゃんと除外されるようになっています（ヒント：例外を発生させる可能性がある命令を含む Block のグループは充足可能か？）。

2. は、FindingInterestingInputsService が担います。SMT-LIB 標準形式を表す構成要素のルート（SmtForm）から、Z3 が解釈できる SMT-LIB 標準形式の文字列を取り出し、グループ毎に充足可能性をチェックしていきます。

さて、最初に Web 上の REPL で Z3 を動かした結果は、SMT-LIB 標準形式で言う「定義」の形（define-fun）で返ってくるように見えましたね。実際の C# の API ではどうなっているのでしょう？調査したところ、C# 上で、Z3 を SMT-LIB 標準形式の文字列を渡すような形で使う場合、以下のような流れの処理になるようでした（公式 .NET サンプルに ParseSMTLIB2String を使ったものがないため、ちょっと怪しいかも…）：

	// Z3 向けのコンテキストを生成。
	using (var ctx = new Context())
	{
	// SMT-LIB 標準形式の文字列を渡し、Expr オブジェクトにパース。
	var expr = ctx.ParseSMTLIB2String(...);

	// ソルバーを生成し、先ほど取得した Expr オブジェクトをアサート。
	var solver = ctx.MkSolver();
	solver.Assert(expr);

	// 充足可能性を計算。充足可能でなければ（充足不能 or 計算不可）、処理をやめる。
	if (solver.Check() != Status.SATISFIABLE)
	...

	// アサートした結果をすべて満たす解釈（Expr オブジェクト）を取得。
	foreach (var constDecl in solver.Model.ConstDecls)
	{
	var interp = solver.Model.ConstInterp(constDecl);
	// 取得した Expr オブジェクトを使って何かする。
	...
	}
	}

view raw 661425685-07.cs hosted with ❤ by GitHub

ポイントは Expr オブジェクト。構造は単純で、基本的に名前や戻り値のソート（型のこと）を示す関数情報と引数になる Expr オブジェクトのコレクションを持つツリー構造になっています。整数や文字列に直接デコードできるものは、これに加えて実際値が取得できます。
最終的に .NET オブジェクトが欲しいので、この Expr オブジェクトを走査し、.NET オブジェクトにデコードする必要があります（よくある Visitor パターンでのデータ収集になると思います）。SMT-LIB 標準形式は、元々そんな複雑な仕様ではないので、ここはそこまで悩まずに実装できるでしょう。

終わりに
Pex やそのコアライブラリである Z3 は、これまでもちょいちょい勉強を進めていたのですが、Prig のほうがだいぶ落ち着いたのと、久々に GW に長期休暇が取れたこともあって、やっとがっつり手を付けられたかなーと思います。それにしても、やはり全然やったことのない分野のライブラリは、難しい分、動くようになったときの感動もひとしおですね。

うっほ！Z3使ってフルパスカバレッジ通すメソッド引数バリエーション求めるの、1パスｷﾀ━━━━(ﾟ∀ﾟ)━━━━!!!!!!! pic.twitter.com/N99Q8p52dj
— Akira Sugiura (@urasandesu) July 13, 2016

まあ、現状ハードコーディングごりごりの試作なので、今後、Z3 に標準で用意されていない型はどう Datatypes にエンコードするのー？とか、メソッドの呼び出しはどうするのー？とか、呼び出せたとしても再帰してたり、ネットワークやファイルシステムとかの外部環境に依存してたらどうなるのー？とか、ループはどう解釈するのー？とか、isinst みたいな継承階層チェックする命令はどう制約として表現するのー？とか、参照の比較はどうするのー？とか、解決していくべき課題は多いのですが、ボチボチやっていけたらと思います。

最後になりましたが、新しいライブラリを作るに当たり、名前のアイデア出しを協力してくださった職場の皆さん、この場を借りてお礼させていただければと思います。ありがとうございました！！

「Fayle」は Fay（妖精）+ le（道具を表す接尾語）の造語。TDD の黄金の回転の始まりである Red、つまり Fail の捩りにもなっています。いつの日か、テスト作りは妖精さんにお願い！とか言えちゃうような日が来ることを夢見て。俺たちの戦いはこれからだ！（迫真）

うらぶろぐ @urasandesu

2016年7月18日月曜日

C# で仕様化テストを自動生成するための基礎 - The road to Pex/Code Digger/IntelliTest -

自己紹介

ブログアーカイブ

うらぶろぐ @urasandesu

2016年7月18日月曜日

C# で仕様化テストを自動生成するための基礎 - The road to Pex/Code Digger/IntelliTest -

自己紹介

ブログ アーカイブ

ブログアーカイブ