2017年1月4日水曜日

C# パラメタライズド テスト自動生成基礎 ツヴァイ！ -The road to Pex/Code Digger/IntelliTest Zwei!-

前回に引き続き、C# で仕様化テストを自動生成するための基礎を固めて行きます。今回は、宿題だった「Z3 に標準で用意されていない型はどう Datatypes にエンコードするのー？」「メソッドの呼び出しはどうするのー？」辺りを見ていきましょう。


今回説明した箇所の全体像については、前回同様 spike ブランチを切り、公開しました（今回は ja_spike-02）。規模感ですが、プロトタイプ 01 でステップ数：約 4 kloc、クラス数：133 あったものが、プロトタイプ 02 ではステップ数：約 13 kloc、クラス数：305、と 3 倍近くになっています。ただ、感覚としては全体の 1 割できたかな？ぐらいの感じなので、やはり最終的には、Prig と同じぐらいの規模（ステップ数：約 126 kloc、クラス数：2500 前後）になるのかな、と思います。先は長いですが、一歩一歩進みましょう。


以下の記事、論文およびライブラリを使用/参考にさせていただいています。本当にありがとうございました！ ( ･ㅂ･)و ̑̑
How to code this in Z3 - Stack Overflow
Services in Domain-Driven Design (DDD) - Lev Gorodinski
Code rant: Using the Visitor Pattern with Domain Entities
DDDのドメインイベントについて勉強 - Mitsuyuki.Shiiba
Experimenting with Z3 - Proving opaque predicates | Tomislav Zubcic's blog
Experimenting with Z3 - Dead code elimination | Tomislav Zubcic's blog
.NET Type Internals - From a Microsoft CLR Perspective - CodeProject
Resolve() and generics - Google Groups
ソートと指標と型、実例をまじえて - 檜山正幸のキマイラ飼育記
いまさらながらだけど、オブジェクトとクラスの関係を究めてみようよ - 檜山正幸のキマイラ飼育記
VB.NETでも制約ソルバーを用いて数独を解きたい　その１ - レンコン畑でつかまえて
VB.NETでも制約ソルバーを用いて数独を解きたい　その２ - レンコン畑でつかまえて
Z3による汎用大域的最適化 by @kotauchisunsun on @Qiita
Z3によるXORを再現するニューラルネットワークの構築 by @kotauchisunsun on @Qiita
c# - Mono.Cecil TypeReference to Type? - Stack Overflow
急にEventSourceクラスを使ってEvent Tracing for Windows経由でイベントログにログを書くことになった人向けのチュートリアル - Qiita
20140329 modern logging and data analysis pattern on .NET by @tanaka_733 #aws #azure
EnterpriseLibrary 6のSemantic Logging Application Block (SLAB) で Out-of-Process なログ出力を試… - 銀の光と碧い空
z3 (smtソルバ) で遊ぶ - Qiita
いくつかの発表論文のファイル - 東京工業大学 情報理工学研究科 数理・計算科学専攻 佐々研究室





目次

型
前回、型は「先人の知恵を参考に Datatypes にエンコードしています」としていましたが、だいぶ端折っており、いくつか問題がありました。特に、以下のものは今後のプロトタイピングを進めていく上ですぐ問題になりそうです。解決しておきたいですね：


