日本ソフトウェア科学会第 36 回大会 (2019 年度) 講演論文集

競技プログラミングコンテストの提出プログラムを利用した記号実行ツール KLEE の定量的評価
岡野 兼也

吉田 則裕

山本 椋太

高田 広章

ソフトウェアの大規模化・複雑化により人手での網羅的なテストケース作成が困難になってきている．このことか
ら，網羅的なテストケース自動生成には期待が寄せられている．テストケース自動生成を目的とした記号実行ツール
KLEE が開発されている．約 160 のソフトウェアに KLEE を適用したところ，生成されたテストケースのコード
カバレッジは 90%を超えたと主張されている．しかし，対象としたソフトウェアのほとんどは，システムソフトウェ
アと呼ばれるものであり，多様性に欠ける．そこで，多様なアルゴリズムが利用されている，競技プログラミングコ
ンテストの提出プログラムに KLEE を適用し，定量的な評価を実施した．評価の結果，シンボルとなる変数が利用するメモリ使用量の大きい場合に KLEE が異常終了しやすく，プログラムの循環的複雑度は KLEE の生成するテストケースのコードカバレッジに影響を与えないということがわかった．

The increases in the scale and complexity of a software system make the manual creation of exhaustive
test cases more diﬃcult. The automatic generation of exhaustive test cases is needed to alleviate it. A
symbolic execution tool KLEE has developed for the automatic test case generation. It is insisted that thecode coverage is greater than 90% when KLEE is applied to approximately 160 targets. However, most of
the targets are categorized into system software and lack variety. Therefore, we performed a quantitativeevaluation of KLEE with competitive programming archives that include the implementations of various
algorithms. As a result, we found that KLEE tends to terminate abnormally when symbol variables consume
much memory. Also, the cyclomatic complexity of a target program makes an insignificant impact on thecode coverage of the generated test cases.

路を網羅的に抽出する技術である [5]．記号実行の実

1 はじめに

行中にでは変数をシンボルとして扱い，1 つの実行経

ソフトウェアの信頼性や機密性を確かめるために路を取りうる変数の値を導出することができる．このは，十分なソフトウェアテストの実施が必要不可欠特性を利用すると，論理的にはプログラムのすべてのである．しかし，ソフトウェアの大規模・複雑化によ実行経路を網羅したテストケースを生成することが可り，ソフトウェアテストは非常に時間のかかる作業で能である．記号実行の研究は 1970 年代から学術的にあり，開発工程のうち 4 割弱を占める [2]．この割合

は盛んに行われ，多くの成果を挙げている．しかし，は年々増加しており，大きな問題となっている [8]．

記号実行の計算コストの高さなどに起因して，実際の以上から，ソフトウェアテストの自動化には高い期

ソフトウェア開発の現場で利用されることはほとんど待が寄せられている．自動化可能なテストケースの生無かった．2000 年代になると，計算機の性能向上や，成手法の 1 つに，記号実行を利用したものがある．記

充足可能性判定問題を高速に解く SAT (satisfiability

号実行はプログラムを擬似的に実行し，実行可能な経

problem) Solver の飛躍的進化 [3] から，十分現実的

Quantitative Evaluation of Symbolic Execution Tool
KLEE with Competitive Programming Archives.
Kenya Okano, 株式会社サイバーエージェント, CyberAgent, Inc.
Norihiro Yoshida, Ryota Yamamoto, Hiroaki Takada,
名古屋大学, Nagoya University.

な時間で記号実行によるプログラムの解析が可能になった．
記号実行を利用したテストケース生成ツールとして最も有名なものに，KLEE [1] がある．KLEE は

LLVM (Low Level Virtual Machine) ビットコード

に変換された C 言語のプログラムに対して記号実行

記号実行を利用したテストケース生成ツールとしを行い，テストケースを作成するツールである．実

て最も有名なものに，KLEE [1] がある．LLVM ビッ

際に Coreutils や Busybox を始めとする，約 150 のトコードに変換された C 言語のプログラムに対して

OSS (Open Source Software) に対して適用されてい記号実行を行い，テストケースを生成する．同時に，る．生成されたテストケースは平均で 90%のコード

