JAIST Repository
https://dspace.jaist.ac.jp/

Title

モデル検査技術を利用したプログラム解析器の生成ツール

Author(s)山岡, 裕司; 胡, 振江; 武市, 正人; 小川, 瑞史

Citation

情報処理学会論文誌:プログラミング,
44(SIG13(PRO18)): 25‑37

Issue Date

2003‑10‑15

Type

Journal Article

Text version

publisher

URL

http://hdl.handle.net/10119/4566

Rights社団法人 情報処理学会, 山岡 裕司, 胡 振江, 武市
正人, 小川 瑞史, 情報処理学会論文誌:プログラミン
グ, 44(SIG13(PRO18)), 2003, 25‑37. ここに掲載した著作物の利用に関する注意: 本著作物の著作権は（社）情報処理学会に帰属します。本著作物は著作権者である情報処理学会の許可のもとに掲載するものです。ご利用に当たっては「著作権法」ならびに「情報処理学会倫理綱領」に従うことをお願いいたします。
Notice for the use of this material: The
copyright of this material is retained by the
Information Processing Society of Japan (IPSJ).
This material is published on this web site withthe agreement of the author (s) and the IPSJ.
Please be complied with Copyright Law of Japanand the Code of Ethics of the IPSJ if any users
wish to reproduce, make derivative work,
distribute or make available to the public any
part or whole thereof. All Rights Reserved,
Copyright (C) Information Processing Society ofJapan.

Description

Japan Advanced Institute of Science and Technology

Vol. 44

No. SIG 13(PRO 18)

Oct. 2003

情報処理学会論文誌：プログラミング

モデル検査技術を利用したプログラム解析器の生成ツール
山
武

岡
市

裕
正

司†
人†

胡
小

川

振
瑞

江†,††
史†,††

本論文では，時相論理式によって仕様が記述されたプログラム解析をモデル検査技術の利用によって行うツールについて述べる．本ツールは，対象プログラム言語は Jimple，プログラム解析の仕様記述
言語は時相論理 CTL-FV である．Jimple は Java と相互変換可能な 3 番地コードからなる中間言語であり，Java に比べプログラム解析や最適化が適用しやすい．また，CTL-FV は CTL（ Computation
Tree Logic ）を拡張した時相論理であり，プログラム中の情報を述語に引用することを許したところに大きな特徴がある．CTL-FV によって多くのプログラム解析が記述できるため，本ツールを使用す
ると Jimple プログラムに対し様々な解析を自動的に行うことができるようになる．今回，モデル検査を既存のモデル検査ツール SMV をそのまま利用することによって実装が非常に簡単になり，Java
言語で約 500 行（コメント除く）のプログラムでこれが実現できた．また，標準ライブラリのいくつかのクラスに対して無用命令の検出を本ツールにより実行したところ，比較的大きなサイズのクラスに対しても数分で解析することができた．ここでは，主に本ツールの設計と実装について説明する．

Generation of Program Analyzer Based on Model Checking
Yuji Yamaoka,† Zhenjiang Hu,†,†† Masato Takeichi†
and Mizuhito Ogawa†,††In this paper, we describe a tool that automatically performs program analysis using modelchecking techniques. The tool has two characteristics; the target program is Jimple, and thespecification of program analysis is described in temporal logic CTL-FV. Jimple is mutuallyconvertible with Java; it is a 3-address intermediate language and is easier to perform program
analyses and optimizations than Java. CTL-FV is an extension of CTL (Computation Tree
Logic) to allow quoting information in a program to formulas. CTL-FV can describe many
program analyses, thus our tool can carry out various analyses automatically. By the use of
the well-developed model-checker SMV, we implemented this tool with only 500 lines of codein Java. As an example, dead code detection is performed to some classes in the standard
library, and relatively large classes can be analyzed in a few minutes. We explain the design
and the implementation of the tool.

1. 序によって自動生成されるときの利益は大きい．

論• プログラム解析の仕様はほとんどの文書で自然言語によって記述されている．それを手動で正しくコントロールフロー解析やデータフロー解析といったプログラム解析は伝統的なプログラム最適化におい

実装するのは容易ではない．
• プログラム最適化においては次々とヒューリスティ
クスによるアルゴ リズムが考案され，実装されいて必要不可欠な基本的な解析である．プログラム最適化はそれら基本的な解析の結果を用いて，適切なプロ
グラム変換を適用する．たとえば無用命令の検出や定る．最適化効果を高めるため新たなアルゴ リズム

数伝播解析などはその例である1),7) ．これらの解析はを考案したとき，その効果について手軽に実験で手動で実装したもので行われるのが普通だが，特に以きる．
このような背景のもとで，プログラム解析とモデル

下のような理由で意図するプログラム解析器がツール

検査の親和性が指摘され 9) ，モデル検査技術を利用することによって自動的に意図するプ ログラム解析器† 東京大学大学院情報理工学系研究科
Graduate School of Information Science and Technology, The University of Tokyo†† 科学技術振興事業団
Japan Science and Technology Corporationが生成される可能性について論じられるようになってきた．
モデル検査とはシステムがある仕様を満たしている25

26

Oct. 2003

情報処理学会論文誌：プログラミング

かど うかを検証する形式的検証法の 1 つであり2) ，シ
ステムの有限状態モデルとそのシステムが満たすべき仕様として記述された時相論理式を与えられたとき，システムがその仕様を満たしているかど うかを網羅的

2. 設

計

この章では，我々が開発したプログラム解析器生成
ツールの設計方針について述べる．

に検査する．この方法の最大の特徴は十分な計算資源

我々は本ツールを以下の方針で作成することにした．

