今回説明した箇所の全体像については、前回同様 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 型とも比較可能である」といった特別扱いはもちろんされません。例えば、以下のようなコードは、定数があいまいという旨のエラーになります：
エラー メッセージにある通り、どのソートの Null 値なのかを明示的に指定する必要があります：
Int32 型を、Int ソートとしてエンコードしていた
これが問題になるのは、ボックス化やボックス化解除が発生する場合です。以下の、どうということはない C# のコードを考えてみましょう：
Int32 型の値がボックス化されて渡ってきた場合はアウト、それ以外の場合はセーフという処理です。SSA 形式にするところまでは順調に変換できるのですが・・・
そこから SMT-LIB 標準形式に変換しようとしても、以下のように isinst の制約が書けません：
temp1 と temp2 は何らかの関係があるはずですが、Object 型の値と Int ソートの値には共通項が無いため、制約が掛けられないのですね。
これを回避するには、.NET の型全てに、ポインタと型を付与するようなルールにします。そして、同じインスタンスを指している（isinst の結果がヌルポにならない）ならば、それらが等しいことを制約にします。そうすると、先ほどの例は、以下のようにエンコードできるようになります：
オンラインの 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" を表す制約は以下のようになります：
改善前
改善後
だいぶ汎用化できたのではないでしょうか。
ところで、型と言えば、大物のジェネリクス対応がまだ残っているのですが、これに関しては、難しいというのと、全体の設計に影響しそうな課題がまだプロトタイピングできていないというのがあるため、とりあえず後回しにしておきます。なあに、.NET も 1.1 → 2.0 で下位互換性保ったままジェネリクス導入できたのですから後からでも全然問題ないですよ！（小声）
副作用がないメソッド
.NET の型が SMT-LIB 標準形式として表現できるようになったところで、今度は .NET のメソッドをモデル化していきます。まずは簡単な副作用がないメソッド。単純な足し算処理なんかがわかりやすそうですね。C# で書いたサンプルはこんな感じ：
引数として渡された数に 10 を足した値が 42 未満ならアウト、それ以外ならセーフっていうものです。つまり、全ての実行パスを通すパラメータとしては、32 未満の何某か 32 以上の何某の 2 つが欲しいということになります。早速変換してみましょう。SSA 形式にするとこう：
Puzzle メソッド
Add メソッド
そして SMT-LIB 標準形式に・・・と、このままではもちろん変換できません。うーん、どうしましょうか・・・。
ここも先人の知恵をお借りしたいところですが、「メソッド呼び出しの展開を行う」みたいにサラッと書いてあるだけで、具体例などは見つけることができませんでした。展開ねぇ・・・こうですか？
使っている定数がどのメソッドのものなのかわからなくなるため、識別子を付けてみましたが・・・あれ？なんとなくそれっぽい感じです。あとは、これに引数と戻り値をつなぐグルー コードを足してやれば良いのでしょう、きっと：
"GC_0000: Add_ldarg.0 = Puzzle_temp1" 等の、"GC_" で始まるラベルが付いているのがグルー コードです。
ここまで来れば SMT-LIB 標準形式に変換できますね！結果はこうなります：
結果から "Puzzle_ldarg_0" を探すと・・・-10: Int32（＜32）と 70: Int32（≧32）です！良さそうですね。
ちなみに、呼び出す先のメソッドの中に分岐があった場合、それらも全て制約として生成しないと答えが出せません。このままだと組み合わせが爆発してしまうでしょうから、よく出てくるメソッドは Z3 のマクロとして予め定義しておくなどの対策が必要になりそうです。
副作用があるメソッド
メソッド呼び出しの展開を行い、引数と戻り値をつなぐグルー コードを足せば、副作用がないメソッドの呼び出しは解決できることがわかりました。ではフィールドを更新するような、副作用があるメソッドはどう表現すれば良いでしょう？例えばこんな C# コードです：
全ての実行パスを通すパラメータとしては、4 以下の何某と 4 より大きい何某の 2 つが欲しいところ。SSA 形式にするとこう：
Puzzle メソッド
Set メソッド
IsLessThanOrEqualTo メソッド
展開して、グルー コードを足せば・・・？
ダメみたいですね。。。thisなんて無くなればいい（ぐるぐる目）
— Akira Sugiura (@urasandesu) November 17, 2016
"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" が別モノになっている）。
副作用をどう扱うかは先人の知恵にもなかったため、イチから考える必要がありました。今回採った方針は以下のようなものです：
- SMT-LIB 標準形式に変換時、現在処理中のコンテキストにアクセスできるようにする。
- ストア系（メソッド呼び出し含む）の命令で、現在処理中のコンテキストに、
呼び出し階層命令のオフセット、ストア対象とスタック変数の紐付けを保存する（※ここで言う「スタック変数」は、SSA 形式に現れる tempX という形の一時変数のこと）。 - ロード系の命令で、自分より
呼び出し階層が深い命令のオフセットが前の場所でロード対象がスタック変数に紐付けられていないかを、現在処理中のコンテキストに問い合わせる。なお、同じ 1 つ目のローカル変数でも、現在解析中のメソッドとは別のインスタンス メソッドの呼び出しにより、内部で stfld されて状態が変わっていることがある。従って、検索処理は、以下の通り再帰的に紐付きを検索しなければならない：- ローカル変数と紐付いているスタック変数を検索する。
- スタック変数に紐付いているインスタンス変数を検索する。
これに沿って処理の進み方を見ていくと、以下のような動きになります：
- "IL_0000: Puzzle_temp1 = Puzzle_ldloca.s 0" で変数の紐付きを検索する（ロード系の命令）
⇒対象なしのためそのまま - "IL_0008: Puzzle_temp2 = Puzzle_ldloca.s 0" で変数の紐付きを検索する（ロード系の命令）
⇒対象なしのためそのまま - "IL_000a: Puzzle_temp3 = Puzzle_ldarg.0" で変数の紐付きを検索する（ロード系の命令）
⇒対象なしのためそのまま - "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_0010: Puzzle_temp4 = Puzzle_ldloca.s 0" で変数の紐付きを検索する（ロード系の命令）
⇒8. で保存した変数が見つかる
⇒値変更後の this を見るよう制約を書き換え（"Set_ldarg.0_new" のような感じに）
"Puzzle_ldarg_0" として出力されている値は・・・-34: Int32（≦4）と 5: Int32（＞4）です！やったぜ！
なおこの方法、ライブラリの力を借りず SSA 形式の生成ちっくなことをやっていることになるので、正直かなりシンドイ処理になっています（コードで言うと、起点は SmtLibStringContext の RetrieveAssignmentRelation や UpdateAssignmentRelation 辺り。半年後に見て思い出せるか・・・）。
Roslyn 時代になっても、この辺りのフロー解析機能が搭載される予定は今のところないのが辛いところ。何か良いライブラリをご存じの方がいらっしゃれば、是非 @urasandesu にリプいただきたいところです。
終わりに
2 つ目のプロトタイピング成功にてすでに語彙力が失われてきています・・・まあ、この時は「クリスマス」が「苦理済ます」になってしまうかどうかの瀬戸際でしたので、今後はもう少し冷静に成功をご報告できればと思いますが、しかし複雑な問題が解けた時の嬉しさたるや・・・。通ったア゜ーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーーー pic.twitter.com/1cG9LGWmQE
— Akira Sugiura (@urasandesu) December 25, 2016
いや、処理は複雑になってきてはいるのですが、実装に関して言えば、DDD に沿っているおかげで、そこまで苦も無く変更できています。やはり難しいのは、論文に書いてあることを C# へ落とし込むプロセスでしょう。
これは、アカデミックな世界では、中間言語を介して行う静的解析手法を、Java で示す場合が多いからかな？と、個人的には感じています。
そこには、構造体や null 合体演算子、as 演算、checked/unchecked、相互運用のための unsafe コードの考慮なんてものはありません。型のセクションでも今後の懸念として挙げましたが、特に大きいと感じるのはジェネリクスの違い。Java では、バイト コード上、型消去が行われるため、考慮しなくて良いのです。これが .NET だと「ジェネリクスのない世界では、すべてが上手く行き、みんな幸せです。」と言われるほど複雑に。.NET が使われているのをあまり見ないのは、これまでの MS の戦略のせいだけではないのでしょう。
ただ、業務で使われるようなある程度信頼性が必要なシステムを動かすことが多いであろうデスクトップ PC で、まだまだ Windows のシェアが高いことを鑑みると、その機能をフルに扱える .NET でもこういった解決手法が適用できるようになるのは、何かしらの価値にはなりそう。そんなモチベーションで、ボチボチやっていければと思います。
さて、次回は外部環境への依存やループの解釈についてですかね。俺達の旅はまだ始まったばかりだ！（@urasandesu の次回作にご期待ください）
