(1)研究上の成果
[モードづけできないプログラムの解析]
これまで、モードづけ可能(well-moded)なプログラムについては、効率的な解 析アルゴリズムが確立していたが、モードづけできない(ill-moded)プログラ ムに対して、モード誤りの原因を効率良く特定する方法は確立していなかった。 モードづけできないとは、モード制約の論理積が全体として矛盾するというこ とであるが、そのことを指摘しただけでは、大きなプログラムのデバッグには ほとんど役に立たない。
そこで、全体として矛盾している制約集合の中から、矛盾する極小の部分集合 を効率よく見つけ出すアルゴリズムを開発し、それに基づき、矛盾する制約を 課したプログラム中の記号(または記号出現)を提示する方式を開発した。これ によって、バグの可能性のある箇所をかなり絞り込んで提示することが可能に なった。
極小集合は、プログラムの大きさと極小集合の大きさとにほぼ比例する手間で 探索できる。実験によれば、極小集合の大きさは、プログラムの大きさによら ない小さな定数で抑えることができる。
さらに、互いに共通部分を持たない複数の極小部分集合を見つけ出すことで、複 数のバグが一回の解析で検出できることもわかった。
大規模なプログラムの場合には、プログラムの層化構造にしたがった解析によ り、探索空間を狭めることができ、また、より直観的な説明を得ることができ る。
本年度は、以上の機能を実現するために、まずモードづけできないプログラム について、矛盾するモード制約の極小集合を求めるアルゴリズムを実装し、既 存の klint 処理系と結合した。また、これを拡張することにより、重なりを もたない複数の極小集合を求めるアルゴリズムを実装した。
さらに、求まった極小集合の中から、バグの真の原因となっている制約式を絞 り込むアルゴリズムをいくつか提案し、比較検討した。それらは、次のような ヒューリスティクスに基づいている:
| 方針1 | その制約式を除くだけで、全体が矛盾しなくなる制約式は、原因とし て疑わしい |
| 方針2 | ある単一バグに対して、いくつかの極小部分集合が考えられる場合、 それらの極小部分集合の多くに含まれる制約式は、原因として疑わしい |
| 方針3 | 求まった極小集合の補集合と矛盾する制約は疑わしい |
[バグの自動修正]
モード誤りの原因となっている制約式が特定できると、その制約式を課したプ ログラム中の記号ないしは記号出現も特定できる。すると、モード情報に基づ いて、プログラムのバグを機械的に修正することが考えられる。
ここで考えるプログラムのバグとは、「変数や定数のN個以内の書き誤 り」のことである。これを ニアミスという。
自動修正アルゴリズムは、プログラム中の記号の追加や削除によってモード誤 りを除去する方法を深さ漸増探索する。本年度は、プログラムを木構造と見立 てた場合の終端記号、すなわち変数や定数の修正を中心に考察した。
個々の修正案すべてに対してモードを求めると計算量が大きくなる危険がある が、ヒューリスティクスの利用により、探索空間および計算時間の増大を抑え ている。
現在はデータ型情報を利用していないが、型情報の利用によって、さらに探索 空間を縮小し、修正案の品質を向上させることができる。またこれによって、 非終端記号（関数記号やゴール）の追加削除の探索もより現実的になってくる と考えられる。
これまでの実験で、多くの場合、正しい修正案が最初に発見されることがわかっ た。しかし、モード制約に冗長性がないプログラムなどについては、モード的 に正しい複数の修正案が呈示されることもある。
[制約に基づく解析の最適化への応用]
静的解析の応用として昨年度はジェネリックオブジェクトの最適化を検討した が、本年度は分散 KLIC 処理系のプロセッサ間通信の最適化の検討を行なった。
モード、型、参照数の 3 種類の基本情報を制約ベースの解析で得ることによ り、分散 KLIC 処理系の通信プロトコルの単純化を行なうことができる。本年 度は、その初期検討を行なった。現段階ではまだ詳細な評価データは得られて いないが、12-queens 問題を 2 プロセッサで実行した場合の評価では、通常 転送モードの場合と比べ、転送バイト数で 1/5 に、メッセージ数で 1/10 以 下に減少した。バッチ転送モードと比べても、転送バイト数は 56% に、メッ セージ数は60% に減少した。
(2) ソフトウェアとしての成果
公開中の静的解析ツール klint 第 1 版をもとに、ill-moded な KL1 プログ ラムの解析システム kima を作成した。kima は、これまでに提案したバグ探 索アルゴリズムおよび修正アルゴリズムの中で、比較的少ない計算量で実際の デバッグに役立つものを実装している。
kima は以下の機能を備える:
kimaは、KL1ソースプログラムからモード制約を抽出するklint101、および klint101から得られた制約を解析するkima2から構成される(図-1)。
|
プロセス構造認識は、各述語の呼出し関係を認識して述語グラフを生成し、述 語グラフをTarjanによる深さ優先探索による分割アルゴリズムによって強連結 成分に分割することによって行なう。
kima を用いることで、従来の処理系では動的なエラーとしてしか検出できな かった多くのバグを、静的に検出することが可能になる。しかも、多くの場合、 そのバグの存在するプログラムソース上での箇所を特定することができるため、 デバッグはより容易になる。
また、これらの解析は、プログラムの仕様を与えたり、モード宣言を行なった りすることなく行なうことができる。そのため、ユーザにかかる負担は少ない。
図-2 に、kima によるデバッグ例を示す。 Mode Error の行の下に表示されている4個のモード制約が、一つの 極小部分集合である。そのうち最初の ! のついた制約が、最も疑わ しい制約である。この制約は、誤りの箇所(4引数の fib の第2節の、 fib の第4引数として現れる変数 N1 )を正しく同定してい る。! のついた制約の下の行は、kima の提示した修正案である。正 しい修正法( Ns1 に書き直す)を示している。
 |