さえあれば全自動的に検証が行われるということであ• 仕様が時相論理で記述されたプログラム解析をモ
デル検査技術の利用によって全自動で行う．

る．高度な数学的な知識などが必要とされないうえ，
専門家たちによって開発された SMV 6) や SPIN 4) などのモデル検査ツールが無償で利用できるなどの手軽さもあって，ハード ウェアの設計段階での検証などに• 解析対象のプログラミング言語は現在広く使用されている実用的なものとする．
• 時相論理は，プログラム解析の仕様を記述するの

実し，モデル検査技術がさらに発展するにともなって，に有用なものとする．
• 既存のツールを組み合わせた簡潔な実装法でも，モデルがとる状態空間が非常に大きくなるなどの問題

ある程度大きなプログラムを対象とすることがで積極的に利用され発展してきた．そして計算資源が充があって難しいとされてきたソフトウェアの検証にもモデル検査が利用され始めた．

きることを示す．
この目的に適合するように設計した本ツールの全体モデル検査技術をプログラム解析に利用するには，

図を図 1 に示す．本ツールは，解析対象プログラムとプログラム解析の仕様が時相論理で記述される必要

して Jimple，解析仕様記述言語として CTL-FV を受がある．近年，時相論理 CTL に自由変数を導入した

け付ける．図 1 において大きな四角で囲まれた部分がCTL-FV によって多くのプログラム解析が自然に記述

本ツールにあたる．本ツールは互いに非依存である，できることが Lacey ら 5) によって示された．CTL-FV

解析対象となる Jimple プログラムと解析の仕様記述の特徴は対象プログラム中の情報を論理式中の述語にである時相論理 CTL-FV 式を入力として受け付ける．

引用可能とした自由変数を導入したところにあり，そそしてその仕様で記述された解析をモデル検査によっれによってプログラム解析が簡潔にかつ美しく記述でて行えるようなモデルを対象プログラムから作成し ，きるようになった．しかし，CTL-FV のような自由変モデル検査ツールの入力言語を生成する．この際，対数を持つ時相論理は既存のモデル検査ツールにそのま象プログラムに非依存であった CTL-FV 式は対象プ

までは受け入れられないという問題点があった．

ログラムに特化された CTL 式に変換される．そして

本論文では，時相論理 CTL-FV によって記述され最後にモデル検査ツールによる検証が自動的に行われ，たプログラム解析をモデル検査技術の利用によって自その結果を出力する．モデル検査ツールによる検証が動的に行うツールの実装について説明し，例を用いて成功した場合はプログラム解析の結果何も検出されな

その有用性などについて考察する．本ツールは Java

かったことを意味する．また，モデル検査ツールによと相互変換可能な Jimple を対象プログラムとしている検証が失敗した場合はその反例出力を解析することるため，実用的なプログラムを解析対象とすることがにより，プログラム解析の結果に対応する対象プログできる．さらに，既存のモデル検査ツール SMV を利

ラム中の場所を出力する．

用することなどで 500 行程度の Java プログラムで簡このように本ツールを使用すれば，解析対象 Jimple

潔に実現できた．このような簡潔さはツールの拡張やプログラムと解析仕様 CTL-FV 式を入力するだけで管理を容易にする．

そのプログラムに対する仕様どおりのプログラム解析

本論文の以下は次のように構成される．2 章ではその生成ツールの設計について述べる．3 章ではプログ結果を得ることができる．
以下では本ツールで使用した言語やモデル検査ツー

ラム解析の一種である無用命令の検出を例として用い

ルについて述べる．

ながら実装の詳細について述べる．4 章では Java のク
本ツールを用いて実際にプログラム解析を行い，その2.1 対象言語：Jimple
Jimple とは Java クラスファイルと相互変換が可能
な 3 番地コード の言語である12) ．Java バイトコード

実行時間をもとにツールの有効性について考察する．

はスタックマシン上のコードでありそのままでは解析

5 章では主にプログラム解析器の生成という視点でのが難しいため，それと等価でより解析が簡単な Jimple

関連研究について述べる．そして 6 章で結論を述べる．

をプログラム解析の対象言語とした．Jimple の主な

ラスライブラリ java.math.*の 5 つのクラスについて

命令文を図 2 に示す．なお，図 2 以外の命令文は多Vol. 44

No. SIG 13(PRO 18)

モデル検査技術を利用したプログラム解析器の生成ツール
Jimple27

CTL-FV

CTL

SMV

SMV

SMV

図 1 プログラム解析器生成ツールの全体図
Fig. 1 The whole picture of the generation of program analyzer.

図 2 Jimple の主な命令文
Fig. 2 The main statements of Jimple.

分岐やモニタや例外に関係する命令文であり，ここでは説明を割愛した．

Jimple で記述されたプログラムはたとえば図 3 の2.2 プログラム解析の仕様記述：CTL-FV
CTL-FV は，分岐時間時相論理（ branching-time
temporal logic ）の一種である CTL（ Computation

ようになる．これは図 4 の Java プログラムと等価で，Tree Logic ）に自由変数を引数に持つ述語を導入した

そのクラスファイルと相互変換が可能なものである．

時相論理である5) ．

このプログラムは M yLib という名前のクラス定義でプログラム解析の内容を時相論理によって簡潔に記あり，クラス M yLib はデフォルトコンストラクタと述するためには，その論理体系にプログラムの状態を

static メソッド int mss(int[]) を持っている．なお，

抽象化した述語の存在が不可欠である．手続き的なプ