実行可能な経路の総数や，実行経路に対応した変数のカバレッジを実現し，脆弱性を発見することにも成功

具対値を出力する．

している．また，商用の静的解析ツールと比較した評

前述したように記号実行には計算コストが非常に

価 [6] も行われており，静的解析ツールでは検出する

大きいという欠点が存在する．この問題点を解決することができなかったソフトウェアの脆弱性の発見に成ために KLEE では SAT Solver に与える経路制約を功している [1]．しかし，対象としたソフトウェアの

事前に簡単化する，キャッシュを利用して複数回の問

ほとんどはシステムソフトウェアと呼ばれるものであい合わせがある場合に高速化を図るなどの工夫が行り，多様性に欠ける．

われている．

そこで，本研究では多様な特性を持つプログラムを利用して，KLEE を定量的に評価することを目的と

2. 2 KLEE の評価する．目的を達成するべく，競技プログラミングコン
テスト運営サイト AtCoder †1 に提出されたプログラKLEE は Open Source Software（以下 OSS）を利用して，性能の評価がされている [1]．対象にはムに対して KLEE を適用した．競技プログラミング

Coreutils に含まれる 89 のプログラム，BusyBox にコンテストでは，数学的問題を解決するために多くの含まれる 75 のプログラム等が利用されている．

アルゴリズムやデータ構造が利用される．この特徴をはじめに，Coreutils を対象とした評価について紹生かし，多様な特徴を持つプログラムに KLEE を適介する．対象とした Coreutils ではそれぞれ開発者の用した結果と，プログラムから得られるメトリクスの手によってテストプログラムが公開されている．そこ

関係を調査する．また，どのようなプログラムであれ

で，KLEE の実行により生成されたテストケースと，

ば KLEE を利用したテストケースの自動生成に向い開発されてきたテストプログラムでコードカバレッジているのか，あるいは向いていないのかを考察する．

の比較がなされた．KLEE の実行により生成されたテストと，開発者が人手により作成したテストプロ

2 関連研究グラムのコードカバレッジ分布を表 1 に示す．さら2. 1 記号実行ツール KLEEに，15 の Coreutils のプログラムに対しては，ランダ

記号実行はプログラムを擬似的に実行し，実行可能

ムテストを加えてコードカバレッジを比較している．

な経路を網羅的に抽出する技術である [5]．実行中にKLEE の実行により生成されたテストと，開発者がは変数にシンボルを割り当てることで，具体値を伴人手により作成したテストプログラムとランダムテ

わない値として扱う．記号実行では，条件分岐によっ

ストでのコードカバレッジの差を図 1 に示す．表 1，て分かれるすべての経路を網羅的に実行する．1 つの図 1 を確認すると，KLEE を利用することでコード実行経路における分岐条件は，実行終了時にまとめらのカバレッジが大きく上昇している．

れ，そのすべての条件を組み合わせたものを経路制約

次に，BusyBox を対象とした評価について紹介すと呼ぶ．経路制約を SAT Solver に与えることで，実る．BusyBox についても，開発者によって作成され行経路に対応した変数の具体値を求めることができたテストプログラムとの比較がなされている．KLEE

る．求められた具体値は，1 つ実行経路での挙動を確の実行により生成されたテストと，開発者が人手によかめるためのテストケースに対応する．

り作成したテストプログラムのコードカバレッジ分布を表 2 に示す．BusyBox でも同様に，KLEE を利用†1 https://atcoder.jp/

して生成したテストケースではコードカバレッジが高表1

Coreutils を対象としたコードカバレッジの分布

表2

Busybox を対象としたコードカバレッジの分布

カバレッジ

KLEE

開発者

カバレッジ

KLEE

開発者

100%

16

1

100%

31

4

90%-100%40

690%-100%24

3

80%-90%2120

80%-90%10

15

70%-80%7

23

70%-80%5

6

60%-70%5

15

60%-70%2

7

50%-60%-10

50%-60%-4

40%-50%-6

40%-50%--30%-40%-3

30%-40%-2

