(57)【要約】計算機プログラムのソースコードが意味するプログラムの振る舞いに関する諸性質を検査するソースコード検査器及びソースコード検査方法、当該方法を実行させるプログラム、当該プログラムを格納する記憶媒体が開示されている。このソースコード検査方法は、パス抽出ステップと、検査内容決定ステップと、を含む。パス抽出ステップは、あらかじめ入力された計算機用プログラムのソースコードによって記述されたプログラムを模擬に実行することで実際に実行される命令列を抽出する。検査内容決定ステップは、パス抽出ステップで抽出した命令列に基づいてソースコードの検査内容を決定する。【特許請求の範囲】
【請求項１】
あらかじめ入力された計算機用プログラムのソースコードによって記述されたプログラムを模擬に実行することで実際に実行される命令列を抽出するパス抽出ステップと、前記パス抽出ステップで抽出した命令列に基づいて前記ソースコードの検査内容を決定する検査内容決定ステップと、を含むソースコード検査方法。
【請求項２】
前記検査内容決定ステップは、モデル記述と前記ソースコードを検査する性質を表す仕様とにより前記ソースコードのモデル検査を行うモデル検査実行ステップに前置し、前記パス抽出ステップで抽出した命令列からモデルグラフを構成するモデルグラフ構成ステップと、前記モデルグラフ構成ステップで構成したモデルグラフからモデル記述を生成するモデル記述生成ステップと、を備え、前記モデル記述生成部が生成したモデル記述とあらかじめ入力された仕様とにより前記モデル検査実行ステップで前記ソースコードの検査を行う請求項１記載のソースコード検査方法。
【請求項３】
前記パス抽出ステップは、前記ソースコードを論理式に変換し前記論理式の充足可能性判定を行うことで前記実際実行される命令列を抽出する請求項１記載のソースコード検査方法。
【請求項４】
前記仕様を自動で生成する仕様自動生成ステップをさらに含み、前記あらかじめ入力された仕様は、前記仕様自動生成ステップで生成した仕様である請求項２記載のソースコード検査方法。
【請求項５】
前記仕様自動生成ステップは、前記ソースコードによって記述されたプログラムがメモリの不正使用を行わないことを意味する仕様を自動生成する請求項４記載のソースコード検査方法。
【請求項６】
前記検査内容決定ステップは、前記パス抽出ステップで抽出した命令列がメモリの不正使用を行わないかどうかを検証するための検証プログラムを生成する検証プログラム生成ステップと、前記検証プログラム生成ステップで生成した検証プログラムを実行する検証プログラム実行ステップと、を含む請求項１記載のソースコード検査方法。
【請求項７】
コンピュータにソースコード検査方法を実行させる方法実行プログラムであって、前記方法は、
あらかじめ入力された計算機用プログラムのソースコードによって記述された応用プログラムを模擬に実行することで実際に実行される命令列を抽出するパス抽出ステップと、前記パス抽出ステップで抽出した命令列に基づいて前記ソースコードの検査内容を決定する検査内容決定ステップと、を有する。
【請求項８】
コンピュータにソースコード検査方法を実行させる方法実行プログラムを格納する記憶媒体であって、前記方法は、
あらかじめ入力された計算機用プログラムのソースコードによって記述された応用プログラムを模擬に実行することで実際に実行される命令列を抽出するパス抽出ステップと、前記パス抽出ステップで抽出した命令列に基づいて前記ソースコードの検査内容を決定する検査内容決定ステップと、を有する。
【請求項９】
あらかじめ入力された計算機用プログラムのソースコードによって記述されたプログラムを模擬に実行することで実際に実行される命令列を抽出するパス抽出部と、前記パス抽出部が抽出した命令列に基づいて前記ソースコードの検査内容を決定する検査内容決定部と、を備えるソースコード検査器。
【請求項１０】
前記検査内容決定部は、モデル記述と前記ソースコードを検査する性質を表す仕様とにより前記ソースコードのモデル検査を行うモデル検査器実行部に前置し、
前記パス抽出部が抽出した命令列からモデルグラフを構成するモデルグラフ構成部と、前記モデルグラフ構成部が構成したモデルグラフからモデル記述を生成するモデル記述生成部と、を備え、前記モデル記述生成部が生成したモデル記述とあらかじめ入力された仕様とにより前記モデル検査器実行部で前記ソースコードの検査を行う請求項９記載のソースコード検査器。
【請求項１１】
前記パス抽出部は、前記ソースコードを論理式に変換し前記論理式の充足可能性判定を行うことで前記実際に実行される命令列を抽出する請求項９記載のソースコード検査器。
【請求項１２】
前記仕様を自動で生成する仕様自動生成部をさらに備え、前記あらかじめ入力された仕様は、前記仕様自動生成部が生成した仕様である請求項１０記載のソースコード検査器。
【請求項１３】
前記仕様自動生成部は、前記ソースコードによって記述されたプログラムがメモリの不正使用を行わないことを意味する仕様を自動生成する請求項１２記載のソースコード検査器。
【請求項１４】
前記検査内容決定部は、前記パス抽出部で抽出した命令列がメモリの不正使用を行わないかどうかを検証するための検証プログラムを生成する検証プログラム生成部と、前記検証プログラム生成部が生成した検証プログラムを実行する検証プログラム実行部と、を備えた請求項９記載のソースコード検査器。
【発明の詳細な説明】
【技術分野】
【０００１】  本発明は、計算機プログラムのソースコードが意味するプログラムの振る舞いに関する諸性質を検査するソースコード検査器及びソースコード検査方法、当該方法を実行させるプログラム、当該プログラムを格納する記憶媒体に関する。
【背景技術】
【０００２】  従来のソースコード検査器として、ソースコードが意味するプログラム（以下、応用プログラムとも記す）の振る舞いに関する諸性質を検査するソースコード分析器がある。ソースコード分析器の例としては、モデル検査技術を用いてソースコードを分析するソースコードモデル検査器がある。【０００３】  ソースコードが意味する応用プログラムの振る舞いとは、ソースコードに記述された一連の命令に従う、プログラムの一連の動作を意味する。この振る舞いに関する諸性質の例として、メモリを動的に確保した場合は必ずそのメモリを解放する性質、プログラム中のある命令を実行した場合は必ずいつか対応する特定の命令を実行する性質などが挙げられる。【０００４】  モデル検査とは、検査する性質を表す仕様と検査の対象となるモデルとを入力とし、モデルが仕様の表す性質を有するかどうかを判定することである。モデル検査を行う装置をモデル検査器と呼び、検査の対象となるモデルを記述したものをモデル記述と呼ぶ。モデルを記述するための言語は、モデル検査器によって様々に異なる。例えば、モデル検査器ＳＰＩＮの場合、モデルを記述するための言語はプロメラ（Ｐｒｏｍｅｌａ）と呼ばれるものである。【０００５】  モデル検査器ＳＰＩＮは、有限状態遷移系としてモデル化したシステムが線形時間論理式で記述された検査式を満たすかを全状態検索で網羅的に検査する検査器である。モデル検査器ＳＰＩＮは、例えば、Ｇｅｒａｒｄ  Ｊ．Ｈｏｌｚｍａｎｎ，’Ｔｈｅ  ｍｏｄｅｌ  Ｃｈｅｃｋｅｒ  Ｓｐｉｎ’，ＩＥＥＥ  Ｔｒａｎｓ，Ｏｎ  Ｓｏｆｔｗａｒｅ  Ｅｎｇｉｎｅｅｒｉｎｇ，Ｖｏｌ．２３，Ｎｏ．５，Ｍａｙ  １９９７，ｐｐ．２７９−２９５に開示されている。【０００６】  ソースコードモデル検査とは、ソースコードを検査の対象としたモデル検査を指し、論理回路などハードウェアを対象とするモデル検査であるハードウェアモデル検査との対比のため用いる語である。【０００７】  従来のソースコード検査器としては、ソースコードをモデル検査器の入力言語に翻訳するための変換表を用いるものがある。この構成は、例えば、米国特許出願公開第２００１／０３７４９２号、米国特許出願公開第２００２／１０００２２号に開示されている。図１４は、米国特許出願公開第２００１／０３７４９２号に記載された従来のソースコード検査器の構成を示すブロック図である。【０００８】  図１４に示す従来のソースコード検査器であるモデル検査器は、検査の対象となるソースコード１３０１をソースコード入力部１３０２から入力する。次に、このソースコード検査器は、ソースコード変換テーブル生成部１３０３において、ソースコード入力部１３０２によって受け入れたソースコード１３０１を基に制御フローグラフを構成する。そして、その制御フローグラフから検査の対象となるソースコード１３０１の各文について、対応するモデル記述言語、例えばプロメラの記述で書かれた対訳例を集めたソースコード変換テーブル１３０４を生成する。【０００９】  次に、モデル記述生成部１３０５が、ソースコード変換テーブル１３０４に含まれる対訳例を用いてソースコード１３０１をモデル記述言語に変換する。また、仕様入力部１３０７は、入���された検査するソースコード１３０１の性質を表す仕様を記載した検査する仕様１３０８をモデル検査器実行部１３０６へ渡す。そして、モデル検査器実行部１３０６が、仕様入力部１３０７からの仕様１３０８と、モデル記述生成部１３０５において生成されたモデル記述とを用いてモデル検査を実行し、検査結果１３０９を出力する。【００１０】  また、自動的に生成されたソースコード変換テーブル１３０４がソースコードモデル検査器の使用者の意に沿わない場合、使用者の修正手段１３１０がソースコード変換テーブル１３０４を適宜修正する必要がある。それは、例えば、検査の対象となるソースコード１３０１が、そのソースコード以外のもの、例えば外部モジュールとの通信など、を扱う場合などである。ソースコード変換テーブル生成部１３０３が適正な翻訳例を示すことができない場合も多く、これを使用者が補う必要がある。【００１１】  ソースコードモデル検査で用いるプロメラなどのモデル記述言語と、ソースコードを記述している例えばＣ言語などのプログラミング言語とでは表現力が違う。具体的には、プログラミング言語では記述できて、モデル記述言語では記述できない遷移条件が存在する。このため、ソースコードの意味する振る舞いをモデル記述言語に正確に翻訳することが本質的に困難であり得、適切なソースコード変換テーブルを生成することが困難な場合が多い。よって、検査の対象となるソースコードの意味する振る舞いを正確に再現するモデル記述が得られず、不正確な検査になる場合が多いという問題があり得る。【００１２】  詳細に説明すると、モデル検査は、モデルの記述を基にラベル付き有向グラフを生成し、このグラフが例えば線形時間論理式などで与えられる仕様の意味する制約を満たしているかどうかを判定する、という手順で行われる。線形時間論理式とは、命題論理式に時間の概念を追加して構成されるもので、状態遷移モデルを形式的に記述する際等で広く用いられている。【００１３】  ラベル付き有向グラフとは、頂点と辺の集合からなる。各辺は２頂点間の関係を表し、頂点同士を結ぶ辺には向きが存在する。すなわち、ラベル付き有向グラフには、辺の起点、および終点に一つずつ対応する頂点が存在し、各頂点にはラベルが付記されている。【００１４】  ラベル付き有向グラフの各頂点を状態とみなし、辺の向きに沿って頂点を移動することを状態遷移とみなすとき、ラベル付き有向グラフは状態遷移図とみなすことができる。各頂点のラベルは、各状態で生起されるイベントであるとみなすことができる。そして、モデル検査は、そのイベントの生起の列が与えられた仕様の制約を満たしているかどうかを判定する。【００１５】  しかしながら、ラベル付き有向グラフは、遷移条件が存在しない。遷移条件とは、ある頂点を起点とした複数の辺があるとき、どの辺の終点の頂点に遷移するべきかを判断する条件である。遷移条件が存在しないということは、ある頂点を起点とした複数の辺があるとき、どちらの辺の頂点に対応する状態を次の状態とみなすかは任意に選択可能であるということを意味する。モデル検査は通常、検査する仕様の制約に違反しているかどうかを確認するため、任意に選択可能な遷移先については、常に最悪の���合を選択する。【００１６】  しかしながら、ソースコードが意味する振る舞いを表す状態遷移図は、一般に遷移条件付きラベル付き有向グラフで表される。例えばｉｆ文などで表される条件節は、その条件式の真偽によって次状態が決定される。【００１７】  以上の理由から、遷移条件のないラベル付き有向グラフによって意味づけられるモデル記述言語と、遷移条件付きラベル付き有向グラフによって意味づけられる一般のプログラミング言語との間を逐語訳で変換することは本質的な困難さを伴うという問題があり得る。また、従来の方法では、検査器の使用者がソースコード変換テーブルを修正することは困難であり得る。【００１８】  詳細に説明すると、検査器の使用者はソースコード変換テーブルの修正を行う際、変換テーブルに記述されたモデル記述を理解する必要がある。さらに、ソースコードの意味する応用プログラムの振る舞いを正確に反映していない箇所を特定する必要があり、その箇所について代替となる翻訳を与える必要がある。また、検査の対象となるソースコード以外の部分について、モデル検査が適切に行われるように配慮しながら、その部分を補完するモデル記述を与える必要がある。これは使用者がモデル検査の専門家であったとしても、困難さや煩雑さを伴う作業となり得る。
【発明の開示】
【００１９】  本発明は、検査の対象となるソースコードの意味する振る舞いをより正確に検査するソースコード検査器及びソースコード検査方法、当該方法を実行させる方法実行プログラム、当該プログラムを格納する記憶媒体を提供する。
【００２０】  本発明は、あらかじめ入力された計算機用プログラムのソースコードによって記述された応用プログラムを模擬に実行することで実際に実行される命令列を抽出するパス抽出ステップと、パス抽出ステップで抽出した命令列に基づいてソースコードの検査内容を決定する検査内容決定ステップと、を含むようにした。本発明によれば、ソースコードの意味する振る舞いをより正確に検査することができる。
【図面の簡単な説明】
【００２１】
【図１】図１は本発明の第１実施例におけるソースコード検査器を含むソースコード検査システムのブロック図である。
【図２】図２は同実施例における検証の対象となるソースコードの例を示す図である。
【図３】図３は図２で示したソースコードを基に構成した制御フローグラフを示す図である。
【図４】図４は図２で示したソースコードをパス抽出用に改変したソースコードを示す図である。
【図５】図５は図２で示したソースコードからパスを抽出した結果を基に構成したモデルグラフを示す図である。
【図６】図６は図５のモデルグラフを基に生成したモデル記述を示す図である。
【図７】図７は本発明の第２実施例に係わり、図２で示したソースコードを、ＣＢＭＣを用いたパス抽出用に改変したソースコードを示す図である。
【図８】図８は本発明の第３実施例におけるソースコード検査器を含むソースコード検査システムのブロック図である。
【図９】図９は本発明の第４実施例におけるソースコード検査器のブロック図である。
【図１０】図１０は同実施例における検証プログラムの例を示す図である。
【図１１】図１１は同実施例における、検証プログラムの一部を示す第１の図である。
【図１２】図１２は同実施例における、検証プログラムの一部を示す第２の図である。
【図１３】図１３は同実施例における、検証プログラムの一部を示す第３の図である。
【図１４】図１４は従来のソースコード検査器の構成を表すブロック図である。
【符号の説明】
【００２２】  １００，６００  ソースコード検査システム
１０２  ソースコード入力部
１０３  パス抽出部
１０４  モデルグラフ構成部
１０５  モデル記述生成部
１０６  モデル検査器実行部
１０７  仕様入力部
１２０，１２２  検査内容決定部
１３０，１３１，７００  ソースコード検査器
１４０  制御部
１５０  記憶媒体
６０１  仕様自動生成部
７０１  検証プログラム生成部
７０２  検証プログラム実行部
【発明を実施するための最良の形態】
【００２３】  本発明のソースコード検査方法は、パス抽出ステップと、検査内容決定ステップと、を含む。パス抽出ステップは、あらかじめ入力された計算機用プログラムのソースコードによって記述された応用プログラムを模擬に実行することで実際に実行される命令列を抽出する。検査内容決定ステップは、パス抽出ステップで抽出した命令列に基づいてソースコードの検査内容を決定する。【００２４】  これにより、検査の対象とするソースコードの意味するプログラムの振る舞いを逸脱することなく、ソースコードの検査を行うことができる。【００２５】  また、本発明のソースコード検査方法は、検査内容決定ステップが、モデル記述とソースコードを検査する性質を表す仕様とによりソースコードのモデル検査を行うモデル検査実行ステップに前置し、モデルグラフ構成ステップと、モデル記述生成ステップと、を含むようにしてもよい。モデルグラフ構成ステップは、パス抽出ステップで抽出した命令列からモデルグラフを構成する。モデル記述生成ステップは、モデルグラフ構成ステップで構成したモデルグラフからモデル記述を生成する。モデル記述生成部が生成したモデル記述とあらかじめ入力された仕様とによりモデル検査実行ステップでソースコードの検査を行うようにしてもよい。【００２６】  この方法によれば、モデル検査手法を用いて、さらに検査の対象とするソースコードの意味するプログラムの振る舞いを逸脱するモデル記述が生成されることがなくなる。このため、検査の対象とするソースコードの意味するプログラムの振る舞いを逸脱した部分に対応するモデル記述によって引き起こされる、誤った異常な検出が行われなくなる。すなわち、本発明の方法では、ソースコードの振る舞いを逸脱するモデル記述が存在しない。このため、元々のソースコードの振る舞いでは検査対象の仕様の制約を満たしていたにもかかわらず、仕様を満たさないという誤った検査結果を報告されることがなくなる。また、モデル検査を行う前にモデルグラフを抽出しておくことで、モデルグラフを縮退させるなどの効率化手段を適用する余地を残すことが可能となる。【００２７】  また、本発明のソースコード検査方法は、パス抽出ステップが、ソースコードを論理式に変換し、論理式の充足可能性判定を行うことでソースコードの実行される可能性のある命令列を抽出するようにしてもよい。【００２８】  この方法によれば、さらに検査の対象とするソースコードで与えられるプログラムを模擬に、すなわち、条件文が成り立つか成り立たないかを充足可能性判定していくことにより、プログラムの振る舞いを抽出することができる。このように、検証の対象とするソースコードをコンパイル、リンクして実行可能にする必要がないため、例えばリンクなどができない、一連のソースコード群から一部のソースコードの集合だけを対象としたモデル検査を行うことが可能となる。【００２９】  また、本発明のソースコード検査方法は、仕様を自動で生成する仕様自動生成ステップをさらに含み、あらかじめ入力された仕様は、仕様自動生成ステップで生成した仕様であるようにしてもよい。【００３０】  この方法によれば、さらに仕様を手で入力する必要とがなくなる。つまり、煩わしく、とき��専門知識を要する仕様の手入力を必要としなくなる。【００３１】  また、本発明のソースコード検査方法は、仕様自動生成ステップが、ソースコードによって記述されたプログラムがメモリの不正使用を行わないことを意味する仕様を自動生成するようにしてもよい。【００３２】  この方法によれば、さらにメモリの不正使用に関する知識を必要とせず、メモリの不正使用に関するモデル検査を行うことが可能となる。また、仕様の手入力を必要とせず、プログラムのメモリの不正使用に関する検査を行うことができるようになる。【００３３】  さらに、本発明のソースコード検査方法は、検査内容決定ステップが、検証プログラム生成ステップと、検証プログラム実行ステップと、を含むようにしてもよい。検証プログラム生成ステップは、抽出された命令列がメモリの不正使用を行わないかどうかを単独で判定するための検証プログラムを生成する。検証プログラム実行ステップは、生成された検証プログラムを実行する。【００３４】  これにより、モデル検査実行ステップせずソースコードの検査を行うことができる。すなわち外部のモデル検査方法を用いる必要がなくなるため、可搬性、および利便性が向上する。【００３５】  本発明の方法実行プログラムは、コンピュータに上記ソースコード検査方法を実行させるプログラムである。また、本発明の記憶媒体は、上記方法実行プログラムを格納する記憶媒体である。【００３６】  以下、本発明の実施例について、図面を参照しながら説明する。【００３７】  （第１実施例）
本発明の第１実施例にかかるソースコード検査器を含むソースコード検査システムについて、図１を用いて説明する。図１は、第１実施例におけるソースコード検査器を含むソースコード検査システムのブロック図である。【００３８】  第１実施例にかかるソースコード検査システム１００は、コンピュータシステムであって、ソースコード検査器１３０と、モデル検査器１０６と、仕様入力部１０７とを備える。ソースコード検査器１３０は、ソースコード入力部１０２と、パス抽出部１０３と、検査内容決定部１２０と、制御部１４０と、記憶媒体１５０とを備える。検査内容決定部１２０は、モデルグラフ構成部１０４と、モデル記述生成部１０５とを備える。【００３９】  ソースコード入力部１０２は、計算機用のプログラムであるソースコード１０１を入力する。パス抽出部１０３は、ソースコード入力部１０２によって受け入れられたソースコード１０１の実行される可能性のある命令列を抽出し、抽出した命令列をモデルグラフ構成部１０４に送る。モデルグラフ構成部１０４は、パス抽出部１０３で抽出されたパスの情報をグラフとしてまとめ、まとめたグラフをモデル記述生成部１０５に送る。【００４０】  モデル記述生成部１０５は、モデルグラフ構成部１０４において構成されたグラフを基にモデル記述を生成し、生成したモデル記述を、ソースコード検査器１３０の外部にあるモデル検査器実行部１０６に送る。【００４１】  制御部１４０は、記憶媒体１５０に記憶されたソースコード検査方法を実行させる方法実行プログラムにより、ソースコード検査器１３０の各部を制御する。記憶媒体１５０は、ハードディスク記憶装置や半導体メモリ、ＣＤ−ＲＯＭなどで構成される。【００４２】  モデル検査器実行部１０６は、仕様入力部１０７から受け入れた検査するソースコード１０１の性質を表す制約を記載した検査する仕様１０８と、モデル記述生成部１０５において生成されたモデル記述とを用いてモデル検査を実行し、検査結果１０９を出力する。上記制御部１４０は、記憶媒体１５０に記憶されたプログラムによって、モデル検査器実行部１０６を制御するようにしてもよい。ソースコード検査器の各部は、ランダムロジックを用いたハードウエアで構成しても、コンピュータに実行させるソフトウエアで構成しても、あるいはそれらの混成であってもよい。【００４３】  次に、パス抽出部１０３について詳細に説明する。【００４４】  パス抽出部１０３では、まず検査の対象となるソースコード１０１を基に、その制御フローグラフを構成する。【００４５】  制御フローグラフとは、ソースコード１０１の制御構造を表現したものであり、処理ブロックノード、判定ノード、合流ノードの三つの基本要素から成るグラフである。処理ブロックノードとは、判定による分岐のない連続したソースコードの命令列に対応するグラフの頂点である。判定ノードとは、ある式の真偽値によって実行する命令列が分岐する点を意味するグラフの頂点である。合流ノードとは、複数の命令列が合流する点を意味するグラフの頂点である。【００４６】  図２に本実施例におけるソースコードの例、図３に図２のソースコードに基づいて構成した制御フローグラフの例をそれぞれ示す。【００４７】  図３は処理ブロックノード３０１、３０３、３０５、および３０６と、判定ノード３０２と、合流ノード３０４と、各ノードをつなぐ有向辺とからなる。【００４８】  パス抽出部１０３は、このような制御フローグラフを生成する。【００４９】  次に、パス抽出部１０３は、構成した制御フローグラフに基づいた実行されうる命令列の抽出、すなわち実行パス抽出する。ここではＣ言語に基づいた実行パス抽出例を示すが、Ｃ言語に限らず、Ｃ＋＋やＪａｖａ（登録商標）などの言語においても同様の方法によって命令列を抽出することができる。【００５０】  パス抽出部１０３は、検査の対象となるソースコード１０１を改変し、改変されたソースコードをコンパイルし、実行することによって実行パス抽出を行う。パス抽出部１０３が行うソースコード１０１の改変は、実行される命令列を抽出するためのものであり、元のソースコード１０１が意味する振る舞いには影響を与えない。すなわちパス抽出部１０３は、ソースコード１０１を模擬に実行し、そこで実行された命令列を抽出する。【００５１】  以下、パス抽出部１０３の処理について、図３および図４を用いて具体的に説明する。図４は図２に示したソースコードを実行パス抽出のために改変した例を示す図である。【００５２】  ４０１で示される文はフラグ変数を定義、初期化する文である。４０２で示される文は開始点を表すラベルと変数定義に含まれる初期化文である。４０３で示される文は不定値を持つ変数を改変する関数である。４０４で示される文は分岐命令に対応したフラグ変数に１を代入する文である。４０５で示される文はフラグ変数が全て１かどうかを判定する関数である。【００５３】  まず、パス抽出部１０３は、制御フローグラフに含まれる判定ノードの数と同じ数のフラグ変数をグローバル変数定義領域に定義する。図４の例では、パス抽出部１０３は、ｉｎｔ  ｍａｉｎ（）｛から始まって、この｛に対応する最後の｝で終わる領域の外、つまり４０１のある所か、最後の｝の下の領域に、グローバル変数定義領域を定義する。【００５４】  フラグ変数は、それぞれ異なる名前を持ち、０で初期化され、０あるいは１の２値を格納する領域を持つグローバル変数であるとする。例えば、制御フローグラフに含まれる判定ノードが三つである場合、パス抽出部１０３は、改変するソースコードの冒頭のグローバル変数定義領域に、「ｉｎｔ  ｆｌａｇ１＝０，ｆｌａｇ２＝０，ｆｌａｇ３＝０；」と記述する。【００５５】  次に、パス抽出部１０３は、制御フローグラフに含まれる判定ノード３０２のそれぞれについて、一つの分岐を選び、分岐先の処理ブロックノード３０３に対応する命令列（ｆｒｅｅ（ｐ）；）の先頭に、フラグ変数に１を代入する命令文４０４を挿入する。【００５６】  パス抽出部１０３は、一度使用したフラグ変数は用いずに、フラグ変数に１を代入する操作を繰り返す。また、パス抽出部１０３は、それぞれの判定ノードに対応する分岐命令文の直前に、不定値となっている変数を実行パス探索のために改変する関数４０３を挿入する。【００５７】  不定値となる変数は、ソースコード記述範囲外からの入力、例えばプログラム使用者から入力、によって改変される値や乱数によって決定される���、そしてその値に依存して決定される値を持つ変数を意味する。データフロー解析によってそれぞれの変数が不定値を持つかどうかを判定することができる。【００５８】  挿入する関数は、対応する分岐命令文に含まれる不定値となっている変数を引数にとり、それぞれの変数の値を改変する。またこの関数は、呼び出されるたびに異なる値の組み合わせを、引数で与えられたそれぞれの変数に代入する。【００５９】  次に、パス抽出部１０３は、ソースコード１０１中の、変数定義文を除いて最初に実行される命令に対応する命令文（図４中の４０２で示される部分の直後にあるｐ＝ｍａｌｌｏｃ（ｓｉｚｅｏｆ（ｃｈａｒ）））の前に、開始点を表すラベル（４０２で示される一行目、ｉｎｉｔ＿ｐｏｉｎｔ）を挿入し、そのラベルを挿入した場所の直後に、変数定義文中に含まれる変数の初期化命令（４０２で示される部分の二行目、ｐ＝０；）を追加する。【００６０】  次に、パス抽出部１０３は、ソースコード中に含まれるプログラム終了を意味する文の直前（４０５で示される部分の直後、ｒｅｔｕｒｎ  ０；）に、それぞれ上記手続きで挿入したフラグ変数の全てに１が代入されているかどうかを判定し、全てに１が代入されている場合は終了し、それ以外の場合は上記手続きで挿入したラベルに戻る関数（４０５で示されるｃｈｅｃｋ＿ｐｏｉｎｔ（ｆｌａｇ１））を挿入する。【００６１】  ここで終了した場合、パス抽出部１０３は、実行した命令列の情報をモデルグラフ構成部１０４に受け渡す。【００６２】  このように、パス抽出部１０３は、図２に示すソースコードに４０１〜４０５で示される文を挿入する。【００６３】  これにより、パス抽出部１０３が、全ての判定ノードの組み合わせにフラグ変数の代入を繰り返すことで、実行しうる命令列の全てを抽出することができる。【００６４】  なお、ソースコードの規模が大きく、組み合わせの数が膨大になる場合は、使用できる計算機資源により適宜上記抽出を中止し、下記手続きに進むことが好ましい。【００６５】  次に、検査内部決定部１２０に含まれるモデルグラフ構成部１０４について詳細に説明する。【００６６】  パス抽出部１０３の実行によって、実行された命令列の集合がモデルグラフ構成部１０４に受け渡される。モデルグラフ構成部１０４は、この集合を基に、モデルグラフを構成する。ここで構成するモデルグラフは、頂点と辺の集合からなり、各頂点には対応する命令文がラベルとしてそれぞれ付記され、各辺は起点と終点にそれぞれグラフ中の頂点が一つずつ対応する有向辺である。【００６７】  以下、モデルグラフ構成部１０４がモデルグラフを構成する方法について述べる。【００６８】  まず、モデルグラフ構成部１０４は、命令列の集合から一つの命令列を取り出す。次に、モデルグラフ構成部１０４は、この列の命令の出現順に対応する命令文を表すラベルを付記した頂点を生成、１つ前に生成した頂点と新たに生成された頂点をそれぞれ起点、終点とする辺を生成する。この操作によって、一つの選ばれた命令列に対応する一列のモデルグラフが構成される。ここで最初に生成される頂点を開始頂点と呼ぶ。【００６９】  次に、モデルグラフ構成部１０４は、（１）命令列の集合から一つの命令列��取り出し、上記と同様に一列のモデルグラフを構成する。【００７０】  次に、モデルグラフ構成部１０４は、（２）すでに構成されているモデルグラフと、それぞれの開始頂点から比較し、異なる命令文に対応するラベルが付記されている頂点が出現した場合にグラフを枝分かれさせ、元のモデルグラフに残りの命令列に対応する新たなモデルグラフを付加する。【００７１】  次に、モデルグラフ構成部１０４は、（３）命令列の集合の要素がなくなるまで（１）に戻る、の手続きを（１）から順に実行する。これによってモデルグラフを構成することができる。そして、モデルグラフ構成部１０４は、構成されたモデルグラフを、モデル記述生成部１０５に受け渡す。図５に示すグラフは、図２で示したソースコードからパスを抽出した結果を基に構成したモデルグラフである。【００７２】  このように、モデルグラフ構成部１０４は、図５に示すように遷移条件付き、つまりソースコードの意味する振る舞いを正確に再現したモデルグラフを構成する。【００７３】  次に、モデル記述生成部１０５について詳細を述べる。ここでは、モデルグラフ構成部１０４から受け渡された図５に示すモデルグラフを基に、モデル検査器ＳＰＩＮ用モデル記述言語のプロメラによるモデル記述（図６に図示）を生成する例を挙げる。ここで生成するモデル記述は文字列の列である。図６は、図５のモデルグラフを基に生成したプロメラによるモデル記述である。【００７４】  まず、モデル記述生成部１０５は、プロメラで記述するモデルの開始点を生成する。ここで開始点の記述は、６０１で示される部分で、「ｐｒｏｃｔｙｐｅ  ｍａｉｎ（）｛」である。【００７５】  次に、モデル記述生成部１０５は、モデルグラフの開始点から順に頂点を選び、以下を実行する。【００７６】  まず、モデル記述生成部１０５は、（１）選んだ頂点の次が分岐になっていない場合（図５中の５００ａ〜５００ｉで示される部分）、その頂点に付記されているラベルをＬとしたとき、図６中の６０２ａ〜６０２ｉに示すように、「Ｌ：ｓｋｉｐ；」をモデル記述に付加する。【００７７】  次に、モデル記述生成部１０５は、続くモデルグラフ中の頂点を選び、（１）あるいは以下の（２）を実行する。【００７８】  （２）、モデル記述生成部１０５は、選んだ頂点の次が分岐になっている場合（図５中の５０１で示される部分）、その頂点に付記されているラベルをＬとしたとき、図６中の６０３で示される部分以降に示すように、「Ｌ：ｉｆ：：Ａ：：Ｂ  ｆｉ；」をモデル記述に付加する。【００７９】  次に、モデル記述生成部１０５は、それぞれの分岐先の頂点を選び、それぞれ（１）、（２）を実行し、上記Ａ、Ｂを書き換える。この場合、Ａは図６中の６０４で示される部分、Ｂは６０５で示される部分である。【００８０】  そして、モデル記述生成部１０５は、以上をモデルグラフの頂点全てを選び実行するまで繰り返す。最後に、図６中の６０６で示される、「｝」をモデル記述に加える。【００８１】  モデル記述生成部１０５は、ここで得られたモデル記述をモデル検査器実行部１０６に受け渡す。【００８２】  そして、モデル検査器実行部１０６では、上記モデル記述生成部から受け渡されたモデル記述と、仕様入力��１０７から受け取る仕様をモデル検査器に入力し、モデル検査の結果を検査結果１０９として出力する。【００８３】  以上説明したように、第１実施例によれば、パス抽出部１０３がソースコードによって記述された応用プログラムを模擬に実行することで、実際に実行される命令列を抽出する。そして、検査内容決定部１２０に含まれるモデルグラフ構成部１０４が抽出した命令列からモデルグラフを構成し、モデル記述生成部１０５が構成したモデルグラフからモデル記述を生成するようにでき、ソースコードの検査を行うことができる。【００８４】  このように、ソースコードを模擬に実行することにより、検査の対象とするソースコードの意味するプログラムの振る舞いを逸脱するモデル記述が生成されることがなくなる。このため、検査の対象とするソースコードの意味するプログラムの振る舞いを逸脱た部分に対応するモデル記述によって引き起こされる、誤った異常の検出が行われなくなる。すなわち、元々のソースコードの振る舞いでは検査対象の仕様の制約を満たしていたにもかかわらず、その振る舞いを逸脱したモデル記述が存在したために仕様の性質を満たさなくなった場合に検出される、仕様を満たさないという誤った検査結果を報告されることがなくなる。【００８５】  また、モデル検査を行う前にモデルグラフを抽出しておくことで、モデルグラフを縮退させるなどの効率化手段を適用する余地を残すことが可能となる。【００８６】  また、第１実施例によれば、従来必要だったソースコード変換テーブルをなくすことができるので、ソースコードを検査する人がソースコード変換テーブルを修正する必要がなくなる。【００８７】  （第２実施例）
本発明の第２実施例について説明する。第２実施例では、パス抽出部１０３がプログラムを模擬に実行する方法として、ソースコードを論理式に変換し、その論理式の充足可能性判定を行うことで、実際に実行される命令列を抽出する。論理式の充足可能性判定とは、与えられた論理式全体を１、すなわち真とするような変数値の割り当てが存在するか否かを判定することである。【００８８】  第２実施例におけるソースコード検査器を含むソースコード検査システムの構成は第１実施例と同様であるので、第１実施例におけるソースコード検査器について、図１を用いて説明する。【００８９】  第２実施例におけるソースコード検査器１３０は、パス抽出部１０３において、ソースコード１０１を論理式に変換し、その論理式の充足可能性判定を行うことで、ソースコードの実行される命令列を抽出する。【００９０】  ここでは、パス抽出部１０３は、ソースコード１０１を論理式に変換し、充足可能性判定を行うツールとして、モデル検査器ＣＢＭＣ（Ｂｏｕｎｄｅｄ  Ｍｏｄｅｌ  Ｃｈｅｃｋｅｒ  ｆｏｒ  ＡＮＳＩ−Ｃ  ｐｒｏｇｒａｍｓ）を利用する。ＣＢＭＣは、Ｃ言語のソースコードを入力とし、これを論理式に変換し、その論理式の充足可能性判定を行うことで入力されたソースコードの諸性質を検査するモデル検査器である。パス抽出部１０３は、パス抽出のため、アサート文を常に満たす、という性質を検査する機能を利用する。【００９１】  パス抽出部１０３の処理について、図７を用いて具体的に説明する。図７は、本発明の第２実施例において、図２に示したソースコードを実行パス抽出のために改変した例を示す図である。【００９２】  図７で示すソースコードは、図２に示すソースコードに対し、フラグ変数５０４、５０２および、アサート文５０３が挿入されている。【００９３】  パス抽出部１０３は、検査の対象となるソースコード１０１を基に、その制御フローグラフを構成する。次に、パス抽出部１０３は、ＣＢＭＣに入力するためのＣ言語のソースコードを、入力のソースコードを改変することによって生成する。【００９４】  まず、パス抽出部１０３は、第１実施例と同様、フラグ変数５０４の定義の挿入、代入文５０３の挿入を行う。【００９５】  次に、パス抽出部１０３は、ソースコード１０１中に含まれるプログラム終了を意味する文の直前に、それぞれ上記手続きで挿入したフラグ変数の全てに１が代入されているということはないという意味の宣言文、すなわちアサート（ａｓｓｅｒｔ）文５０３を挿入する。例えば、フラグ変数がｆｌａｇ１、ｆｌａｇ２、ｆｌａｇ３の３つであったとするとき、挿入するアサート文は、「ａｓｓｅｒｔ（ｆｌａｇ１！＝１｜｜ｆｌａｇ２！＝１｜｜ｆｌａｇ３！＝１）」となる。【００９６】  次に、パス抽出部１０３は、上記手続きによって改変し、得られたソースコードをＣＢＭＣに入力する。【００９７】  このとき、もしアサート文の宣言に違反する場合がＣＢＭＣによって指摘されれば、挿入したフラグ変数が全て１になる場合があることを意味する。すなわち、フラグ変数に１を代入した箇所を全て通過する実行可能パスが存在することを意味する。【００９８】  よって、ＣＢＭＣによるアサート文の違反の指摘は、���ＢＭＣに入力し、実行した結果に、「Ｆａｉｌｅｄ  ａｓｓｅｒｔｉｏｎ：」の文字列が含まれる場合であり、パス抽出部１０３は、出力の文字列を検索することにより、アサート文の違反を判定できる。【００９９】  パス抽出部１０３は、実行可能パスと判定された場合、そのパスに対応する命令列の情報を検査内容決定部１２０に含まれるモデルグラフ構成部１０４に受け渡す。【０１００】  パス抽出部１０３は、上記手続きをフラグ変数５０２に１を代入する箇所を変更しながら繰り返すことで、モデルグラフ構成部１０４に実行可能な命令列の情報を集積する。【０１０１】  このように、十分な情報が集積された後、第１実施例で挙げたモデルグラフ構成部１０４の実行、およびそれ以後の実行を同様に行うことで、ソースコードの検査を行うことができる。【０１０２】  以上説明したように、本実施例によれば、パス抽出部１０３において、ソースコード１０１を論理式に変換し、論理式の充足可能性判定を行うことで、ソースコード１０１の実行される可能性のある命令列を抽出できる。これにより、検査の対象とするソースコード１０１で与えられるプログラムを実際に実行することを必要とせずにプログラムの振る舞いを抽出することができる。このように、検証の対象とするソースコード１０１を実際にコンパイル、リンクして実行可能にする必要がないため、例えばリンクなどができない、一連のソースコード群から一部のソースコードの集合だけを対象としたモデル検査を行うことが可能となる。【０１０３】  （第３実施例）
本発明の第３実施例は、ソースコードの情報を基にモデル検査器実行部に入力する仕様を自動的に生成する手段を備えたものである。【０１０４】  以下、第３実施例にかかるソースコード検査器について説明する。図８は、本発明の第３実施例におけるソースコード検査器を含むソースコード検査システムのブロック図である。なお、図１の構成と同様の構成を有するものについては、同一符号を付しその説明を省略する。【０１０５】  本実施例におけるソースコード検査システム６００は、ソースコード入力部１０２によって受け入れられたソースコード１０１の情報を基に、モデル検査器実行部１０６に入力する仕様を自動的に生成する仕様自動生成部６０１を備えた点が特徴である。ソースコード検査器１３１は、ソースコード入力部１０２と、パス抽出部１０３と、検査内容決定部１２０と、仕様自動生成部６０１と、制御部１４０と、記憶媒体１５０とを備える。【０１０６】  次に、仕様自動生成部６０１の仕様の自動生成法について述べる。【０１０７】  まず、仕様自動生成部６０１は、ソースコード入力部１０２によって受け入れられたソースコード１０１を読み込み、必ず対になって使われるべき命令文を全て検索する。【０１０８】  例えば、Ｃ言語で記述されたソースコードを扱う場合は、ｆｏｐｅｎに対するｆｃｌｏｓｅ、ｏｐｅｎに対するｃｌｏｓｅ、ｍａｌｌｏｃやｃａｌｌｏｃなどメモリをヒープ領域に確保する文に対するｆｒｅｅを含む命令文などが、それぞれ必ず対になって使われるべき命令文である。【０１０９】  次に、仕様自動生成部６０１は、上記手続きで検索した結果として検出された命令文の対Ａ、Ｂについて、仕様に以下の式、「［］（Ａ−＞＜＞Ｂ）」を加える。【０１１０】  上式は、Ａが出現した場合に、必ずＢが出現するという制約を表す式である。【０１１１】  例えばｆｐ＝ｆｏｐｅｎ（ｆｎａｍｅ，“ｗ”）と、ｆｃｌｏｓｅ（ｆｐ）という対になる命令文が存在した場合、仕様自動生成部６０１は、以下の式、「［］（“ｆｐ＝ｆｏｐｅｎ（ｆｎａｍｅ，“ｗ”）”−＞＜＞“ｆｃｌｏｓｅ（ｆｐ）”）」を仕様に加える。【０１１２】  仕様自動生成部６０１は、以上の処理を、全ての検出された文の対について繰り返す。【０１１３】  また、仕様自動生成部６０１は、すでに仕様として式が存在し、これに新たな式を加える場合は、演算子“＆＆”を用いて連結する。演算子“＆＆”は論理積を表し、制約を新たに追加する場合に用いられる。【０１１４】  以上説明したように、第３実施例によれば、第１実施例と違いユーザが仕様有力部１０７から仕様１０８を入力する必要がなくなり、例えばソースコードによって記述された応用プログラムがメモリの不正使用を行わないことを意味する仕様を自動生成できる。つまり、煩わしく、ときに専門知識を要する仕様１０８の入力を必要としなくなる。【０１１５】  （第４実施例）
本発明の第４実施例は、抽出された実行される可能性のある命令列がメモリの不正使用を行わないかどうかを判定するものである。【０１１６】  以下、本実施例におけるソースコード検査器について、図９を用いて説明する。図９は、本実施例におけるソースコード検査器の構成を示すブロック図である。なお、図１の構成と同様の構成を有するものについては、同一符号を付しその説明を省略する。【０１１７】  第４実施例におけるソースコード検査器７００は、ソースコード入力部１０２と、パス抽出部１０３と、検査内容決定部１２２と、制御部１４０と、記憶媒体１５０とを備える。検査内容決定部１２２は、検証プログラム生成部７０１と、検証プログラム実行部７０２とを備える。検証プログラム生成部７０１は、パス抽出部１０３によって抽出された実行される可能性のある命令列を受け取り、その命令列がメモリの不正使用を行わないかどうかを単独で判定するための検証プログラムを生成する。検証プログラム実行部７０２は、検証プログラム生成部７０１で生成された検証プログラムを実行する。【０１１８】  次に、検証プログラム生成部７０１における、検証プログラム生成方法について、詳細を述べる。検証プログラム生成部７０１が、生成する検証プログラムは、パス抽出部１０３によって抽出された実行される可能性のある命令列を基に生成する文字列からなる。【０１１９】  検証プログラム生成部７０１が、この文字列を生成する手順について、図１０を用いて説明する。図１０は、本実施例において、図５に示すグラフの左側の分岐をもとに、検証プログラム生成部７０１での処理によって生成されたプログラムの例を示す図である。【０１２０】  まず、検証プログラム生成部７０１は、１００１で示される部分、「ｉｎｔ  ｍａｉｎ（）｛（１００１）」を開始文字列とする。検証プログラム生成部７０１は、この開始文字列１００１に文字列を順に付加していくことで、検証プログラムの文字列を構成する。次に、検証プログラム生成部７０１は、パス抽出部１０３で生成された命令列に対応する命令文にセミコロンを付加した文字列を順に上記開始文字列に付加する。【０１２１】  このとき、図５の５００ｃに示すようにｍａｌｌｏｃ関数が存在し、かつ、図５の５００ｄ、５００ｅに示すようにｗｚ＿ｍａｌｌｏｃ、ｆｒｅｅ関数が存在した場合、検証プログラム生成部７０１は、ｗｚ＿ｍａｌｌｏｃ、ｆｒｅｅ関数を図１０中の１００２に示すようにｗｚ＿ｆｒｅｅと置き換える。【０１２２】  また、命令列に含まれる式中にポインタ変数が含まれる場合、検証プログラム生成部７０１は、そのポインタ変数のそれぞれについて、そのポインタ変数を引数としたｗｚ＿ｃｈｅｃｋ関数の呼び出し文を式の前に挿入する。【０１２３】  また、命令列の最後がｒｅｔｕｒｎ文でなかった場合は、検証プログラム生成部７０１は、「ｒｅｔｕｒｎ  ０；｝」を、また、ｒｅｔｕｒｎであった場合は、図１０中１００３に示すように、「｝」を付加する。【０１２４】  最後に、検証プログラム生成部７０１は、図１１〜図１３に示す文字列を付加する。【０１２５】  以上のように、検証プログラム生成部７０１は、検証プログラムを生成する。そして、検証プログラム生成部７０１は、生成した検証プログラムを検証プログラム実行部７０２に受け渡す。【０１２６】  検証プログラム実行部７０２では、検証プログラム生成部７０１から受け渡された検証プログラムをコンパイルし、実行する。実行した結果を検査結果１０９として表示する。ここで、「Ｍｅｍｏｒｙ  ｌｅａｋ  ｗａｓ  ｄｅｔｅｃｔｅｄ．」と表示されると、パス抽出部１０３によって抽出された命令列が実行された場合に、メモリリークが発生することを検出したことを意味する。【０１２７】  また、「Ｕｓｅｄ  ｎｏｎ−ａｃｔｉｖｅ  ｏｂｊｅｃｔ．」と表示されると、パス抽出部１０３によって抽出された命令列が実行された場合に、ヌルポインタを使用しようとすることを検出したことを意味する。【０１２８】  以上説明したように、本実施例によれば、検証プログラム生成部７０１で、プログラムがメモリの不正使用を行わないことを意味する仕様を自動的に生成するので、メモリの不正使用に関する知識を必要とせず、メモリの不正使用に関するソースコード検査を行うことが可能となる。また、第１実施例における仕様入力部１０７を必要とせず、プログラムのメモリの不正使用に関する検査を行うことができるようになる。【０１２９】  また、本実施例によれば、単独でソースコード検査を行えるプログラムを出力することにより、第１実施例におけるモデル検査器実行部１０６を不要とすることができる。すなわち外部のモデル検査器を用いる必要がなくなるため、可搬性、および利便性が向上する。
【産業上の利用可能性】
【０１３０】  以上のように、本発明によれば、ソースコードの意味するプログラムの振る舞いを逸脱することなく、ソースコードの検査を行うことができる。検査の対象とするソースコードの意味する振る舞いを逸脱することなく、より正確にソースコードの検査を実現することができる。また、本発明は、ソフトウェアの正当性検査等の分野に適用でき、その利用可能性は大きい。
【図１】
2006038394.tif 000002
【図２】
2006038394.tif 000003
【図３】
2006038394.tif 000004
【図４】
2006038394.tif 000005
【図５】
2006038394.tif 000006
【図６】
2006038394.tif 000007
【図７】
2006038394.tif 000008
【図８】
2006038394.tif 000009
【図９】
2006038394.tif 000010
【図１０】
2006038394.tif 000011
【図１１】
2006038394.tif 000012
【図１２】
2006038394.tif 000013
【図１３】
2006038394.tif 000014
【図１４】
2006038394.tif 000015
【手続補正書】
【提出日】平成19年1月9日(2007.1.9)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
あらかじめ入力された計算機用プログラムのソースコードによって記述されたプログラムを模擬に実行することで実際に実行される命令列を抽出するパス抽出ステップと、前記パス抽出ステップで抽出した命令列に基づいて前記ソースコードの検査内容を決定する検査内容決定ステップと、を含むソースコード検査方法。
【請求項２】
前記検査内容決定ステップは、モデル記述と前記ソースコードを検査する性質を表す仕様とにより前記ソースコードのモデル検査を行うモデル検査実行ステップに前置し、前記パス抽出ステップで抽出した命令列からモデルグラフを構成するモデルグラフ構成ステップと、前記モデルグラフ構成ステップで構成したモデルグラフからモデル記述を生成するモデル記述生成ステップと、を備え、前記モデル記述生成部が生成したモデル記述とあらかじめ入力された仕様とにより前記モデル検査実行ステップで前記ソースコードの検査を行う請求項１記載のソースコード検査方法。
【請求項３】
前記パス抽出ステップは、前記ソースコードを論理式に変換し前記論理式の充足可能性判定を行うことで前記実際実行される命令列を抽出する請求項１記載のソースコード検査方法。
【請求項４】
前記仕様を自動で生成する仕様自動生成ステップをさらに含み、前記あらかじめ入力された仕様は、前記仕様自動生成ステップで生成した仕様である請求項２記載のソースコード検査方法。
【請求項５】
前記仕様自動生成ステップは、前記ソースコードによって記述されたプログラムがメモリの不正使用を行わないことを意味する仕様を自動生成する請求項４記載のソースコード検査方法。
【請求項６】
前記検査内容決定ステップは、前記パス抽出ステップで抽出した命令列がメモリの不正使用を行わないかどうかを検証するための検証プログラムを生成する検証プログラム生成ステップと、前記検証プログラム生成ステップで生成した検証プログラムを実行する検証プログラム実行ステップと、を含む請求項１記載のソースコード検査方法。
【請求項７】
コンピュータにソースコード検査方法を実行させる方法実行プログラムであって、前記方法は、
あらかじめ入力された計算機用プログラムのソースコードによって記述された応用プログラムを模擬に実行することで実際に実行される命令列を抽出するパス抽出ステップと、前記パス抽出ステップで抽出した命令列に基づいて前記ソースコードの検査内容を決定する検査内容決定ステップと、を有する。
【請求項８】
コンピュータにソースコード検査方法を実行させる方法実行プログラムを格納する記憶媒体であって、前記方法は、
あらかじめ入力された計算機用プログラムのソースコードによって記述された応用プログラムを模擬に実行することで実際に実行される命令列を抽出するパス抽出ステップと、前記パス抽出ステップで抽出した命令列に基づいて前記ソースコードの検査内容を決定する検査内容決定ステップと、を有する。
【請求項９】
あらかじめ入力された計算機用プログラムのソースコードによって記述されたプログラムを模擬に実行することで実際に実行される命令列を抽出するパス抽出部と、前記パス抽出部が抽出した命令列に基づいて前記ソースコードの検査内容を決定する検査内容決定部と、を備えるソースコード検査器。
【請求項１０】
前記検査内容決定部は、モデル記述と前記ソースコードを検査する性質を表す仕様とにより前記ソースコードのモデル検査を行うモデル検査器実行部に前置し、
前記パス抽出部が抽出した命令列からモデルグラフを構成するモデルグラフ構成部と、前記モデルグラフ構成部が構成したモデルグラフからモデル記述を生成するモデル記述生成部と、を備え、前記モデル記述生成部が生成したモデル記述とあらかじめ入力された仕様とにより前記モデル検査器実行部で前記ソースコードの検査を行う請求項９記載のソースコード検査器。
【請求項１１】
前記パス抽出部は、前記ソースコードを論理式に変換し前記論理式の充足可能性判定を行うことで前記実際に実行される命令列を抽出する請求項９記載のソースコード検査器。
【請求項１２】
前記仕様を自動で生成する仕様自動生成部をさらに備え、前記あらかじめ入力された仕様は、前記仕様自動生成部が生成した仕様である請求項１０記載のソースコード検査器。
【請求項１３】
前記仕様自動生成部は、前記ソースコードによって記述されたプログラムがメモリの不正使用を行わないことを意味する仕様を自動生成する請求項１２記載のソースコード検査器。
【請求項１４】
前記検査内容決定部は、前記パス抽出部で抽出した命令列がメモリの不正使用を行わないかどうかを検証するための検証プログラムを生成する検証プログラム生成部と、前記検証プログラム生成部が生成した検証プログラムを実行する検証プログラム実行部と、を備えた請求項９記載のソースコード検査器。
【手続補正２】
【補正対象書類名】明細書
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、計算機プログラムのソースコードが意味するプログラムの振る舞いに関する諸性質を検査するソースコード検査器及びソースコード検査方法、当該方法を実行させるプログラム、当該プログラムを格納する記憶媒体に関する。
【背景技術】
【０００２】
従来のソースコード検査器として、ソースコードが意味するプログラム（以下、応用プログラムとも記す）の振る舞いに関する諸性質を検査するソースコード分析器がある。ソースコード分析器の例としては、モデル検査技術を用いてソースコードを分析するソースコードモデル検査器がある。
【０００３】
ソースコードが意味する応用プログラムの振る舞いとは、ソースコードに記述された一連の命令に従う、プログラムの一連の動作を意味する。この振る舞いに関する諸性質の例として、メモリを動的に確保した場合は必ずそのメモリを解放する性質、プログラム中のある命令を実行した場合は必ずいつか対応する特定の命令を実行する性質などが挙げられる。
【０００４】
モデル検査とは、検査する性質を表す仕様と検査の対象となるモデルとを入力とし、モデルが仕様の表す性質を有するかどうかを判定することである。モデル検査を行う装置をモデル検査器と呼び、検査の対象となるモデルを記述したものをモデル記述と呼ぶ。モデルを記述するための言語は、モデル検査器によって様々に異なる。例えば、モデル検査器ＳＰＩＮの場合、モデルを記述するための言語はプロメラ（Ｐｒｏｍｅｌａ）と呼ばれるものである。
【０００５】
モデル検査器ＳＰＩＮは、有限状態遷移系としてモデル化したシステムが線形時間論理式で記述された検査式を満たすかを全状態検索で網羅的に検査する検査器である。モデル検査器ＳＰＩＮは、例えば、Ｇｅｒａｒｄ  Ｊ．Ｈｏｌｚｍａｎｎ，’Ｔｈｅ  ｍｏｄｅｌ  Ｃｈｅｃｋｅｒ  Ｓｐｉｎ’，ＩＥＥＥ  Ｔｒａｎｓ，Ｏｎ  Ｓｏｆｔｗａｒｅ  Ｅｎｇｉｎｅｅｒｉｎｇ，Ｖｏｌ．２３，Ｎｏ．５，Ｍａｙ  １９９７，ｐｐ．２７９−２９５に開示されている。
【０００６】
ソースコードモデル検査とは、ソースコードを検査の対象としたモデル検査を指し、論理回路などハードウェアを対象とするモデル検査であるハードウェアモデル検査との対比のため用いる語である。
【０００７】
従来のソースコード検査器としては、ソースコードをモデル検査器の入力言語に翻訳するための変換表を用いるものがある。この構成は、例えば、米国特許出願公開第２００１／０３７４９２号、米国特許出願公開第２００２／１０００２２号に開示されている。図１４は、米国特許出願公開第２００１／０３７４９２号に記載された従来のソースコード検査器の構成を示すブロック図である。
【０００８】
図１４に示す従来のソースコード検査器であるモデル検査器は、検査の対象となるソースコード１３０１をソースコード入力部１３０２から入力する。次に、このソースコード検査器は、ソースコード変換テーブル生成部１３０３において、ソースコード入力部１３０２によって受け入れたソースコード１３０１を基に制御フローグラフを構成する。そして、その制御フローグラフから検査の対象となるソースコード１３０１の各文について、対応するモデル記述言語、例えばプロメラの記述で書かれた対訳例を集めたソースコード変換テーブル１３０４を生成する。
【０００９】
次に、モデル記述生成部１３０５が、ソースコード変換テーブル１３０４に含まれる対訳例を用いてソースコード１３０１をモデル記述言語に変換する。また、仕様入力部１３０７は、入力された検査するソースコード１３０１の性質を表す仕様を記載した検査する仕様１３０８をモデル検査器実行部１３０６へ渡す。そして、モデル検査器実行部１３０６が、仕様入力部１３０７からの仕様１３０８と、モデル記述生成部１３０５において生成されたモデル記述とを用いてモデル検査を実行し、検査結果１３０９を出力する。
【００１０】
また、自動的に生成されたソースコード変換テーブル１３０４がソースコードモデル検査器の使用者の意に沿わない場合、使用者の修正手段１３１０がソースコード変換テーブル１３０４を適宜修正する必要がある。それは、例えば、検査の対象となるソースコード１３０１が、そのソースコード以外のもの、例えば外部モジュールとの通信など、を扱う場合などである。ソースコード変換テーブル生成部１３０３が適正な翻訳例を示すことができない場合も多く、これを使用者が補う必要がある。
【００１１】
ソースコードモデル検査で用いるプロメラなどのモデル記述言語と、ソースコードを記述している例えばＣ言語などのプログラミング言語とでは表現力が違う。具体的には、プログラミング言語では記述できて、モデル記述言語では記述できない遷移条件が存在する。このため、ソースコードの意味する振る舞いをモデル記述言語に正確に翻訳することが本質的に困難であり得、適切なソースコード変換テーブルを生成することが困難な場合が多い。よって、検査の対象となるソースコードの意味する振る舞いを正確に再現するモデル記述が得られず、不正確な検査になる場合が多いという問題があり得る。
【００１２】
詳細に説明すると、モデル検査は、モデルの記述を基にラベル付き有向グラフを生成し、このグラフが例えば線形時間論理式などで与えられる仕様の意味する制約を満たしているかどうかを判定する、という手順で行われる。線形時間論理式とは、命題論理式に時間の概念を追加して構成されるもので、状態遷移モデルを形式的に記述する際等で広く用いられている。
【００１３】
ラベル付き有向グラフとは、頂点と辺の集合からなる。各辺は２頂点間の関係を表し、頂点同士を結ぶ辺には向きが存在する。すなわち、ラベル付き有向グラフには、辺の起点、および終点に一つずつ対応する頂点が存在し、各頂点にはラベルが付記されている。
【００１４】
ラベル付き有向グラフの各頂点を状態とみなし、辺の向きに沿って頂点を移動することを状態遷移とみなすとき、ラベル付き有向グラフは状態遷移図とみなすことができる。各頂点のラベルは、各状態で生起されるイベントであるとみなすことができる。そして、モデル検査は、そのイベントの生起の列が与えられた仕様の制約を満たしているかどうかを判定する。
【００１５】
しかしながら、ラベル付き有向グラフは、遷移条件が存在しない。遷移条件とは、ある頂点を起点とした複数の辺があるとき、どの辺の終点の頂点に遷移するべきかを判断する条件である。遷移条件が存在しないということは、ある頂点を起点とした複数の辺があるとき、どちらの辺の頂点に対応する状態を次の状態とみなすかは任意に選択可能であるということを意味する。モデル検査は通常、検査する仕様の制約に違反しているかどうかを確認するため、任意に選択可能な遷移先については、常に最悪の場合を選択する。
【００１６】
しかしながら、ソースコードが意味する振る舞いを表す状態遷移図は、一般に遷移条件付きラベル付き有向グラフで表される。例えばｉｆ文などで表される条件節は、その条件式の真偽によって次状態が決定される。
【００１７】
以上の理由から、遷移条件のないラベル付き有向グラフによって意味づけられるモデル記述言語と、遷移条件付きラベル付き有向グラフによって意味づけられる一般のプログラミング言語との間を逐語訳で変換することは本質的な困難さを伴うという問題があり得る。また、従来の方法では、検査器の使用者がソースコード変換テーブルを修正することは困難であり得る。
【００１８】
詳細に説明すると、検査器の使用者はソースコード変換テーブルの修正を行う際、変換テーブルに記述されたモデル記述を理解する必要がある。さらに、ソースコードの意味する応用プログラムの振る舞いを正確に反映していない箇所を特定する必要があり、その箇所について代替となる翻訳を与える必要がある。また、検査の対象となるソースコード以外の部分について、モデル検査が適切に行われるように配慮しながら、その部分を補完するモデル記述を与える必要がある。これは使用者がモデル検査の専門家であったとしても、困難さや煩雑さを伴う作業となり得る。
【発明の開示】
【００１９】
本発明は、検査の対象となるソースコードの意味する振る舞いをより正確に検査するソースコード検査器及びソースコード検査方法、当該方法を実行させる方法実行プログラム、当該プログラムを格納する記憶媒体を提供する。
【００２０】
本発明は、あらかじめ入力された計算機用プログラムのソースコードによって記述された応用プログラムを模擬に実行することで実際に実行される命令列を抽出するパス抽出ステップと、パス抽出ステップで抽出した命令列に基づいてソースコードの検査内容を決定する検査内容決定ステップと、を含むようにした。本発明によれば、ソースコードの意味する振る舞いをより正確に検査することができる。
【発明を実施するための最良の形態】
【００２１】
本発明のソースコード検査方法は、パス抽出ステップと、検査内容決定ステップと、を含む。パス抽出ステップは、あらかじめ入力された計算機用プログラムのソースコードによって記述された応用プログラムを模擬に実行することで実際に実行される命令列を抽出する。検査内容決定ステップは、パス抽出ステップで抽出した命令列に基づいてソースコードの検査内容を決定する。
【００２２】
これにより、検査の対象とするソースコードの意味するプログラムの振る舞いを逸脱することなく、ソースコードの検査を行うことができる。
【００２３】
また、本発明のソースコード検査方法は、検査内容決定ステップが、モデル記述とソースコードを検査する性質を表す仕様とによりソースコードのモデル検査を行うモデル検査実行ステップに前置し、モデルグラフ構成ステップと、モデル記述生成ステップと、を含むようにしてもよい。モデルグラフ構成ステップは、パス抽出ステップで抽出した命令列からモデルグラフを構成する。モデル記述生成ステップは、モデルグラフ構成ステップで構成したモデルグラフからモデル記述を生成する。モデル記述生成部が生成したモデル記述とあらかじめ入力された仕様とによりモデル検査実行ステップでソースコードの検査を行うようにしてもよい。
【００２４】
この方法によれば、モデル検査手法を用いて、さらに検査の対象とするソースコードの意味するプログラムの振る舞いを逸脱するモデル記述が生成されることがなくなる。このため、検査の対象とするソースコードの意味するプログラムの振る舞いを逸脱した部分に対応するモデル記述によって引き起こされる、誤った異常な検出が行われなくなる。すなわち、本発明の方法では、ソースコードの振る舞いを逸脱するモデル記述が存在しない。このため、元々のソースコードの振る舞いでは検査対象の仕様の制約を満たしていたにもかかわらず、仕様を満たさないという誤った検査結果を報告されることがなくなる。また、モデル検査を行う前にモデルグラフを抽出しておくことで、モデルグラフを縮退させるなどの効率化手段を適用する余地を残すことが可能となる。
【００２５】
また、本発明のソースコード検査方法は、パス抽出ステップが、ソースコードを論理式に変換し、論理式の充足可能性判定を行うことでソースコードの実行される可能性のある命令列を抽出するようにしてもよい。
【００２６】
この方法によれば、さらに検査の対象とするソースコードで与えられるプログラムを模擬に、すなわち、条件文が成り立つか成り立たないかを充足可能性判定していくことにより、プログラムの振る舞いを抽出することができる。このように、検証の対象とするソースコードをコンパイル、リンクして実行可能にする必要がないため、例えばリンクなどができない、一連のソースコード群から一部のソースコードの集合だけを対象としたモデル検査を行うことが可能となる。
【００２７】
また、本発明のソースコード検査方法は、仕様を自動で生成する仕様自動生成ステップをさらに含み、あらかじめ入力された仕様は、仕様自動生成ステップで生成した仕様であるようにしてもよい。
【００２８】
この方法によれば、さらに仕様を手で入力する必要とがなくなる。つまり、煩わしく、ときに専門知識を要する仕様の手入力を必要としなくなる。
【００２９】
また、本発明のソースコード検査方法は、仕様自動生成ステップが、ソースコードによって記述されたプログラムがメモリの不正使用を行わないことを意味する仕様を自動生成するようにしてもよい。
【００３０】
この方法によれば、さらにメモリの不正使用に関する知識を必要とせず、メモリの不正使用に関するモデル検査を行うことが可能となる。また、仕様の手入力を必要とせず、プログラムのメモリの不正使用に関する検査を行うことができるようになる。
【００３１】
さらに、本発明のソースコード検査方法は、検査内容決定ステップが、検証プログラム生成ステップと、検証プログラム実行ステップと、を含むようにしてもよい。検証プログラム生成ステップは、抽出された命令列がメモリの不正使用を行わないかどうかを単独で判定するための検証プログラムを生成する。検証プログラム実行ステップは、生成された検証プログラムを実行する。
【００３２】
これにより、モデル検査実行ステップせずソースコードの検査を行うことができる。すなわち外部のモデル検査方法を用いる必要がなくなるため、可搬性、および利便性が向上する。
【００３３】
本発明の方法実行プログラムは、コンピュータに上記ソースコード検査方法を実行させるプログラムである。また、本発明の記憶媒体は、上記方法実行プログラムを格納する記憶媒体である。
【００３４】
以下、本発明の実施例について、図面を参照しながら説明する。
【００３５】
（第１実施例）
本発明の第１実施例にかかるソースコード検査器を含むソースコード検査システムについて、図１を用いて説明する。図１は、第１実施例におけるソースコード検査器を含むソースコード検査システムのブロック図である。
【００３６】
第１実施例にかかるソースコード検査システム１００は、コンピュータシステムであって、ソースコード検査器１３０と、モデル検査器１０６と、仕様入力部１０７とを備える。ソースコード検査器１３０は、ソースコード入力部１０２と、パス抽出部１０３と、検査内容決定部１２０と、制御部１４０と、記憶媒体１５０とを備える。検査内容決定部１２０は、モデルグラフ構成部１０４と、モデル記述生成部１０５とを備える。
【００３７】
ソースコード入力部１０２は、計算機用のプログラムであるソースコード１０１を入力する。パス抽出部１０３は、ソースコード入力部１０２によって受け入れられたソースコード１０１の実行される可能性のある命令列を抽出し、抽出した命令列をモデルグラフ構成部１０４に送る。モデルグラフ構成部１０４は、パス抽出部１０３で抽出されたパスの情報をグラフとしてまとめ、まとめたグラフをモデル記述生成部１０５に送る。
【００３８】
モデル記述生成部１０５は、モデルグラフ構成部１０４において構成されたグラフを基にモデル記述を生成し、生成したモデル記述を、ソースコード検査器１３０の外部にあるモデル検査器実行部１０６に送る。
【００３９】
制御部１４０は、記憶媒体１５０に記憶されたソースコード検査方法を実行させる方法実行プログラムにより、ソースコード検査器１３０の各部を制御する。記憶媒体１５０は、ハードディスク記憶装置や半導体メモリ、ＣＤ−ＲＯＭなどで構成される。
【００４０】
モデル検査器実行部１０６は、仕様入力部１０７から受け入れた検査するソースコード１０１の性質を表す制約を記載した検査する仕様１０８と、モデル記述生成部１０５において生成されたモデル記述とを用いてモデル検査を実行し、検査結果１０９を出力する。上記制御部１４０は、記憶媒体１５０に記憶されたプログラムによって、モデル検査器実行部１０６を制御するようにしてもよい。ソースコード検査器の各部は、ランダムロジックを用いたハードウエアで構成しても、コンピュータに実行させるソフトウエアで構成しても、あるいはそれらの混成であってもよい。
【００４１】
次に、パス抽出部１０３について詳細に説明する。
【００４２】
パス抽出部１０３では、まず検査の対象となるソースコード１０１を基に、その制御フローグラフを構成する。
【００４３】
制御フローグラフとは、ソースコード１０１の制御構造を表現したものであり、処理ブロックノード、判定ノード、合流ノードの三つの基本要素から成るグラフである。処理ブロックノードとは、判定による分岐のない連続したソースコードの命令列に対応するグラフの頂点である。判定ノードとは、ある式の真偽値によって実行する命令列が分岐する点を意味するグラフの頂点である。合流ノードとは、複数の命令列が合流する点を意味するグラフの頂点である。
【００４４】
図２に本実施例におけるソースコードの例、図３に図２のソースコードに基づいて構成した制御フローグラフの例をそれぞれ示す。
【００４５】
図３は処理ブロックノード３０１、３０３、３０５、および３０６と、判定ノード３０２と、合流ノード３０４と、各ノードをつなぐ有向辺とからなる。
【００４６】
パス抽出部１０３は、このような制御フローグラフを生成する。
【００４７】
次に、パス抽出部１０３は、構成した制御フローグラフに基づいた実行されうる命令列の抽出、すなわち実行パス抽出する。ここではＣ言語に基づいた実行パス抽出例を示すが、Ｃ言語に限らず、Ｃ＋＋やＪａｖａ（登録商標）などの言語においても同様の方法によって命令列を抽出することができる。
【００４８】
パス抽出部１０３は、検査の対象となるソースコード１０１を改変し、改変されたソースコードをコンパイルし、実行することによって実行パス抽出を行う。パス抽出部１０３が行うソースコード１０１の改変は、実行される命令列を抽出するためのものであり、元のソースコード１０１が意味する振る舞いには影響を与えない。すなわちパス抽出部１０３は、ソースコード１０１を模擬に実行し、そこで実行された命令列を抽出する。
【００４９】
以下、パス抽出部１０３の処理について、図３および図４を用いて具体的に説明する。図４は図２に示したソースコードを実行パス抽出のために改変した例を示す図である。
【００５０】
４０１で示される文はフラグ変数を定義、初期化する文である。４０２で示される文は開始点を表すラベルと変数定義に含まれる初期化文である。４０３で示される文は不定値を持つ変数を改変する関数である。４０４で示される文は分岐命令に対応したフラグ変数に１を代入する文である。４０５で示される文はフラグ変数が全て１かどうかを判定する関数である。
【００５１】
まず、パス抽出部１０３は、制御フローグラフに含まれる判定ノードの数と同じ数のフラグ変数をグローバル変数定義領域に定義する。図４の例では、パス抽出部１０３は、ｉｎｔ  ｍａｉｎ()｛から始まって、この｛に対応する最後の｝で終わる領域の外、つまり４０１のある所か、最後の｝の下の領域に、グローバル変数定義領域を定義する。
【００５２】
フラグ変数は、それぞれ異なる名前を持ち、０で初期化され、０あるいは１の２値を格納する領域を持つグローバル変数であるとする。例えば、制御フローグラフに含まれる判定ノードが三つである場合、パス抽出部１０３は、改変するソースコードの冒頭のグローバル変数定義領域に、「ｉｎｔ  ｆｌａｇ１＝０，ｆｌａｇ２＝０，ｆｌａｇ３＝０；」と記述する。
【００５３】
次に、パス抽出部１０３は、制御フローグラフに含まれる判定ノード３０２のそれぞれについて、一つの分岐を選び、分岐先の処理ブロックノード３０３に対応する命令列（ｆｒｅｅ（ｐ）；）の先頭に、フラグ変数に１を代入する命令文４０４を挿入する。
【００５４】
パス抽出部１０３は、一度使用したフラグ変数は用いずに、フラグ変数に１を代入する操作を繰り返す。また、パス抽出部１０３は、それぞれの判定ノードに対応する分岐命令文の直前に、不定値となっている変数を実行パス探索のために改変する関数４０３を挿入する。
【００５５】
不定値となる変数は、ソースコード記述範囲外からの入力、例えばプログラム使用者から入力、によって改変される値や乱数によって決定される値、そしてその値に依存して決定される値を持つ変数を意味する。データフロー解析によってそれぞれの変数が不定値を持つかどうかを判定することができる。
【００５６】
挿入する関数は、対応する分岐命令文に含まれる不定値となっている変数を引数にとり、それぞれの変数の値を改変する。またこの関数は、呼び出されるたびに異なる値の組み合わせを、引数で与えられたそれぞれの変数に代入する。
【００５７】
次に、パス抽出部１０３は、ソースコード１０１中の、変数定義文を除いて最初に実行される命令に対応する命令文（図４中の４０２で示される部分の直後にあるｐ＝ｍａｌｌｏｃ（ｓｉｚｅｏｆ（ｃｈａｒ）））の前に、開始点を表すラベル（４０２で示される一行目、ｉｎｉｔ＿ｐｏｉｎｔ）を挿入し、そのラベルを挿入した場所の直後に、変数定義文中に含まれる変数の初期化命令（４０２で示される部分の二行目、ｐ＝０；）を追加する。
【００５８】
次に、パス抽出部１０３は、ソースコード中に含まれるプログラム終了を意味する文の直前（４０５で示される部分の直後、ｒｅｔｕｒｎ  ０；）に、それぞれ上記手続きで挿入したフラグ変数の全てに１が代入されているかどうかを判定し、全てに１が代入されている場合は終了し、それ以外の場合は上記手続きで挿入したラベルに戻る関数（４０５で示されるｃｈｅｃｋ＿ｐｏｉｎｔ（ｆｌａｇ１））を挿入する。
【００５９】
ここで終了した場合、パス抽出部１０３は、実行した命令列の情報をモデルグラフ構成部１０４に受け渡す。
【００６０】
このように、パス抽出部１０３は、図２に示すソースコードに４０１〜４０５で示される文を挿入する。
【００６１】
これにより、パス抽出部１０３が、全ての判定ノードの組み合わせにフラグ変数の代入を繰り返すことで、実行しうる命令列の全てを抽出することができる。
【００６２】
なお、ソースコードの規模が大きく、組み合わせの数が膨大になる場合は、使用できる計算機資源により適宜上記抽出を中止し、下記手続きに進むことが好ましい。
【００６３】
次に、検査内部決定部１２０に含まれるモデルグラフ構成部１０４について詳細に説明する。
【００６４】
パス抽出部１０３の実行によって、実行された命令列の集合がモデルグラフ構成部１０４に受け渡される。モデルグラフ構成部１０４は、この集合を基に、モデルグラフを構成する。ここで構成するモデルグラフは、頂点と辺の集合からなり、各頂点には対応する命令文がラベルとしてそれぞれ付記され、各辺は起点と終点にそれぞれグラフ中の頂点が一つずつ対応する有向辺である。
【００６５】
以下、モデルグラフ構成部１０４がモデルグラフを構成する方法について述べる。
【００６６】
まず、モデルグラフ構成部１０４は、命令列の集合から一つの命令列を取り出す。次に、モデルグラフ構成部１０４は、この列の命令の出現順に対応する命令文を表すラベルを付記した頂点を生成、１つ前に生成した頂点と新たに生成された頂点をそれぞれ起点、終点とする辺を生成する。この操作によって、一つの選ばれた命令列に対応する一列のモデルグラフが構成される。ここで最初に生成される頂点を開始頂点と呼ぶ。
【００６７】
次に、モデルグラフ構成部１０４は、（１）命令列の集合から一つの命令列を取り出し、上記と同様に一列のモデルグラフを構成する。
【００６８】
次に、モデルグラフ構成部１０４は、（２）すでに構成されているモデルグラフと、それぞれの開始頂点から比較し、異なる命令文に対応するラベルが付記されている頂点が出現した場合にグラフを枝分かれさせ、元のモデルグラフに残りの命令列に対応する新たなモデルグラフを付加する。
【００６９】
次に、モデルグラフ構成部１０４は、（３）命令列の集合の要素がなくなるまで（１）に戻る、の手続きを（１）から順に実行する。これによってモデルグラフを構成することができる。そして、モデルグラフ構成部１０４は、構成されたモデルグラフを、モデル記述生成部１０５に受け渡す。図５に示すグラフは、図２で示したソースコードからパスを抽出した結果を基に構成したモデルグラフである。
【００７０】
このように、モデルグラフ構成部１０４は、図５に示すように遷移条件付き、つまりソースコードの意味する振る舞いを正確に再現したモデルグラフを構成する。
【００７１】
次に、モデル記述生成部１０５について詳細を述べる。ここでは、モデルグラフ構成部１０４から受け渡された図５に示すモデルグラフを基に、モデル検査器ＳＰＩＮ用モデル記述言語のプロメラによるモデル記述（図６に図示）を生成する例を挙げる。ここで生成するモデル記述は文字列の列である。図６は、図５のモデルグラフを基に生成したプロメラによるモデル記述である。
【００７２】
まず、モデル記述生成部１０５は、プロメラで記述するモデルの開始点を生成する。ここで開始点の記述は、６０１で示される部分で、「ｐｒｏｃｔｙｐｅ  ｍａｉｎ（）｛」である。
【００７３】
次に、モデル記述生成部１０５は、モデルグラフの開始点から順に頂点を選び、以下を実行する。
【００７４】
まず、モデル記述生成部１０５は、（１）選んだ頂点の次が分岐になっていない場合（図５中の５００ａ〜５００ｉで示される部分）、その頂点に付記されているラベルをＬとしたとき、図６中の６０２ａ〜６０２ｉに示すように、「Ｌ：ｓｋｉｐ；」をモデル記述に付加する。
【００７５】
次に、モデル記述生成部１０５は、続くモデルグラフ中の頂点を選び、（１）あるいは以下の（２）を実行する。
【００７６】
（２）、モデル記述生成部１０５は、選んだ頂点の次が分岐になっている場合（図５中の５０１で示される部分）、その頂点に付記されているラベルをＬとしたとき、図６中の６０３で示される部分以降に示すように、「Ｌ：  ｉｆ  ：：Ａ  ：：Ｂ  ｆｉ；」をモデル記述に付加する。
【００７７】
次に、モデル記述生成部１０５は、それぞれの分岐先の頂点を選び、それぞれ（１）、（２）を実行し、上記Ａ、Ｂを書き換える。この場合、Ａは図６中の６０４で示される部分、Ｂは６０５で示される部分である。
【００７８】
そして、モデル記述生成部１０５は、以上をモデルグラフの頂点全てを選び実行するまで繰り返す。最後に、図６中の６０６で示される、「｝」をモデル記述に加える。
【００７９】
モデル記述生成部１０５は、ここで得られたモデル記述をモデル検査器実行部１０６に受け渡す。
【００８０】
そして、モデル検査器実行部１０６では、上記モデル記述生成部から受け渡されたモデル記述と、仕様入力部１０７から受け取る仕様をモデル検査器に入力し、モデル検査の結果を検査結果１０９として出力する。
【００８１】
以上説明したように、第１実施例によれば、パス抽出部１０３がソースコードによって記述された応用プログラムを模擬に実行することで、実際に実行される命令列を抽出する。そして、検査内容決定部１２０に含まれるモデルグラフ構成部１０４が抽出した命令列からモデルグラフを構成し、モデル記述生成部１０５が構成したモデルグラフからモデル記述を生成するようにでき、ソースコードの検査を行うことができる。
【００８２】
このように、ソースコードを模擬に実行することにより、検査の対象とするソースコードの意味するプログラムの振る舞いを逸脱するモデル記述が生成されることがなくなる。このため、検査の対象とするソースコードの意味するプログラムの振る舞いを逸脱した部分に対応するモデル記述によって引き起こされる、誤った異常の検出が行われなくなる。すなわち、元々のソースコードの振る舞いでは検査対象の仕様の制約を満たしていたにもかかわらず、その振る舞いを逸脱したモデル記述が存在したために仕様の性質を満たさなくなった場合に検出される、仕様を満たさないという誤った検査結果を報告されることがなくなる。
【００８３】
また、モデル検査を行う前にモデルグラフを抽出しておくことで、モデルグラフを縮退させるなどの効率化手段を適用する余地を残すことが可能となる。
【００８４】
また、第１実施例によれば、従来必要だったソースコード変換テーブルをなくすことができるので、ソースコードを検査する人がソースコード変換テーブルを修正する必要がなくなる。
【００８５】
（第２実施例）
本発明の第２実施例について説明する。第２実施例では、パス抽出部１０３がプログラムを模擬に実行する方法として、ソースコードを論理式に変換し、その論理式の充足可能性判定を行うことで、実際に実行される命令列を抽出する。論理式の充足可能性判定とは、与えられた論理式全体を１、すなわち真とするような変数値の割り当てが存在するか否かを判定することである。
【００８６】
第２実施例におけるソースコード検査器を含むソースコード検査システムの構成は第１実施例と同様であるので、第１実施例におけるソースコード検査器について、図１を用いて説明する。
【００８７】
第２実施例におけるソースコード検査器１３０は、パス抽出部１０３において、ソースコード１０１を論理式に変換し、その論理式の充足可能性判定を行うことで、ソースコードの実行される命令列を抽出する。
【００８８】
ここでは、パス抽出部１０３は、ソースコード１０１を論理式に変換し、充足可能性判定を行うツールとして、モデル検査器ＣＢＭＣ（Ｂｏｕｎｄｅｄ  Ｍｏｄｅｌ  Ｃｈｅｃｋｅｒ  ｆｏｒ  ＡＮＳＩ−Ｃ  ｐｒｏｇｒａｍｓ）を利用する。ＣＢＭＣは、Ｃ言語のソースコードを入力とし、これを論理式に変換し、その論理式の充足可能性判定を行うことで入力されたソースコードの諸性質を検査するモデル検査器である。パス抽出部１０３は、パス抽出のため、アサート文を常に満たす、という性質を検査する機能を利用する。
【００８９】
パス抽出部１０３の処理について、図７を用いて具体的に説明する。図７は、本発明の第２実施例において、図２に示したソースコードを実行パス抽出のために改変した例を示す図である。
【００９０】
図７で示すソースコードは、図２に示すソースコードに対し、フラグ変数５０４、５０２および、アサート文５０３が挿入されている。
【００９１】
パス抽出部１０３は、検査の対象となるソースコード１０１を基に、その制御フローグラフを構成する。次に、パス抽出部１０３は、ＣＢＭＣに入力するためのＣ言語のソースコードを、入力のソースコードを改変することによって生成する。
【００９２】
まず、パス抽出部１０３は、第１実施例と同様、フラグ変数５０４の定義の挿入、代入文５０３の挿入を行う。
【００９３】
次に、パス抽出部１０３は、ソースコード１０１中に含まれるプログラム終了を意味する文の直前に、それぞれ上記手続きで挿入したフラグ変数の全てに１が代入されているということはないという意味の宣言文、すなわちアサート（ａｓｓｅｒｔ）文５０３を挿入する。例えば、フラグ変数がｆｌａｇ１、ｆｌａｇ２、ｆｌａｇ３の３つであったとするとき、挿入するアサート文は、「ａｓｓｅｒｔ（ｆｌａｇ１！＝１｜｜ｆｌａｇ２！＝１｜｜ｆｌａｇ３！＝１）」となる。
【００９４】
次に、パス抽出部１０３は、上記手続きによって改変し、得られたソースコードをＣＢＭＣに入力する。
【００９５】
このとき、もしアサート文の宣言に違反する場合がＣＢＭＣによって指摘されれば、挿入したフラグ変数が全て１になる場合があることを意味する。すなわち、フラグ変数に１を代入した箇所を全て通過する実行可能パスが存在することを意味する。
【００９６】
よって、ＣＢＭＣによるアサート文の違反の指摘は、ＣＢＭＣに入力し、実行した結果に、「Ｆａｉｌｅｄ  ａｓｓｅｒｔｉｏｎ：」の文字列が含まれる場合であり、パス抽出部１０３は、出力の文字列を検索することにより、アサート文の違反を判定できる。
【００９７】
パス抽出部１０３は、実行可能パスと判定された場合、そのパスに対応する命令列の情報を検査内容決定部１２０に含まれるモデルグラフ構成部１０４に受け渡す。
【００９８】
パス抽出部１０３は、上記手続きをフラグ変数５０２に１を代入する箇所を変更しながら繰り返すことで、モデルグラフ構成部１０４に実行可能な命令列の情報を集積する。
【００９９】
このように、十分な情報が集積された後、第１実施例で挙げたモデルグラフ構成部１０４の実行、およびそれ以後の実行を同様に行うことで、ソースコードの検査を行うことができる。
【０１００】
以上説明したように、本実施例によれば、パス抽出部１０３において、ソースコード１０１を論理式に変換し、論理式の充足可能性判定を行うことで、ソースコード１０１の実行される可能性のある命令列を抽出できる。これにより、検査の対象とするソースコード１０１で与えられるプログラムを実際に実行することを必要とせずにプログラムの振る舞いを抽出することができる。このように、検証の対象とするソースコード１０１を実際にコンパイル、リンクして実行可能にする必要がないため、例えばリンクなどができない、一連のソースコード群から一部のソースコードの集合だけを対象としたモデル検査を行うことが可能となる。
【０１０１】
（第３実施例）
本発明の第３実施例は、ソースコードの情報を基にモデル検査器実行部に入力する仕様を自動的に生成する手段を備えたものである。
【０１０２】
以下、第３実施例にかかるソースコード検査器について説明する。図８は、本発明の第３実施例におけるソースコード検査器を含むソースコード検査システムのブロック図である。なお、図１の構成と同様の構成を有するものについては、同一符号を付しその説明を省略する。
【０１０３】
本実施例におけるソースコード検査システム６００は、ソースコード入力部１０２によって受け入れられたソースコード１０１の情報を基に、モデル検査器実行部１０６に入力する仕様を自動的に生成する仕様自動生成部６０１を備えた点が特徴である。ソースコード検査器１３１は、ソースコード入力部１０２と、パス抽出部１０３と、検査内容決定部１２０と、仕様自動生成部６０１と、制御部１４０と、記憶媒体１５０とを備える。
【０１０４】
次に、仕様自動生成部６０１の仕様の自動生成法について述べる。
【０１０５】
まず、仕様自動生成部６０１は、ソースコード入力部１０２によって受け入れられたソースコード１０１を読み込み、必ず対になって使われるべき命令文を全て検索する。
【０１０６】
例えば、Ｃ言語で記述されたソースコードを扱う場合は、ｆｏｐｅｎに対するｆｃｌｏｓｅ、ｏｐｅｎに対するｃｌｏｓｅ、ｍａｌｌｏｃやｃａｌｌｏｃなどメモリをヒープ領域に確保する文に対するｆｒｅｅを含む命令文などが、それぞれ必ず対になって使われるべき命令文である。
【０１０７】
次に、仕様自動生成部６０１は、上記手続きで検索した結果として検出された命令文の対Ａ、Ｂについて、仕様に以下の式、「［］（Ａ−＞＜＞Ｂ）」を加える。
【０１０８】
上式は、Ａが出現した場合に、必ずＢが出現するという制約を表す式である。
【０１０９】
例えばｆｐ＝ｆｏｐｅｎ（ｆｎａｍｅ，“ｗ”）と、ｆｃｌｏｓｅ（ｆｐ）という対になる命令文が存在した場合、仕様自動生成部６０１は、以下の式、「［］（“ｆｐ＝ｆｏｐｅｎ（ｆｎａｍｅ，“ｗ”）”−＞＜＞“ｆｃｌｏｓｅ（ｆｐ）”）」を仕様に加える。
【０１１０】
仕様自動生成部６０１は、以上の処理を、全ての検出された文の対について繰り返す。
【０１１１】
また、仕様自動生成部６０１は、すでに仕様として式が存在し、これに新たな式を加える場合は、演算子“＆＆”を用いて連結する。演算子“＆＆”は論理積を表し、制約を新たに追加する場合に用いられる。
【０１１２】
以上説明したように、第３実施例によれば、第１実施例と違いユーザが仕様有力部１０７から仕様１０８を入力する必要がなくなり、例えばソースコードによって記述された応用プログラムがメモリの不正使用を行わないことを意味する仕様を自動生成できる。つまり、煩わしく、ときに専門知識を要する仕様１０８の入力を必要としなくなる。
【０１１３】
（第４実施例）
本発明の第４実施例は、抽出された実行される可能性のある命令列がメモリの不正使用を行わないかどうかを判定するものである。
【０１１４】
以下、本実施例におけるソースコード検査器について、図９を用いて説明する。図９は、本実施例におけるソースコード検査器の構成を示すブロック図である。なお、図１の構成と同様の構成を有するものについては、同一符号を付しその説明を省略する。
【０１１５】
第４実施例におけるソースコード検査器７００は、ソースコード入力部１０２と、パス抽出部１０３と、検査内容決定部１２２と、制御部１４０と、記憶媒体１５０とを備える。検査内容決定部１２２は、検証プログラム生成部７０１と、検証プログラム実行部７０２とを備える。検証プログラム生成部７０１は、パス抽出部１０３によって抽出された実行される可能性のある命令列を受け取り、その命令列がメモリの不正使用を行わないかどうかを単独で判定するための検証プログラムを生成する。検証プログラム実行部７０２は、検証プログラム生成部７０１で生成された検証プログラムを実行する。
【０１１６】
次に、検証プログラム生成部７０１における、検証プログラム生成方法について、詳細を述べる。検証プログラム生成部７０１が、生成する検証プログラムは、パス抽出部１０３によって抽出された実行される可能性のある命令列を基に生成する文字列からなる。
【０１１７】
検証プログラム生成部７０１が、この文字列を生成する手順について、図１０を用いて説明する。図１０は、本実施例において、図５に示すグラフの左側の分岐をもとに、検証プログラム生成部７０１での処理によって生成されたプログラムの例を示す図である。
【０１１８】
まず、検証プログラム生成部７０１は、１００１で示される部分、「ｉｎｔ  ｍａｉｎ（）｛  （１００１）」を開始文字列とする。検証プログラム生成部７０１は、この開始文字列１００１に文字列を順に付加していくことで、検証プログラムの文字列を構成する。次に、検証プログラム生成部７０１は、パス抽出部１０３で生成された命令列に対応する命令文にセミコロンを付加した文字列を順に上記開始文字列に付加する。
【０１１９】
このとき、図５の５００ｃに示すようにｍａｌｌｏｃ関数が存在し、かつ、図５の５００ｄ、５００ｅに示すようにｗｚ＿ｍａｌｌｏｃ、ｆｒｅｅ関数が存在した場合、検証プログラム生成部７０１は、ｗｚ＿ｍａｌｌｏｃ、ｆｒｅｅ関数を図１０中の１００２に示すようにｗｚ＿ｆｒｅｅと置き換える。
【０１２０】
また、命令列に含まれる式中にポインタ変数が含まれる場合、検証プログラム生成部７０１は、そのポインタ変数のそれぞれについて、そのポインタ変数を引数としたｗｚ＿ｃｈｅｃｋ関数の呼び出し文を式の前に挿入する。
【０１２１】
また、命令列の最後がｒｅｔｕｒｎ文でなかった場合は、検証プログラム生成部７０１は、「ｒｅｔｕｒｎ  ０；｝」を、また、ｒｅｔｕｒｎであった場合は、図１０中１００３に示すように、「｝」を付加する。
【０１２２】
最後に、検証プログラム生成部７０１は、図１１〜図１３に示す文字列を付加する。
【０１２３】
以上のように、検証プログラム生成部７０１は、検証プログラムを生成する。そして、検証プログラム生成部７０１は、生成した検証プログラムを検証プログラム実行部７０２に受け渡す。
【０１２４】
検証プログラム実行部７０２では、検証プログラム生成部７０１から受け渡された検証プログラムをコンパイルし、実行する。実行した結果を検査結果１０９として表示する。ここで、「Ｍｅｍｏｒｙ  ｌｅａｋ  ｗａｓ  ｄｅｔｅｃｔｅｄ．」と表示されると、パス抽出部１０３によって抽出された命令列が実行された場合に、メモリリークが発生することを検出したことを意味する。
【０１２５】
また、「Ｕｓｅｄ  ｎｏｎ−ａｃｔｉｖｅ  ｏｂｊｅｃｔ．」と表示されると、パス抽出部１０３によって抽出された命令列が実行された場合に、ヌルポインタを使用しようとすることを検出したことを意味する。
【０１２６】
以上説明したように、本実施例によれば、検証プログラム生成部７０１で、プログラムがメモリの不正使用を行わないことを意味する仕様を自動的に生成するので、メモリの不正使用に関する知識を必要とせず、メモリの不正使用に関するソースコード検査を行うことが可能となる。また、第１実施例における仕様入力部１０７を必要とせず、プログラムのメモリの不正使用に関する検査を行うことができるようになる。
【０１２７】
また、本実施例によれば、単独でソースコード検査を行えるプログラムを出力することにより、第１実施例におけるモデル検査器実行部１０６を不要とすることができる。すなわち外部のモデル検査器を用いる必要がなくなるため、可搬性、および利便性が向上する。
【産業上の利用可能性】
【０１２８】
以上のように、本発明によれば、ソースコードの意味するプログラムの振る舞いを逸脱することなく、ソースコードの検査を行うことができる。検査の対象とするソースコードの意味する振る舞いを逸脱することなく、より正確にソースコードの検査を実現することができる。また、本発明は、ソフトウェアの正当性検査等の分野に適用でき、その利用可能性は大きい。
【図面の簡単な説明】
【０１２９】
【図１】本発明の第１実施例におけるソースコード検査器を含むソースコード検査システムのブロック図
【図２】同実施例における検証の対象となるソースコードの例を示す図
【図３】図２で示したソースコードを基に構成した制御フローグラフを示す図
【図４】図２で示したソースコードをパス抽出用に改変したソースコードを示す図
【図５】図２で示したソースコードからパスを抽出した結果を基に構成したモデルグラフを示す図
【図６】図５のモデルグラフを基に生成したモデル記述を示す図
【図７】本発明の第２実施例に係わり、図２で示したソースコードを、ＣＢＭＣを用いたパス抽出用に改変したソースコードを示す図
【図８】本発明の第３実施例におけるソースコード検査器を含むソースコード検査システムのブロック図
【図９】本発明の第４実施例におけるソースコード検査器のブロック図
【図１０】同実施例における検証プログラムの例を示す図
【図１１】同実施例における、検証プログラムの一部を示す第１の図
【図１２】同実施例における、検証プログラムの一部を示す第２の図
【図１３】同実施例における、検証プログラムの一部を示す第３の図
【図１４】従来のソースコード検査器の構成を表すブロック図
【符号の説明】
【０１３０】
１００，６００    ソースコード検査システム
１０２    ソースコード入力部
１０３    パス抽出部
１０４    モデルグラフ構成部
１０５    モデル記述生成部
１０６    モデル検査器実行部
１０７    仕様入力部
１２０，１２２    検査内容決定部
１３０，１３１，７００    ソースコード検査器
１４０    制御部
１５０    記憶媒体
６０１    仕様自動生成部
７０１    検証プログラム生成部
７０２    検証プログラム実行部
【手続補正３】
【補正対象書類名】図面
【補正対象項目名】全図
【補正方法】変更
【補正の内容】
【図１】
2006038394.tif 000016
【図２】
2006038394.tif 000017
【図３】
2006038394.tif 000018
【図４】
2006038394.tif 000019
【図５】
2006038394.tif 000020
【図６】
2006038394.tif 000021
【図７】
2006038394.tif 000022
【図８】
2006038394.tif 000023
【図９】
2006038394.tif 000024
【図１０】
2006038394.tif 000025
【図１１】
2006038394.tif 000026
【図１２】
2006038394.tif 000027
【図１３】
2006038394.tif 000028
【図１４】
2006038394.tif 000029
【国際調査報告】
2006038394.tif 000030
2006038394.tif 000031
2006038394.tif 000032
2006038394.tif 000033