mss(int[]) は最大部分列和問題（ Maximum Segment
Sum，mss ）を解くメソッドである．Java プログラムの変数 a，ret，debug ，s，i はそれぞれ Jimple プログ

なものは主に変数の状態であるので，論理体系がプロ
グラムの変数に対応付けられる述語を許容しているこ

ラムの変数 r0，i0，i4，i1，i2 に対応しており，Jim-とが望ましい．しかし一般に時相論理は命題論理であログラミング言語で書かれたプログラムの状態で重要

ple プログラムのその他の変数は 3 番地コードに変換

るためプログラム内の変数ごとに述語が必要となり，される際に導入されたものである．Jimple プログラ

そのままでは記述が煩雑となる．そのために自由変数

ムのラベル label0 以前が Java プログラムの for 文のでプログラムの変数などを論理式中に引用する機能を初期化文までに対応し，label0 と label1 と label2 で付加した CTL-FV をプログラム解析の仕様記述言語

名付けられたブロックが Java プログラムの for 文のとした．

中身に対応し，同様に label3 と label4 が for 文および return 文に対応している．

たとえばプ ログラム中の無用命令の検出にあたる
記述「プログラム中で，それ以降使用されることがな
い変数の値が定義されていることがない．
」というも

28

Oct. 2003

情報処理学会論文誌：プログラミング

図 5 CTL-FV の構文
Fig. 5 CTL-FV syntax.

AG !(def & AX !EF use) であることを表現する論
理式を記述しなくてはならない．なお，式 dead-spec
中の def (x) は自由変数 x を引数に持つ述語で「 変数 x の値が定義されている場所で真，そうでない場
図 3 図 4 と等価な Jimple プログラム
Fig. 3 A Jimple program equivalent to the Java programin Fig. 4.

所で偽」であることを表現するものであるとする．同
様に use(x) は「変数 x の値が使用されている場所で真，そうでない場所で偽」を表現している．論理式中で同じ名前で表現された 2 つの自由変数 x は，対象プ
ログラム中の同一な変数に束縛されることになる．なお，これらの述語の意味をプログラム解析器生成ツー
ルにど う組み込むかという問題が考えられるが，ここでは簡単のため本ツール内でそれらの意味は定義済みとした．
分岐時間時相論理である時相論理 CTL は経路限定子（ path quantiﬁer ）と時相演算子（ temporal oper-

ator ）の組によって時相を表現する．経路限定子は経路の分岐構造についての記述に使用され，A，E の 2
図 4 図 3 と等価な Java プログラム
Fig. 4 A Java program equivalent to the Jimple programin Fig. 3.

種類がある．時相演算子は経路の性質についての記述に使用され，F，G，X，U の 4 種類がある．

CTL-FV の構文を図 5 に示す．図中の記号!は否定，のを時相論理式で表現することを考えよう．その式をdead-spec と名付けると CTL-FV 式で，
dead-spec :& は連言，| は選言，-> は条件法をそれぞれ表す．
CTL-FV が CTL と異なる点は自由変数を持つ述語が
 ，E
 という逆向きの経路限定導入されている点と A

AG !(def (x) & AX !EF use(x))など と 表現することがで きる．し かし もし ，自由子（ path quantiﬁer ）が導入されている点である．逆変 数を 許 容し な い 時 相 論 理で こ れ を 表 現し よ うのに役立つ．

と すると ，プ ログ ラ ム中のすべての 変数に ついて向きの経路限定子も多くのプログラム解析を表現する

 ，E
 は結
経路限定子 A，E およびその逆向きの A

Vol. 44

No. SIG 13(PRO 18)

モデル検査技術を利用したプログラム解析器の生成ツール

果として状態式 φ を返すような経路式 ψ に関する演
算子で，それぞれ，• Aψ
これ以降のすべての経路で ψ を満たせば真の状態．
• Eψ
これ以降に ψ を満たす経路が存在すれば真の状態．
• Aψ
ここからさかのぼるのすべての経路で ψ を満たせば真の状態．
• Eψ
ここからさかのぼって ψ を満たす経路が存在す
れば真の状態．
という意味を持つ．
また，時相演算子 F，G，X，U は結果として経路式 ψ を返すような状態式 φ に関する演算子で，それ
ぞれ，

• Fφ
この経路上でいつか φ を満たせば真の経路．

• Gφ
この経路上でつねに φ を満たし続ければ真の経路．
• Xφ
この経路上の次の時間で φ を満たせば真の経路．
• [φ1 U φ2 ]この経路上でいつか φ2 を満たしかつそれまで φ1を満たし続ければ真の経路．
という意味である．
なお，時相論理の記述力によってどれだけ多くのプ
ログラム解析が表現できるか異なるわけだが，Lacey
らは伝統的な最適化で利用されるほとんど のプ ログ

29• trans(e)：式 e 中のすべての変数について，どの変数もその値が定義されていないような場所で真．
• use(x)：変数 x の値が使用されている場所で真．
• useExp(e)：式 e と同じ構造がある場所で真．
これらの述語を用いて，CTL-FV 式で以下のように解析仕様を与えることができる．

• 定数伝播（ constant propagation ）の解析
「ある変数 x が定数 c として実行前にあらかじ
め計算できる，という状態の検出」という解析仕様は，

AG !(use(x) & A[!def(x) U(def V ar(x, c) & conLit(c))]).
• 共通部分式（ common subexpression ）の検出「ある式 e がそこでの利用可能な式として変数y としてすでに定義されている，という状態の検出」という解析仕様は，

AG !(useExp(e) &A[(!def(y) & trans(e)) U def Exp(y, e)]).
• ループ不変（ loop invariant ）式の検出「ある式 e がループ不変である，という状態の検出」という解析仕様は，

