next up previous
Next: 残された課題 Up: 研究の成果 Previous: 制約に基づく解析の最適化への応用

ソフトウェアの成果

公開中の静的解析ツールklint第1版をもとに、klint第2版を作成した。klint第2 版は、

の三者からなっている。

制約生成系は、与えられたプログラムモジュールの中の各記号(ないしは記号出 現)が課するモード制約、型制約、参照数制約を抽出し、標準出力ファイルに書 き出す。klint第1版からの大きな改良点として、型や参照数情報の抽出が可能に なったこと以外に、現在のKLICがサポートしている組込み機能のほとんどに対応 したことが挙げられる。主な改良点は次の通りである:

また、組込み述語は多相(polymorphic)述語としてサポートしており、異なる述 語呼出しは異なるモード制約や型制約をもつことができる。

モード制約解析系は、新たに参照数制約解析機能を追加して、モード・参照数制 約解析系となった。両者を一体としたのは、参照数解析がモード情報を利用する からである。本解析系は、non-binaryな制約の解析能力をklint第1版よりも強化 している。具体的には、プログラム節に3回以上出現する変数は、ほとんど例外 なく単方向通信に用いているという観察に基づき、最汎ではないが単純で実際的 な解を具体的に求めるようにした。これにより、non-binaryな制約が解けないで 解析が終了することがほとんどなくなった。

型解析は、モード解析や参照数解析とは独立に行なうことができる。klint第2版 においては、プログラマに型宣言をさせるのではなく、整数、浮動小数点数、ス トリング、ベクタ、非空リスト、空リスト、上記以外の定数(0引数関数)、上記 以外の関数(1引数以上)のうちのどのカテゴリのデータが各パスに出現しうるか を解析して出力する。型宣言を許すように拡張することは困難でない。

klint第2版ははすべてKL1で記述してあり、行数は約2500行である。



next up previous
Next: 残された課題 Up: 研究の成果 Previous: 制約に基づく解析の最適化への応用



www-admin@icot.or.jp