kima は単純な変数名の書き誤りなど、プログラムの意図を知るプログラマが 見ればすぐに分かるが、KL1 の文法としては間違っていないため、実行は可能 になってしまうようなバグを、プログラムを実行する前に発見するという機能 に重点を置いている。変数名の書き換えの候補を提示する機能を採用した理由 も、KL1 プログラムを書いていると極めてよく発生するわりに、実行時エラー からソース上のバグを発見するのが難しい、変数名の書き間違いというバグを 特定したかったためである。
kima の採用しているアルゴリズムは、少ない計算量で多くのバグの箇所を正 確に指摘できるように考えられている。しかし、いくつかの場合にそのアルゴ リズムが利用しているいくつかの仮定が成り立たないため、バグの箇所が特定 できないこともある。
kima はすべて KL1 で記述してあり、行数は 3000 行強である。使用説明書も ほぼ完成している。
(3) 残された課題
本年度までの研究で、制約に基づくプログラム解析を用いた静的デバッグは、 技術的にほぼ確立したと言える。KL1 が Flat GHC から拡張した機能について は、ベクタの解析のサポートが最重要である。技法は開発済であるので早急に 対応する予定である。
今後の静的デバッグと最適化の研究開発のためには、 モード解析とともに、 型および参照数の解析も重要であるので、それらの実装もあわせて進めてゆく 必要がある。それに基づき、プログラムの自動修正技術の一般化、高度化を検 討してゆきたい。
(4) 評価
制約に基づく静的デバッグ技術は、Moded Flat GHCのために開発したものであ るが、論理型に限らず、強い型体系をもつプログラミング言語の静的デバッグ に広く適用できる汎用の技術であり、言語パラダイムを越えて、今後の幅広い 実用化が期待できる。
また、これまでの静的解析がバグ検出に主眼をおいていたのに対し、本年度の 研究でバグ修正に踏み込むことができたのは収穫であった。ただし、この研究 は始まったばかりであり、課題も多く残されている。
分散処理系の通信最適化への応用については、「解析情報が有用である」とい う一般論から具体的設計へとようやく踏み出した段階である。プロセッサ台数 が価格に直接反映する並列処理環境においては、手続き型並列言語との性能の 違いを小さくすることは必須である。この観点から、並列論理型言語の実装の 研究開発に関しては、まだなすべきことが非常に多く残っている。