AG !((node(n) & useExp(e)) &E[trans(e) U node(n)]).
• 無用命令（ dead code ）の検出
「任意の変数 x の値が定義された後 x の値が使用されることがない，という状態の検出」という解析仕様は，AG !(def (x) & AX !EF use(x)).

ラム解析は CTL-FV によって記述することができる

なお，すべての仕様記述において AG ! で全体が括と予想している．以下では，定数伝播，共通部分式のられているのは，「プログラムがある性質を満たすこと

削除，ループ不変式の巻き上げ，無用命令の削除，のがない」という断言にすることによって，もしそのよ

4 つの最適化でそれぞれ利用されるプログラム解析の
CTL-FV による仕様記述例をあげる．

の反例出力によってその位置を確かめられるようにす

まず CTL-FV 式中で用いるいくつかの述語について説明する．

うな性質がプログラムにあったときモデル検査ツール
るためである．

2.3 モデル検査ツール：SMV• conLit(x)：他の述語で用いられている自由変数

モデル検査の技術は既存の研究の蓄積が大きい．広x が定数であるような場所で真．
• def (x)：変数 x の値が定義されている場所で真．

る非常に洗練されたアルゴ リズムが実装されているたく利用されているモデル検査ツールではその成果によ• def Exp(x, e)：変数 x の値が式 e による代入
x = e によって定義されている場所で真．
• def V ar(x, y)：変数 x の値が変数 y の値（まため，モデル検査には既存のツール SMV をそのまま利は定数 yconLit ）による代入 x = y によって定義の入力言語ではモデルと仕様の両方を同時に記述する．

されている場所で真．

• node(n)：場所を同定するラベルである n によって示された場所で真．

用することにした．
以下 SMV の入出力について簡単に説明する．SMV
モデルはクリプケ構造（ Kripke structure ）の記述そのものであり，いわばそれぞれの状態が変数の値で決まるようにモデル化されたシステムの有限状態遷移グ

30

情報処理学会論文誌：プログラミング

Oct. 2003

仕様を記述した CTL-FV 式を入力として与えられた
後，以下の順に動作する．なお以下の ( 1 ) から ( 3 ) は，

CTL-FV 式は SMV に受け入れられないため，SMVが受け入れる CTL 式に変換するステップである．( 4 )はこの実装で最も重要なモデル生成を行うステップであり，( 5 ) は SMV による検証とその結果の出力に関
図 6 SMV への入力記述の例
Fig. 6 An SMV program.

するステップである．

(1)

自由変数の抽出
入力として与えられた CTL-FV 式をパーズし，ラフをそのまま変換したような単純なものである．
図 6 に SMV の入力の簡単な例をあげ る．まず，VAR ブロックではこのモデルで使用される変数の宣

自由変数の集合を得る．

(2)

自由変数の束縛
それらを対象プログラム中の具体的な情報に束言とその定義域が定義される．例では request が f ，縛させる．束縛の場合の数は幾通りかあるが，t， state が ready ， busy の 2 値のみをとる変数であることが宣言されている．そして，ASSIGN ブロッ

それぞれの場合について以降の手続きを実行

クではこのモデルの状態遷移の記述がなされる．例で

する．

(3)

CTL-FV 式から CTL 式への変換

はまず，変数 request の初期値および 任意の時点の前までのステップで今や自由変数が束縛された状態での値が f ，t のど ちらでもありうることが記述こと，任意の状態にいるときの state の次の時点でのCTL-FV 式を CTL 式に変換する．
モデルの生成
対象プログラムを抽象化して前のステップで得状態が記述されており，「 次の時点での状態は，現時られた CTL 式を検証するのに十分なモデルをされている．続いて state の初期値が ready である(4)点での状態が state = ready かつ request = t なら

生成し，その CTL 式とともに SMV の入力言ば state := busy な状態に，それ以外ならば state は語にする．

busy あるいは ready のど ちらかの状態に遷移する．
」(5)

検証結果の出力という記述がなされている．最後に SPEC ブロックで，SMV によってモデル検査をする．検証結果がこのモデルに対する仕様が CTL 式によって与えられ失敗に終わったら SMV の反例出力をもとに，る．この例での仕様は「このモデルは request = t を対象プログラム中のどこで，CTL-FV 式中の満たす状態になるといつか必ず state = busy を満た

自由変数がど う束縛されたときに，検証に失敗

す状態になる．
」という意味であり，このモデルは仕したかを出力する．

様を満たしていると予想される．

これらの動作を以降では具体的な例に対応付けてよ

実際，これを SMV に入力すると，SMV は初期状

り詳細に説明する．プログラム解析の仕様の例として態からたどりうるすべての状態において仕様が満たさ

先に式 dead-spec として紹介した，プログラムの最適れていることを検査し，化の際に行われるプログラム解析の一種である無用命

speciﬁcation AG (request = t -> AF state= busy) is trueという結果が出力される．もし，満たされないような令の検出を，また，このプログラム解析を適用する対象プログラムの例として先にあげた図 3 のプログラムを使用する．

仕様を入力として与えていた場合は，満たされない状

な お ，今 回の 実 装で は CTL-FV 式 中の 述 語は態になるに至る初期状態からの状態遷移が 1 つ反例とdef (x) と use(x) のみを対象としているので CTLFV 式中の自由変数はすべてプログラム中の変数に束して出力される．

3. 実装の詳細

縛されることになる．

この章では，前章の設計方針に基づいて実装したプ

