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

こんにちは。株式会社 日立製作所 研究開発グループの曾我 遼です。
この記事では、日立グループ OSS Advent Calendar 2020 の22日目として、Z3を用いてテストケースを生成する方法について紹介します。

Z3の説明

• Z3とは、元々Microsoft Researchが開発していた、MITライセンスのOSSです(Githubページ)。
• 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$ を加算するプログラムです。

    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を使って、テストケースを生成してみます。

• この記事では、先ほどよりも難しい例に対して、入力値の生成例を示します。

  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形式で宣言。
  2. if文に対応した論理式の記述。1行目：(= x 1)、4行目：(= x 2)、7行目：(= (+ y 11) 100)
     • (7行目の論理式の補足) 7行目のif文の条件式へ、2,5行目を実行した結果を反映しています。
  3. 論理式を満たす値が存在するか判定。

  ; 変数の宣言
  (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形式で宣言。
  2. if文に対応した論理式の記述。1行目：(= x 1)、7行目：(= (+ y 1) 100)
  3. 論理式を満たす値が存在するか判定。
  4. 論理式を満たす値を生成。

  ; 変数の宣言
  (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サイトにて、お試し実行できます。この記事で示した論理式を入力して、テストケースを生成してみてください。
• 本記事に関連する研究として、国際会議(APSEC2020)で発表しました。
  • 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.