Null 値を Int32 型一次元配列専用のものとしてエンコードしていた
Z3 に無い null を表すために導入した Null 値ですが、C# のように「null はどんな object 型とも比較可能である」といった特別扱いはもちろんされません。例えば、以下のようなコードは、定数があいまいという旨のエラーになります：
(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
(declare-datatypes () ((Fuga null (Fuga (pointer Int) (value Int)))))
(declare-const a SystemInt32Array)
(assert (= a null)) ; ambiguous constant reference,
; more than one constant with the same sort,
; use a qualified expression (as <symbol> <sort>) to disumbiguate null
(check-sat)
view raw -1180194706-01.lisp hosted with ❤ by GitHub

エラー メッセージにある通り、どのソートの Null 値なのかを明示的に指定する必要があります：
(declare-datatypes () ((SystemInt32Array null (SystemInt32Array (pointer Int) (value (Seq Int))))))
(declare-datatypes () ((Fuga null (Fuga (pointer Int) (value Int)))))
(declare-const a SystemInt32Array)
(assert (= a (as null SystemInt32Array))) ; OK!
(check-sat)
view raw -1180194706-02.lisp hosted with ❤ by GitHub


Int32 型を、Int ソートとしてエンコードしていた
これが問題になるのは、ボックス化やボックス化解除が発生する場合です。以下の、どうということはない C# のコードを考えてみましょう：
class InstanceInspection
{
public static void Puzzle(object v)
{
if (v is int)
throw new Exception("instance inspection!");
}
}
view raw -1180194706-03.cs hosted with ❤ by GitHub

Int32 型の値がボックス化されて渡ってきた場合はアウト、それ以外の場合はセーフという処理です。SSA 形式にするところまでは順調に変換できるのですが・・・
IL_0000: temp1 = arg_0
IL_0001: temp2 = isinst [mscorlib]System.Int32 (temp1)
IL_0006: brfalse.s IL_0013 (temp2)
IL_0008: temp3 = ldstr \"instance inspection!\"
IL_000d: temp4 = newobj instance void [mscorlib]System.Exception::.ctor(string) (temp3)
IL_0012: throw(temp4)
IL_0013: ret
view raw -1180194706-04.ssa hosted with ❤ by GitHub

そこから SMT-LIB 標準形式に変換しようとしても、以下のように isinst の制約が書けません：
(declare-datatypes () ((Object null (Object (pointer Int)))))
(declare-const arg_0 Object)
(declare-const temp1 Object)
(declare-const temp2 Int)
(assert (= temp1 arg_0))
(assert ???) ; isinst は、temp1 と temp2 の間の制約になるはずなのに、Object と Int の間に共通項は無いゾイ？？？
view raw -1180194706-05.lisp hosted with ❤ by GitHub

temp1 と temp2 は何らかの関係があるはずですが、Object 型の値と Int ソートの値には共通項が無いため、制約が掛けられないのですね。

これを回避するには、.NET の型全てに、ポインタと型を付与するようなルールにします。そして、同じインスタンスを指している（isinst の結果がヌルポにならない）ならば、それらが等しいことを制約にします。そうすると、先ほどの例は、以下のようにエンコードできるようになります：
(declare-datatypes () ((Type (Type (pointer Int)))))
(declare-datatypes () ((Object null (Object (pointer Int) (type Type)))))
(declare-datatypes () ((Int32 (Int32 (pointer Int) (type Type) (value Int)))))
(push)
(echo "1: ")
(declare-const arg_0 Object)
(declare-const temp1 Object)
(declare-const temp2 Int32)
(assert (= temp1 arg_0))
(assert (=> (not (= (pointer temp2) 0))
(and (not (= temp1 (as null Object))) (= (pointer temp2) (pointer temp1)) (= (type temp2) (type temp1)))))
(assert (= (pointer temp2) 0))
(check-sat)
(get-model)
(pop)
(push)
(echo "2: ")
(declare-const arg_0 Object)
(declare-const temp1 Object)
(declare-const temp2 Int32)
(assert (= temp1 arg_0))
(assert (=> (not (= (pointer temp2) 0))
(and (not (= temp1 (as null Object))) (= (pointer temp2) (pointer temp1)) (= (type temp2) (type temp1)))))
(assert (not (= (pointer temp2) 0)))
(check-sat)
(get-model)
(pop)
; Result ---
; 1:
; sat
; (model
; (define-fun temp2 () Int32
; (Int32 0 (Type 1) 2))
; (define-fun arg_0 () Object
; null)
; (define-fun temp1 () Object
; null)
; )
; 2:
; sat
; (model
; (define-fun arg_0 () Object
; (Object 3 (Type 1)))
; (define-fun temp2 () Int32
; (Int32 3 (Type 1) 2))
; (define-fun temp1 () Object
; (Object 3 (Type 1)))
; )
view raw -1180194706-06.lisp hosted with ❤ by GitHub

オンラインの REPL で実行した結果はこちら。結果を見ますと、確かに null と 2: Int32 にデコード可能なモデルが出力されています！

話は逸れますが、ここで使っている "(=> P Q)"（論理包含、P ならば Q）、個人的にはどうも好きになれないです (-_-;)
「P が偽ならば、Q の真偽にかかわらず『P ならば Q』は真」っていう定義が直感的に受け入れにくいからでしょうか（業務システムの仕様決めとかに使ってしまうとトラブルの種になること請け合い）。論理計算的には、"(or (not P) Q)" と等しいため、認識のずれをなくすにはそう書いたほうが良いのかもしれませんね。

閑話休題。あとは、「配列の宣言は、型パラメータを取る定義部と分け、実体は新しいソートとして定義するとデバッグしやすくなる」とか「長さや要素への制約は対象の配列が null でない時だけ有効にして演算を効率化すべき」とかの細かな改善を行いました。最終的なアルゴリズムで型変換を行った場合、例えば前回の "!(v == null) && v.Length > 0 && v[0] == 1234567890" を表す制約は以下のようになります：
改善前
(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)
view raw -1180194706-07.lisp hosted with ❤ by GitHub

改善後
(echo "#3. !(v == null) && v.Length > 0 && v[0] == 1234567890 ------")
(declare-datatypes () ((Type (Type (pointer Int)))))
(declare-datatypes () ((Int32 (Int32 (pointer Int) (type Type) (value Int)))))
(declare-datatypes (T) ((ArrayType null (ArrayType (pointer Int) (type Type) (value (Seq T))))))
(define-sort Int32Array () (ArrayType Int32))
(declare-const v Int32Array)
(declare-const length Int32)
(declare-const element Int32)
(declare-const value_1234567890 Int32)
(assert (not (= v (as null (ArrayType Int32)))))
(assert (= (value length) 0))
(assert (not (< (value length) 0)))
(assert (not (=> (not (= v (as null (ArrayType Int32)))) (<= (seq.len (value v)) (value length)))))
(assert (=> (not (= v (as null (ArrayType Int32)))) (= (seq.unit element) (seq.at (value v) (value length)))))
(assert (= (value value_1234567890) 1234567890))
(assert (not (not (= element value_1234567890))))
(check-sat)
(get-model)
view raw -1180194706-08.lisp hosted with ❤ by GitHub

だいぶ汎用化できたのではないでしょうか。
ところで、型と言えば、大物のジェネリクス対応がまだ残っているのですが、これに関しては、難しいというのと、全体の設計に影響しそうな課題がまだプロトタイピングできていないというのがあるため、とりあえず後回しにしておきます。なあに、.NET も 1.1 → 2.0 で下位互換性保ったままジェネリクス導入できたのですから後からでも全然問題ないですよ！（小声）





副作用がないメソッド
.NET の型が SMT-LIB 標準形式として表現できるようになったところで、今度は .NET のメソッドをモデル化していきます。まずは簡単な副作用がないメソッド。単純な足し算処理なんかがわかりやすそうですね。C# で書いたサンプルはこんな感じ：
class ReferentialTransparent
{
public static void Puzzle(int v)
{
if (Add(v, 10) < 42)
throw new Exception("referential transparent!");
}
static int Add(int x, int y)
{
return x + y;
}
}
view raw -1180194706-09.cs hosted with ❤ by GitHub

引数として渡された数に 10 を足した値が 42 未満ならアウト、それ以外ならセーフっていうものです。つまり、全ての実行パスを通すパラメータとしては、32 未満の何某か 32 以上の何某の 2 つが欲しいということになります。早速変換してみましょう。SSA 形式にするとこう：
Puzzle メソッド
IL_0000: temp1 = ldarg.0
IL_0001: temp2 = ldc.i4.s 10
IL_0003: temp3 = call int32 HowDoesPexWork.ReferentialTransparent::Add(int32, int32) (temp1, temp2)
IL_0008: temp4 = ldc.i4.s 42
IL_000a: bge.s IL_0017 (temp3, temp4)
IL_000c: temp5 = ldstr \"referential transparent!\"
IL_0011: temp6 = newobj instance void [mscorlib]System.Exception::.ctor(string) (temp5)
IL_0016: throw(temp6)
IL_0017: ret
view raw -1180194706-10.ssa hosted with ❤ by GitHub

Add メソッド
IL_0000: temp1 = ldarg.0
IL_0001: temp2 = ldarg.1
IL_0002: temp3 = add(temp1, temp2)
IL_0003: ret(temp3)
view raw -1180194706-11.ssa hosted with ❤ by GitHub

そして SMT-LIB 標準形式に・・・と、このままではもちろん変換できません。うーん、どうしましょうか・・・。
ここも先人の知恵をお借りしたいところですが、「メソッド呼び出しの展開を行う」みたいにサラッと書いてあるだけで、具体例などは見つけることができませんでした。展開ねぇ・・・こうですか？
IL_0000: Puzzle_temp1 = Puzzle_ldarg.0
IL_0001: Puzzle_temp2 = ldc.i4.s 10
//IL_0003: Puzzle_temp3 = call int32 HowDoesPexWork.ReferentialTransparent::Add(int32, int32) (Puzzle_temp1, Puzzle_temp2)
IL_0003: IL_0000: Add_temp1 = Add_ldarg.0
IL_0003: IL_0001: Add_temp2 = Add_ldarg.1
IL_0003: IL_0002: Add_temp3 = add(Add_temp1, Add_temp2)
IL_0003: IL_0003: ret(Add_temp3)
IL_0008: Puzzle_temp4 = ldc.i4.s 42
IL_000a: bge.s IL_0017 (Puzzle_temp3, Puzzle_temp4)
IL_000c: Puzzle_temp5 = ldstr \"referential transparent!\"
IL_0011: Puzzle_temp6 = newobj instance void [mscorlib]System.Exception::.ctor(string) (Puzzle_temp5)
IL_0016: throw(Puzzle_temp6)
IL_0017: ret
view raw -1180194706-12.ssa hosted with ❤ by GitHub

使っている定数がどのメソッドのものなのかわからなくなるため、識別子を付けてみましたが・・・あれ？なんとなくそれっぽい感じです。あとは、これに引数と戻り値をつなぐグルー コードを足してやれば良いのでしょう、きっと：
IL_0000: Puzzle_temp1 = Puzzle_ldarg.0
IL_0001: Puzzle_temp2 = ldc.i4.s 10
//IL_0003: Puzzle_temp3 = call int32 HowDoesPexWork.ReferentialTransparent::Add(int32, int32) (Puzzle_temp1, Puzzle_temp2)
IL_0003: GC_0000: Add_ldarg.0 = Puzzle_temp1
IL_0003: GC_0000: Add_ldarg.1 = Puzzle_temp2
IL_0003: IL_0000: Add_temp1 = Add_ldarg.0
IL_0003: IL_0001: Add_temp2 = Add_ldarg.1
IL_0003: IL_0002: Add_temp3 = add(Add_temp1, Add_temp2)
IL_0003: IL_0003: ret(Add_temp3)
IL_0003: GC_0003: Puzzle_temp3 = Add_temp3
IL_0008: Puzzle_temp4 = ldc.i4.s 42
IL_000a: bge.s IL_0017 (Puzzle_temp3, Puzzle_temp4)
IL_000c: Puzzle_temp5 = ldstr \"referential transparent!\"
IL_0011: Puzzle_temp6 = newobj instance void [mscorlib]System.Exception::.ctor(string) (Puzzle_temp5)
IL_0016: throw(Puzzle_temp6)
IL_0017: ret
view raw -1180194706-13.ssa hosted with ❤ by GitHub

"GC_0000: Add_ldarg.0 = Puzzle_temp1" 等の、"GC_" で始まるラベルが付いているのがグルー コードです。
ここまで来れば SMT-LIB 標準形式に変換できますね！結果はこうなります：
(declare-datatypes () ((Type (Type (pointer Int)))))
(declare-datatypes () ((Int32 (Int32 (pointer Int) (type Type) (value Int)))))
(push)
(echo "1: ")
(declare-const Puzzle_ldarg_0 Int32)
(declare-const Puzzle_temp1 Int32)
(declare-const Puzzle_temp2 Int32)
(declare-const Puzzle_temp3 Int32)
(declare-const Puzzle_temp4 Int32)
(assert (= Puzzle_temp1 Puzzle_ldarg_0))
(assert (= (value Puzzle_temp2) 10))
(declare-const Add_ldarg_0 Int32)
(declare-const Add_temp1 Int32)
(declare-const Add_ldarg_1 Int32)
(declare-const Add_temp2 Int32)
(declare-const Add_temp3 Int32)
(assert (= Add_ldarg_0 Puzzle_temp1))
(assert (= Add_ldarg_1 Puzzle_temp2))
(assert (= Add_temp1 Add_ldarg_0))
(assert (= Add_temp2 Add_ldarg_1))
(assert (= (value Add_temp3) (+ (value Add_temp1) (value Add_temp2))))
(assert (= Puzzle_temp3 Add_temp3))
(assert (= (value Puzzle_temp4) 42))
(assert (not (>= (value Puzzle_temp3) (value Puzzle_temp4))))
(check-sat)
(get-model)
(pop)
(push)
(echo "2: ")
(declare-const Puzzle_ldarg_0 Int32)
(declare-const Puzzle_temp1 Int32)
(declare-const Puzzle_temp2 Int32)
(declare-const Puzzle_temp3 Int32)
(declare-const Puzzle_temp4 Int32)
(assert (= Puzzle_temp1 Puzzle_ldarg_0))
(assert (= (value Puzzle_temp2) 10))
(declare-const Add_ldarg_0 Int32)
(declare-const Add_temp1 Int32)
(declare-const y_4_1 Int32)
(declare-const Add_temp2 Int32)
(declare-const Add_temp3 Int32)
(assert (= Add_ldarg_0 Puzzle_temp1))
(assert (= y_4_1 Puzzle_temp2))
(assert (= Add_temp1 Add_ldarg_0))
(assert (= Add_temp2 y_4_1))
(assert (= (value Add_temp3) (+ (value Add_temp1) (value Add_temp2))))
(assert (= Puzzle_temp3 Add_temp3))
(assert (= (value Puzzle_temp4) 42))
(assert (>= (value Puzzle_temp3) (value Puzzle_temp4)))
(check-sat)
(get-model)
(pop)
; Result ---
; 1:
; sat
; (model
; (define-fun Puzzle_temp1 () Int32
; (Int32 6 (Type 5) (- 10)))
; (define-fun Add_ldarg_1 () Int32
; (Int32 2 (Type 1) 10))
; (define-fun Add_temp3 () Int32
; (Int32 4 (Type 3) 0))
; (define-fun Puzzle_temp2 () Int32
; (Int32 2 (Type 1) 10))
; (define-fun Add_temp2 () Int32
; (Int32 2 (Type 1) 10))
; (define-fun Puzzle_temp4 () Int32
; (Int32 11 (Type 9) 42))
; (define-fun Puzzle_ldarg_0 () Int32
; (Int32 6 (Type 5) (- 10)))
; (define-fun Add_ldarg_0 () Int32
; (Int32 6 (Type 5) (- 10)))
; (define-fun Puzzle_temp3 () Int32
; (Int32 4 (Type 3) 0))
; (define-fun Add_temp1 () Int32
; (Int32 6 (Type 5) (- 10)))
; )
; 2:
; sat
; (model
; (define-fun Puzzle_temp1 () Int32
; (Int32 4 (Type 3) 70))
; (define-fun Add_temp3 () Int32
; (Int32 6 (Type 5) 80))
; (define-fun Puzzle_temp2 () Int32
; (Int32 2 (Type 1) 10))
; (define-fun Add_temp2 () Int32
; (Int32 2 (Type 1) 10))
; (define-fun Puzzle_temp4 () Int32
; (Int32 9 (Type 8) 42))
; (define-fun Puzzle_ldarg_0 () Int32
; (Int32 4 (Type 3) 70))
; (define-fun Add_ldarg_0 () Int32
; (Int32 4 (Type 3) 70))
; (define-fun Puzzle_temp3 () Int32
; (Int32 6 (Type 5) 80))
; (define-fun y_4_1 () Int32
; (Int32 2 (Type 1) 10))
; (define-fun Add_temp1 () Int32
; (Int32 4 (Type 3) 70))
; )
view raw -1180194706-14.lisp hosted with ❤ by GitHub

結果から "Puzzle_ldarg_0" を探すと・・・-10: Int32（＜32）と 70: Int32（≧32）です！良さそうですね。
ちなみに、呼び出す先のメソッドの中に分岐があった場合、それらも全て制約として生成しないと答えが出せません。このままだと組み合わせが爆発してしまうでしょうから、よく出てくるメソッドは Z3 のマクロとして予め定義しておくなどの対策が必要になりそうです。





副作用があるメソッド
メソッド呼び出しの展開を行い、引数と戻り値をつなぐグルー コードを足せば、副作用がないメソッドの呼び出しは解決できることがわかりました。ではフィールドを更新するような、副作用があるメソッドはどう表現すれば良いでしょう？例えばこんな C# コードです：
class StateRelationForStruct
{
public static void Puzzle(int v)
{
MyInteger integer = new MyInteger();
integer.Set(v);
if (integer.IsLessThanOrEqualTo(4))
throw new Exception("state relation!");
}
public struct MyInteger
{
int m_value;
public void Set(int value)
{
m_value = value;
}
public bool IsLessThanOrEqualTo(int value)
{
return m_value <= value;
}
}
}
view raw -1180194706-15.cs hosted with ❤ by GitHub

全ての実行パスを通すパラメータとしては、4 以下の何某と 4 より大きい何某の 2 つが欲しいところ。SSA 形式にするとこう：
Puzzle メソッド
IL_0000: temp1 = ldloca.s 0
IL_0002: initobj HowDoesPexWork.StateRelationForStruct/MyInteger (temp1)
IL_0008: temp2 = ldloca.s 0
IL_000a: temp3 = ldarg.0
IL_000b: call instance void HowDoesPexWork.StateRelationForStruct/MyInteger::Set(int32) (temp2, temp3)
IL_0010: temp4 = ldloca.s 0
IL_0012: temp5 = ldc.i4.4
IL_0013: temp6 = call instance bool HowDoesPexWork.StateRelationForStruct/MyInteger::IsLessThanOrEqualTo(int32) (temp4, temp5)
IL_0018: brfalse.s IL_0025 (temp6)
IL_001a: temp7 = ldstr \"state relation!\"
IL_001f: temp8 = newobj instance void [mscorlib]System.Exception::.ctor(string) (temp7)
IL_0024: throw(temp8)
IL_0025: ret
view raw -1180194706-16.ssa hosted with ❤ by GitHub

Set メソッド
IL_0000: temp1 = ldarg.0
IL_0001: temp2 = ldarg.1
IL_0002: stfld int32 HowDoesPexWork.StateRelationForStruct/MyInteger::m_value (temp1, temp2)
IL_0007: ret
view raw -1180194706-17.ssa hosted with ❤ by GitHub

IsLessThanOrEqualTo メソッド
IL_0000: temp1 = ldarg.0
IL_0001: temp2 = ldfld int32 HowDoesPexWork.StateRelationForStruct/MyInteger::m_value (temp1)
IL_0006: temp3 = ldarg.1
IL_0007: temp4 = cgt(temp2, temp3)
IL_0009: temp5 = ldc.i4.0
IL_000a: temp6 = ceq(temp4, temp5)
IL_000c: ret(temp6)
view raw -1180194706-18.ssa hosted with ❤ by GitHub

展開して、グルー コードを足せば・・・？
IL_0000: Puzzle_temp1 = Puzzle_ldloca.s 0
IL_0002: initobj HowDoesPexWork.StateRelationForStruct/MyInteger (Puzzle_temp1)
IL_0008: Puzzle_temp2 = Puzzle_ldloca.s 0
IL_000a: Puzzle_temp3 = Puzzle_ldarg.0
// IL_000b: call instance void HowDoesPexWork.StateRelationForStruct/MyInteger::Set(int32) (Puzzle_temp2, Puzzle_temp3)
IL_000b: GC_0000: Set_ldarg.0 = Puzzle_temp2
IL_000b: GC_0000: Set_ldarg.1 = Puzzle_temp3
IL_000b: IL_0000: Set_temp1 = Set_ldarg.0
IL_000b: IL_0001: Set_temp2 = Set_ldarg.1
IL_000b: IL_0002: stfld int32 HowDoesPexWork.StateRelationForStruct/MyInteger::m_value (Set_temp1, Set_temp2)
IL_000b: IL_0007: ret
IL_0010: Puzzle_temp4 = Puzzle_ldloca.s 0 // ▂▅▇█▓▒░('ω')░▒▓█▇▅▂
IL_0012: Puzzle_temp5 = ldc.i4.4
// IL_0013: Puzzle_temp6 = call instance bool HowDoesPexWork.StateRelationForStruct/MyInteger::IsLessThanOrEqualTo(int32) (Puzzle_temp4, Puzzle_temp5)
IL_0013: GC_0000: IsLessThanOrEqualTo_ldarg.0 = Puzzle_temp4
IL_0013: GC_0000: IsLessThanOrEqualTo_ldarg.1 = Puzzle_temp5
IL_0013: IL_0000: IsLessThanOrEqualTo_temp1 = IsLessThanOrEqualTo_ldarg.0
IL_0013: IL_0001: IsLessThanOrEqualTo_temp2 = ldfld int32 HowDoesPexWork.StateRelationForStruct/MyInteger::m_value (IsLessThanOrEqualTo_temp1)
IL_0013: IL_0006: IsLessThanOrEqualTo_temp3 = IsLessThanOrEqualTo_ldarg.1
IL_0013: IL_0007: IsLessThanOrEqualTo_temp4 = cgt(IsLessThanOrEqualTo_temp2, IsLessThanOrEqualTo_temp3)
IL_0013: IL_0009: IsLessThanOrEqualTo_temp5 = ldc.i4.0
IL_0013: IL_000a: IsLessThanOrEqualTo_temp6 = ceq(IsLessThanOrEqualTo_temp4, IsLessThanOrEqualTo_temp5)
IL_0013: IL_000c: ret(IsLessThanOrEqualTo_temp6)
IL_0013: GC_000c: Puzzle_temp6 = IsLessThanOrEqualTo_temp6
IL_0018: brfalse.s IL_0025 (Puzzle_temp6)
IL_001a: Puzzle_temp7 = ldstr \"state relation!\"
IL_001f: Puzzle_temp8 = newobj instance void [mscorlib]System.Exception::.ctor(string) (Puzzle_temp7)
IL_0024: throw(Puzzle_temp8)
IL_0025: ret
view raw -1180194706-19.ssa hosted with ❤ by GitHub

ダメみたいですね。。。
"IL_0000: Puzzle_temp1 = Puzzle_ldloca.s 0" と "IL_0008: Puzzle_temp2 = Puzzle_ldloca.s 0" は問題なく制約を組むことができるのですが、"IL_0010: Puzzle_temp4 = Puzzle_ldloca.s 0" を同じように組むとおかしなことになってしまいます（Set メソッドの中で this の値が変わっているため、"Puzzle_ldloca.s 0" が別モノになっている）。

副作用をどう扱うかは先人の知恵にもなかったため、イチから考える必要がありました。今回採った方針は以下のようなものです：
  1. SMT-LIB 標準形式に変換時、現在処理中のコンテキストにアクセスできるようにする。
  2. ストア系（メソッド呼び出し含む）の命令で、現在処理中のコンテキストに、呼び出し階層命令のオフセット、ストア対象とスタック変数の紐付けを保存する（※ここで言う「スタック変数」は、SSA 形式に現れる tempX という形の一時変数のこと）。
  3. ロード系の命令で、自分より呼び出し階層が深い命令のオフセットが前の場所でロード対象がスタック変数に紐付けられていないかを、現在処理中のコンテキストに問い合わせる。なお、同じ 1 つ目のローカル変数でも、現在解析中のメソッドとは別のインスタンス メソッドの呼び出しにより、内部で stfld されて状態が変わっていることがある。従って、検索処理は、以下の通り再帰的に紐付きを検索しなければならない：
    1. ローカル変数と紐付いているスタック変数を検索する。
    2. スタック変数に紐付いているインスタンス変数を検索する。
【2017/01/07 修正】ローカル変数へのストアも副作用ですので、呼び出し階層ではなく、命令のオフセットの前後関係で変数紐付けと辿らないとダメでしたね。失礼しました m(_ _)m【2017/01/07 修正】
これに沿って処理の進み方を見ていくと、以下のような動きになります：
  1. "IL_0000: Puzzle_temp1 = Puzzle_ldloca.s 0" で変数の紐付きを検索する（ロード系の命令）
    ⇒対象なしのためそのまま
  2. "IL_0008: Puzzle_temp2 = Puzzle_ldloca.s 0" で変数の紐付きを検索する（ロード系の命令）
    ⇒対象なしのためそのまま
  3. "IL_000a: Puzzle_temp3 = Puzzle_ldarg.0" で変数の紐付きを検索する（ロード系の命令）
    ⇒対象なしのためそのまま
  4. "IL_000b: GC_0000: Set_ldarg.0 = Puzzle_temp2" で変数の紐付きを保存する（メソッド呼び出し）
  5. "IL_000b: GC_0000: Set_ldarg.1 = Puzzle_temp3" で変数の紐付きを保存する（メソッド呼び出し）
  6. "IL_000b: IL_0000: Set_temp1 = Set_ldarg.0" で変数の紐付きを検索する（ロード系の命令）
    ⇒対象なしのためそのまま
  7. "IL_000b: IL_0001: Set_temp2 = Set_ldarg.1" で変数の紐付きを検索する（ロード系の命令）
    ⇒対象なしのためそのまま
  8. "IL_000b: IL_0002: stfld int32 HowDoesPexWork.StateRelationForStruct/MyInteger::m_value (Set_temp1, Set_temp2)" で変数の紐付きを保存する（ストア系の命令）
  9. "IL_0010: Puzzle_temp4 = Puzzle_ldloca.s 0" で変数の紐付きを検索する（ロード系の命令）
    ⇒8. で保存した変数が見つかる
    ⇒値変更後の this を見るよう制約を書き換え（"Set_ldarg.0_new" のような感じに）
SMT-LIB 標準形式だとこんな感じに（長いので 1 パス側だけ、完全版はこちらに）：
(declare-datatypes () ((Type (Type (pointer Int)))))
(declare-datatypes () ((Int32 (Int32 (pointer Int) (type Type) (value Int)))))
(declare-datatypes () ((StateRelationForStructMyInteger null (StateRelationForStructMyInteger (pointer Int) (type Type) (m_value Int32)))))
(push)
(echo "1: ")
(declare-const Puzzle_ldloca_s_0 StateRelationForStructMyInteger)
(declare-const Puzzle_temp1 StateRelationForStructMyInteger)
(declare-const Puzzle_temp2 StateRelationForStructMyInteger)
(declare-const Puzzle_ldarg_0 Int32)
(declare-const Puzzle_temp3 Int32)
(declare-const Puzzle_temp4 StateRelationForStructMyInteger)
(declare-const Puzzle_temp5 Int32)
(declare-datatypes () ((Boolean (Boolean (pointer Int) (type Type) (value Bool)))))
(declare-const Puzzle_temp6 Boolean)
(assert (= Puzzle_temp1 Puzzle_ldloca_s_0))
(assert (= Puzzle_temp1 (StateRelationForStructMyInteger 3 (Type 3) (Int32 3 (Type 2) 0))))
(assert (= Puzzle_temp2 Puzzle_ldloca_s_0))
(assert (= Puzzle_temp3 Puzzle_ldarg_0))
(declare-const Set_ldarg_0 StateRelationForStructMyInteger)
(declare-const Set_temp1 StateRelationForStructMyInteger)
(declare-const Set_ldarg_1 Int32)
(declare-const Set_temp2 Int32)
(declare-const Set_ldarg_0_new StateRelationForStructMyInteger)
(assert (= Set_ldarg_0 Puzzle_temp2))
(assert (= Set_ldarg_1 Puzzle_temp3))
(assert (= Set_temp1 Set_ldarg_0))
(assert (= Set_temp2 Set_ldarg_1))
(assert (= Set_ldarg_0_new (StateRelationForStructMyInteger (pointer Set_temp1) (type Set_temp1) Set_temp2)))
(assert (= Puzzle_temp4 Set_ldarg_0_new))
(assert (= (value Puzzle_temp5) 4))
(declare-const IsLessThanOrEqualTo_ldarg_0 StateRelationForStructMyInteger)
(declare-const IsLessThanOrEqualTo_temp1 StateRelationForStructMyInteger)
(declare-const this1_3_2 StateRelationForStructMyInteger)
(declare-const IsLessThanOrEqualTo_temp2 Int32)
(declare-const IsLessThanOrEqualTo_ldarg_1 Int32)
(declare-const IsLessThanOrEqualTo_temp3 Int32)
(declare-const IsLessThanOrEqualTo_temp4 Boolean)
(declare-const IsLessThanOrEqualTo_temp5 Int32)
(declare-const IsLessThanOrEqualTo_temp6 Boolean)
(assert (= IsLessThanOrEqualTo_ldarg_0 Puzzle_temp4))
(assert (= IsLessThanOrEqualTo_ldarg_1 Puzzle_temp5))
(assert (= IsLessThanOrEqualTo_temp1 IsLessThanOrEqualTo_ldarg_0))
(assert (= IsLessThanOrEqualTo_temp2 (m_value IsLessThanOrEqualTo_temp1)))
(assert (= IsLessThanOrEqualTo_temp3 IsLessThanOrEqualTo_ldarg_1))
(assert (= (value IsLessThanOrEqualTo_temp4) (> (value IsLessThanOrEqualTo_temp2) (value IsLessThanOrEqualTo_temp3))))
(assert (= (value IsLessThanOrEqualTo_temp5) 0))
(assert (= (value IsLessThanOrEqualTo_temp6) (= IsLessThanOrEqualTo_temp4 (ite (= (value IsLessThanOrEqualTo_temp5) 0) (Boolean 11 (Type 0) false) (Boolean 12 (Type 0) true)))))
(assert (= Puzzle_temp6 IsLessThanOrEqualTo_temp6))
(assert (not (= (value Puzzle_temp6) false)))
(check-sat)
(get-model)
(pop)
; Result ---
; 1:
; sat
; (model
; (define-fun Puzzle_ldloca_s_0 () StateRelationForStructMyInteger
; (StateRelationForStructMyInteger 3 (Type 3) (Int32 3 (Type 2) 0)))
; (define-fun IsLessThanOrEqualTo_temp1 () StateRelationForStructMyInteger
; (StateRelationForStructMyInteger 3 (Type 3) (Int32 9 (Type 8) (- 34))))
; (define-fun Puzzle_temp5 () Int32
; (Int32 5 (Type 1) 4))
; (define-fun IsLessThanOrEqualTo_temp6 () Boolean
; (Boolean 13 (Type 12) true))
; (define-fun Set_temp2 () Int32
; (Int32 9 (Type 8) (- 34)))
; (define-fun IsLessThanOrEqualTo_temp2 () Int32
; (Int32 9 (Type 8) (- 34)))
; (define-fun Puzzle_ldarg_0 () Int32
; (Int32 9 (Type 8) (- 34)))
; (define-fun Set_temp1 () StateRelationForStructMyInteger
; (StateRelationForStructMyInteger 3 (Type 3) (Int32 3 (Type 2) 0)))
; (define-fun Set_ldarg_0 () StateRelationForStructMyInteger
; (StateRelationForStructMyInteger 3 (Type 3) (Int32 3 (Type 2) 0)))
; (define-fun Puzzle_temp6 () Boolean
; (Boolean 13 (Type 12) true))
; (define-fun Puzzle_temp3 () Int32
; (Int32 9 (Type 8) (- 34)))
; (define-fun Puzzle_temp1 () StateRelationForStructMyInteger
; (StateRelationForStructMyInteger 3 (Type 3) (Int32 3 (Type 2) 0)))
; (define-fun IsLessThanOrEqualTo_ldarg_0 () StateRelationForStructMyInteger
; (StateRelationForStructMyInteger 3 (Type 3) (Int32 9 (Type 8) (- 34))))
; (define-fun IsLessThanOrEqualTo_ldarg_1 () Int32
; (Int32 5 (Type 1) 4))
; (define-fun IsLessThanOrEqualTo_temp3 () Int32
; (Int32 5 (Type 1) 4))
; (define-fun IsLessThanOrEqualTo_temp4 () Boolean
; (Boolean 11 (Type 0) false))
; (define-fun Set_ldarg_0_new () StateRelationForStructMyInteger
; (StateRelationForStructMyInteger 3 (Type 3) (Int32 9 (Type 8) (- 34))))
; (define-fun Puzzle_temp2 () StateRelationForStructMyInteger
; (StateRelationForStructMyInteger 3 (Type 3) (Int32 3 (Type 2) 0)))
; (define-fun Puzzle_temp4 () StateRelationForStructMyInteger
; (StateRelationForStructMyInteger 3 (Type 3) (Int32 9 (Type 8) (- 34))))
; (define-fun IsLessThanOrEqualTo_temp5 () Int32
; (Int32 7 (Type 6) 0))
; (define-fun Set_ldarg_1 () Int32
; (Int32 9 (Type 8) (- 34)))
; )
view raw -1180194706-20.lisp hosted with ❤ by GitHub

"Puzzle_ldarg_0" として出力されている値は・・・-34: Int32（≦4）と 5: Int32（＞4）です！やったぜ！

なおこの方法、ライブラリの力を借りず SSA 形式の生成ちっくなことをやっていることになるので、正直かなりシンドイ処理になっています（コードで言うと、起点は SmtLibStringContext の RetrieveAssignmentRelation や UpdateAssignmentRelation 辺り。半年後に見て思い出せるか・・・）。
Roslyn 時代になっても、この辺りのフロー解析機能が搭載される予定は今のところないのが辛いところ。何か良いライブラリをご存じの方がいらっしゃれば、是非 @urasandesu にリプいただきたいところです。





終わりに
2 つ目のプロトタイピング成功にてすでに語彙力が失われてきています・・・まあ、この時は「クリスマス」が「苦理済ます」になってしまうかどうかの瀬戸際でしたので、今後はもう少し冷静に成功をご報告できればと思いますが、しかし複雑な問題が解けた時の嬉しさたるや・・・。

いや、処理は複雑になってきてはいるのですが、実装に関して言えば、DDD に沿っているおかげで、そこまで苦も無く変更できています。やはり難しいのは、論文に書いてあることを C# へ落とし込むプロセスでしょう。

これは、アカデミックな世界では、中間言語を介して行う静的解析手法を、Java で示す場合が多いからかな？と、個人的には感じています。

そこには、構造体や null 合体演算子、as 演算、checked/unchecked、相互運用のための unsafe コードの考慮なんてものはありません。型のセクションでも今後の懸念として挙げましたが、特に大きいと感じるのはジェネリクスの違い。Java では、バイト コード上、型消去が行われるため、考慮しなくて良いのです。これが .NET だと「ジェネリクスのない世界では、すべてが上手く行き、みんな幸せです。」と言われるほど複雑に。.NET が使われているのをあまり見ないのは、これまでの MS の戦略のせいだけではないのでしょう。
ただ、業務で使われるようなある程度信頼性が必要なシステムを動かすことが多いであろうデスクトップ PC で、まだまだ Windows のシェアが高いことを鑑みると、その機能をフルに扱える .NET でもこういった解決手法が適用できるようになるのは、何かしらの価値にはなりそう。そんなモチベーションで、ボチボチやっていければと思います。

さて、次回は外部環境への依存やループの解釈についてですかね。俺達の旅はまだ始まったばかりだ！（@urasandesu の次回作にご期待ください）

投稿者 時刻: 0 件のコメント:
登録: 投稿 (Atom)