3.1 自由変数の抽出
入力として与えられた CTL-FV 式より自由変数のログラム解析器生成ツールの内部的な動作について述集合を得る．今，CTL-FV 式から自由変数の集合をべる．まず概要を述べ，その後詳細な動作を具体的な得る操作を F V とすると，無用命令の検出を表現し例を用いて説明する．

た式 dead-spec

本ツールは，解析対象の Jimple プログラムと解析のAG !(def (x) & AX !EF use(x))

Vol. 44

No. SIG 13(PRO 18)

モデル検査技術を利用したプログラム解析器の生成ツール

に対して，

F V (dead-spec) = {x}31たとえば，式 dead-spec は前のステップによって自由変数 x が図 3 の mss() の i1 に束縛されたときにとなる．また，たとえば，定数伝播（ constant prop-

次のような CTL 式に変換される．

agation ）の解析を表現した CTL-FV 式である，
const-spec :
AG !(use(x) & A[!def(x) U

AG !(def i1 & AX !EF use i1 )CTL-FV 式の def (x)， use(x) はその引数が i1 に(def V ar(x, c) & conLit(c))])特化されたことにより，def i1 は「 mss() 中の変数

i1 の値が定義されている場所で真，そうでない場所でに対しては，

偽」である述語，use i1 は「 mss() 中の変数 i1 のF V (const-spec) = {c, x}のようになる．

値が使用されている場所で真，そうでない場所で偽」3.2 自由変数の束縛
CTL-FV 式中の自由変数を対象プログラム中の各メ
ソッドの各変数に順番に束縛させ，それぞれの場合にである述語となる．

3.4 モデルの生成
対象プログラムを抽象化して前のステップで得られた CTL を検証するのに十分なモデルを生成する．

ついて 3.3 節以降のステップを実行できるようにする．

対象プログラムである Jimple は 3 番地コード なの

ここでは式 dead-spec を図 3 のプログラムに適用

で各命令の粒度が小さい．すなわち Jimple の 1 命令

する例で説明する．この例では，前のステップで抽出がプログラムの状態を変化させる最小の単位と考えてされる変数は x のみであるので，これをこのプログラ

よい．そこで生成するモデルの各状態にプログラムのムの各変数に順番に束縛し，解析していくことになる．

各命令文を割り当てることで，ほとんどのプログラム

さて，まずこのプログラムには 2 つのメソッドがあ解析を行うのに十分なモデルが生成されると考えた．

ることが分かる．まずは 1 つ目のメソッド < init > ()各状態は変数の値によって定められなくてはならな（デフォルトコンストラクタ）について無用命令の検いため，各命令に対応する状態をその命令を表現する

出を行う．< init > () にはただ 1 つの変数 r0 があような値で抽象化する必要がある．各状態が保持しなるので，これに x を束縛し，3.3 節以降のステップをければならない情報は，検証しようとする CTL 式で実行することによって < init > () の変数 r0 につい用いられている述語の真偽を観測するためのものとそての無用命令の検出を行うことによってこのメソッドの状態がプログラムのどの命令にあたるかというものの解析をすることができる．

だけなので，これらの情報を変数によって表現すれば

続いて，もう 1 つのメソッド mss() について無用

よい．

命令の検出を行う．今度の場合は変数が複数あるので，また，状態遷移については各状態がプログラムの命

それぞれの変数についての無用命令の検出を行う必要

令文に対応していることからプログラムのコントローがある．そのため，まず x をメソッド mss() の r0 にルフローをマッピングすればよい．ただし，条件分岐

束縛し ，< init > () の場合と同様に解析を行う．そ文に対応する状態からの遷移については，一般にはそれが終わったら，メソッド mss() の i0 についての解の条件式の値は実行時まで知ることはできないので，

析，続いて i1 についての解析というように順に解析

どの分岐先にも非決定的に遷移しうるという抽象化をし，mss() すべての変数に x を束縛していくことに行った．

よってすべての無用命令の検出を行う．

このように生成されたモデルの例を図 7 に示した．

このように対象プログラム中のすべてのローカル変

この図は図 3 のプログラムに対して，式 dead-spec の数について CTL-FV 式に相当する解析を行う．なお，

自由変数 x が mss() の i1 に束縛されたものに相当

今回の実装では intraprocedure な解析，つまりそれぞする CTL 式，

れの単一メソッド 内だけで行う解析のみを対象とした．

AG !(def i1 & AX !EF use i1 )3.3 CTL-FV 式から CTL 式への変換
CTL-FV はそのままではモデル検査ツールに受け入れられないので，自由変数が束縛された CTL-FVを検証するときに生成するモデルの一部で，図 3 の式を CTL 式に変換する．CTL-FV 式中の述語を，そにそれぞれ対応した状態を示している．また，それぞのプログラム中の具体的な変数となった引数によってれの状態をつなぐ 矢印がプログラムのコントロールフ

特化し，引数のない述語へと変換することによってこローに相当する状態遷移を示している．各状態はそのれを実現する．

label0 から label3 までに対応するものである．図中の四角い枠が枠外の括弧で示したプ ログラムの命令32

情報処理学会論文誌：プログラミング

Oct. 2003

図 7 図 3 の label0 から label3 までに対応するモデル
Fig. 7 The model corresponding to label0 to label3 in Fig. 3.

メソッド 中で第何番目の命令文か☆ を表す変数 inst の式 dead-spec の 自由変数 x が 今度は mss() の値，def i1 および use i1 の情報を保持している．

i4 に 束縛され たときの SMV の 入力言語を 示す．

たとえば ，プログラムの label1 の最初の命令文であ

