Z3でテストケースを生成してみる

こんにちは。株式会社 日立製作所 研究開発グループの曾我 遼です。
この記事では、日立グループ [OSS Advent Calendar 2020](https://qiita.com/advent-calendar/2020/hitachi-oss) の22日目として、Z3を用いてテストケースを生成する方法について紹介します。

## Z3の説明

- Z3とは、元々Microsoft Researchが開発していた、MITライセンスのOSSです([Githubページ](https://github.com/Z3Prover/z3))。
- Z3は、SMT2形式で記述された論理式を受け取り、真とする値が存在するかどうか判定し、存在する場合は値を返します。
    - (例1) 
        - (論理式) ``(and (= (+ x y) 10) (= (- x y) 6))`` 
            - この論理式は、「$(x+y=10)$かつ$(x-y=6)$」を意味します。
        - (答え) 存在する。$(x, y) = (8, 2)$
    - (例2) 
        - (論理式) ``(and (= x 1) (= x 2))``
            - この論理式は、「$(x=1)$かつ$(x=2)$」を意味します。
        - (答え) 存在しない。
- この記事では、Z3を使って、テストケースをどのように生成するのか紹介します。

## テストケース作成の課題

- テストケースとは、プログラムが期待通りに動くかどうかをテストするため、入力値とそれに対応した期待値を含むデータのことです。
- 私が研究対象としている、COBOLプログラムを用いて説明します。
    - こちらのCOBOLプログラムは、$x=1$ のときに、$y$ に $1$ を加算するプログラムです。

        ```C
        1 IF x = 1 THEN
        2   COMPUTE y = y + 1
        3 END-IF.
        ```

    - テストケースでは、「$x=1$ の時に、$y$ に $1$ 加算するかどうか」検証するため、入力値と期待値を準備します。
        - 入力値 : $x=1, y=0$
        - 期待値 : $y=1$
- if文の数が多かったり、条件式が複雑だと、テストケースの作成がとても大変になります。

## Z3を使ってテストケースの入力値を生成する

- そこで、Z3を使って、テストケースを生成してみます。
- この記事では、先ほどよりも難しい例に対して、入力値の生成例を示します。

    ```C
    1 IF x = 1 THEN
    2   COMPUTE y = y + 1
    3 END-IF.
    4 IF x = 2 THEN
    5  COMPUTE y = y + 10
    6 END-IF.
    7 IF y = 100 THEN
    8   COMPUTE z = z + 1
    9 END-IF.
    ```

- このプログラムには、変数へ値を代入する命令が、2,5,8行目にあります。
- これらの命令をテストする入力値は、どうすれば生成できるのでしょうか。

### 欲張ったテスト方法：(2,5,8行目)を一気にテストする入力値はあるのか？

- まず、欲張って、3つの命令を一気にテストできるのか確認してみましょう。
- 人間の目で見ると、1行目と4行目のif文を両方真にするxの値は存在しないため、2,5,8行目を一気に検証する入力値がないことがすぐにわかります。
- Z3で、同じことを証明できるでしょうか。

#### if文(1,4,7行目)に対応した論理式をSMT2形式で書いて、Z3を実行する

- こちらに、1,4,7行目のif文に対応した論理式を示します。
    1. COBOLプログラムの変数を、SMT2形式で宣言。
    1. if文に対応した論理式の記述。1行目：``(= x 1)``、4行目：``(= x 2)``、7行目：``(= (+ y 11) 100)``
        - (7行目の論理式の補足) 7行目のif文の条件式へ、2,5行目を実行した結果を反映しています。
    1. 論理式を満たす値が存在するか判定。

    ```lisp
    ; 変数の宣言
    (declare-const x Int)
    (declare-const y Int)
    (declare-const z Int)

    ; if文に対応した論理式
    (define-fun if_target () Bool (and (and (= x 1) (= x 2)) (= (+ y 11) 100))) 

    ; 論理式を満たす値が存在するか判定
    (assert if_target)
    (check-sat) 
    ```

- Z3に論理式を入力・実行すると、``unsat`` が出力されます。
- これは、予想通り満たす値が存在しないことを意味します。

### 正しいテスト方法：(2,8行目)をテストする入力値はあるのか？

- では、今度は、5行目の命令を除いた、2つの命令をテストできるか確認してみましょう。

#### if文(1,7行目)に対応した論理式をSMT2形式で書いて、Z3を実行する

- こちらに、1,7行目のif文に対応した論理式を示します。
    1. COBOLプログラムの変数を、SMT2形式で宣言。
    1. if文に対応した論理式の記述。1行目：``(= x 1)``、7行目：``(= (+ y 1) 100)``
    1. 論理式を満たす値が存在するか判定。
    1. 論理式を満たす値を生成。

    ```lisp
    ; 変数の宣言
    (declare-const x Int)
    (declare-const y Int)
    (declare-const z Int)

    ; if文に対応した論理式
    (define-fun if_target () Bool (and (= x 1) (= (+ y 1) 100)))

    ; 論理式を満たす値が存在するか判定
    (assert if_target)
    (check-sat)

    ; 論理式を満たす値を生成
    (get-model)
    ```

- Z3に論理式を入力・実行すると、``sat`` に続いて $x = 1, y = 99$ が出力されます。
- これは、満たす値が存在して、2,8行目をテストする入力値を生成できたことを示します。

## 補足

- Z3は、こちらの[Webサイト](https://rise4fun.com/z3/tutorial)にて、お試し実行できます。この記事で示した論理式を入力して、テストケースを生成してみてください。
- 本記事に関連する研究として、国際会議([APSEC2020](https://formal-analysis.com/apsec/2020/))で発表しました。
    - R. Soga, T. Yonemitsu, M. Inagaki, Y. Fujisaki, H. Sugou, H. Kanuka, “A Program Simplification Method for Generating Test Input Values Using Symbolic Execution,” in 2020 27th Asia-Pacific Software Engineering Conference(APSEC), 2020.