20%-30%-1

20%-30%-1

10%-20%-3

10%-20%--0%-10%-

10%-10%-

30

テスト対象全体のカバレッジ

84.5%

67.7%

テスト対象全体のカバレッジ

90.5%

44.8%

アプリごとのカバレッジの中央値

94.7%

72.5%

アプリごとのカバレッジの中央値

97.5%

58.9%

アプリごとのカバレッジの平均値

90.9%

68.4%

アプリごとのカバレッジの平均値

93.5%

43.7%

な解析において大きな成果を上げている．しかし，調

査対象となっているプログラムはシステムプログラム॥‫ॻش‬ढ़ংঞॵ४ と呼ばれるものばかりである．よって，プログラムの

特徴には偏りがあるということが予想され，異なる特

徴を持つプログラムを利用して評価がされていない．



そのため，多様なプログラムによるテストによってその性能を確認する必要がある．



3 評価実験
ৌ଴উটॢছ঒
5DQGRP

'HYHO

./((

本研究では以下のリサーチクエスチョン (RQ) に基づいて，KLEE を評価する．

図1

ランダムテストと人手で作成されたテストと KLEEで生成されたテストの比較 [1]

RQ1 KLEE をプログラムに適用した時に，KLEEの実行時エラーが発生しないかどうか．

RQ2 10 分間で 10 個以上の実行経路に対するテ
くなっている．
論文のまとめとして，Coreutils や Busybox など合計 150 以上のソフトウェアで，平均 90%以上のコード

ストケースが生成されるかどうか．

RQ3 生成されたテストケースのコードカバレッ
ジが 50%を超えるかどうか．

カバレッジのテストケースを生成できたため，KLEE

まず，これらの項目をなぜ RQ としたのか解説すを利用したテストケースの自動生成は十分に実用的る．RQ1 は，KLEE を異なる多くの特徴を持つプロであるという評価がされている．

グラムに対して適用した時に，正しく実行が完了す以上から，KLEE はテストケースの生成や網羅的るかどうかを調べるための項目である．ソフトウェア

テストを自動化するためには，できるだけ多くのプために，競技プログラミングでは処理速度が高速で，ログラムで KLEE が正常に動作することが好ましい．

実行時のメモリ使用量が少ない C 言語/C++が好ん

あるいは，KLEE の得手不得手を明らかにして，別で利用される．

のツールと組み合わせる必要がある．そこで，KLEE

多くの競技プログラミングコンテストでは，問題がどのような特徴を持つプログラムに対して正常にを解くために利用したプログラムをオンラインジャッ

動作するのかを調べる必要がある．RQ2 は，KLEE

ジシステムに提出する．オンラインジャッジシステム

によるテストケースの生成が現実的な時間で可能かとは，ユーザから提出されたプログラムを必要に応どうかを調べるための項目である．SAT Solver の性

じてコンパイル，厳格なテストデータを入力として能が向上しているが，記号実行が持つ分岐に対して指実行することで，提出プログラムが問題に即してい数的に計算量が増加するという問題は，本質的には解るか検査するシステムである [7]．多くのオンライン

決していない．そこで，一定の時間で KLEE の実行

ジャッジシステムでは，検査結果はリアルタイムで競を打ち切った際に，どの程度テストケースが生成され技者にフィードバックされ，プログラムが受理された

るのかを調べる必要がある．RQ3 は，KLEE により際にはコンテストの得点に反映される．

生成されたテストケースがどの程度プログラムを網以上から，競技プログラミングコンテストの提出プ

羅的に実行するのか調べるための項目である．ソフト

ログラムは以下のような特性を持つことがわかる．

ウェアテストを自動化するにあたり，KLEE で生成• 問題で指定された条件を満たすため，多くのデーされるテストケースは実行経路を網羅的に実行できる必要がある．そこで，KLEE により生成されたテ
ストコードが，どの程度のコードカバレッジとなるのか調べる必要がある．
以降，本研究で行った 2 つの実験について記述する．

タ構造やアルゴリズムを利用する．

• C 言語/C++等のプログラミング言語が利用される．

• オンラインジャッジシステムで受理されたプログラムはすべて，問題用に設定されたテストケースに対して正常に動作する．

3. 1 競技プログラミング
競技プログラミングとは，参加者に問題が与えられ，より早く与えられた問題の条件を満たすプログラ
ムを記述する競技である [7]．

• プログラムは標準入力から与えられ，決められた入力によってのみ振る舞いを変える．
また，これらの特徴は多様な特徴を持つプログラムに対して KLEE を適用するという目的に即している．

多くの競技プログラミングの問題には，問題文，入力形式とその制約，出力，メモリ制約，時間制約が記3. 2 実験方法

述されている．問題文は処理の内容，入力形式とそのまず，本節では実験で共通している部分について説

制約はどのような入力となるか，出力はどのような出明を行う．実験ごとに異なる部分については 3. 3, 3. 4

力にする必要があるか，メモリ制約はプログラムの実節でそれぞれ述べる．

行メモリの最大値，時間制約はプログラムの実行時間

3. 2. 1 実験の流れの最大値を示している．一般に入力は標準入力，出力は標準出力を利用して行う．問題にはメモリ，時間制

実験方法の概要を以下に記述する．以降，各項目での詳細を説明する．

約が存在するため，競技者は問題を解くための空間計

1. 競技プログラミングの提出プログラムを取得

算量，時間計算量を意識してプログラムを記述する必2. 入力変数を KLEE のシンボルに変更

要がある．そのため，問題の難易度が上昇すると素朴

3. Clang で LLVM ビットコードに変換

なアルゴリズムを利用した解答では制約を満たすこ

4. KLEE の実行とが困難になり，様々なデータ構造，応用的なアルゴ

5. KLEE の実行結果や，プログラムのメトリクス

リズムが求められる．また，これらの制約が存在するを収集

6. 評価まず，競技プログラミングの提出プログラムを競技

表3

SourceMonitor で取得したメトリクス

メトリクスの名称

説明

Lines

プログラムの行数

Statements

命令数% Branches

制御構文の数% Comments

コメントの割合

るのか，シンボル値の制限にはどのようなものがある

Functions

関数数のかをプログラムに記述する必要がある．3. 1 項で説Avg Stmts/Function

命令数の平均/関数数

明したように競技プログラミングコンテストの提出

Max Complexity

循環的複雑度の最大値

プログラムは，標準入力によってのみ振る舞いを変え

Max Depth

関数内の最大ネスト数る．そこで，標準入力を受け取っている変数をシンボ

Avg Depth

関数内の平均ネスト数

ルとし，標準入力から入力を受け付けるプログラム

Avg Complexity

循環的複雑度の平均

プログラミングコンテスト運営サイト AtCoder から収集した．アルゴリズムの偏りを避けるため同一問題のプログラムは 10 以下となるようにした．
次に KLEE を適用するための準備を行った．KLEE
を適用するためにはシンボルをどの変数に割り当てをコメントアウトすることで KLEE の適用を可能にした．なお，シンボル値の制約については実験によっ

す．なお，これらのメトリクスは改行が適切になされて変更しているため実験ごとに説明する．ただし，不ない場合や，マクロが利用されている場合等には正常要な経路探索を行わないようにし，高速化を図るために計測できないものがある．

AtCoder の入力制約の範囲内でシンボル値の制限を行っている．

KLEE の実行結果については KLEE の出力ファイ
ルや KLEE の補助コマンドの ‘‘klee-stats’’ の実プログラムの変更後，Clang を利用してプログラ

行結果を利用して情報を収集した．また，コードカ

ムを LLVM ビットコードに変換した．このとき，イバレッジについては ‘‘klee-stats’’ コマンドのう

ンクルードパスに KLEE 用のヘッダファイルのあるち “ICov (%) ”，“BCov (%) ” の項目を利用して調ディレクトリを指定し，KLEE のシンボルを制御す

べた．これらはそれぞれ，命令カバレッジ，ブランチ

るための関数群を利用できるようにした．

カバレッジを示す．

ここまでで KLEE の実行準備が整ったため，作成

さらに，time コマンドを利用してプログラムの実

した LLVM ビットコードに対して KLEE を適用し

行メモリも測定した．測定には AtCoder で提供された．実行環境や KLEE に与えたオプション等についているオンラインジャッジのテストケースを利用し，ては 3. 2. 2 に記述する．

すべてのテストケースを入力した際の最大のメモリ

KLEE の実行後，評価するためのメトリクスを収

使用量をプログラムの実行メモリとして扱った．

集した．プログラムのメトリクス収集には SourceMonitor †2 を利用した．SourceMonitor はプログラ

RQ に対してどのような結果になったか確認するこムの関数の数，行数，循環的複雑度，ブロックのネスとで評価を行った．

ト数などの静的メトリクスを測定するためのツール

3. 2. 2 実験環境である．C++, Java, C#など様々なプログラミング

本実験で KLEE を実行した環境について表 4-6 に言語に対応しており，プロジェクト全体の測定結果，最後に，収集したメトリクスを利用して定義した

示す．

ファイルごとの測定結果など用途に合わせて出力す

本実験を行うにあたりオペレーティングシステムにることが可能である．C 言語のプログラムに対して行った調整として，プロセスのスタックサイズの上限

SourceMonitor で取得可能なメトリクスを表 3 に示変更がある．これは，記号実行を行った時にシンボルのサイズが大きく，まとめられた経路制約が複雑なも†2 http://www.campwoodsw.com/sourcemonitor.htmlのになった場合，SAT Solver が再帰を繰り返すため

表4

オペレーティングシステムの環境

仮想化マシン

VMware Workstation Player 15

CPU

CPU: Core i5-7300U @ 2.60GHz

メモリ

Memory: 6GiB

OS

Ubuntu 16.04 LTS

プロセスのスタックサイズの上限

無制限

表5

表6

コンテナの環境

Docker バージョン

18.09.0

コンテナイメージ

klee/klee:latest (2018/12/17)

メモリ

4GiB

プロセスのスタックサイズの上限

無制限

KLEE の実行制約の導出が完了していない場合がある．

SLOW

打ち切り時間10 分

メモリ使用上限

3GiB

KLEE の実行時エラーが起こらず，10 未満の実

フォーク数上限

15000

行経路に対応したテストケースが生成される．かつ，KLEE の実行時エラーが起こらず，経路探である．制限を緩和することで SAT Solver は KLEE

索により発見された実行経路のうち，半分未満のに割り当てられているメモリに余裕がある限り，再帰実行経路に対応したテストケースが生成される．

呼出しが可能となる．
また，KLEE の実行環境には公開されている Docker
Image†3 を利用した．理由として，インストールの方法や依存パッケージの推奨バージョンの違いなど細か

SIGSEGV
セグメンテーションフォールトが発生し，KLEE
が異常終了する．

SHAREDMEM

い環境による差をなるべく少なくすることが挙げら“LLVM ERROR: not enough shared memory

れる．

for counterexample ” というエラーが発生し，

3. 2. 3 結果の分類実験を行ったところ，結果は以下のように大別され

KLEE が異常終了する．
FORKERR

ることがわかった．以降，実験結果を示す際に下記の“ERROR: fork failed (for STP) ” というエラー

表記を利用する．

が発生し，KLEE が異常終了する．

GREEN
KLEE の実行時エラーが起こらず，10 以上の実

3. 3 競技プログラミングの制約に合わせた実験

行経路で対応したテストケースが生成された．

3. 3. 1 評価対象

あるいは，KLEE の実行時エラーが起こらず，

本節の実験では競技プログラミングの問題で与え

KLEE の経路探索により発見された実行経路のられた入力値の制約をそのまま KLEE のシンボル制

うち，半分以上で実行経路に対応したテストケー

約として利用する．

スが生成された．なお，KLEE で実行を途中で3. 3. 2 結果打ち切った場合経路探索やテストケースの具体値プログラムに 3. 2. 1 項に記述した手順で KLEEを適用したところ 100 のプログラムのうち 18 が†3 https://hub.docker.com/r/klee/klee/

GREEN，9 が SLOW，30 が SIGSEGV，38 が

図2

3. 3 でシンボルとした変数のメモリサイズ

SHAREDMEM となった．残りの 5 プログラムについては実行ごとに結果が大きく変化するため，定図3

3. 4 でシンボルとした変数のメモリサイズ

義しなかった．結果ごとのメトリクスの平均値を表 7に示す．なお，本実験では正常に KLEE の実行が終入力として与えられる変数の配列の長さを 10,000 未了したプログラムが 27/100 と非常に少数であったた

満と変更した．プログラムが静的に変数領域を確保しめ，コードカバレッジについては評価していない．

ていた場合については，変数領域を入力数と対応さ

また，KLEE の実行中にユーザがシンボルとしてせた．

指定した変数に割り当てるメモリサイズが大きく，低3. 4. 2 結果

速になるかクラッシュするという旨の警告がほとんどプログラムに 3. 2. 1 項に記述した手順で KLEEのプログラムで発生した．そこで，シンボルとした変を適用したところ 100 のプログラムのうち 55 が数に割り当てたメモリの大きさを調査した．その結果

GREEN，27 が SLOW，4 が FORKERR，6 がを図 2 に示す．

SHAREDMEM となった．残りの 6 プログラムに

図 2 を見ると，異常終了しているプログラムではついては実行ごとに結果が大きく変化するため，定正常終了しているプログラムに比べて明らかにシン義しなかった．結果ごとのメトリクスの平均値を表 8ボルとした変数に割り当てられているメモリサイズに示す．また，先ほどと同様にシンボルとした変数にが大きい．

与えたメモリの大きさの分布を図 3 に示す．さらに，行った実験から，シンボルとした変数のメモリサイ

コードカバレッジについて表 9 に示す．これらの図表ズが大きい場合に記号実行に影響を及ぼし，KLEEについては結果が変化する 6 のプログラムを除いたの実行が失敗しているということが推測できる．そ94 のプログラムを対象としている．

こで，3. 4 節ではシンボルとなる変数に与えるメモリ

また，本実験ではどのメトリクスがコードカバレッ

サイズを小さくし，再度プログラムに KLEE を適用

ジに対して大きな影響を与えるのかを調べるため，命した．

令カバレッジ，ブランチカバレッジを対象として線形回帰分析を行った．線形回帰分析の結果を表 10 に

3. 4 入力サイズを制限した実験
3. 4. 1 評価対象示す．
表 10 を見ると，コードカバレッジにはブロックの3. 3 節の実験で，シンボルとした変数に与えるメモ

最大ネスト数のみが大きな影響を与えているというリのサイズが大きいと KLEE は異常終了することがことが見て取れる．以上の実験結果を踏まえて，結果多いということがわかった．そこで，本節の実験ではと RQ との対応を下記に示す．

表7

命令数
循環的複雑度の最大値
ブロックの最大ネスト数
実行メモリ (KB)

表8

命令数
循環的複雑度の最大値
ブロックの最大ネスト数
実行メモリ (KB)表9

3. 3 で取得したメトリクスの平均値

全体(n=100)
121.3
12.2
3.8
19,927.7

GREEN(n=18)
86.1
9.8
3.9
14,115.6

SLOW
(n=9)
98.8
15.8
4.0
4,721.8

SIGSEGV(n=30)
105.5
12.7
3.7
11,644.1

SHAREDMEM(n=38)
166.5
12.8
3.8
35,271.6

3. 4 で取得したメトリクスの平均値

全体(n=100)
143.1
11.9
3.8
12,573.7

GREEN(n=55)
146.7
13.5
3.8
4,385.4

SLOW(n=27)
185.3
12.2
3.8
20,056.6

SHAREDMEM
(n=6)
53.2
7.0
3.0
61,998.1

FORKERR
(n=4)
98.8
7.5
3.8
8,926.0

3. 5 考察3. 3 でのコードカバレッジ

50%を超えた

50%を下回った3. 4 節に記した各 RQ の回答に対する考察を行う．

コード数

コード数

まず，RQ1 について考える．記号実行では実行経

ICov

44

50

路に対応した経路制約を SAT Solver に与えることで

BCov

9

85

変数の具体値を算出する．この時シンボルとした変数のメモリサイズが大きくなるとは SAT Solver に与え

表 10

コードカバレッジの線形回帰分析結果る変数の数の増加を指し示している．SAT Solver の
最悪計算量は変数の数に対して指数的に上昇する [4]．

n=94

ICov

BCov

命令数

0.02

0.01

循環的複雑度の最大値

-0.41

-0.31

ブロックの最大ネスト数

5.54

5.78

ムの再帰回数が大幅に増えてしまい，SAT Solver はシンボルのローカルメモリ

0.00

0.00

多量のメモリを利用し，エラーが発生したと考えら

シンボルのグローバルメモリ

0.00

0.00

れる．

シンボルの合計メモリ

0.00

0.00

次に，RQ2 について考える．KLEE による記号実

実行メモリ

0.00

0.00

行では複数のスレッドでグローバル変数が共有され平均計算時間は指数ほど大きなものにはならないが，それでも変数の数の増加に伴い大きな計算量になっているということが予測される．結果としてプログラる．したがって，変数のアクセスは場合により排他的になってしまう．結果としてローカル変数のみを対象

RQ1
シンボルに与えるメモリサイズが大きい場合にKLEE が異常終了する．
RQ2としたプログラムよりも，動作が低速なものになっていると考えられる．
続いて，RQ3 について考える．KLEE は，処理の高速化を図るため，可能な限り並列に記号実行を進めシンボルにグローバル変数を多用すると記号実るように設計されている．そのため，記号実行を並列行が低速になる．

に実行可能であるプログラムでは高速になる．ブロッ

RQ3

クのネストが深いとはプログラム内に分岐が連続してブロックのネストが深いプログラムではテスト存在することを指す．その結果，ブロックのネストがケースのコードカバレッジが上昇する．

浅いプログラムより分岐が増えることが多く，実行経

路の数が増加する．実行経路が増加した結果として，的評価を行った．研究を行うにあたり設定した RQ

記号実行の並列性が高まり，網羅的なテストケースがは以下である．

高速に生成されたと考えられる．
以上から，開発者や研究者が KLEE でカバレッジの高いテストケースを生成したい場合には，シンボルとなる変数のメモリサイズを小さなものとし，グロー
バル変数の多用は避けるべきということが言える．一方で，シンボルとした変数の多くがローカル変数で，RQ1 KLEE の実行時エラーが発生しないかど
うか．

RQ2 10 分間で 10 個以上の実行経路に対するテストケースが生成されるかどうか．

RQ3 生成されたテストケースのコードカバレッ
ジが 50%を超えるかどうか．

ブロックのネスト数の多いプログラムでは高いコード

AtCoder から抽出した 100 のプログラムに 10 分

カバレッジを誇るテストケース生成を期待できる．

間の記号実行を行い，RQ に基づいて評価をしたとまた，表 10 を確認すると循環的複雑度はコードカ
バレッジにあまり影響しないということが見て取れ
る．一般的にプログラムが複雑になると人手での網羅的なテストケース，テストプログラムの作成は困難になる．しかし，KLEE であれば LLVM ビットコードを機械的に解釈してテストケースの作成が可能なため，複雑度の上昇に強い．したがって，KLEE は複
雑すぎて人手によりテストケースの作成が困難な場
合に大きな効果を発揮できると考えられる．

ころ，以下のことが明らかになった．

• シンボルとなる変数に与えるメモリサイズが大きい場合に異常終了する．

• シンボルにグローバル変数を多用すると実行が低速になる．

• プログラムのネストが深いとテストケースのコー
ドカバレッジが上昇する．
この結果を受けて，KLEE を利用する開発者，研究者は KLEE を利用する際に，シンボルとなる変数

一方で，本実験ではシンボルのメモリサイズやプのメモリサイズを小さなものとし，グローバル変数

ログラムの実行メモリの大きさなどのメモリに関すの多用を避けるべきということが示された．一方で，る項目は，コードカバレッジに対して大きな影響を与シンボルとする変数にグローバル変数が少なく，分岐えなかった．KLEE での変数の具体値の算出方法をや繰り返し処理の多いプログラムでは高いコードカ

考えると，これは非常に不可解な結果である．本実験

バレッジを誇るテストケースの生成が可能であるといで対象としたプログラムは競技プログラミングコン

うことが明らかになった．

テストの提出プログラムを利用しており，その書き方

今後の課題として，他のプログラミングコンテストや問題が与える制約は様々である．ある問題では数バ

運営サイトからプログラムを抽出し，同様の実験を行

イトのメモリ領域で入力を受け取ることが可能だが，うということが挙げられる．各プログラミングコン

あるプログラムでは数十キロバイトのメモリ領域がテスト運営サイトでは作問者がそれぞれ異なるため，必要となってまう．結果としてシンボルのメモリサイ作成される問題には偏りがある．一方，本研究の目

ズには大きな振れ幅が存在する．このため，シンボル

的は多用な特徴を持つプログラムに KLEE を適用し，のメモリサイズは線形的にはコードカバレッジとの関KLEE の性能を評価することである．より偏りの少係を表現しきれなかった可能性があると考えられる．

ないプログラムを対象として KLEE を評価するためしたがって，将来的にはメモリサイズとコードカバには，各プログラミングコンテスト運営サイトからそ

レッジの関係を様々な計算式に当てはめて近似し，どれぞれプログラムを抽出し，KLEE の適用対象とすのような関係になるか調査する必要があると考える．

る必要がある．
また，評価に利用する分析手法についても改めて検4 おわりに討する必要がある．本実験では線形回帰分析を利用

本研究では競技プログラミングコンテストの提出プして評価をしたが，シンボルとなる変数のメモリサ

ログラムを利用して，記号実行ツール KLEE を定量

イズやプログラムの実行メモリはコードカバレッジ

にほとんど影響を与えていなかった．しかし，SAT

Solver の仕様を考えるとこれは不可解な結果である．
このような結果となった原因にコードカバレッジとシ
ンボルとなる変数のメモリサイズやプログラムの実
行メモリとの間に線形回帰分析で表現できない関係があるということが考えられる．そこで，様々な計算式に当てはめて近似することで，シンボルとなる変数のメモリサイズやプログラムの実行メモリを始めとする各メトリクスと，コードカバレッジの関係をより正確に調査する必要がある．

参 考 文 献[1] Cadar, C., Dumbar, D., and Engler, D.: KLEE:
Unassisted and Automatic Generation of HighCoverage Tests for Complex Systems Programs,

Proc. of OSDI, Vol. 8, 2008, pp. 209–224.
[2] 片岡晃: ソフトウェア開発データ白書 2018-2019, 独立行政法人情報処理推進機構, 2018, pp. 178–188.
[3] 宋剛秀, 番原睦則, 田村直之, 鍋島英知: SAT ソル
バーの最新動向と利用技術, コンピュータソフトウェア,
Vol. 35, 日本ソフトウェア科学会, 2018, pp. 72–92.
[4] 井上克己, 田村直之: SAT ソルバーの基礎, 人工知能
学会誌, Vol. 25, 人工知能学会, 2010, pp. 57–67.
[5] 上原忠弘: シンボリック実行を利用した網羅的テスト
ケース生成, FUJITSU, Vol. 66(2015), pp. 34–40.
[6] 徳本普, 上原忠宏, 宗像一樹, 菊地英幸, 江口享, 石田晴行, 馬場匡史: C/C++シンボリック実行ツール KLEEの適用と CPPUNIT 連携ツールの開発, ESS, (2011).
[7] 渡部有隆: オンラインジャッジの開発と運用-Aizu Online Judge-, 情報処理, Vol. 56, 情報処理学会, 2015,
pp. 998–1005.
[8] 中野隆司, 田中裕大, ダン ティ ホンイエン: ソフト
ウェアのテスト工数・期間を削減するためのシステム
テスト自動化技術, 東芝レビュー, Vol. 73, 東芝, 2018,
pp. 40–44.