図中の MODULE N extInsts が inst の遷移を ，る if 文は，モデルである図 7 の中列の一番上の状態で示されている．この命令はメソッド mss() 中で第 11P redicate use i4 がそれぞれの inst に対応する状
態での use i4 の値を，P redicate def i4 がそれぞ番目の命令であり，変数 i1 の値を使用している命令でれの inst に対応する状態での def i4 の値を表現しあるので，対応する状態は inst = 11 および use i1ている．また，変数 inst は次の時点での状態に対応を保持することになる．

する値が代入されているものなので，変数 output はそして最後に，以上のように生成されたモデルとCTL 式を SMV の入力言語に 変換する．図 8 に ，今の時点での状態に対応する値が代入されておりこれを結果表示の際に利用することになる．
なお，この方法は逆向きの経路限定子を含むような☆

メソッド の最初の命令文を第 0 番目の命令文とする．

CTL-FV 式に対してはそのままでは使用することがVol. 44

No. SIG 13(PRO 18)

モデル検査技術を利用したプログラム解析器の生成ツール

33

図 8 x が i4 に束縛されたときの SMV への入力
Fig. 8 The input to SMV when x is bound to i4.

できないが，式中の経路限定子がすべて逆向きであSMV の反例出力として得られるのでそれを元のプロ

る☆ ような場合はモデルの状態遷移を反転させるだけ

グラムに対応付けて出力する．

で実現することができる．仕様記述中に順向きと逆向以下では例として，再び図 3 のプログラムに対して，

きの経路限定子が混在するようなプログラム解析は少式 dead-spec の自由変数 x が mss() の i4 に束縛さないので，実用上十分と考えている．

れた場合について説明する．この場合，もし検証に成3.5 検証結果の出力
前のステップで生成したものを SMV によってモデル検査をする．検証に成功し たときは，そのときの功したら，メソッド mss() の i4 についての無用命令

CTL-FV 式の変数の束縛では解析結果が true になったことに相当し，検証に失敗したときは，解析結果がは存在しなかったということであるので，( 2 ) に戻って x を次の変数に束縛する．また，検証に失敗したら，それはそのモデル中の場所に対応する Jimple プ
ログラム中の場所で CTL-FV 式 dead-spec が i4 について満たされていないということを意味している．

☆

最外の AG ! は除く．

実際にはこの例の場合は SMV への入力は図 8 で

34

情報処理学会論文誌：プログラミング

Oct. 2003

図 9 モデル図 8 に対する SMV の反例出力の一部
Fig. 9 Part of SMV counterexample to the model described in Fig. 8.

あるので検証は失敗し，SMV により反例出力としてライブラリを利用したため，約 500 行のソースコード

図 9 のように出力される．図の 1 行目に検証が失敗しを書くだけで実装することができた．

たことが明記されているのが分かる．それ以下の行で表 1 に Java1.3.1 のクラスライブラリ java.math.*

仕様が満たされなくなった状態にいたる遷移が表示さの 5 つのクラスについて無用命令の検出にかかる時れているが，興味があるのは仕様が満たされなくなっ間の測定結果を示す．表には，対象プログラムのサイた状態だけなので，そのときのプログラムの命令を示

ズおよび メソッド 数，解析にかかった全時間，解析にす情報である output の値を得ることによって解析結かかった時間のうちモデル検査に費やされた時間を果が得られる．すなわち，元の Jimple プログラム図 3載せた．測定した環境は，OS が Windows98，Javaの mss() の output = 14 番目の命令文，すなわちランタイムのバージョンは 1.3.1，CPU が 333 MHzlabel2 のPentium II MMX でメインメモリは 128 MB である．

i4 = i1;

この表から BigInteger のように比較的大きいサイズ

が無用命令として検出された文であることが特定され，のクラスに対する解析も，このような遅い計算機上でそのことがツールにより出力される．

も数分で解析できることが分かる．

以上，3.1 節から 3.5 節までのステップを経ることによってプログラム解析が自動的に行われる．

4. 実

験

2 章で述べたように設計されたプログラム解析器生
成ツールが，現実的な大きさのプ ログラムの解析を行うのにどれくらい時間がかかるか測定した．今回，Java により実装し Jimple のパーズには soot フレー
ムワーク12) という既存のフレームワークに含まれる

なお，この表が示すようにこの実験によっていくつかの無用命令が検出された．たとえば，クラス BigIn-

teger から以下のコード に無用命令が発見された．
int multpos = ebits;
ebits–;
boolean isone = true;
multpos = ebits - wbits;
このコードにおいて，1 行目の代入によって定義された multpos の値は使用される前に 4 行目によってVol. 44

No. SIG 13(PRO 18)

35

モデル検査技術を利用したプログラム解析器の生成ツール
表 1 java.math.* の無用命令の検出にかかった時間
Table 1 Dead code detection of java.math.*.

クラス名

SignedMutableBigInteger
BitSieve
BigDecimal
MutableBigInteger
BigInteger

サイズ（ bytes ）メソッド 数検出された
無用命令の数解析全体に使用された
時間（ sec ）

1,146
1,948
7,217
12,96628,888

8
10
35
50
104

0
0
0
11
14

1.81
5.77
26.70
167.96346.58

表 2 java.math.BitSieve に対する解析にかかった時間
Table 2 Analysis times for java.math.BitSieve.

AG !(def (x) & AX AG (def (x) & use(x)))
AG !(def (x) & AX AG (def (y) & use(y)))
AG !(def (x) & AX AG (def (y) & use(z)))

CTL-FV 中の自由変数の数
123

再定義されているのが分かる．よってこの 1 行目の代

全時間（ sec ）モデル検査時間（ sec ）6.32
106.17
7,137.79

1.97
52.46
3,953.41

