C# で作られた既存のシステムを改修する際、安全のため、現在の仕様を自動化された単体テストで囲ってから手を加えるっていうのはよくやるんですが、全ての振る舞いを通すよう、パラメータのバリエーションを考えるのは結構大変だったりします。フロー解析したい。フロー解析したくない？
— Akira Sugiura (@urasandesu) September 29, 2014
対象の機能が、時間が無かったなどの理由で急いで作ったのであれば、整理されていない幾重にもなる && や || が条件分岐として立ちはだかることも少なくなく、心が折れること必至。かと言って、「うーん、あっちがそっちで、ここがこうで……まあいっか！」などと勢いに任せてやってしまえば、さらなる複雑化や不具合の混入を招くこと必至です。冒頭のつぶやきのように、「コンピュータが、うまいこと処理の流れ解析してくれて、全てのパス通すパラメータのバリエーション作ってくれないもんかなー」と誰しもが思い始めるでしょう。
こんな時、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
目次
やりたいこと
Pex for fun で解説されているサンプルそのもので恐縮ですが、対象のプログラムとして、以下のようなものを考えてみます：
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)）
- null
- new int[0]
- new[] { 1234567890 }
- new[] { 1234567890 以外の整数 }
対象のプログラムのメソッド定義情報を取得し（methDef）、それを①の機能（Fay.GetInterestingInputs）に与えると、各実行パス向けの引数のバリエーションを全て求めてくれる寸法です。メソッド定義情報の取得については、後述のライブラリの仕様の関係で Mono.Cecil を使っていますが、こちらはすでに色々なところで紹介されていると思いますので、ここでは特に解説はしません。①の実現方法についてのみ考えていきたいと思います。
Z3
Pex はどうやって値のバリエーションを生成していたの？と調べ始めると、すぐ Z3 という定理証明器を使っていることがわかります。当初はテイリショウメイキ？なにそれ？おいしいの？という感じでしたが、ライブラリの公式ガイドを見る限り、今回のような用途で使う分にはそこまで難しいことはありませんでした。要は「与えた制約を全て満たす解を求めてくれる」ものです。ムズカシイ言葉だと「充足可能性を調べる」と言うそうですが、今のところ「連立方程式みたいなのが解けるのかー」ぐらいの理解デ大丈夫デス（棒読み）。
制約に当たる部分はもうありますね（上記 4 パターン）。Z3 が解釈できる SMT-LIB 標準形式 で書き下してみましょう（Z3 は v2.0 を大体サポート、v2.5 は実装中）：
Web 上の REPL で動かした結果はこちら。.NET のクラスは、先人の知恵を参考に Datatypes にエンコードしています。配列のような、長さと要素を持つものは、シーケンスにエンコードすると扱いやすかったですね（Z3 にも配列があるが、無限長なので長さに対する制約が書きにくい）。
さて、結果を確認すると、
- null
- new int[0]
- new[] { 1234567890 }
- new[] { 5 }
Flow Analysis
各実行パス向けの制約を求めるには、IL の並びから処理の流れを解析する必要があります。この辺りも、調べるとすぐ ILSpy がそういう機能を持っている風の情報が見つかりますので、ありがたく使わせていただきましょう。ちなみに、ILSpy は、エンジン部分が分離されて Nupkg 化されていますので、今回のように UI を必要とせず、ライブラリとして使いたい場合は、こちらを使うと何かと捗ります。
中を見ると、その名もズバリ FlowAnalysis っていう名前空間がありますので、迷うことはないと思います。エントリー ポイントは SsaFormBuilder。SSA 形式もこの時はまだ？？？だったのですが、@linerlock さんから静的単一代入形式なるものだということを教えていただけました。静的単一代入形式にしておくことで、同じ変数に値が代入されるようなコードが書かれていたとしても、無理なく制約にエンコードできるようになります。
SsaFormBuilder から出力される SsaForm には、自身を dot 言語に変換可能な機能があります。処理の流れを確認するには、以下のようなコードでこの情報を出力し・・・（※Mono.Cecil を使ったのは、ここの機能が依存していたからでした）：
Graphviz を使ってグラフ化するとわかりやすいでしょう：
これを眺めると、SSA 形式上の変数（tempXX）に値が割り当てられる度に制約を積み、ブランチ命令や例外を発生させる命令毎にそれらをグルーピングすることさえできれば、各実行パスを通す全ての条件を考慮できそうですね！
実装
ここまでで、処理は、大きく分けて 2 つのことを行えば良さそうなことがわかってきました：
- SMT-LIB 標準形式へのエンコード
対象メソッド定義情報→SSA 形式→SMT-LIB 標準形式へと順にエンコード。SSA 形式→SMT-LIB 標準形式は、SSA 形式上の変数に値が割り当てられる度に制約を積み、ブランチ命令や例外を発生させる命令毎にそれらをグルーピングする。 - 関心がある入力値の検索
各実行パス向けの制約の SMT-LIB 標準形式を Z3 に与え、各々を満たす解を取得する。取得した解を解析し、.NET のオブジェクトにデコードする。
- brfalse.s や ble.s、bne.un_s といったブランチ命令は、「条件を満たしブランチするパターン」と「条件を満たさずそのまま進むパターン」の制約を積む。
- ldlen や ldelem.i4 といった例外を発生させる可能性がある命令も同様、「条件を満たし例外を発生させるパターン」と「条件を満たさずそのまま進むパターン」の制約を積む。
ブランチ命令と異なるのは、例外は、1 つの命令で複数のものが発生する可能性があること。例えば、ldelem.i4 は「必要とするオブジェクト参照が null のパターン」「そのオブジェクト参照とされた配列の型が違うパターン」「インデックスが配列の範囲外（負の方向）のパターン」「インデックスが配列の範囲外（正の方向）のパターン」の計 4 パターンが発生する可能性があることに注意し、全てのパターンの制約を積むようにする。 - それ以外は、SSA 形式上の変数に値が割り当てられる毎に制約を積んで行く。
各グループの #(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 を使ったものがないため、ちょっと怪しいかも…）：
ポイントは Expr オブジェクト。構造は単純で、基本的に名前や戻り値のソート（型のこと）を示す関数情報と引数になる Expr オブジェクトのコレクションを持つツリー構造になっています。整数や文字列に直接デコードできるものは、これに加えて実際値が取得できます。
最終的に .NET オブジェクトが欲しいので、この Expr オブジェクトを走査し、.NET オブジェクトにデコードする必要があります（よくある Visitor パターンでのデータ収集になると思います）。SMT-LIB 標準形式は、元々そんな複雑な仕様ではないので、ここはそこまで悩まずに実装できるでしょう。
終わりに
Pex やそのコア ライブラリである Z3 は、これまでもちょいちょい勉強を進めていたのですが、Prig のほうがだいぶ落ち着いたのと、久々に GW に長期休暇が取れたこともあって、やっとがっつり手を付けられたかなーと思います。それにしても、やはり全然やったことのない分野のライブラリは、難しい分、動くようになったときの感動もひとしおですね。
まあ、現状ハード コーディングごりごりの試作なので、今後、Z3 に標準で用意されていない型はどう Datatypes にエンコードするのー？とか、メソッドの呼び出しはどうするのー？とか、呼び出せたとしても再帰してたり、ネットワークやファイル システムとかの外部環境に依存してたらどうなるのー？とか、ループはどう解釈するのー？とか、isinst みたいな継承階層チェックする命令はどう制約として表現するのー？とか、参照の比較はどうするのー？とか、解決していくべき課題は多いのですが、ボチボチやっていけたらと思います。うっほ！Z3使ってフルパスカバレッジ通すメソッド引数バリエーション求めるの、1パス ｷﾀ━━━━(ﾟ∀ﾟ)━━━━!!!!!!! pic.twitter.com/N99Q8p52dj
— Akira Sugiura (@urasandesu) July 13, 2016
最後になりましたが、新しいライブラリを作るに当たり、名前のアイデア出しを協力してくださった職場の皆さん、この場を借りてお礼させていただければと思います。ありがとうございました！！
「Fayle」は Fay（妖精）+ le（道具を表す接尾語）の造語。TDD の黄金の回転の始まりである Red、つまり Fail の捩りにもなっています。いつの日か、テスト作りは妖精さんにお願い！とか言えちゃうような日が来ることを夢見て。俺たちの戦いはこれからだ！（迫真）
0 件のコメント:
コメントを投稿