(57)【要約】【課題】関数実行に伴って書き換えられる可能性がある変数と、当該変数の書き換え条件を判断するための情報を出力できる副作用解析装置を提供する。【解決手段】条件検出部１１７は、記憶装置１２３に記憶されたプログラムソースコード１２４に対して記号実行を行う。条件検出部１１７は、プログラムソースコード１２４に含まれる関数が入力変数に与える影響を調べると共に、入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する。副作用解析部１１６は、関数の実行に伴って書き換えられる可能性がある入力変数に対して、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する。【選択図】図１
2011034250.tif 000002
【特許請求の範囲】
【請求項１】
記憶装置に記憶されたプログラムのソースコードに対して記号実行を行い、前記ソースコードに含まれる関数が入力変数に与える影響を調べると共に、前記入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する条件検出部と、
前記関数の実行に伴って書き換えられる可能性がある入力変数に対して、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する副作用解析部とを備える副作用解析装置。
【請求項２】
記号実行に際し、関数が書き換えられる可能性がある変数と該変数の書き換え条件とを含む表明情報を参照して、関数呼び出しを含むブロックに到達する経路条件と前記表明情報に含まれる書き換え条件とを組み合わせた論理式が証明可能か否かを調べ、呼び出し先の関数で、前記表明情報に含まれる書き換えられる可能性がある変数が書き換えられる可能性があるか、可能性がないか、又は、書き換えられる可能性があるか否かが不明かを判定するステート処理部を更に備える、請求項１に記載の副作用解析装置。
【請求項３】
前記ステート処理部は、関数呼び出しを含むブロックに到達する経路条件をcとし、前記変数の書き換え条件をpとして、c→pが証明可能なときは当該変数は書き換えられる可能性があると判定し、c→¬pが証明可能なときは当該変数は書き換えられる可能性がないと判定し、c→pとc→¬pとの双方が証明できないときは書き換えられる可能性があるか否かが不明と判定する、請求項２に記載の副作用解析装置。
【請求項４】
前記ステート処理部は、前記書き換えられる可能性があるか否かが不明と判定した変数を不明リストに保存し、該不明リストに含まれる各変数に対して、書き換えが発生するときと発生しないときとの組み合わせを生成し、該組み合わせに対応して、記号実行で用いる実行状態を生成する、請求項２又は３に記載の副作用解析装置。
【請求項５】
前記ステート処理部は、書き換えが発生するときと発生しないときとの組み合わせに対応して、各変数の書き換え条件を∧（ＡＮＤ）結合した条件式、各変数の書き換え条件の否定を∧（ＡＮＤ）結合した条件式、又は、各変数の書き換え条件と書き換え条件の否定とを∧（ＡＮＤ）結合した条件式と、関数呼び出しを含むブロックに到達する経路条件とを∧（ＡＮＤ）結合した条件式を、各組み合わせに対応する実行状態における経路条件とする、請求項４に記載の副作用解析装置。
【請求項６】
前記ソースコードを解析し、前記入力変数のうち、関数実行に伴って書き換えられる可能性がある入力変数を識別し、解析用変数リストに保存する識別部を更に備え、
前記条件検出部は、前記解析用変数リストに含まれる入力変数に対して、該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する、請求項１乃至５の何れか一に記載の副作用解析装置。
【請求項７】
前記副作用解析部は、前記書き換えられる可能性がある入力変数について、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件の否定を、当該入力変数が書き換えられる可能性がある条件として出力する、請求項１乃至６の何れか一に記載の副作用解析装置。
【請求項８】
前記副作用解析部は、１以上の記号実行で得られた、前記入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を∨（ＯＲ）で連結した条件式を生成し、該条件式の否定を、当該入力変数が書き換えられる可能性がある条件として出力する、請求項７に記載の副作用解析装置。
【請求項９】
前記副作用解析部は、前記書き換えが発生する入力変数について、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を、前記入力変数が書き換えられない条件として出力する、請求項１乃至６の何れか一に記載の副作用解析装置。
【請求項１０】
前記副作用解析部は、１以上の記号実行で得られた、前記入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を∧（ＡＮＤ）で連結した条件式を生成し、該条件式を、当該入力変数が書き換えられない条件として出力する、請求項９に記載の副作用解析装置。
【請求項１１】
コンピュータが、記憶装置に記憶されたプログラムのソースコードに対して記号実行を行い、前記ソースコードに含まれる関数が入力変数に与える影響を調べると共に、前記入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する条件検出ステップと、
前記コンピュータが、前記関数の実行に伴って書き換えられる可能性がある入力変数に対し、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する副作用解析ステップとを有する副作用解析方法。
【請求項１２】
前記コンピュータが、記号実行に際し、関数が書き換えられる可能性がある変数と該変数の書き換え条件とを含む表明情報を参照して、関数呼び出しを含むブロックに到達する経路条件と前記表明情報に含まれる書き換え条件とを組み合わせた論理式が証明可能か否かを調べ、呼び出し先の関数で、前記表明情報に含まれる書き換えられる可能性がある変数が書き換えられる可能性があるか、可能性がないか、又は、書き換えられる可能性があるか否かが不明かを判定するステート処理ステップを更に有する、請求項１１に記載の副作用解析方法。
【請求項１３】
前記ステート処理ステップでは、前記コンピュータは、関数呼び出しを含むブロックに到達する経路条件をcとし、前記変数の書き換え条件をpとして、c→pが証明可能なときは当該変数は書き換えられる可能性があると判定し、c→¬pが証明可能なときは当該変数は書き換えられる可能性がないと判定し、c→pとc→¬pとの双方が証明できないときは書き換えられる可能性があるか否かが不明と判定する、請求項１２に記載の副作用解析方法。
【請求項１４】
前記ステート処理ステップに後続して、前記コンピュータが、前記書き換えられる可能性があるか否かが不明と判定した変数を不明リストに保存し、該不明リストに含まれる各変数に対して、書き換えが発生するときと発生しないときとの組み合わせを生成し、該組み合わせに対応して、記号実行で用いる実行状態を生成するステップを更に有する、請求項１２又は１３に記載の副作用解析方法。
【請求項１５】
前記実行状態を生成するステップでは、前記コンピュータは、書き換えが発生するときと発生しないときとの組み合わせに対応して、各変数の書き換え条件を∧（ＡＮＤ）結合した条件式、各変数の書き換え条件の否定を∧（ＡＮＤ）結合した条件式、又は、各変数の書き換え条件と書き換え条件の否定とを∧（ＡＮＤ）結合した条件式と、関数呼び出しを含むブロックに到達する経路条件とを∧（ＡＮＤ）結合した条件式を、各組み合わせに対応する実行状態における経路条件とする、請求項１４に記載の副作用解析方法。
【請求項１６】
前記コンピュータが、前記ソースコードを解析し、前記入力変数のうち、関数実行に伴って書き換えられる可能性がある入力変数を識別し、解析用変数リストに保存する識別ステップを更に有し、
前記コンピュータは、前記条件検出ステップで、前記解析用変数リストに含まれる入力変数に対して、該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する、請求項１１乃至１５の何れか一に記載の副作用解析方法。
【請求項１７】
前記副作用解析ステップでは、前記コンピュータは、前記書き換えられる可能性がある入力変数について、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件の否定を、当該入力変数が書き換えられる可能性がある条件として出力する、請求項１１乃至１６の何れか一に記載の副作用解析方法。
【請求項１８】
前記副作用解析ステップでは、前記コンピュータは、１以上の記号実行で得られた、前記入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を∨（ＯＲ）で連結した条件式を生成し、該条件式の否定を、当該入力変数が書き換えられる可能性がある条件として出力する、請求項１７に記載の副作用解析方法。
【請求項１９】
前記副作用解析ステップでは、前記コンピュータは、前記書き換えが発生する入力変数について、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を、前記入力変数が書き換えられない条件として出力する、請求項１１乃至１６の何れか一に記載の副作用解析方法。
【請求項２０】
前記副作用解析ステップでは、前記コンピュータは、１以上の記号実行で得られた、前記入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を∧（ＡＮＤ）で連結した条件式を生成し、該条件式を、当該入力変数が書き換えられない条件として出力する、請求項１９に記載の副作用解析方法。
【請求項２１】
コンピュータに、
記憶装置に記憶されたプログラムのソースコードに対して記号実行を行い、前記ソースコードに含まれる関数が入力変数に与える影響を調べると共に、前記入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する条件検出処理と、
前記関数の実行に伴って書き換えられる可能性がある入力変数に対し、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する副作用解析処理とを実行させるプログラム。
【請求項２２】
前記コンピュータに、記号実行に際し、関数が書き換えられる可能性がある変数と該変数の書き換え条件とを含む表明情報を参照して、関数呼び出しを含むブロックに到達する経路条件と前記表明情報に含まれる書き換え条件とを組み合わせた論理式が証明可能か否かを調べ、呼び出し先の関数で、前記表明情報に含まれる書き換えられる可能性がある変数が書き換えられる可能性があるか、可能性がないか、又は、書き換えられる可能性があるか否かが不明かを判定するステート処理を更に実行させる、請求項２１に記載のプログラム。
【請求項２３】
前記ステート処理は、関数呼び出しを含むブロックに到達する経路条件をcとし、前記変数の書き換え条件をpとして、c→pが証明可能なときは当該変数は書き換えられる可能性があると判定し、c→¬pが証明可能なときは当該変数は書き換えられる可能性がないと判定し、c→pとc→¬pとの双方が証明できないときは書き換えられる可能性があるか否かが不明と判定する、請求項２２に記載のプログラム。
【請求項２４】
前記ステート処理に後続して、前記コンピュータに、前記書き換えられる可能性があるか否かが不明と判定した変数を不明リストに保存し、該不明リストに含まれる各変数に対して、書き換えが発生するときと発生しないときとの組み合わせを生成し、該組み合わせに対応して、記号実行で用いる実行状態を生成する処理を更に実行させる、請求項２２又は２３に記載のプログラム。
【請求項２５】
前記実行状態を生成する処理では、書き換えが発生するときと発生しないときとの組み合わせに対応して、各変数の書き換え条件を∧（ＡＮＤ）結合した条件式、各変数の書き換え条件の否定を∧（ＡＮＤ）結合した条件式、又は、各変数の書き換え条件と書き換え条件の否定とを∧（ＡＮＤ）結合した条件式と、関数呼び出しを含むブロックに到達する経路条件とを∧（ＡＮＤ）結合した条件式を、各組み合わせに対応する実行状態における経路条件とする、請求項２４に記載のプログラム。
【請求項２６】
前記コンピュータに、前記ソースコードを解析し、前記入力変数のうち、関数実行に伴って書き換えられる可能性がある入力変数を識別し、解析用変数リストに保存する識別処理を更に実行させ、
前記条件検出ステップでは、前記解析用変数リストに含まれる入力変数に対して、該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する、請求項２１乃至２５の何れか一に記載のプログラム。
【請求項２７】
前記副作用解析処理では、前記書き換えられる可能性がある入力変数について、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件の否定を、当該入力変数が書き換えられる可能性がある条件として出力する、請求項２１乃至２６の何れか一に記載のプログラム。
【請求項２８】
前記副作用解析処理では、１以上の記号実行で得られた、前記入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を∨（ＯＲ）で連結した条件式を生成し、該条件式の否定を、当該入力変数が書き換えられる可能性がある条件として出力する、請求項２７に記載のプログラム。
【請求項２９】
前記副作用解析処理では、前記書き換えが発生する入力変数について、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を、前記入力変数が書き換えられない条件として出力する、請求項２１乃至２６の何れか一に記載のプログラム。
【請求項３０】
前記副作用解析処理では、１以上の記号実行で得られた、前記入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を∧（ＡＮＤ）で連結した条件式を生成し、該条件式を、当該入力変数が書き換えられない条件として出力する、請求項２９に記載のプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、副作用解析装置、方法、及び、プログラムに関し、更に詳しくは、プログラム実行時に、関数が入力変数の書き換えを行うか否かを解析する副作用解析装置、方法、及び、プログラムに関する。
【背景技術】
【０００２】
副作用解析装置は、プログラムのソースコードを解析し、関数が持つ副作用を解析する装置である。ここで、プログラミングにおける副作用とは、ある機能が、コンピュータの論理的な状態を変化させ、それ以降で得られる結果に影響を与えることを指す。例えば、広域変数gと、局所変数xとがあり、ある関数でxを引数とする関数呼び出しがある場合を考える。この場合、関数呼び出し後に、呼び出し元の関数で変数gと変数xとが変化しなければ、呼び出し先の関数は副作用を持たない。
【０００３】
非特許文献１は、副作用解析装置が記載された文献である。非特許文献１に記載の副作用解析装置は、プログラム全体を静的に、つまり、プログラムを実行せずに解析し、各関数について、関数が書き換える可能性がある入力変数の一覧を出力する。図１５は、ソースプログラムの具体例を示している。このソースプログラムに記述された関数Sampleは、x、y、fを入力変数として持つ。非特許文献１に記載の副作用解析装置は、図１５に示すソースコードを静的に解析し、入力変数のうち、変数x、yが書き換えられる可能性がある変数と判定する。
【０００４】
関数の副作用を、プログラムに対する付加情報（表明）として記述する手法（表明記法と呼ぶ）には、非特許文献２に記載された記法を利用することができる。非特許文献２に記載されたＪＭＬ（Java Modeling Language）は、メソッドの事前条件、事後条件、及び、オブジェクトのフィールドに対する普遍条件を記述するための記法を提供する。その中で、modifies或いはassignableと呼ばれる式は、当該メソッドが書き換える可能性がある変数を記述するために利用される。
【０００５】
図１６は、図１５に示すソースコードを解析して得られた結果を、非特許文献２に記載の表明記法を用いて記述した例である。図１６の１行目は、“@modifies x:”であり、これは、変数xが書き換えられる可能性がある変数であることを示す記述である。２行目は、“@modifies y;”であり、これは、変数yが書き換えられる可能性があることを示す記述である。この記述は、プログラムの理解を促進するほか、プログラムの正しさを機械的に検査するためにも利用される。
【０００６】
ここで、非特許文献３は、プログラムソースコードに対して記号実行を行うことが記載された文献である。非特許文献３に記載の記号実行装置は、プログラムのソースコードについて、プログラムの実行経路を記号的に解析し、任意の実行時点における実行状態を出力する。この記号実行装置を利用し、関数からの脱出時点における実行状態を求めることで、各実行経路での関数の副作用を求めることができる。記号実行を行い、プログラムの実行を解析することで、プログラムの理解を深めることができると共に、得られた経路条件をテストケースの生成に利用することもできる。
【先行技術文献】
【非特許文献】
【０００７】
【非特許文献１】Barbara G. Ryder、他著「A Schema for Interprocedural Modification Side-Effect Analysis with Pointer Aliasing」ACM Transactions on Programming Languages and Systems、USA、ACM、２００１年３月、２３巻、１号、pp.１０５-１８６
【非特許文献２】Gary T. Leavens、他著「Preliminary Design of JML: A Behavioral Interface Specification Language for Java」ACM SIGSOFT Software Engineering Notes、USA、ACM、２００６年５月、３１巻、３号、ｐｐ．１−３７
【非特許文献３】James C. King、他著「Symbolic Execution and Program Testing」Communications of the ACM、USA、ACM、１９７６年７月、１９巻、７号、ｐｐ．３８５−３９４
【発明の概要】
【発明が解決しようとする課題】
【０００８】
ところで、変数がどのような条件が成り立つときに書き換えられるかという情報を得ることは、プログラム理解にとって非常に有用である。また、機械的にプログラムを検査する際の精度向上にも大きく寄与する。しかし、非特許文献１に記載の副作用解析装置は、書き換えられる可能性がある変数の一覧を示すのみであり、変数が書き換えられる条件は考慮していない。また、非特許文献２に記載の表明記法は、書き換えられる可能性がある変数を記述する記法を提供するが、書き換え条件を記述する記法は提供していない。非特許文献３に記載の記号実行装置は、実行経路上での実行状態を出力するのみであり、書き換えられる可能性がある変数と、その書き換え条件とを出力するものではない。
【０００９】
本発明は、上記に鑑み、関数実行に伴って書き換えられる可能性がある変数と、当該変数の書き換え条件を判断するための情報を出力できる副作用解析装置、方法、及び、プログラムを提供することを目的とする。
【課題を解決するための手段】
【００１０】
上記目的を達成するために、本発明は、記憶装置に記憶されたプログラムのソースコードに対して記号実行を行い、前記ソースコードに含まれる関数が入力変数に与える影響を調べると共に、前記入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する条件検出部と、前記関数の実行に伴って書き換えられる可能性がある入力変数に対して、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する副作用解析部とを備える副作用解析装置を提供する。
【００１１】
本発明は、コンピュータが、記憶装置に記憶されたプログラムのソースコードに対して記号実行を行い、前記ソースコードに含まれる関数が入力変数に与える影響を調べると共に、前記入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する条件検出ステップと、前記コンピュータが、前記関数の実行に伴って書き換えられる可能性がある入力変数に対し、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する副作用解析ステップとを有する副作用解析方法を提供する。
【００１２】
本発明は、コンピュータに、記憶装置に記憶されたプログラムのソースコードに対して記号実行を行い、前記ソースコードに含まれる関数が入力変数に与える影響を調べると共に、前記入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する条件検出処理と、前記関数の実行に伴って書き換えられる可能性がある入力変数に対し、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する副作用解析処理とを実行させるプログラムを提供する。
【発明の効果】
【００１３】
本発明の副作用解析装置、方法、及び、プログラム関数実行に伴って書き換えられる可能性がある変数と、当該変数の書き換え条件を判断するための情報を出力することができる。
【図面の簡単な説明】
【００１４】
【図１】本発明の第１実施形態の副作用解析装置を示すブロック図。
【図２】実行状態を示す図。
【図３】変数表を示す図。
【図４】動作手順を示すフローチャート。
【図５】制御フローグラフを示すブロック図。
【図６】出力例を示す図。
【図７】本発明の第２実施形態の副作用解析装置を示すブロック図。
【図８】代入場所識別表を示す図。
【図９】第２実施形態における動作手順を示すフローチャート。
【図１０】ステート処理の動作手順を示すフローチャート。
【図１１】ステート処理で生成される実行状態を示す図。
【図１２】プログラムソースコードを示す図。
【図１３】表明情報を示す図。
【図１４】制御フローグラフを示すブロック図。
【図１５】プログラムソースコードを示す図。
【図１６】非特許文献１に記載の副作用解析装置で得られる結果の出力例を示す図。
【発明を実施するための形態】
【００１５】
以下、図面を参照し、本発明の実施の形態を詳細に説明する。図１は、本発明の第１実施形態の副作用解析装置を示している。副作用解析装置１００は、入力装置１１１、計算機１１２、出力装置１２２、及び、記憶装置１２３を有する。計算機１１２は、構文解析部１１３、初期化部１１５、副作用解析部１１６、条件検出部１１７、代入処理部１１８、分岐判定部１２０、及び、定理証明部１２１を有する。副作用解析装置１００は、記号実行を行い、書き換えられる可能性がある入力変数と、その入力変数が書き換えられる条件を判断するための情報とを出力する。
【００１６】
計算機１１２は、プログラム制御で動作する中央処理装置、プロセッサ、或いは、データ処理装置である。計算機１１２内の各部の機能は、計算機１１２が所定のプログラムに従って処理を実行することで実現できる。入力装置１１１は、キーボートやマウスなどの入力装置である。出力装置１２２は、モニターなどの出力装置である。記憶装置１２３は、ハードディスクドライブやメモリ装置などの記憶装置である。なお、以下では、関数の値は参照渡しであるとする。
【００１７】
構文解析部１１３は、記憶装置１２３からプログラムソースコード１２４を読み込む。プログラムソースコード１２４は、１以上の関数を含む。構文解析部１１３は、ソースコードの構文解析を行い、制御フローグラフを生成する。なお、本明細書では、説明を簡潔にするため、関数の引数は参照渡しを仮定する。すなわち、関数の仮引数に対する書き換えが発生すると、呼び出し元の実引数に渡される変数の値が書き換えられるものとする。
【００１８】
初期化部１１５は、記憶装置１２３内の待機実行リスト１２６を初期化する。待機実行リスト１２６は、記号実行の際に使用される実行状態１２７を格納するリストである。副作用解析部１１６は、待機実行リスト１２６から実行状態１２７を取り出し、条件検出部１１７に記号実行を指示する。
【００１９】
条件検出部１１７は、実行状態１２７に対して記号実行を進める。条件検出部１１７は、記号実行を行い、プログラムソースコード１２４に含まれる関数が入力変数に与える影響を調べる。ここで、入力変数とは、関数の入力となる引数や広域変数を指す。条件検出部１１７は、記号実行の結果、入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する。代入処理部１１８は、記号実行の際に、代入文に対応する処理を行う。分岐判定部１２０は、分岐条件に対応する記号実行を行う。定理証明部１２１は、経路条件と分岐条件とから、分岐先に進めるか否かを判定するための定理証明を行う。
【００２０】
副作用解析部１１６は、条件検出部１１７から、書き換えられる可能性がある入力変数の一覧を受け取る。また、副作用解析部１１６は、条件検出部１１７から、書き換えられる可能性がある入力変数について、その入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を受け取る。副作用解析部１１６は、その経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する。副作用解析部１１６は、出力装置１２２に、関数の実行に伴って書き換えられる可能性がある入力変数を出力すると共に、当該入力変数が書き換えられる条件を判断するための情報を出力する。
【００２１】
図２は、実行状態１２７の例を示している。実行状態１２７は、プログラムカウンタ、経路条件、及び、変数表を含む。プログラムカウンタは、記号実行にて、実行状態１２７がプログラム中のどの部分を実行中かを指すカウンタである。変数表は、プログラムで使用する変数と、プログラムカウンタが示すプログラム箇所での変数の値とを対応付けた表である。図３は、変数表を示している。変数表を参照することで、記号実行に際し、プログラムカウンタが示す場所に該当するプログラム箇所で、各変数が、どのような値をとるかを知ることができる。
【００２２】
経路条件は、実行状態が経由した条件分岐の条件から構成される論理式である。経路条件は、各変数が変数表に示す値で、プログラムカウンタが示すプログラム箇所に到達する条件を表している。この条件は、関数の入力（引数や広域変数）に対応する論理式として表現されるため、経路条件は、実行状態のプログラムカウンタが示すプログラム箇所に到達するために必要となる入力に対する制約条件と見ることができる。
【００２３】
図４は、動作手順を示している。ユーザは、入力装置１１１を用いて、記号実行をすべき対象のプログラム（関数）の名称や場所を指定する。構文解析部１１３は、指定されたプログラムソースコード１２３を読み込み、プログラムの構文解析を行うと共に、解析に適した制御フローグラフを生成する（ステップＡ１）。
【００２４】
図５は、制御フローグラフを示している。図５に示す制御フローグラフは、図１５に示す関数sampleに対応した制御フローグラフである。制御フローグラフ（図５）は、ソースプログラム（図１５）の各文に対応するブロックを、制御の流れに従って有向辺で接続したものである。各ブロックには、一意に識別可能な値が割り当てられる。図５では、条件分岐の前にSkip文を挿入するようにしている。Skipから出る辺には、条件文に含まれる条件式に対応するラベルが貼られる。
【００２５】
初期化部１１５は、初期化した実行状態（初期実行状態）を生成し、空の待機実行リスト１２６に生成した初期実行状態を加える（ステップＡ２）。初期化部１１５は、初期実行状態のプログラムカウンタに、制御フローグラフの開始ブロック（entry）に割り当てられた値（識別番号）を格納する。また、初期化部１１５は、経路条件の式をtrueに設定する。初期化部１１５は、ソースプログラム中に含まれる変数について変数表を作成し、これを初期実行状態に格納する。
【００２６】
初期化部１１５は、変数表の作成では、入力変数に対して、当該変数に対応する記号値を割り当て、それ以外の変数については未定義（UNKOWN）の値を割り当てる。初期化部１１５は、例えば入力変数xに対する記号値を、s(x)で表現する。図１５のソースプログラムでは、関数の引数であるx、y、fが入力変数に該当する。初期化部１１５は、これら入力変数に対してそれぞれ、s(x)、s(y)、s(f)を、初期の記号値として割り当て、変数表に格納する。入力変数に対する記号値の表現は、上記したもの限られず、任意の記法を用いることができる。
【００２７】
副作用解析部１１６は、待機実行リスト１２６が空か否かを判断する（ステップＡ３）。副作用解析部１１６は、待機実行リスト１２６が空でないときは、待機実行リスト１２６から実行状態１２７を一つ取り出し、それを条件検出部１１７に渡す。はじめ、待機実行リストには、初期化部１１５が生成した初期実行状態が含まれるので、副作用解析部１１６は、初期実行状態を条件検出部１１７に渡す。
【００２８】
条件検出部１１７は、実行状態１２７に対して記号実行を進める。条件検出部１１７は、制御フローグラフの脱出ブロック、つまり、それ以上遷移が発生しないブロックに到達したか否かを判断する（ステップＡ４）。条件検出部１１７は、実行状態１２７のプログラムカウンタが示す制御フロー内のブロックが、脱出ブロックでないときは、記号実行を継続する。
【００２９】
条件検出部１１７は、実行状態１２７のプログラムカウンタが示すブロックが、代入を行うブロックであるか、又は、条件分岐を行うブロックであるかを判断する（ステップＡ５）。条件検出部１１７は、プログラムカウンタが示すブロックが代入ブロックであれば処理を代入処理部１１８に移す。条件検出部１１７は、プログラムカウンタが示すブロックが条件分岐（すなわちskip）であれば、処理を分岐判定部１２０に移す。
【００３０】
代入処理部１１８は、実行状態のプログラムカウンタが示すブロックに含まれる式の作用を、当該実行状態に含まれる変数表の値に反映させる（ステップＡ６）。例えば、代入文がv=e；であったとする。vは代入される変数であり、式eは、定数又は変数を含む式である。代入処理部１１８は、変数表を参照して式eに含まれる変数を記号値に置き換えた上で式eを計算し、計算した値を、変数表のvに対応する記号値に格納する。
【００３１】
式eに含まれる変数の値（記号値）に、s(*)の形式の記号が含まれなければ、式eは計算可能である。この場合、代入処理部１１８は、式eに含まれる変数を変数表に格納された記号値で定数化し、vの記号値に式eを計算した値を格納する。一方、式eに含まれる変数の値にs(*)の形式の記号が含まれる場合、代入処理部１１８は、まず、変数表を参照して、式eにて計算が可能な部分を計算し定数化する。次いで、代入処理部１１８は、定数化した部分とs(*)形式の記号とを含む式を、変数表におけるvの記号値に格納する。代入処理部１１８は、変数表の値を更新した後、プログラムカウンタの値を当該ブロックに続くブロックの値に書き換える。その後、代入処理部１１８は、処理を条件検出部１１７に戻す。
【００３２】
分岐判定部１２０は、分岐判定処理を行う（ステップＡ７）。分岐判定部１２０は、まず、プログラムカウンタが示すブロックから出力される有向辺に割り当てられたラベルを取得する。次いで、分岐判定部１２０は、当該ラベルに含まれる条件式eと、実行状態に含まれる経路条件cとを用いて、c→eという論理式を作成する。c→eは、経路条件cならば条件式eが成立するという論理式である。この論理式の値は、¬c∨eと同値である。分岐判定部１２０は、定理証明部１２１を用いて、作成した論理式が証明可能か否かを判定する。定理証明部１２１は、条件式eに含まれる変数を、変数表に格納された記号値で置き換えた上で定理証明を行う。条件式eに含まれる変数を記号値で置き換える処理は、代入処理における式eに対する処理と同様である。
【００３３】
論理式c→eが証明可能であるということは、経路条件cで分岐ブロックへ到達したとき、分岐ブロックの分岐条件が成立するということを意味する。つまり、制御フローグラフにて、分岐ブロックの有向辺が指すブロックへの遷移が可能であることを意味する。分岐判定部１２０は、定理証明部１２１で論理式c→eが証明可能であると判定されると、実行状態のプログラムカウンタの値を、ラベルに対応する有向辺が指すブロックに割り当てられた値に書き換える。
【００３４】
分岐判定部１２０は、分岐ブロックから出力される２つの有向辺に割り当てられたラベルのそれぞれについて、定理証明部１２１を用いて証明可能か否かを判定する。分岐ブロックの一方のラベル含まれる条件式は、他方のラベルに含まれる条件式の否定であるため、何れか一方のラベルが証明できた場合、常に、もう一方のラベルは証明に失敗する。従って、何れか一方が証明された場合、分岐ブロックからどちらか一方への遷移しか発生しない。一方、定理証明部１２１にて、２つのラベルのそれぞれについて証明に失敗する場合は、分岐ブロックから、２つのブロックの何れへ遷移するかは不定である。その場合、分岐判定部１２０は、２つの分岐のそれぞれに対応する実行状態を生成する。その後、分岐判定部１２０は、処理を条件検出部１１７に戻す。
【００３５】
２つの分岐のそれぞれに対応する実行状態の生成の詳細な手順について説明する。分岐ブロックの２つのラベル（ラベル１、ラベル２）に含まれる条件式をそれぞれe、¬eとする。これら式に含まれる変数の値は、変数表を用いて対応する記号値に置き換えておく。分岐判定部１２０は、ラベル１に対応する実行状態におけるプログラムカウンタの値に、ラベル１に対応する有向辺が指すブロックに割り当てられた値を格納する。また、分岐判定部１２０は、経路条件cに条件式ｅを連接したc∧eを、新しい経路条件として格納する。変数表の値は、変化しない。分岐判定部１２０は、ラベル２についても同様に、実行状態を生成する。分岐判定部１２０は、生成した実行状態のうちの１つを待機実行リスト１２６に追加する。分岐判定部１２０は、生成した残り１つを条件検出部１１７に渡す。条件検出部１１７は、渡された実行状態について、記号実行を継続する。
【００３６】
条件検出部１１７は、代入処理部１１８又は分岐判定部１２０から処理が戻ると、ステップＡ４で、プログラムカウンタが示すブロックが脱出ブロックであるか否かを判断する。条件検出部１１７は、脱出ブロックに到達したときは、記号実行を終了する。なお、条件検出部１１７は、記号実行のステップ数をカウントし、カウント数が事前に定義した上限に達したときは、脱出ブロックに到達していなくても、その時点で記号実行を終了してもよい。或いは、条件検出部１１７は、タイマーを用いて、記号実行開始からの経過時間を計測し、経過時間が所定の時間を超えたら、その時点で記号実行を終了してもよい。
【００３７】
条件検出部１１７は、記号実行を終了すると、脱出ブロックにおける実行状態に基づいて、入力変数に対する変数書き換えの有無を検出する。例えば、入力変数xがあり、実行状態の変数表におけるxの記号値がs(x)であれば、条件検出部１１７は、入力変数xは書き換えが発生しない変数と判断する。条件検出部１１７は、実行状態の変数表におけるxの記号値がs(x)以外の値のときは、入力変数xは書き換えが発生する変数であると判断する。
【００３８】
条件検出部１１７は、書き換えられることなく関数の脱出ブロックに到達した入力変数があるか否かを判断する。条件検出部１１７は、書き換えられない入力変数があるときは、脱出ブロックに到達した実行状態に含まれる経路条件を、当該入力変数が書き換えられることなく脱出ブロックに到達する経路条件として検出する。条件検出部１１７は、書き換え発生の有無と、書き換えが発生しない入力変数が脱出ブロックに到達する経路条件とを、副作用解析部１１６に渡し、処理を副作用解析部１１６に戻す。
【００３９】
副作用解析部１１６は、ステップＡ３で、待機実行リスト１２７に未処理の実行状態があるか否かを調べる。副作用解析部１１６は、ステップＡ７の分岐判定処理で生成された実行状態が待機実行リスト１２７に残っているときは、実行状態を１つ取り出して、条件検出部１１７に渡す。条件検出部１１７は、記号実行を行い、各入力変数について、書き換え発生の有無と、書き換えが発生しない入力変数が脱出ブロックに到達する経路条件とを副作用解析部１１６に渡す。
【００４０】
副作用解析部１１６は、待機実行リスト１２６に含まれる実行状態の全てについて記号実行が終了すると、条件検出部１１７から受け取った入力変数に対する書き換え発生の有無、及び、入力変数が書き換えられることなく脱出ブロックに到達する経路条件に基づいて、書き換えが発生する入力変数が書き換えられる条件を判断するための情報を生成する。副作用解析部１１６は、書き換えられる可能性がある入力変数と、その入力変数が書き換えられる可能性がある条件とを、出力装置１２２に出力する（ステップＡ８）。
【００４１】
副作用解析部１１６は、ステップＡ８では、まず、入力変数のうち、１以上の記号実行の何れかで書き換えが発生した入力変数を、書き換えられる可能性がある入力変数とする。次いで、副作用解析部１１６は、書き換えられる可能性があるとした入力変数について、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を求める。副作用解析部１１６は、１以上の記号実行で得られた、書き換えられる可能性がある入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を∨（ＯＲ）で連結した条件式を生成する。
【００４２】
副作用解析部１１６は、上記で生成した論理式の否定を、入力変数が書き換えられる条件を判断するための情報として生成する。或いは、これに代えて、副作用解析部１１６は、１以上の記号実行で得られた、書き換えられる可能性がある入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を∧（ＡＮＤ）で連結した条件式を、入力変数が書き換えられる条件を判断するための情報として生成してもよい。
【００４３】
図１５と図５とに示す具体例を用いて、副作用解析装置１００の振る舞いをより具体的に説明する。図５に示す制御フローグラフで、点線で囲われた箇所は、記号実行の結果を表している。実行状態１は、初期化部１１５が生成した初期実行状態に該当する。初期実行状態における経路条件は、PC={true}である。図１５に示すソースプログラムは、x,y,fの３つの入力変数を持っており、変数表には、これら入力変数に対応して、それぞれs(x),s(y),s(f)が格納される。プログラムカウンタの値は、entryのブロックに対応する識別番号“１”が格納される。
【００４４】
副作用解析部１１６は、実行状態１を待機実行リスト１２６から取り出し、条件検出部１１７に渡す。条件検出部１１７は、プログラムカウンタが示す識別番号“１”のブロックから記号実行を開始する。条件検出部１１７は、識別番号“２”のブロックは条件分岐のブロックであるので、処理を分岐判定部１２０に渡す。分岐判定部１２０は、定理判定部１２１を用いて、経路条件（true）→分岐条件（f==1）と経路条件（true）→分岐条件¬（f==1）とがそれぞれ証明可能か否かを判定する。
【００４５】
定理証明部１２１は、true→s(f)==1とtrue→¬(s(f)==1)はどちらも証明できないため、証明に失敗する。分岐判定部１２０は、分岐先に対応する実行状態を２つ生成する。分岐判定部１２０は、s(f)==1のラベルに対応して、経路条件をPC={(s(f)==1)}としプログラムカウンタを識別番号“３”とした実行状態を生成する。また、分岐判定部１２０は、経路条件をPC={!(s(f)==1)}としプログラムカウンタを識別番号“４”とした実行状態を生成する。分岐判定部１２０は、生成した２つの実行状態のうちの１つを条件検出部１１７に渡して記号実行を継続させると共に、もう１つを待機実行リスト１２６に追加する。ここでは、s(f)==1のラベルに対応した実行状態を条件検出部１１７に渡し、¬s(f)==1のラベルに対応した実行状態を待機実行リスト１２６に追加するものとする。
【００４６】
条件検出部１１７は、識別番号“３”のブロックに進む。このブロックは代入文であるので、条件検出部１１７は、代入処理部１１８に処理を渡す。代入文の内容は、y=x-1である。代入処理部１１８は、変数表を参照して、代入文の右辺を、記号値を用いた式に書き換える。変数表を参照すると、x=s(x)であるので、代入文の右辺はs(x)-1となる。代入処理部１１８は、変数表におけるyの記号値を、s(x)-1に書き換える。図５に示す実行状態２−１は、代入処理が終わった後の値が変数表に反映された実行状態を表している。実行状態２−１の経路条件は、PC={(s(f)==1)}で、変数表は、x=s(x),y=s(x)-1,f=s(f)となる。
【００４７】
条件検出部１１７は、実行状態２−１について、記号実行を進める。条件検出部１１７は、次のブロックは条件分岐のブロックであるので、分岐判定部１２０に処理を渡す。分岐判定部１２０は、定理証明部１２１を用いて、経路条件PC={(s(f)==1)}→分岐条件x>yが証明可能か否かを判定する。変数表を用いてx,yを記号値に置き換えると、証明すべき論理式は、s(f)==1→s(x)>s(x)-1となる。定理証明部１２１は、s(x)>s(x)-1は常に真なので、証明可能と判断する。分岐判定部１２０は、分岐条件が定理証明部１２１にて証明可能と判断されるので、プログラムカウンタに、x>yのラベルに対応する有向辺が向かうブロックの番号（識別番号“６”）を格納する。
【００４８】
条件検出部１１７は、識別番号“６”のブロックは代入文であるので、処理を代入処理部１１８へ渡す。代入文の内容は、x=1であるので、代入処理部１１８は、変数表におけるxに対応する記号値を1に書き換える。図５に示す実行状態３−１は、代入処理が終わった後の値が変数表に反映された実行状態を表している。条件検出部１１７は、識別番号“７”のブロックに進む。条件検出部１１７は、識別番号“７”のブロックは、脱出ブロックであるので、制御を副作用解析部１１６に戻す。図５に示す実行状態４−１は、実行状態２−１から進んだ場合の最終的な実行状態を表している。
【００４９】
条件検出部１１７は、実行状態２−１を参照して、入力変数x、yが書き換えが発生する変数である旨を副作用解析部１１６に渡す。また、条件検出部１１７は、入力変数fが書き換えられずに関数の脱出ブロックに到達する経路条件はf==1である旨を副作用解析部１１６に渡す。
【００５０】
副作用解析部１１６は、待機実行リスト１２６から、未処理の実行状態１２７を取り出し、条件検出部１１７に渡す。待機実行リスト１２６には、識別番号“２”の分岐ブロックに対する処理で生成した経路条件PC={!s(f)==1})の実行状態が格納されている。副作用解析部１１６は、待機実行リスト１２６からその実行状態１２７を取り出して、条件検出部１１７に渡す。この実行状態のプログラムカウンタは識別番号“４”であるので、条件検出部１１７は、識別番号“４”のブロックから記号実行を開始する。
【００５１】
条件検出部１１７は、識別番号“４”のブロックは代入文であるので、処理を代入処理部１１８に渡す。代入処理部１１８は、代入文y=xに従って、変数表におけるyの記号値を、y=s(x)に書き換える。図５に示す実行状態２−２は、代入後の実行状態を表している。条件検出部１１７は、識別番号“５”のブロックに進み、このブロックは条件分岐であるので、処理を分岐判定部１２０に渡す。
【００５２】
分岐判定部１２０は、定理証明部１２１を用いて、条件式x>yが証明可能か否かを判定する。変数表を用いてx,yを記号値に置き換えると、証明すべき論理式は、!(s(f)==1)→s(x)>s(x)となる。この論理式は常に偽（¬(s(x)>s(x))が常に真）なので、分岐判定部１２０は、プログラムカウンタに、!(x>y)のラベルに対応する有向辺が向かうブロックの番号（識別番号“７”）を格納する。このブロックは、脱出ブロックであるので、条件検出部１１７は、制御を副作用解析部１１６に戻す。図５に示す実行状態３−２は、実行状態２−２から進んだ場合の最終的な実行状態を表している。
【００５３】
条件検出部１１７は、実行状態３−２を参照して、入力変数yが書き換えが発生する変数である旨を副作用解析部１１６に渡す。また、条件検出部１１７は、入力変数x、fが書き換えられずに関数の脱出ブロックに到達する経路条件はf!=1である旨を副作用解析部１１６に渡す。
【００５４】
副作用解析部１１６は、待機実行リスト１２６を参照するが、待機実行リスト１２６には未処理の実行状態がない。副作用解析部１１６は、１以上の記号実行で得られた結果に基づいて、書き換えが発生する可能性がある変数と、その書き換え条件とを生成する。副作用解析部１１６は、条件検出部１１７から入力変数x,yが書き換えられる可能性がある変数である旨を受け取っている。入力変数x、yについて、書き換えられずに関数の脱出ブロックに到達する経路条件があるか否かを調べると、入力変数xはfが1でないとき、書き換えられずに脱出ブロックに到達する。これは、逆に考えれば、fが1のとき、入力変数xは書き換えられる可能性があるということを意味している。副作用解析部１１６は、出力装置１２２に、入力変数xが、fが1のとき書き換えられる可能性がある旨を出力する。或いは、副作用解析部１１６は、入力変数xが、fが1でないときは書き換えられない旨を出力装置１２２に出力する。副作用解析部１１６は、入力変数yについては、書き換えられずに脱出ブロックに到達する経路条件がないので、入力変数yは常に書き換えられる可能性がある入力変数である旨を出力する。
【００５５】
図６は、出力例を示している。出力には、例えば、ＪＭＬを拡張した記法を利用する。@modifiesは、書き換えられる可能性がある変数を表す記述である。図６を参照すると、変数xとyが書き換えられる可能性がある変数であることがわかる。図６にて、when以下は、変数の書き換え条件を表す。この例では、変数xの書き換え条件はf==1である。
【００５６】
本実施形態では、条件検出部１１７は、プログラムソースコード１２４に対して記号実行を行い、プログラムソースコード１２４に含まれる関数が入力変数に与える影響を調べる。条件検出部１１７は、記号実行の結果として、入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する。副作用解析部１１６は、関数の実行に伴って書き換えられる可能性がある入力変数に対し、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する。副作用解析部１１６は、出力装置１２２に、書き換えられる可能性がある入力変数と、その入力変数が書き換えられる条件を判断するための情報とを出力する。
【００５７】
例えば、ある入力変数について、ある実行経路を通るときは関数の脱出ブロックに到達するまでに書き換えが生じ、別の実行経路を通るときは書き換えが生じることなく関数の脱出ブロックに到達するとする。この場合、その入力変数は、書き換えが生じないときの実行経路以外の経路を通るとき、書き換えられる可能性があることになると言える。副作用解析部１１６は、書き換えられる可能性がある入力変数に対し、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する。このようにすることで、関数呼び出しに伴い書き換えられる可能性がある変数を出力するだけでなく、当該変数が書き換えられる条件を入力変数に対する制約条件として出力できる。
【００５８】
ところで、入力変数が書き換えられる条件を判断するための情報として、入力変数が関数の脱出ブロックに到達するまでに書き換えられる経路条件を用いることも考えられる。しかし、書き換え条件を直接に求めると、全ての実行経路を網羅的に記号実行することは困難であるので、必要ではあるが十分ではない条件が得られることになる。そこで、本実施形態では、書き換えが発生する可能性がある入力変数について、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を求め、その経路条件に基づいて書き換えの発生を判断するための情報を生成している。コードの正しさを検証するためには、書き換えられる可能性がある全ての条件を求めることが望ましい。書き換えが発生しない必要条件を求め、その否定を取ることで書き換えが発生する十分条件を得ることができ、コードの正確な検証が可能になる。
【００５９】
ここで、ある関数の検査において、当該関数から別の関数への呼出しが発生する場合を考える。書き換えられる可能性がある変数のみが与えられ、その変数が書き換えられる条件が不明であれば、関数の検査において、呼び出される関数が書き換える可能性がある変数の値は全て未定義、つまり、どのような値になるか分からないと仮定しなくてはならない。このことは、検査の精度を低下させることにつながる。一方、変数がどのような条件で書き換えられるかの情報があれば、未定義と仮定しなくてはならない変数を削減することができる。本実施形態では、書き換えられる可能性がある入力変数と、その書き換え条件を判断するための情報とを出力するので、未定義と仮定しなければならない変数の数を削減し、検査の精度低下を軽減することができる。
【００６０】
例えば、図１５に示す関数を解析したとき、非特許文献１に記載の副作用解析装置では、図１６に示すように、入力変数x、yが書き換えられる可能性がある入力変数であることが出力されるのみである。しかしながら、図１５に示す関数では、変数yは入力変数の値が何れの値でも書き換えられるのに対し、変数xは変数fの値が1のときにのみ書き換えられる。従って、関数の副作用の情報として、図１６に示す情報では不十分である。本実施形態では、例えば図６に示すように、変数xがf==1のとき書き換えられる可能性があるという情報を含んでいる。従って、図１５に示す関数を呼び出す別の関数の検査では、変数xに対し、変数fの値が1以外の値のときは、変数xに未定（UNKOWN）を割り当てる必要がなく、検査の精度低下を軽減できるという効果が得られる。
【００６１】
続いて、本発明の第２実施形態について説明する。図７は、本発明の第２実施形態の副作用解析装置を含む記号実行装置を示している。副作用解析装置２００は、入力装置２１１、計算機２１２、出力装置２２２、及び、記憶装置２２３を有する。計算機２１２は、構文解析部２１３、識別部２１４、初期化部２１５、副作用解析部２１６、条件検出部２１７、ステート処理部２１８、表明解析部２１９、分岐判定部２２０、及び、定理証明部２２１を有する。記憶装置２２３は、プログラムソースコード２２４、代入場所識別表２２５、待機実行リスト２２６、表明情報２２８、及び、解析用変数リスト２２９を記憶する。
【００６２】
計算機２１２は、プログラム制御で動作する中央処理装置、プロセッサ、或いは、データ処理装置である。計算機２１２内の各部の機能は、計算機２１２が所定のプログラムに従って処理を実行することで実現できる。入力装置２１１は、キーボードやマウスなどの入力装置である。出力装置２２２は、ディスプレイ等の出力装置である。記憶装置２２３は、ハードディスクドライブやメモリ装置などの記憶装置である。
【００６３】
構文解析部２１３は、プログラムソースコード２２４を読み出し、プログラムソースコード２２４の構文解析を行って、検査用の制御フローグラフを生成する。識別部２１４は、制御フローグラフを参照して、開始ブロックから脱出ブロックまでの間で、入力変数を書き換える可能性があるブロックを代入場所識別表に記録する。代入場所識別表２２５は、入力変数と、当該入力変数に対して書き換えが発生する可能性があるブロックのリスト（代入場所リスト）とを対応付けて保持する。識別部２１４は、代入場所識別表２２５の作成後、書き換えられる可能性がある入力変数の一覧を、解析用変数リスト２２９に保存する。初期化部２１５は、待機実行リスト２２６の初期化を行う。
【００６４】
副作用解析部２１６は、解析用変数リスト２２９から入力変数を１つずつ取り出し、条件検出部２１７に対して記号実行を指示する。条件検出部２１７は、副作用解析部２１６が取り出した入力変数を解析対象の変数として記号実行を行い、関数が解析対象の変数に与える影響を調べる。条件検出部２１７は、解析対象の変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する。
【００６５】
ステート処理部２１８は、記号実行にて、入力変数に対して代入を行うブロックや、関数呼び出しを含むブロックに対する処理を行う。ステート処理部２１８が行う処理は、関数呼び出しを考慮しなければ、図１に示す副作用解析装置における代入処理部１１８が行う処理と同様である。分岐判定部２２０は、記号実行にて、条件分岐を含むブロックに対する処理を行う。定理証明部２２１は、分岐判定部２２０が条件分岐を含むブロックに対して処理を行う際に、そのブロックの分岐条件が証明可能か否かを判断する。
【００６６】
表明解析部２１９は、表明情報２２８を解析する。表明情報２２８には、関数実行に伴って書き換える可能性がある変数の一覧が記述されている。表明情報は、書き換えられる可能性がある変数について、その書き換え条件を含んでいてもよい。識別部２１４は、関数呼び出しを含むブロックがあるとき、表明解析部２１９を用いて、当該ブロックが入力変数を書き換える可能性がある否かを調べる。また、ステート処理部２１８は、関数呼び出しを含む処理を行う際に、表明解析部２１９を用いて、当該ブロックが入力変数を書き換える可能性がある否かを調べる。
【００６７】
副作用解析部２１６は、条件検出部２１７から、解析用変数リスト２２９から取り出した入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を受け取る。副作用解析部２１６は、その経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する。副作用解析部２１６は、出力装置２２２に、関数の実行に伴って書き換えられる可能性がある入力変数を出力すると共に、当該入力変数が書き換えられる条件を判断するための情報を出力する。
【００６８】
図８は、代入場所識別表２２５を示している。識別部２１４は、例えば、入力変数である変数xが、制御フローグラフ中の識別番号“４”のブロック、及び、識別番号“６”のブロックで代入が発生する可能性があるとき、代入場所リスト｛４，６｝を、変数xに対応して記録する。図８では、入力変数zの代入場所リストは空になっている。代入場所リストが空の入力変数は、書き換えが発生する可能性がない入力変数を表している。代入場所識別表２２５から、代入場所リストが空でない入力変数を取り出したものが、解析用変数リスト２２９となる。なお、実行状態は、第１実施形態と同じである（図２、図３）。
【００６９】
図９は、副作用解析装置１０の動作手順を示している。ユーザは、入力装置２１１を用いて、解析対象のプログラムを指定する。ユーザは、例えば、解析対象とする関数の名称や、必要であれば、その関数が保存されている場所、及び、対応する表明情報が保存されている場所を入力する。構文解析部２１３は、解析対象のプログラムソースコード２２４を記憶装置２２３から読み出す。構文解析部２１３は、ソースコードの構文解析を行い、制御フローグラフを生成する（ステップＢ１）。
【００７０】
識別部２１４は、ステップＢ１で生成された制御フローグラフから、入力変数に対して代入を行う可能性があるブロックを検出する。入力変数は、関数が参照渡しであれば、関数の引数と、当該関数からアクセス可能な広域変数とが該当する。識別部２１４は、入力変数に対して代入を行う可能性があるブロックを検出すると、そのブロックを識別する情報（ブロック識別番号）を、該当する入力変数と対応付けて代入場所識別表２２５に記録する（ステップＢ２）。識別部２１４は、代入場所識別表２２５の作成後、書き換えられる可能性がある入力変数の一覧を、解析用変数リスト２２９に保存する。
【００７１】
識別部２１４は、エイリアス関係が発生する場合は、入力変数への直接の代入だけでなく、入力変数とエイリアス関係にある変数への代入を、対応する入力変数への代入とみなして処理する。エイリアス関係が発生する例としては、例えばＣ言語で、入力変数xがあったとき、ポインタpに対してp=&xという代入がなされた場合が挙げられる。この場合、*pはxと同じメモリ領域を参照することになるので、xと*pとはエイリアス関係にある。
【００７２】
また、識別部２１４は、入力変数に対する直接の代入だけでなく、関数呼び出しに伴う入力変数の書き換えも検査する。識別部２１４は、関数呼び出しに伴って入力変数が書き換えられるか否かを、表明解析部２１９を用いて調べる。表明解析部２１９は、プログラムソースコード２２４から呼び出される関数の表明情報を解析し、書き換えられる可能性がある変数を調べる。このとき、表明解析部２１９は、関数の引数について、表明情報に含まれる仮引数の変数名と、引数として与えられる実引数の変数名との対応付けを行った上で、書き換えられる可能性がある変数を調べる。
【００７３】
識別部２１４は、表明情報に書き換え条件が含まれるときでも、書き換え条件を判断せずに、表明情報に含まれる書き換えられる可能性がある変数は、全て書き換えられるものとして取り扱う。表明解析部２１９は、関数呼び出しに伴って書き換えられる可能性がある変数の一覧を、識別部２１４に返す。識別部２１４は、表明解析部２１９から受け取った変数一覧に、入力変数が含まれるとき、関数呼び出しを行うブロックで入力変数に対して代入が発生した解釈し、代入場所識別表２２５に、当該ブロックの識別情報と書き換えられる可能性がある入力変数とを記録する。
【００７４】
なお、プログラムソースコード２２４から呼び出される関数に対応する表明情報が、常に存在するとは限らず、対応する表明情報が存在しない場合もある。表明情報が存在しない場合は、当該関数にて入力変数の書き換えが発生する可能性がないとする方針（方針Ａ）と、当該関数から参照可能な全ての入力変数が書き換わるものとする方針（方針Ｂ）とがある。副作用解析装置では、利用者が、何れの方針を選択するかを選択可能であることが好ましい。利用者は、例えば、解析オプションなどを用いて、何れの方針を選択するかを指定すればよい。
【００７５】
ステップＢ２で生成された解析用変数リスト２２９は、プログラムソースコード２２４の実行に伴って、書き換えられる可能性がある入力変数の一覧を示している。副作用解析部２１６は、解析用変数リストに含まれる入力変数に対し、記号実行を行うことで、どのような条件で書き換えが発生するかを解析する。
【００７６】
副作用解析部２１６は、解析用変数リスト２２９に未処理の入力変数があるか否かを判断する（ステップＢ３）。副作用解析部２１６は、解析用変数リスト２２９に未処理の入力変数があるときは、そのうちの１つを選択する。副作用解析部２１６は、選択した入力変数に対して、書き換えが発生する可能性がある条件を求めるために、記号実行を行う。副作用解析部２１６は、記号実行の開始に際して、初期化部２１５を用いて、待機実行リストの初期化を行う（ステップＢ４）。
【００７７】
初期化部２１５は、プログラムカウンタに、制御フローグラフの開始ブロックの識別番号を格納し、経路条件にtrueを格納した初期実行状態を生成する。初期化部２１５は、初期実行状態の変数表には、入力変数に対してはs（変数名）からなる記号を値とし、それ以外の局所変数については、UNKOWN（未定義）を値として持つ記号値を格納する。なお、ここでは、便宜上、入力変数に対応する記号値をs（変数名）で表現したが、これには限定されず、入力変数に対応する記号値は任意の記号を用いて表現してよい。初期化部２１５は、生成した初期実行状態を待機実行リスト２２６に保存する。記号実行開始時、待機実行リスト２２６は、初期実行状態を１つ含む。
【００７８】
副作用解析部２１６は、待機実行リスト２２６が空か否かを判断する（ステップＢ５）。副作用解析部２１６は、待機実行リスト２２６が空でないときは、待機実行リスト２２６から実行状態２２７を１つ取り出し、条件検出部２１７に渡す。条件検出部２１７は、副作用解析部２１６が取り出した実行状態２２７に対して、記号実行を開始する。副作用解析部２１６が最初に取り出す実行状態２２７は、初期化部２１５が生成した初期実行状態である。
【００７９】
条件検出部２１７は、副作用解析部２１６が選択した入力変数を解析対象の入力変数として記号実行を行い、当該入力変数の書き換えられる可能性がある条件を求める。本実施形態では、入力変数が書き換えられる可能性がある条件を求めるために、当該入力変数の書き換えが発生しない経路条件を求める。記号実行が、関数の開始ブロックから開始して脱出ブロックまで到達し、その間の経路に当該入力変数への書き換えを行うブロックが存在しなければ、脱出ブロックまで到達した実行状態に含まれる経路条件は、当該入力変数への書き換えが発生しない条件を表している。
【００８０】
条件検出部２１７は、実行状態のプログラムカウンタを参照し、プログラムカウンタが示すブロックを、制御フローグラフから取り出す。記号実行の開始時に、条件検出部２１７が参照する実行状態は、初期化部２１５が生成した初期実行状態である。条件検出部２１７は、記号実行終了を判断する（ステップＢ６）。条件検出部２１７は、取り出したブロックが、脱出ブロック（return文や、例外発生文など）に該当する場合、記号実行終了と判断する。条件検出部２１７は、脱出ブロックに到達したときの実行状態の経路条件を、副作用解析部２１６に渡す。
【００８１】
条件検出部２１７は、記号実行終了でない場合は、実行状態のプログラムカウンタが示すブロックが、条件分岐を含むブロックであるか否かを判断する（ステップＢ７）。条件検出部２１７は、プログラムカウンタが示すブロックが条件分岐を含まないとき、つまり、ブロックが代入文や関数呼び出しを含むブロックのときは、ステート処理部２１８に処理を移す（ステップＢ８）。ステート処理部２１８は、代入分や関数呼び出しを含むブロックに対する処理を行い、実行状態を更新する。条件検出部２１７は、プログラムカウンタが示すブロックが条件分岐を含むとき、分岐判定部２２０に処理を移す（ステップＢ９）。分岐判定部２２０の処理は、第１実施形態における分岐判定部の処理と同様である。ステート処理部２１８の処理の詳細は後述する。
【００８２】
条件検出部２１７は、ステート処理又は分岐判定の実行後、ステップＢ６へ戻り、記号実行の終了を判定する。条件検出部２１７は、ステップＢ６では、脱出ブロックに到達していなくても、ステップＢ８でステート処理部２１８が処理した結果、解析対象の入力変数が書き換えられたときは、その時点で記号実行終了と判断する。これは、記号実行で求めるのは、解析対象の入力変数が書き換えられることなく脱出ブロックに到達した際の経路条件であるので、当該入力変数が書き換えられたときは、それ以降、記号実行を行う必要がないからである。この場合、条件検出部２１７は、falseを副作用解析部２１６に返す。或いは、返り値はなくてもよい。条件検出部２１７は、処理時間を一定時間に収めるため、一定回数の以上の記号実行を行ったとき、或いは、一定時間以上の記号実行を行ったときは、記号実行終了と判断してもよい。
【００８３】
ここで、条件検出部２１７は、プログラムカウンタが示すブロックが、代入場所識別表２２５にて当該入力変数に対応する代入場所リストに含まれるときは、ステップＢ８のステート処理を経ずに、ステップＢ６で記号実行終了と判断してもよい。ただし、代入場所リストに含まれていても、当該ブロックが関数呼び出しを含み、解析対象の入力変数が関数呼び出しの副作用で書き換えられる可能性がある場合は、ステップＢ８へ進んで解析対象の入力変数が書き換えられるか否かを調べるものとする。なお、表明情報がない関数の呼び出しであって、前述の方針Ｂ（当該関数から参照可能な全ての入力変数が書き換わるものとする方針）が選択されているときは、解析対象の入力変数は書き換えられるものとして取り扱われるので、その時点で、記号実行終了と判断してよい。
【００８４】
副作用解析部２１６は、条件検出部２１７がステップＢ６で記号実行終了と判断すると、条件検出部２１７が出力した、解析対象の入力変数の書き換えが発生しない経路条件を記憶する。副作用解析部２１６は、ステップＢ５へ戻り、待機実行リストが空であるか否かを判断する。副作用解析部２１６は、待機実行リストに実行状態が残っているときは、それを条件検出部２１７に渡し、記号実行を継続する。副作用解析部２１６は、待機実行リストが空になると、解析対象の変数に対する記号実行を終了する。副作用解析部２１６は、１回以上の記号実行で得られた入力変数の書き換えが発生しない経路条件を用いて、解析対象の入力変数に対する書き換えが発生する可能性がある条件を生成する（ステップＢ１０）。
【００８５】
副作用解析部２１６は、ステップＢ１０では、１回以上の記号実行で得られた入力変数を書き換えない経路条件を全て∨（ＯＲ）結合した条件式を生成し、その条件式の否定をとる。具体的には、副作用解析部２１６は、得られた経路条件をＣ１、Ｃ２、・・・、Ｃｎとして、これら∨で結合したＣ１∨Ｃ２∨・・・∨Ｃｎという条件式を生成する。副作用解析部２１６は、生成した条件式の否定である¬（Ｃ１∨Ｃ２∨・・・∨Ｃｎ）を、書き換えが発生するために必要な解析対象の入力変数に対する制約条件とする。副作用解析部２１６は、書き換えが発生するために必要な入力変数に対する制約条件を、解析対象の入力変数の書き換え条件を判断するための情報として記憶装置２２３に記憶する。
【００８６】
或いは、上記に代えて、副作用解析部２１６は、１回以上の記号実行で得られた入力変数を書き換えない経路条件を全て∧（ＡＮＤ）結合した条件式を生成してもよい。例えば、得られた経路条件をＣ１、Ｃ２、・・・、Ｃｎとして、副作用解析部２１６は、これら∧で結合したＣ１∧Ｃ２∧・・・∧Ｃｎという条件式を生成する。この条件式は、書き換えが発生する可能性がある入力変数が、書き換えられないときの入力変数に対する制約条件を表している。副作用解析部２１６は、書き換えられない条件を、解析対象の入力変数の書き換え条件を判断するための情報として記憶装置２２３に記憶する。
【００８７】
副作用解析部２１６は、制約条件を生成した後、ステップＢ３に戻り、解析用変数リスト２２９から次の入力変数を選択する。なお、多くのプログラムでは、経路が無数に存在し、また、ループが存在することで、待機実行リスト２２６に含まれる実行状態の数は増加し続ける可能性がある。そこで、副作用解析部２１６は、待機実行リスト２２６が空でなくても、一定回数の記号実行を処理するか、或いは、記号実行開始から一定時間が経過したときは、ステップＢ３に戻って、次の入力変数を選択するようにしてもよい。記号実行の回数は、カウンタを用意することで計測でき、記号実行開始からの経過時間は、タイマーを用意することで計測できる。
【００８８】
副作用解析部２１６は、ステップＢ３で解析用変数リスト２２９に未処理の入力変数がないと判断すると、つまり、析用変数リスト２２９に含まれる入力変数に対する解析が終了すると、記憶装置２２３から、解析対象の入力変数について、各入力変数の書き換え条件を判断するための情報を読み出す。副作用解析部２１６は、出力装置２２２に、書き換えられる可能性がある変数の一覧と、書き換え条件を判断するための情報とを出力し（ステップＢ１１）、処理を終了する。このとき、副作用解析部２１６は、書き換え条件を判断するための情報に含まれる条件式を、簡略化した上で、出力装置２２２に出力してもよい。
【００８９】
図１０は、ステート処理部２１８の処理手順を示している。ステート処理部２１８は、実行状態のプログラムカウンタが示すブロックが関数呼び出しを含むか否かを判断する（ステップＣ１）。ステート処理部２１８は、当該ブロックの文が関数呼び出しであるか、又は、代入式の右辺に関数呼び出しを含むと判断すると表明解析部２１９から、書き換えられる可能性がある変数とその書き換え条件との一覧を取得する。表明解析部２１９は、呼び出される関数に対応する表明情報２２８を読み出し、書き換えが発生する変数と書き換え条件の一覧をステート処理部２１８に渡す。
【００９０】
ステート処理部２１８は、書き換えられる可能性がある変数の全てについて処理を行ったか否かを判断する（ステップＣ２）。ステート処理部２１８は、未処理の変数があるときは、実行状態の経路条件を用いて、関数呼び出しで書き換えられる可能性がある変数が書き換えられるか、書き換えられないか、或いは、書き換えられるか否かが不明であるかを判定する（ステップＣ３）。ステート処理部２１８は、判定後、ステップＣ２に戻る。
【００９１】
ステート処理部２１８は、ステップＣ２では、選択した変数について、表明情報２２８に記述された書き換え条件がtrue（常に真）の場合は、書き換えが発生すると判定する。ステート処理部２１８は、表明情報２２８に書き換え条件に関する記述がないときは、書き換え条件をtrueと解釈し、書き換えが発生すると判定する。ステート処理部２１８は、書き換え条件がtrueでないときは、実行状態の経路条件cと書き換え条件pとを用いてc→pという論理式を生成し、定理証明を行う。c→pが証明可能であれば、当該変数は書き換えられると判定する。ステート処理部２１８は、証明に失敗した場合は、c→¬pという論理式を生成し、定理証明を試みる。ステート処理部２１８は、論理式が証明可能であれば、当該変数は書き換えられないと判定する。
【００９２】
ステート処理部２１８は、c→pの証明と、c→¬pの証明との双方が証明可能でないときは、当該変数は書き換えられるか否かが不明であると判定する。ステート処理部２１８は、書き換えられると判定した変数を、書き換え発生変数リストに記憶する。また、ステート処理部２１８は、書き換えられるか否かが不明であると判定した変数と、表明情報２２８に記述されたその変数の書き換え条件とを、不明リストに記憶する。なお、書き換え発生変数リストに、解析対象の入力変数が含まれる場合は、関数の実行に伴って当該入力変数が書き換えられることを意味するので、ステート処理部２１８は処理を終了し、条件検出部２１７から副作用解析部２１６にfalseを返す。
【００９３】
ステート処理部２１８は、ステップＣ２で全ての変数について処理したと判断すると、書き換え発生変数リストと不明リストとを用いて、新たな実行状態を生成する（ステップＣ４）。ステート処理部２１８は、まず、実行状態の変数表における、書き換え発生変数リストに含まれる全ての変数の記号値をUNKOWNにする。次いで、ステート処理部２１８は、不明リストに含まれる変数について、各変数が書き換わる場合と書き換わらない場合との組み合わせを生成する。この組み合わせの数は、不明リストに含まれる変数の数をnとすれば、2n個ある。ステート処理部２１８は、各組み合わせについて、書き換えるとした変数の書き換え条件cと、書き換えないとした変数の書き換え条件の否定¬cとを∧（ＡＮＤ）結合した論理式Pを生成する。
【００９４】
ステート処理部２１８は、実行状態のプログラムカウンタに、制御フローグラフ内の次のブロックの識別番号を格納する。ステート処理部２１８は、実行状態を、組み合わせ分だけコピーする。ステート処理部２１８は、コピーした各実行状態の変数表を更新し、上記の組み合わせで書き換えられるとした変数の記号値をUNKOWNにする。また、ステート処理部２１８は、コピーした各実行状態の経路条件を、コピー元の実行状態の経路条件Qと上記で生成した論理式Pとを∧（ＡＮＤ）結合したP∧Qとする。なお、P∧Qが充足できない場合、その実行状態は実行を継続できないので、ステート処理部２１８は、経路条件の生成前にP∧Qが充足できるか否かを確認し、充足できない組み合わせは除外しておくとよい。また、記号実行で求めるべきは解析対象の入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件であるので、ステート処理部２１８は、不明リストに解析対象の入力変数が含まれる場合は、2n個の組み合わせから、当該入力変数が書き換えられるとする組み合わせを除外しておくものとする。
【００９５】
組み合わせの生成について、具体的に説明する。不明リストには、変数x、yの２つが含まれるとする。変数xの書き換え条件はz>0であり、変数yの書き換え条件はa>bであるとする。xとyとから生成される組み合わせは、(x:0,y:0)、(x:1,y:0)、(x:0,y:1)、(x:1,y:1)の4通りになる。ここで、x:0は変数xが書き換えられないことを表し、x:1は変数ｘが書き換えられることを表している。仮に、副作用解析部２１６から記号実行を指示された解析対象の入力変数が変数xであるとすれば、ステート処理部２１８は、この組み合わせから、x:1を含む組み合わせを除外した２通りの組み合わせを生成することになる。
【００９６】
図１１は、元の実行状態と、ステップＣ４で生成される実行状態とを示している。元の実行状態（コピー元の実行状態）における経路条件はQであり、変数表における変数x、yの記号値はそれぞれs(x)、s(y)であるとする。ステート処理部２１８は、元の実行状態から、上記の４通りの組み合わせに対応した４つの実行状態を生成する。(x:0,y:0)は、xもyも書き換わらないときの実行状態に対応しており、変数表におけるx、yの記号値に変更はない。xの書き換え条件がz>0で、yの書き換え条件がa>bであるので、ステート処理部２１８は、元の経路条件Qに、これらの否定を∧（ＡＮＤ）結合したQ∧¬(z>0)∧¬(a>b)を、新たな実行状態の経路条件とする。
【００９７】
(x:0,y:1)は、xは書き換わらず、yが書き換わるときの実行状態に対応している。ステート処理部２１８は、変数表におけるyの記号値をUNKOWNとする。また、ステート処理部２１８は、元の経路条件Qに、xが書き換わらない条件（¬（z>1））とyの書き換え条件（a>b）を∧（ＡＮＤ）で連結したQ∧¬(z>0)∧(a>b)を、新たな実行状態の経路条件とする。(x:1,y:0)は、xが書き換わりyは書き換わらないときの実行状態に対応している。ステート処理部２１８は、変数表におけるxの記号値をUNKOWNとし、経路条件を、Q∧(z>0)∧¬(a>b)とする。(x:1,y:1)は、xもyも書き換わるときの実行状態に対応している。ステート処理部２１８は、変数表におけるx、yの記号値をUNKOWNとし、経路条件をQ∧(z>0)∧(a>b)とする。
【００９８】
ステート処理部２１８は、実行状態のプログラムカウンタが示すブロックが代入文を含むか否かを判断する（ステップＣ５）。ステート処理部２１８は、ブロックが代入文を含むときは、代入処理の作用を実行状態の変数表に反映させる（ステップＣ６）。ステート処理部２１８は、代入式の右辺に記号値がUNKOWNの変数を含むときは、左辺の変数の記号値をUNKOWNとする。ステート処理部２１８は、ステップＣ１からステップＣ５に進んだ場合は、条件検出部２１７が副作用解析部２１６から受け取った実行状態の変数表に、代入処理の作用を反映させる。ステート処理部２１８は、ステップＣ４を経由してステップＣ５に進んだ場合は、ステップＣ４で生成した全ての実行状態の変数表に、代入処理の作用を反映させる。
【００９９】
ステート処理部２１８は、実行状態を条件検出部２１７に渡し、処理を条件検出部２１７に戻す。ステート処理部２１８は、ステップＣ４を経由したときは、ステップＣ４で生成した実行状態のうちの１つを条件検出部２１７に渡し、残りを待機実行リスト２２６に保存する。例えば、ステート処理部２１８は、ステップＣ４で生成した図１１に示す４つの実行状態のうち、xもyも書き換わらないときに対応する実行状態を条件検出部２１７に渡し、残りの３つを待機実行リスト２２６に保存する。条件検出部２１７は、ステート処理部２１８から受け取った実行状態について、記号実行を進める。
【０１００】
なお、呼び出される関数に対応する表明情報２２８が存在しない場合は、前述の方針に従って処理を行う。すなわち、方針Ａ（関数にて入力変数の書き換えが発生する可能性がないとする方針）が採用される場合は、ステート処理部２１８は、関数呼び出しに伴う変数書き換えを調べる必要がないので、ステップＣ１で関数呼び出しを含まないと判断して処理を進める。方針Ｂ（関数から参照可能な全ての入力変数が書き換わるものとする方針）が採用される場合は、関数呼び出しに伴って、解析対象となっている入力変数も書き換えられる。従って、ステート処理部２１８は、ステップＣ２以下を行わずに処理を条件検出部２１７に戻し、条件検出部２１７から副作用解析部２１６にfalseを返せばよい。
【０１０１】
以下、具体例を用いて説明する。図１２は、プログラムソースコードの具体例を示している。図１３は、表明情報の具体例を示している。図１４は、図１２に示すプログラムソースコードから生成される制御フローグラフを示している。図１２にプログラムソースコードでは、広域変数gと引数x、y、zの４つが入力変数に該当する。構文解析部２１３は、図１２に示すプログラムソースコードに対して構文解析を行い、図１４に示す制御フローグラフを生成する。
【０１０２】
識別部２１４は、図１４に示す制御フローグラフ上で、上記入力変数が書き換わる可能性がある箇所を識別する。図１４に示す制御フローグラフを参照すると、識別番号“４”のブロックで変数gへの代入が発生し、識別番号“５”のブロックで変数yへの代入が発生している。識別部２１４は、代入場所識別表２２５における変数yに対応する代入場所リストに“５”を記録し、変数gに対応する代入場所リストに“４”を記録する。
【０１０３】
また、識別部２１４は、識別番号“６”のブロックは関数（bar）を呼び出すブロックであるので、この関数呼び出しに伴う変数の書き換えを、表明解析部２１９を用いて解析する。図１３に示す表明情報を参照すると、第１引数aと第２引数bとが書き換えられる可能性がある変数であることがわかる。表明情報における仮引数と、プログラムソースコードにおける実引数との対応を取ると、仮引数aは実引数xに対応し、仮引数bは実引数yに対応する。識別部２１４は、代入場所識別表２２５における変数xに対応する代入場所リストに“６”を記録し、変数yに対応する代入場所リストに“５”を追加する。このとき、表明情報に含まれる各変数の書き換え条件は、識別部２１４での処理に影響しない。
【０１０４】
識別部２１４での処理の結果、代入場所識別表は、xは{6}、yは｛５，６｝、zは｛｝、gは｛４｝となる。識別部２１４は、解析用変数リストに、x、y、gを保存する。副作用解析部２１６は、解析用変数リストに含まれる変数x、y、gを解析対象の変数とし、記号実行を行って解析対象の変数の書き換え条件を調べる。副作用解析部２１６は、まず、解析用変数リストから変数xを取り出す。初期化部２１５は、初期実行状態を生成し、待機実行リストに保存する。xの記号実行の初期状態は、Counter（プログラムカウンタ）=2、PC（経路条件）={true}、変数表x=s(x),y=s(y),z=s(z),g=s(g)である。
【０１０５】
副作用解析部２１６は、初期実行状態を条件検出部２１７に渡し、解析対象の変数を変数xとして記号実行を指示する。条件検出部２１７は、記号実行を進め、識別番号“３”のブロックに到達する。このブロックは条件分岐のブロックであり、分岐条件はz>0である。条件検出部２１７は、処理を分岐判定部２２０に移す。分岐判定部２２０は、定理証明部２２１を用いて、経路条件→分岐条件（true→s(z)＞0）と、経路条件→¬（分岐条件）（true→¬s(z)＞0）とが証明可能か否かを調べる。
【０１０６】
true→s(z)＞0とtrue→¬(s(z)＞0)とは共に定理ではないため、分岐判定部２２０は、各分岐に対応した実行状態を生成する。生成する２つの実行状態の一方（実行状態３−１）は、Counter=4、PC={s(z)＞0}、変数表x=s(x),y=s(y),z=s(z),g=s(g)であり、他方（実行状態３−２）は、Counter=5、PC={¬(s(z)＞0)}、変数表x=s(x),y=s(y),z=s(z),g=s(g)である。分岐判定部２２０は、実行状態３−２を待機実行リストに保存し、実行状態３−１を条件検出部２１７に渡す。条件検出部２１７は、実行状態３−１について、記号実行を継続する。
【０１０７】
条件検出部２１７は、プログラムカウンタが示す識別番号“４”のブロックは代入ブロックであるので、処理をステート処理部２１８に移す。ステート処理部２１８は、識別番号“４”のブロックは関数呼び出しを含まないブロックであるので、代入文の作用を変数表に反映し、変数gの値を書き換える。ステート処理部２１８は、実行状態を、Counter=6、PC={s(z)＞0}、変数表x=s(x),y=s(y),z=s(z),g=１に更新する。
【０１０８】
条件検出部２１７は、識別番号“６”のブロックは関数呼び出しを含むブロックであるので、処理をステート処理部２１８に移す。ステート処理部２１８は、表明解析部２１９を用いて、図１３に示す表明情報を解析する。表明情報を参照すると、第１引数aは、第３引数cが!(c>0)を満たすとき書き換えられること、及び、第２引数は広域変数gがg==1のとき書き換えられることがわかる。表明情報における仮引数a、b、cを実引数x、y、zに対応する。ステート処理部２１８は、関数呼び出しの引数である変数x、y、zのうち、書き換えられる可能性がある変数x、yについて、関数が変数に与える作用を計算する。
【０１０９】
ステート処理部２１８は、まず、変数xへの作用を計算する。ステート処理部２１８は、関数呼び出しブロックに到達する経路条件(s(z)＞0)と、変数xの書き換え条件!(z>0)とを用いて、関数呼び出しに伴って変数xが書き換えられるか否か、或いは、書き換えられるか否かが不明かを判断する。このとき、ステート処理部２１８は、書き換え条件!(z>0)を、変数表を用いて!(s(z)>0)と置き換えて判断を行う。ステート処理部２１８は、(s(z)＞0)→!(s(z)＞0)と、(s(z)＞0)→(s(z)＞0)とが証明可能か否かを判断する。ステート処理部２１８は、(s(z)＞0)→(s(z)＞0)が証明可能であるので、変数xは書き換えられないと判断する。
【０１１０】
次いで、ステート処理部２１８は、変数yへの作用を計算する。変数yの書き換え条件はg==1である。変数表を参照すると、変数gの記号値は1であるので、ステート処理部２１８は、s(z)＞0→1==1の証明を試みる。ステート処理部２１８は、証明可能なので、変数yは関数呼び出しに伴って書き換えられると判断し、変数yを書き換え発生変数リストに保存する。ステート処理部２１８は、書き換えられる可能性がある変数について関数が変数に与える作用を計算すると、書き換え発生変数リストと不明リストとを用いて、実行状態を生成する。このケースでは、書き換え発生変数リストは変数yを含み、不明リストには変数がない。ステート処理部２１８は、変数表における変数yの記号値を未定義（UNKOWN）に書き換え、実行状態をCounter=7、PC={s(z)＞0}、変数表x=s(x),y=UNKNOWN,z=s(z),g=１に更新する。
【０１１１】
条件検出部２１７は、実行状態が脱出ブロックに到達したことを検知する。条件検出部２１７は、実行状態の経路条件（s(z)>0）を、解析対象の変数xが書き換えられることなく関数の脱出ブロックに到達する経路条件として、副作用解析部２１６に出力する。副作用解析部２１６は、待機実行リストに実行状態が残っているか否かを調べる。待機実行リストには実行状態３−２が残っているので、副作用解析部２１６は、実行状態３−２を条件検出部２１７に渡し、記号実行を指示する。
【０１１２】
実行状態３−２は、Counter=5、PC={¬(s(z)＞0)}、変数表x=s(x),y=s(y),z=s(z),g=s(g)である。条件検出部２１７は、識別番号“５”のブロックが代入ブロックであるので、処理をステート処理部２１８に移す。ステート処理部２１８は、代入文の作用を変数表に反映し、実行状態をCounter=6、PC={¬(s(z)＞0)}、変数表x=s(x),y=1,z=s(z),g=s(g)に更新する。ステート処理部２１８は、識別番号“６”のブロックは関数呼び出しを含むブロックであるので、処理をステート処理部２１８に移す。ステート処理部２１８は、上記と同様な手順で、関数呼び出しが、変数x、yに与える影響を計算する。経路条件は¬(s(z)>0)で、変数xの書き換え条件は!(s(z)>0)であり、¬(s(z)＞0)→!(s(z)＞0)は証明可能なので、ステート処理部２１８は、変数xは書き換えが発生する変数であると判断する。変数xは、解析対象の変数であるので、条件検出部２１７は、記号実行を終了する。
【０１１３】
副作用解析部２１６は、待機実行リストに実行状態が残っているか否かを調べ、残っていないと判断する。これで、解析対象の変数xに対する記号実行が終了する。書き換えが発生する可能性がある変数xに対して記号実行を行うことで、変数xが書き換えられることなく関数の脱出ブロックに到達する経路条件はs(z)>0であるという結果が得られる。副作用解析部２１６は、書き換わらずに関数の脱出ブロックに到達する経路条件の否定（¬(s(z)>o)）を、変数xが書き換わる条件として保存する。
【０１１４】
続いて、副作用解析部２１６は、解析用変数リストから変数yを取り出し、解析対象の変数とする。初期化部２１５は、初期実行状態を生成し、待機実行リストに保存する。この初期実行状態は、変数xに対して記号実行を行うときに初期化部２１５が生成した初期実行状態と同じである。副作用解析部２１６は、初期実行状態を条件検出部２１７に渡し、解析対象の変数を変数yとして、記号実行を指示する。
【０１１５】
記号実行の進め方は、変数ｘに対する記号実行の進めた方と同様である。分岐判定部２２０は、識別番号“３”のブロックに対する処理で、実行状態３−１と実行状態３−２とを生成し、実行状態３−２を待機実行リストに保存する。ステート処理部２１８は、識別番号“４”のブロックに対する処理で、変数表における変数gの記号値を1に書き換える。ステート処理部２１８は、関数呼び出しを含む識別番号“６”のブロックに対して処理を行う。表明情報を参照すると、第２引数bは、広域変数gがg==1のとき書き換えられる。第２引数bは変数yに対応している。ステート処理部２１８は、経路条件（s(z)>0）→1==1が証明可能なので、解析対象の変数yは書き換えられると判断し、記号実行を終了する。
【０１１６】
副作用解析部２１６は、待機実行リストから実行状態３−２を取り出し、条件検出部２１７に渡す。ステート処理部２１８は、識別番号“５”のブロックに対する処理で、代入文の作用を変数表に反映させ、変数表におけるyの記号値を1に書き換える。条件検出部２１７は、解析対象の変数yが書き換えられたので、記号実行を終了する。なお、変数yの代入場所リストには識別番号“５”が含まれている。このため、条件検出部２１７は、プログラムカウンタが代入ブロックである識別番号“５”のブロックを示しているときは、ステート処理部２１８での処理を経ずに、記号実行を終了してもよい。
【０１１７】
副作用解析部２１６は、待機実行リストに実行状態が残っているか否かを判断する。副作用解析部２１６は、待機実行リストに実行状態が残っていないので、変数yを解析対象の変数とする記号実行を終了する。変数yは、どの経路を通っても書き換えられるので、書き換えられることなく関数の脱出ブロックに到達する経路条件はfalseとなる。副作用解析部２１６は、書き換わらずに関数の脱出ブロックに到達する経路条件の否定（¬false=true）を、変数yが書き換わる条件として保存する。
【０１１８】
引き続き、副作用解析部２１６は、解析用変数リストから変数gを取り出し、解析対象の変数とする。初期化部初期化部２１５は、初期実行状態を生成し、待機実行リストに保存する。この初期実行状態は、変数xに対して記号実行を行うときに初期化部２１５が生成した初期実行状態と同じである。副作用解析部２１６は、初期実行状態を条件検出部２１７に渡し、解析対象の変数を変数gとして、記号実行を指示する。条件検出部２１７は、記号実行を行い、上記と同様な記号実行を行い、解析対象gが書き換えられることなく関数の脱出ブロックに到達する経路条件を求める。
【０１１９】
広域変数gは、経路条件s(z)>0のときに書き換えられ、経路条件¬(s(z)>0)のとき書き換えられずに関数の脱出ブロックに到達する。副作用解析部２１６は、書き換わらずに関数の脱出ブロックに到達する経路条件の否定（s(z)>o）を、変数xが書き換わる条件として保存する。副作用解析部２１６は、解析用変数リストに含まれる変数について書き換えられる条件が得られると、出力装置２２２に、書き換えられる可能性がある変数x、y、gと、変数xの書き換え条件!(z>0)、変数yの書き換え条件（true）、変数gの書き換え条件（z>0）とを出力する。
【０１２０】
本実施形態では、識別部２１４は、プログラムソースコード２２４を解析し、入力変数のうち、関数実行に伴って書き換えられる可能性がある入力変数を識別し、解析用変数リスト２２９に保存する。解析対象の関数にて、入力変数が書き換えられるのは、入力変数に対する代入が発生するか、或いは、解析対象の関数から呼び出した別の関数で代入が発生する場合である。本実施形態では、記号実行に先だって、識別部２１４を用いて、書き換えが発生する可能性がある変数を求めておく。この場合、条件検出部２１７は、記号実行を行って、書き換えられる可能性がある変数のそれぞれについて、書き換えられずに関数の脱出ブロックに到達する経路条件を求めればよい。
【０１２１】
第１実施形態では、記号実行を脱出ブロックまで進めて、変数書き換えの有無、及び、入力変数が書き換えられずに関数の脱出ブロックまで到達する経路条件を求めている。第１実施形態では、関数の脱出ブロックに到達するまで、入力変数が書き換えられるか否かがわからないので、どの経路を通っても書き換えられない入力変数についても、記号実行で、書き換えられない経路条件を求めていることになる。これに対し、本実施形態では、識別部２１４を用いて、書き換えられずに関数の脱出ブロックに到達する経路条件を調べるべき入力変数を特定している。このようにすることで、記号実行を効率的に行うことができ、第１実施形態に比して、処理時間を短縮できる効果がある。関数の作用により書き換えられる可能性がある変数の一覧だけでなく、各変数が書き換えられる制約条件（入力変数に対する条件）も得られるという効果は、第１実施形態と同様である。
【０１２２】
本実施形態では、ステート処理部２１８は、記号実行に際し、表明情報２２８を参照して、関数呼び出しを含むブロックに到達する経路条件と表明情報２２８に含まれる書き換え条件とを組み合わせた論理式が証明可能か否かを調べる。ステート処理部２１８は、証明可能か否かに応じて、呼び出し先の関数で、表明情報２２８に含まれる書き換えられる可能性がある変数が書き換えられる可能性があるか、可能性がないか、又は、書き換えられる可能性があるか否かが不明かを判定する。ステート処理部２１８にて、呼び出し先の関数にて入力変数が書き換えられるか否か、又は、書き換えられるか否かが不明かを判定することで、関数呼び出しを考慮しない場合に比して、関数呼び出しが入力変数に与える影響をより正しく判断できる。
【０１２３】
ステート処理部２１８は、書き換えられるか否かが不明と判定した変数を、不明リストに保存し、不明リストに含まれる各変数に対して、書き換えが発生するときと発生しないときとの組み合わせを生成する。ステート処理部２１８は、生成した組み合わせ対応して、記号実行で用いる実行状態を生成する。このときステート処理部２１８は、書き換えが発生するときと発生しないときとの組み合わせに対応して、各変数の書き換え条件を∧（ＡＮＤ）結合した条件式、各変数の書き換え条件の否定を∧（ＡＮＤ）結合した条件式、又は、各変数の書き換え条件と書き換え条件の否定とを∧（ＡＮＤ）結合した条件式と、関数呼び出しを含むブロックに到達する経路条件とを∧（ＡＮＤ）結合した条件式を、各組み合わせに対応する実行状態における経路条件とする。条件検出部２１７は、ステート処理部２１８が生成した実行状態に対して記号実行を行う。書き換えられるか否かが不明な変数を、全て未定義として取り扱えば、記号実行の正確性は、その分だけ低下することになる。本実施形態では、組み合わせに対応するその実行状態に対して記号実行を行うため、書き換えられるか否かが不明な変数を全て未定義として取り扱う場合に比して、記号実行で、より正確に変数が書き換わらない経路条件を求めることができる。
【０１２４】
なお、第１実施形態では、関数呼び出しに伴う入力変数の書き換えは考慮していない。第１実施形態でも、表明情報２２８及び表明解析部２１９を用いて、関数呼び出しを考慮して、入力変数が書き換えられずに関数の脱出ブロックに到達する経路条件を求める構成を採用することができる。
【０１２５】
以上、本発明をその好適な実施形態に基づいて説明したが、本発明の副作用解析装置、方法、及び、プログラムは、上記実施形態にのみ限定されるものではなく、上記実施形態の構成から種々の修正及び変更を施したものも、本発明の範囲に含まれる。
【０１２６】
本発明の最小構成の副作用解析装置は、条件検出部と、副作用解析部とを備える。条件検出部は、記憶装置に記憶されたプログラムのソースコードに対して記号実行を行い、ソースコードに含まれる関数が入力変数に与える影響を調べる。また、条件検出部は、入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する。副作用解析部は、記関数の実行に伴って書き換えられる可能性がある入力変数に対して、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する。
【０１２７】
本発明の副作用解析方法の最小構成は、記憶装置に記憶されたプログラムのソースコードに対して記号実行を行い、ソースコードに含まれる関数が入力変数に与える影響を調べると共に、入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する条件検出ステップと、関数の実行に伴って書き換えられる可能性がある入力変数に対し、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する副作用解析ステップとを有するという構成である。
【０１２８】
本発明のプログラムの最小構成は、コンピュータに、記憶装置に記憶されたプログラムのソースコードに対して記号実行を行い、ソースコードに含まれる関数が入力変数に与える影響を調べると共に、前記入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を検出する条件検出処理と、関数の実行に伴って書き換えられる可能性がある入力変数に対し、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する副作用解析処理とを実行させるという構成である。
【０１２９】
本発明の最小構成では、プログラムソースコードに対して記号実行を行い、関数が入力変数が入力変数に与える影響、つまり、関数が入力変数を書き換える可能性があるか否かを調べると共に、入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件を求める。その後、書き換えられる可能性がある入力変数に対し、当該入力変数が書き換えられることなく関数の脱出ブロックに到達する経路条件に基づいて、当該入力変数が書き換えられる条件を判断するための情報を生成する。本発明では、関数実行に伴って書き換えられる可能性がある変数と、当該変数の書き換え条件を判断するための情報を出力でき、その情報を用いることで、検査の精度低下を軽減することができる。
【産業上の利用可能性】
【０１３０】
本発明は、プログラムを開発するための開発環境のプログラム理解支援機能といった用途に適用できる。また、プログラム検査ツールで利用するための表明情報を導出する機能（検査支援機能）といった用途にも適用可能である。
【符号の説明】
【０１３１】
１００、２００：副作用解析装置
１１１、２１１：入力装置
１１２、２１２：計算機
１１３、２１３：構文解析部
１１５、２１５：初期化部
１１６、２１６：副作用解析部
１１７、２１７：条件検出部
１１８：代入処理部
１２０、２２０：分岐判定部
１２１、２２１：定理証明部
１２２、２２２：出力装置
１２３、２２３：記憶装置
１２４、２２４：プログラムソースコード
１２６、２２６：待機実行リスト
１２７：実行状態
２１４：識別部
２１８：ステート処理部
２１９：表明解析部
２２５：代入場所識別表
２２８：表明情報
２２９：解析用変数リスト
【図１】
2011034250.tif 000003
【図２】
2011034250.tif 000004
【図３】
2011034250.tif 000005
【図４】
2011034250.tif 000006
【図５】
2011034250.tif 000007
【図６】
2011034250.tif 000008
【図７】
2011034250.tif 000009
【図８】
2011034250.tif 000010
【図９】
2011034250.tif 000011
【図１０】
2011034250.tif 000012
【図１１】
2011034250.tif 000013
【図１２】
2011034250.tif 000014
【図１３】
2011034250.tif 000015
【図１４】
2011034250.tif 000016
【図１５】
2011034250.tif 000017
【図１６】
2011034250.tif 000018