実的でないが，通常プログラム解析の CTL-FV 式に入は無用命令である．これは Jimple 上での無用命令よる仕様では自由変数が 5 つ以上になることは稀であの検出の仕様として与えた式 dead-spec とは異なる

り，より速い環境では十分実用的な手法であるといえ仕様の無用命令であるが，このコード を変換した際 3

よう．

番地コード の Jimple では，

i13 = i2;
i39 = i2 + -1;
z0 = 1;

5. 関 連 研 究
文献 5) はプログラム最適化を CTL-FV 式で記述された条件付きの書き換え系により記述することによっ

i40 = i39 - i1;と変換され，i13 という二度と使われない変数が定義されてしまったために検出された無用命令である．なしないことを証明することができることを示した．そお，本ツールによってこれらのクラスのすべての無用

数の畳み込み（ constant folding ），ループ不変変数のて，その最適化がプログラムのセマンティクスを変更，定
こでは，無用命令の削除（ dead code elimination ）命令が検出されたかど うかは確認していないが，検出

巻き上げ（ loop invariant hoisting ）の 3 つのプログラされた結果はすべて無用命令であったことは確認した．

ム最適化の仕様を CTL-FV で与えており，CTL-FV

また，表 2 は 先の実験と同様の環境で ，サ イズ

がプログラム上の性質を簡潔に表現できることを示し

1,948 bytes，
メソッド数 10 のクラス java.math.BitSieveている．

に対して自由変数の数が異なる CTL-FV 式の解析をプログラム解析器の自動生成についての研究には，行ったときの測定結果である．3 種類の CTL-FV 式，

たとえば文献 8) がある．これはプログラム解析の仕AG !(def (x) & AX AG (def (x) & use(x))) ，AG !(def (x) & AX AG (def (y) & use(y))) ，プログラム解析を自動化できるというものであり，本様を Cecil という言語によって記述することで，そのAG !(def (x) & AX AG (def (y) & use(z)))

論文と非常に似ている．しかし，Cecil はプログラムを仕様として入力し，それぞれについて測定した．この経路の性質を正規表現で記述するものであり，表現

れらの式はプログラム解析としての実用性はないが，力は CTL-FV の E を除いたものに相当し，表現力にモデル検査での検証が失敗することがほとんどないた

制限がある．また，その実装はプログラムを抽象化しめ，自由変数の数以外の条件に解析時間があまり影響てモデルを得る部分と不動点計算を行うモデル検査にされないと考えられる．表には CTL-FV 式中の自由

明確に分離していないため拡張性に欠けている．

変数の数，解析にかかった全時間，解析にかかった時また，プログラム解析にモデル検査技術を利用する間のうちモデル検査に費やされた時間を示した．3 章

アイデアは文献 9)〜11) を参考とした．文献 11) はの実装では CTL-FV 式中の自由変数の数が増えるとコントロールフロー解析がモデル検査として見なせる

指数関数的に解析時間が長くなるはずであるが，このことを初めて指摘した．文献 9)，10) はさらに踏み込

表からもそれが確認できる．そのことから CTL-FV

んで，抽象解釈がモデル生成に対応し，そのモデル上

式中の自由変数の数が非常に多いときはこの方法は現でモデル検査を行うことがデータフロー解析やコント

36

Oct. 2003

情報処理学会論文誌：プログラミング

ロールフロー解析に対応していることを示している．

ルはモデルの状態を網羅的に検査しながら，与えられJava プログラム上でのモデル検査という研究につた仕様で検証すべき変数の束縛のみについて選択的にいては，Java プログラムのモデル検査による検証シ

検証し，同一の仕様で何度も同じ状態を検査するよう

ステム Bandera が文献 3) によって紹介されている．

なことはしないだろう．ただ，2 章で述べたように既Bandera は対象プログラムに特化した具体的な仕様し存のモデル検査ツールは非常に洗練されたアルゴ リズ

か受け入れられないところが本論文の手法と大きく異ムがいくつも実装されているので，これを拡張するのなる．Bandera においても既存のモデル検査ツールをは注意が必要と思われる．

そのまま利用しているが，その入力となるモデル生成
することについて力をいれている．この点においては

本ツールは対象プ ログラムが Jimple であったが，Java を Jimple に変換して本ツールに入力することによってクラスライブラリ中の無用命令をいくつか発見

今後おおいに参考になると考えている．また，今回は
2.1 節で述べた理由により解析の対象プログラムとし

で 3 番地コードである Jimple としているため，たとて Jimple を用いたが，Bandera においても Jimple

えば Java プログラムのスタック操作に関する解析なを利用している．Jimple はもともと McGill 大学で

どは本ツールでは扱うことができないと考えられる．

開発された Java バイトコード の最適化フレームワー

このことが Java プログラム解析に対して大きな障害において Java プログラムから生成するモデルを縮小

12)

クにおいて，プログラム解析および最適化用に利用される中間言語である．

6. 結

論

することができた．しかし，対象プログラムはあくまとなるかど うかまだよく分かっていない．

Java プログラム解析においては，解析結果を Javaのソースコード 上に反映したいという要求があると考えられる．前章で紹介した Java プログラムのモデル検

本論文では時相論理によって仕様が記述されたプロ査による検証システム Bandera は，Java ソースコー

グラム解析器生成ツールの，設計と実装について説明

ド を Jimple に変換して検証を行い，その結果を元のした．用いた時相論理 CTL-FV は論理式中にプログ

ソースコード 上で表示するということに成功している．

ラム中の情報を引用できるので，多くのプログラム解

それと同等なテクニックを用いれば，本ツールによっ析を自然に記述することができる．また，対象プログて得られた Java プログラムの解析結果をソースコー

ラムは世の中で広く使用されている Java と相互変換

ド 上で表示するということも可能だと思われる．

可能な Jimple プログラムとした．これらの特徴によ

その他重要な課題として，時相論理 CTL-FV によっり，本ツールは潜在的に多くの人が様々なプログラムて記述できるプログラム解析の性質の定式化について解析を試みるのに役立つことが考えれらる．現在の実の研究もいまだ残っている．今後はこれらの課題を解

装は約 500 行の Java プログラムで書かれたものであ決し，この手法でのプログラム解析の有効性をさらにり，実行効率向上の余地が多く残っているにもかかわ主張していきたい．

らず実験によって現実的な大きさのプログラムに対する解析にも利用できることが確かめられた．このこと
はモデル検査技術を利用するプログラム解析の自動生成が，潜在的に大きな可能性を持っていることを示しているといえる．
現在検討中の，より効率的な実装については大きく
2 通りの方向性があると考えられる．1 つはより縮小されたモデルを生成する方向性である．与えられた仕様に対してモデルを特化し，モデル検査ツールが仕様を検証するに十分な大きさにできるだけモデルを縮小することによって，モデル検査の効率を劇的に向上させることができると考えられる．
もう 1 つは CTL-FV の自由変数とプログラム中の変数を束縛する機構をモデル検査ツールに組み込むといった，プログラム解析に特化したモデル検査ツールを開発する方向性である．このようなモデル検査ツー

参 考

文

献

1) Aho, A. and Ullman, J.: Principles of Compiler Design, Addison-Wesley (1977).
2) Clarke, E., Grumberg, O. and Peled, D.:
Model Checking, MIT Press, Cambridge, Massachusetts (1999).
3) Corbett, J.C., Dwyer, M.B., Hatcliﬀ, J.,
Laubach, S., Păsăreanu, C.S., Robby andZheng, H.: Bandera: extracting ﬁnite-statemodels from Java source code, International
Conference on Software Engineering, pp.439–
448 (2000).
4) Holzmann, G.J.: The Model Checker SPIN,
Software Engineering, Vol.23, No.5, pp.279–295(1997).
5) Lacey, D., Jones, N.D., Wyk, E.V. and Frederiksen, C.C.: Proving correctness of compiler

Vol. 44

No. SIG 13(PRO 18)

モデル検査技術を利用したプログラム解析器の生成ツール

optimizations by temporal logic, Symposium on
Principles of Programming Languages, pp.283–
294 (2002).
6) McMillan, K.: Symbolic Model Checking,Kluwer Academic Publishers (1993).
7) 中田育男：コンパイラの構成と最適化，朝倉書店 (1999).
8) Olender, K. and Osterweil, L.: Cecil: A Sequencing Constraint Language for Automatic
Static Analysis Generation, IEEE Trans.Softw.
Eng., Vol.16, No.3, pp.268–280 (1990).
9) Schmidt, D.: Data Flow Analysis is Model
Checking of Abstract Interpretations, Proc.
25th ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages,
POPL’98, pp.38–48, ACM Press (1998).
10) Schmidt, D. and Steﬀen, B.: Program analysis as model checking of abstract interpretations, Static Analysis, Levi, G.(Ed.), Lecture
Notes in Computer Science, Vol.1503, pp.351–
380, Springer-Verlag (1998).
11) Steﬀen, B.: Data Flow Analysis as Model
Checking, Theoretical Aspects of Computer
Science, Lecture Notes in Computer Science,
Vol.526, pp.346–364, Springer-Verlag (1991).
12) Vallée-Rai, R., Co, P., Gagnon, E., Hendren,
L., Lam, P. and Sundaresan, V.: Soot — a Java
bytecode optimization framework (1999).
(平成 14 年 12 月 24 日受付)
(平成 15 年 7 月 1 日採録)

胡37

振江（ 正会員）

1966 年生．1988 年中国上海交通
大学計算機科学系を卒業．1996 年
東京大学大学院工学系研究科情報工学専攻博士課程修了．同年日本学術振興会特別研究員を経て，1997 年
東京大学大学院工学系研究科情報工学専攻助手，同年10 月同専攻講師，2000 年同専攻助教授．2001 年より東京大学情報理工学系研究科助教授，同年 12 月より
科学技術振興事業団さきがけ 21 研究者を兼任．博士（ 工学）．日本ソフトウェア科学会，ACM 各会員．
武市 正人（ 正会員）

1948 年生．1972 年東京大学工学部助手，講師，電気通信大学講師，
助教授，東京大学工学部助教授を経て，1993 年東京大学大学院工学系研究科教授（情報処理工学講座），2001
年より同大学大学院情報理工学系研究科教授，現在に至る．工学博士．プログラミング言語，関数プログラ
ミング，言語処理システムの研究・教育に従事．日本ソフトウェア科学会，日本応用数理学会，ACM 各会員．
小川 瑞史（ 正会員）

1985 年東京大学大学院理学系研
究科数学専攻修士課程修了．2002 年
博士（ 理学，東京大学・情報科学）
．

山岡 裕司

1985 年 NTT 武蔵野電気通信研究所

1978 年生．2001 年東京大学工学部機械情報工学科を卒業．2003 年
東京大学大学院情報理工学系研究科

析・検証・生成，書き換え系の研究に従事．現在，科数理情報学専攻修士課程修了．

客員研究員．日本ソフトウェア科学会，ACM 各会員．

入所．以来，関数型プログラムの解学技術振興事業団さきがけ 21 研究員および東京大学