(57)【要約】      （修正有）【課題】プログラム検証時間の短縮化を図るプログラム検証装置を提供する。【解決手段】検証装置１０は、プログラム変換器２０としての機能と検証器３０としての機能を有する。プログラム変換器は、検証対象であるプログラム（以下、オリジナルプログラム）をプログラム変換して変換プログラムを生成する。プログラム変換器は、ループ融合部２１としての機能と、ループ逆変換部２２としての機能を有する。プログラム変換器は、オリジナルプログラムＰのコードをスキャンし、ループ融合の対象となる複数のループ文を検出する。プログラム変換器は、複数のループ文を単一の融合ループ文にするループ融合のための２つのモードを有し、第１のモードでは、直接、ループ融合が行われ、第２のモードでは、ループ融合の前に、ループ逆変換が行われる。検証器は、変換プログラムを形式的検証し、形式的検証の結果を出力する。【選択図】図１Ａ
2019113997.tif 000002
【特許請求の範囲】
【請求項１】
形式的検証の対象となる変換プログラムであって、オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成する変換器
を備えるプログラム検証装置。
【請求項２】
前記変換プログラムは、複数の前記ループ文における変数の依存関係が解消されるように、複数の前記ループ文における少なくとも一つのループ文に含まれる変数名が変更されている
請求項１に記載のプログラム検証装置。
【請求項３】
前記変換プログラムは、前記変換プログラムを、前記形式的検証の対象として、前記オリジナルプログラムと等価にするステートメントを含む
請求項２に記載のプログラム検証装置。
【請求項４】
前記変換プログラムは、
前記変換プログラムが可能である実行を列挙するための第１ステートメントと、
前記第１ステートメントによって列挙された実行のうち、前記オリジナルプログラムが可能な実行に対応するものを、前記形式的検証の対象にするための第２ステートメントと、
を含む請求項２に記載のプログラム検証装置。
【請求項５】
前記変換プログラムは、
前記融合ループ文の前に設けられた第１ステートメントと、
前記融合ループ文の後に設けられた第２ステートメントと、
をさらに含み、
前記第１ステートメントは、所定の変数が、前記融合ループ文の実行後にとり得る値を非決定的に列挙するステートメントであり、
前記第２ステートメントは、前記融合ループ文の実行後において前記所定の変数がとる値が、前記第１ステートメントによって非決定的に列挙された前記値と等価である場合を、前記形式的検証の対象にするステートメントである
請求項２に記載のプログラム検証装置。
【請求項６】
前記変換器は、複数の前記ループ文の少なくとも一つの対象ループ文を、前記対象ループ文の逆実行ループ文に変換し、前記対象ループ文に代えて前記逆実行ループ文を含む複数のループ文をループ融合する
請求項１〜５のいずれか１項に記載のプログラム検証装置。
【請求項７】
前記変換プログラムは、前記逆実行ループ文を、前記形式的検証の対象として、前記対象ループ文と等価にするステートメントを含む
請求項６に記載のプログラム検証装置。
【請求項８】
オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成して記憶部に記憶させ、
プログラムを形式的検証する検証器によって、前記記憶部に記憶された前記変換プログラムを形式的検証する
ことを含むプログラム検証方法。
【請求項９】
コンピュータに、プログラム検証処理を実行させるコンピュータプログラムであって、
前記プログラム検証処理は、
オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成し、
前記変換プログラムを形式的検証する
ことを含む、プログラム検証のためのコンピュータプログラム。
【請求項１０】
オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成するプログラム変換器であって、
複数の前記ループ文における変数の依存関係が解消されるように、複数の前記ループ文における少なくとも一つのループ文に含まれる変数名を変更するよう構成されている
プログラム変換器。
【請求項１１】
プログラム変換器が、記憶部に記憶されたオリジナルプログラムに含まれる複数のループ文における変数の依存関係が解消されるように、複数の前記ループ文における少なくとも一つのループ文に含まれる変数名を変更し、
前記プログラム変換器が、変数名が変更された状態で複数の前記ループ文をループ融合した融合ループ文を含む変換プログラムを生成する
ことを含むプログラム変換方法。
【請求項１２】
コンピュータに、プログラム変換処理を実行させるコンピュータプログラムであって、
前記プログラム変換処理は、
オリジナルプログラムに含まれる複数のループ文における変数の依存関係が解消されるように、複数の前記ループ文における少なくとも一つのループ文に含まれる変数名を変更し、
変数名が変更された状態で複数の前記ループ文をループ融合した融合ループ文を含む変換プログラムを生成する
ことを含む、プログラム変換のためのコンピュータプログラム。
【請求項１３】
オリジナルプログラムを作成し、
前記オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成し、
プログラムを形式的検証する検証器によって、前記変換プログラムを形式的検証し、
前記形式的検証の結果に基づいて、前記オリジナルプログラムを修正する
ことを含むプログラムの製造方法。
【請求項１４】
プログラムを形式的検証する検証器によって検証される検証用プログラムであって、
オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を有する
検証用プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、プログラム変換器、プログラム変換方法、プログラム変換のためのコンピュータプログラム、プログラム製造方法、及び検証用プログラムに関するものである。
【背景技術】
【０００２】
プログラムが仕様とおりに動作することを検証する技術を、プログラム検証という。プログラム検証では、プログラムを実行することなく証明するため、プログラムの正当性を数学的な形式的手法で検証する形式的検証（formal verification）が用いられる。
【０００３】
非特許文献１は、与えられたプログラムに等価であるが不変条件がシンプルになるプログラムを生成するプログラム変換手法を開示している。不変条件がシンプルになると、検証を高速化することができる。非特許文献１は、プログラム変換により生成されたプログラムを検証することを開示しているが、ループ融合（Loop Fusion）されたプログラムを検証することを開示していない。
【０００４】
非特許文献２は、ループ融合を開示している。ループ融合は、プログラムに含まれる複数のループ文を単一のループ文に融合することである。従来、ループ融合は、コンパイラ最適化（compiler optimization）に用いられていたが、プログラム検証には用いられていなかった。
【先行技術文献】
【非特許文献】
【０００５】
【非特許文献１】Rahul Sharma, Isil Dillig, Thomas Dillig, and Alex Aiken. Simplifying Loop Invariant Generation Using Splitter Predicates. In CAV 2011 (LNCS), Vol. 6806. 703-719.
【非特許文献２】David F. Bacon, Susan L. Graham, and Oliver J. Sharp. Compiler Transformations for High-performance Computing. ACM Computing Survey 26, 4 (Dec. 1994), pp. 345-420.
【発明の概要】
【０００６】
プログラム中に、複数のループ文が存在すると、プログラム検証器による検証時間が非常に長くなることがあることを本発明者らは見出した。したがって、検証時間の短縮化が望まれる。
【０００７】
本発明の一の態様は、プログラム検証装置である。実施形態において、プログラム検証装置は、形式的検証の対象となる変換プログラムであって、オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成する変換器を備える。
【０００８】
本発明の態様は、プログラム検証方法、プログラム検証のためのコンピュータプログラム、プログラム変換器、プログラム変換方法、プログラム変換のためのコンピュータプログラム、プログラム製造方法、及び検証用プログラムのいずれかであってもよい。
【図面の簡単な説明】
【０００９】
【図１Ａ】図１Ａはプログラム検証装置の機能ブロック図である。
【図１Ｂ】図１Ｂはプログラム検証装置を構成するコンピュータのブロック図である。
【図２】図２はプログラムの製造工程を示すフローチャートである。
【図３Ａ】図３Ａはプログラム変換手順の第１例を示すフローチャートである。
【図３Ｂ】図３Ａはプログラム変換手順の第２例を示すフローチャートである。
【図４】ループ融合前後の等価性を示す説明図である。
【発明を実施するための形態】
【００１０】
［１．プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、プログラム変換器、プログラム変換方法、プログラム変換のためのコンピュータプログラム、プログラム製造方法、及び検証用プログラムの概要］
【００１１】
（１）実施形態に係るプログラム検証器は、形式的検証の対象となる変換プログラムであって、オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成する変換器を備える。
【００１２】
（２）前記変換プログラムは、複数の前記ループ文における変数の依存関係が解消されるように、複数の前記ループ文における少なくとも一つのループ文に含まれる変数名が変更されているのが好ましい。
【００１３】
（３）前記変換プログラムは、前記変換プログラムを、前記形式的検証の対象として、前記オリジナルプログラムと等価にするステートメントを含むのが好ましい。
【００１４】
（４）前記変換プログラムは、前記変換プログラムが可能である実行を列挙するための第１ステートメントと、前記第１ステートメントによって列挙された実行のうち、前記オリジナルプログラムが可能な実行に対応するものを、前記形式的検証の対象にするための第２ステートメントと、含むことができる。
【００１５】
（５）前記変換プログラムは、前記融合ループ文の前に設けられた第１ステートメントと、前記融合ループ文の後に設けられた第２ステートメントと、をさらに含み、前記第１ステートメントは、所定の変数が、前記融合ループ文の実行後にとり得る値を非決定的に列挙するステートメントであり、前記第２ステートメントは、前記融合ループ文の実行後において前記所定の変数がとる値が、前記第１ステートメントによって非決定的に列挙された前記値と等価である場合を、前記形式的検証の対象にするステートメントであるのが好ましい。
【００１６】
（６）前記変換器は、複数の前記ループ文の少なくとも一つの対象ループ文を、前記対象ループ文の逆実行ループ文に変換し、前記対象ループ文に代えて前記逆実行ループ文を含む複数のループ文をループ融合してもよい。
【００１７】
（７）前記変換プログラムは、前記逆実行ループ文を、前記形式的検証の対象として、前記対象ループ文と等価にするステートメントを含むことができる。
【００１８】
（８）実施形態に係るプログラム検証方法は、オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成して記憶部に記憶させ、プログラムを形式的検証する検証器によって、前記記憶部に記憶された前記変換プログラムを形式的検証することを含む。
【００１９】
（９）実施形態に係るプログラム検証のためのコンピュータプログラムは、コンピュータに、プログラム検証処理を実行させる。前記プログラム検証処理は、オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成し、前記変換プログラムを形式的検証することを含む。
【００２０】
（１０）実施形態に係るプログラム変換器は、オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成する。プログラム変換器は、複数の前記ループ文における変数の依存関係が解消されるように、複数の前記ループ文における少なくとも一つのループ文に含まれる変数名を変更するよう構成されている。
【００２１】
（１１）実施形態に係るプログラム変換方法は、プログラム変換器が、記憶部に記憶されたオリジナルプログラムに含まれる複数のループ文における変数の依存関係が解消されるように、複数の前記ループ文における少なくとも一つのループ文に含まれる変数名を変更し、前記プログラム変換器が、変数名が変更された状態で複数の前記ループ文をループ融合した融合ループ文を含む変換プログラムを生成することを含む。
【００２２】
（１２）実施形態に係るプログラム変換のためのコンピュータプログラムは、コンピュータに、プログラム変換処理を実行させる。前記プログラム変換処理は、オリジナルプログラムに含まれる複数のループ文における変数の依存関係が解消されるように、複数の前記ループ文における少なくとも一つのループ文に含まれる変数名を変更し、変数名が変更された状態で複数の前記ループ文をループ融合した融合ループ文を含む変換プログラムを生成することを含む。
【００２３】
（１３）実施形態に係るプログラムの製造方法は、オリジナルプログラムを作成し、前記オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を含む変換プログラムを生成し、プログラムを形式的検証する検証器によって、前記変換プログラムを形式的検証し、前記形式的検証の結果に基づいて、前記オリジナルプログラムを修正することを含む。
【００２４】
（１４）実施形態に係る検証用プログラムは、プログラムを形式的検証する検証器によって検証される。検証用プログラムは、オリジナルプログラムに含まれる複数のループ文をループ融合した融合ループ文を有する。
【００２５】
［２．プログラム検証装置］
【００２６】
図１Ａは、検証対象であるプログラムの形式的検証をする検証装置１０の機能ブロックを示している。検証装置１００は、プログラム変換器２０としての機能を有する。プログラム変換器２０は、検証対象であるプログラム（以下、オリジナルプログラムという）をプログラム変換して変換プログラムを生成する。実施形態において、プログラム変換器２０は、オリジナルプログラムＰのソースコードを、変換プログラムとなるソースコードに変換するソース−ソース変換器（sorce-to-source translator）である。プログラム変換器２０は、ループ融合部２１としての機能を有する。また、プログラム変換器２０は、ループ逆変換部２２としての機能を有する。ループ融合及びループ逆変換については、後述する。
【００２７】
検証装置１００は、検証器３０としての機能を有する。検証器３０は、変換プログラムを形式的検証し、形式的検証の結果を出力する。検証器３０は、例えば、CPAchekerである。CPAcheckerについては、https://cpachecker.sosy-lab.org/を参照。検証器３０は、SeaHornであってもよい。SeaHornについては、http://seahorn.github.io/を参照。
【００２８】
検証装置１０は、例えば、図１Ｂに示すコンピュータ４０によって構成される。コンピュータ４０は、プロセッサ１１と、記憶部１２と、を備える。記憶部１２には、プロセッサ１１によって読み取られる情報が格納されている。
【００２９】
記憶部１２に格納された情報は、プログラム検証処理の実行のための検証用コンピュータプログラム５０を含む。実施形態において、プログラム検証処理は、変換プログラムを生成するプログラム変換処理と、変換プログラムに対する形式的検証処理と、を含む。検証用コンピュータプログラム５０は、コンピュータ４０にプログラム検証処理を実行させる。より具体的には、プロセッサ１１は、記憶部１２から検証用コンピュータプログラム５０を読み出して実行する。これにより、コンピュータ４０は、プログラム変換器２０及び検証器３０としての機能を有する検証装置１０として機能する。
【００３０】
記憶部１２は、オリジナルプログラムを保存する領域１００を有する。領域１００に保存されたオリジナルプログラムが、プログラム検証処理におけるプログラム変換の対象となる。オリジナルプログラムは、検証装置１０の外部から読み込まれて、領域１００に保存される。オリジナルプログラムは、ユーザ操作によって読み込まれてもよいし、検証装置１０の自律動作によって外部サーバ等から読み込まれてもよい。
【００３１】
記憶部１２は、変換プログラムを保存する領域２００を有する。プログラム変換器２０によるプログラム変換処理によって生成された変換プログラムは、領域２００に保存される。形式的検証処理を行う検証器３０は、領域２００に保存された変換プログラムを読み出し、変換プログラムに対する形式的検証をする。
【００３２】
［３．プログラム製造方法］
【００３３】
図２は、実施形態に係るプログラム製造方法を示している。実施形態に係るプログラム製造方法では、作成されたプログラムは、検証装置１０を用いて検証される。作成されたプログラムは、検証結果に基づいて、修正される。１又は複数回の検証と修正とを経て、プログラムが完成する。
【００３４】
より具体的には、まず、ステップＳ１１において、オリジナルプログラムが作成される。オリジナルプログラムは、人（プログラマー）によりコーディングされたプログラムであってもよいし、プログラム生成器により自動生成されたプログラムであってもよい。作成されたオリジナルプログラムは、保存領域１００に保存される。
【００３５】
ステップＳ１２において、プログラム変換器２０は、領域１００に保存されたオリジナルプログラムをプログラム変換し、変換プログラムを生成する。変換プログラムは保存領域２００に保存される。
【００３６】
ステップ１３において、検証器３０は、保存領域２００に保存された変換プログラムに対して形式的検証をし、その検証結果を出力する。検証結果は、オリジナルプログラムが、作成されたオリジナルプログラムが仕様を常に満たしているか否か（例えば、不変条件を満たしているか否か）を示す情報を含む。検証結果は、例えば、検証装置１０に接続されたディスプレイに表示される。
【００３７】
オリジナルプログラムが仕様を満たしていない場合には、ステップＳ１４において、オリジナルプログラムの修正が必要であると判断され、仕様を満たしていれば、ステップＳ１４において、修正は不要であると判断される。ステップＳ１４の判断は、検証装置１０が行ってもよいし、プログラマーが、検証結果を参照して行ってもよい。
【００３８】
オリジナルプログラムの修正が必要な場合、ステップＳ１５において、オリジナルプログラムの修正が行われる。修正は、例えば、プログラマーによって行われる。修正されたオリジナルプログラムは、保存領域１００に保存される。修正されたオリジナルプログラムを新たなオリジナルプログラムとして、検証装置１０は、ステップＳ１２及びステップＳ１３の検証工程を実施する。ステップＳ１２〜ステップＳ１５までの工程は、必要に応じて、複数回繰り返される。ステップＳ１４において、修正が不要と判断されれば、検証されたプログラムが完成する。
【００３９】
実施形態においては、後述するように、形式的検証が効率的に行われるように、オリジナルプログラムのプログラム変換が行われるため、プログラム検証を含むプログラム製造工程全体を効率的に実施することができる。すなわち、形式的検証が効率的に行われなかったり、現実的な時間内に終了しない場合には、プログラム修正に時間を要したり、プログラム検証結果に基づいたプログラム修正が行えなくなるが、本実施形態によれば、プログラムの製造を効率的に行うことができる。
【００４０】
［４．プログラム変換］
【００４１】
プログラム変換器２０は、オリジナルプログラムＰのコードをスキャンし、ループ融合の対象となる複数のループ文を検出する。実施形態のプログラム変換器２０は、ループ融合のための２つのモードを有する。第１のモードでは、図３Ａに示すように、検出された複数のループ文に対して、直接、ループ融合（ステップＳ２１）が行われる。
【００４２】
第２のモードでは、図３Ｂに示すように、ループ融合（ステップＳ２１）の前に、ループ逆変換（ステップＳ２２）が行われる。例えば、２つのループ文を含むオリジナルプログラムがあった場合、ループ融合の前に、ループ融合の対象として検出された２つのループ文のうちの一方のループ文（対象ループ文）を逆実行ループ文に変換する。逆実行ループ文は、変換前のループ文とは実行順序が逆になっているループ文である。例えば、インクリメントされるｉが０からｎ−１になるまでの間実行されるループ文があった場合、逆実行ループ文は、デクリメントされるｉがｎ−１から０になるまでの間実行される。
【００４３】
第２のモードでは、対象ループ文に代えて、逆実行ループ文を含む複数のループ文を、ループ融合（ステップＳ２１）の対象とする。例えば、２つのループ文のループ融合では、逆実行ループ文と、２つのループ文のうちの対象ループ文ではないループ文と、のループ融合が行われる。
【００４４】
後述の実験結果に示すように、逆実行ループ文をループ融合させたほうが、検証を効率的に行うことができる場合があり有利である。
【００４５】
［４．１  ループ融合］
【００４６】
ループ融合は、複数のループ文を単一の融合ループ文にすることである。例えば、Ｃ言語でコーディングされた次のプログラムは、連続する２つのループ文を有する。以下において、第１のループ文は、変数ｉが０からｎ未満まで１ずつ増加するループにおいて、ｉの値を変数ｓｕｍ１に加算する。また、第２のループ文は、変数ｉが０からｎ未満まで１ずつ増加するループにおいて、ｉの値を変数ｓｕｍ２に加算する。
【数１】
2019113997.tif 000003
【００４７】
上のプログラムは、ループ融合により、次のような融合ループ文に変換される。融合ループ文は、変数ｉが０からｎ未満まで１つずつ増加する単一のループ内において、ｉの値を変数ｓｕｍ１と変数ｓｕｍ２に加算する。したがって、ループ融合の前後の両プログラムは等価である。
【数２】
2019113997.tif 000004
【００４８】
このようなループ融合は、プログラム変換器２０により行われる。プログラム変換器２０は、例えば、コンパイラ最適化（compiler optimization）に用いられていたループ融合機能付きプログラム変換器と同様のものでもよい。これまで、ループ融合技術自体はコンパイラ最適化の分野において存在していたが、プログラム検証のためにループ融合は用いられていなかった。しかし、ループ融合をすることにより、プログラムの形式的検証のためのループ不変条件（loop invariant）をシンプルにできる場合があることを、本発明者らは見出した。複雑なループ不変条件は、検証に要する時間を増大させるが、シンプルなループ不変条件は、検証に要する時間を抑えるのに有用である。したがって、ループ融合をしてから形式的検証をすることで、形式的検証を高速かつ効率的に行える。
【００４９】
以下、ループ融合により、ループ不変条件がシンプルになる例について説明する。以下のＣ言語関数（C function）は、数１に示した２つのループ文を含んでいる。
【数３】
2019113997.tif 000005
【００５０】
数３に示すＣ言語関数は、最後の行に、”assert(sum1 == sum2);”とコーディングされた検証用のassertステートメントを有する。このステートメントは、アサーション（assertion;表明）とも呼ばれる。assertステートメントは、assertステートメントが記述されている個所において、成立すべき条件を示している。数３に示すassertステートメントは、２つのforループ文の実行後において、変数sum1と変数sum2の値は等しくなるべきであるという表明である。プログラム検証において、２つのforループ文の実行直後において変数sum1と変数sum2の値が等しくならないことが検出されると、仕様を満たしていないことを示すエラー(バグ)が検証結果として出力される。
【００５１】
ループ文を含むプログラムの形式的検証では、ループ不変条件が生成される。数３のＣ言語関数のループ不変としては、例えば、以下のものが生成される。数４のループ不変条件は、数３のＣ言語関数における第１ループ文のためのループ不変条件であり、数５のループ不変条件は、数３のＣ言語関数における第２ループ文のためのループ不変条件である。
【数４】
2019113997.tif 000006
【数５】
2019113997.tif 000007
【００５２】
これらのループ不変条件は、ｉ＊ｉという非線形の項を有する。非線形の項が含まれるループ不変条件は、検証に係る時間を増大させる。したがって、数３のＣ言語関数において、assertステートメントとして記述されたアサーションは、全てのｎについて成り立つことが明らかであるものの、検証器による形式的検証では、非線形項のために検証に時間を要する。後述のように、発明者らの実験では、９００秒かけても検証を完了することができなかった。
【００５３】
一方、数３のＣ言語関数における２つのループ文を、プログラム変換器２０によってループ融合すると、変換プログラムとして、次のＣ言語関数が得られる。
【数６】
2019113997.tif 000008
【００５４】
数３のＣ言語関数においては、２つのループ文が含まれていたのに対して、数６のＣ言語関数においては、単一の融合ループ文だけが含まれている。数６のＣ言語関数の場合に生成されるループ不変条件は、sum1 == sum2 というシンプルなものとなる。数６のＣ言語関数の場合に生成されるループ不変条件は、非線形の項を含まないシンプルなものであるため、検証の時間の増大が抑制され、検証が効率化される。驚くべきことに、後述の発明者らの実験では、数秒で検証が完了した。
【００５５】
［４．２  ループ融合の制限緩和］
既存のループ融合技術におけるループ融合の適用性には制限がある。例えば、複数のループ文における変数に依存関係があると、既存のループ融合技術では、ループ融合ができない。例えば、以下の２つのループ文におけるそれぞれのループ本体（loop body）は、同じ変数sumを有している。つまり、第１ループ文のループ本体は、第２ループ文のループ本体に依存している。したがって、数７に示す２つのループ文は、既存のループ融合技術では、ループ融合できない。
【数７】
2019113997.tif 000009
【００５６】
これに対して、本実施形態のプログラム変換器２０は、複数のループ文における変数に依存関係があっても、ループ融合が可能である。この点につき、数７に示す２つのループ文を含む次のプログラム（オリジナルプログラム）Ｐに基づいて説明する。プログラムＰは、数７と同様の２つのループ文と、２つのループ文の後のassertステートメントとを含んでいる。
【数８】
2019113997.tif 000010
【００５７】
本実施形態のプログラム変換器２０は、数８に示すオリジナルプログラムＰを、次の変換プログラムへ変換する。数９の変換プログラムにおいては、数８のオリジナルプログラムに生じている変数sumの依存関係がない。また、数９の変換プログラムは、形式的検証の対象として、オリジナルプログラムＰと等価である。
【数９】
2019113997.tif 000011
【００５８】
数９に示す変換プログラムでは、変換器２０により生成されたhavocステートメント及びassertステートメントが登場している。havocステートメント及びassumeステートメントは、検証器３０の振る舞いをコントロールするステートメントであり、CPAcheker及びSeaHornのような検証器でも用いられている。
【００５９】
havocステートメントは、非決定的に値を決定するためのコマンドである（The havoc() statement nondeterministically chooses a value and returns it.）。
【００６０】
assumeステートメントは、assumeステートメント内に記述された条件（数９に示す変換プログラムでは、sum == sum_middleという条件）が成り立つときに検証を続け、成り立たなければ、以後の検証をやめるコマンドである。assumeステートメントは、一般的には、事前条件を規定するために用いられる。なお、assumeステートメントにおいては、条件が成り立たず、検証をやめても、以後のプログラムが検証対象にならないだけで、検証結果がエラー（バグ）になるわけではなく、この点で、assertステートメントとは異なる。
【００６１】
例えば、assume(sum == sum_middle)は、sum_middle==sumが成り立つときは、無動作命令（no operation; no-op）として働くことで以後の検証を続けさせ、sum_middle==sumが成り立たないときは、以後の検証を停止させる。
【００６２】
本実施形態の変換プログラムでは、havocステートメント及びassumeステートメントの用法が、一般的な用法とは異なっている。
【００６３】
変換プログラムにおいて、融合ループ文（数９における単一のforループ文）の前にあるhavocステートメントは、この変換プログラムが可能である実行を列挙するための第１ステートメントになっている。ここでは、変数sum_middleの値が非決定的に全て列挙される。変数sum_middleは、後述のように、変換前の２つのループ文の間における変数sumの値を示す。havocステートメントによって非決定的に全列挙された変数に基づいて、融合ループ文の実行が行われた場合、オリジナルプログラムＰでは起こり得ない実行を含むことになる。
【００６４】
変換プログラムにおいて、融合ループ文の後にあるassumeステートメントは、havocステートメントによって列挙された実行のうち、オリジナルプログラムＰが可能な実行に対応するものだけを、形式的検証の対象にする第２ステートメントになっている。すなわち、融合ループ文の実行後における変数sumの値が、havocステートメントによって列挙された値sum_middleと等しい場合には、havocステートメントによって列挙された値sum_middleに基づく実行は、オリジナルプログラムＰが可能な実行であることになる。
【００６５】
変換プログラムにおけるassumeステートメントは、sum_middle==sumが成り立つときは、無動作命令（no operation; no-op）として働くことで、変換プログラムにおける以後の部分（sum sum2; assert(sum == 0);）の検証を続けさせ、sum_middle==sumが成り立たないときは、以後の検証を停止させる。sum_middle==sumが成り立たないときは、以後の部分の検証が行われず、オリジナルプログラムＰでは起こり得ない実行が検証の対象から排除される。
【００６６】
また、換言すると、havocステートメントは、所定の変数sumが、融合ループ文の実行後に取り得る値sum_middleを非決定的に列挙する第１ステートメントである。そして、assumeステートメントは、融合ループ文の実行後において所定の変数sumがとる値が、havocステートメントによって非決定的に列挙された値sum_middleと等価である場合に、形式的検証の対象とする第２ステートメントである。このように、変数の値（プログラムの状態）をhavocステートメントによって推測し（guess）、その推測が適切な場合だけをassumeステートメントによって検証の対象とするスキームを、以下では、Guess-and-Assumeという。
【００６７】
さて、以下では、数８に示すプログラムＰから数９に示す変換プログラムへの変換を順番に説明する。
【００６８】
まず、プログラムＰが有する２つのループ文のループ本体に含まれる変数名を変更する。プログラムＰの２つのループ文におけるそれぞれのループ本体（loop body）は、同じ変数sumを有している。このため、２つのループ文には、変数の依存関係がある。実施形態においては、少なくとも一つのループ文の変数名を変更することにより、変数の依存関係を解消する。以下の数１０では、変数名変更のために新たな変数sum2が導入され、数８における第２ループ文の変数sumが、新変数sum2に変更されている。数１０のように変数名が変更されたプログラム（変数名変更プログラム）Ｐでは、２つのループ文における変数の依存関係が解消されている。なお、Ｃ言語において、／＊で始まり、＊／で終わるまでの部分は、コメントであり、プログラムの実行に影響を与えない。
【数１０】
2019113997.tif 000012
【００６９】
ここで、複数のループ文が同じ変数を有していても、その変数の値が、複数のループ文の実行中において変動しない場合等においては、変数名を変更しても、その変更前後のプログラムＰは等価である。そのような場合は、複数のループ文の間に形式的には依存関係があるが、実質的には、依存関係がないことになる。その場合、単に変数名が変更されたプログラムＰを、直接、ループ融合し、ループ融合された変換プログラムに対して形式的検証するだけでもよい。
【００７０】
これに対し、数１０のプログラムＰでは、オリジナルプログラムＰにおける２つのループ文間の関係が、変数名の変更によって失われており、数１０のプログラムは、オリジナルプログラムＰと等価ではなく、プログラムの意味としても異なっている。したがって、数１０のプログラムを検証しても、オリジナルプログラムＰを検証したことにはならない。このように、変数名の変更によって、形式的検証の対象としてのプログラムの等価性が失われる場合には、プログラムを等価にするためのステートメントを追加すればよい。そのようなステートメントは、プログラム変換器２０によって追加される。
【００７１】
変数名の変更によって失われた関係が補償されたプログラムＱを以下に示す。プログラムＱでは、新たな変数sum_middleが導入される。プログラムＱにおいて、変数sum_middleは、数１０のコメント（Ｘ）の行の位置（２つのループ文の間の位置）における変数sumの値を表す。
【数１１】
2019113997.tif 000013
【００７２】
数１１に示すプログラムＱでは、コメント（Ｙ）の行の位置における変数sum及び変数sum2の値は、変数sum_middleの値と等しい。これは、assum(sum_middle == sum);というassumeステートメントとsum2 = sum_middle;という代入ステートメントのおかげである。つまり、assum(sum_middle == sum);というassertステートメントによって、変数sum_middleの値と変数sumとの値が等しい場合だけが検証対象となる。また、sum2 = sum_middle;という代入ステートメントによって、変数sum2の値は、変数sum_middleの値とは等しくなる。
【００７３】
さらに、プログラムＱでは、assert(sum == 0)というassertステートメントが実行される手前で、変数sum2の値が、変数sumに代入される。
【００７４】
したがって、プログラムＱは、プログラムＰと形式的検証の対象として等価である。つまり、プログラムＱのassertステートメントが成り立てば、プログラムＰのassertステートメントも成り立つことになる。
【００７５】
ただし、プログラムＱでは、変数sum_middleの値を、プログラムの最初においてどのように予測するのか、という問題が残っている。この問題の対処のため、havoc()ステートメントが用いられる。以下に、havoc()ステートメントによって、変数sum_middleの値を非決定的に選択するようにしたプログラムを示す。
【数１２】
2019113997.tif 000014
【００７６】
数１２のプログラムは、数１１に示すプログラムＱの最初に、havoc()ステートメントにより選択された値を、変数sum_middleに代入する行を追加したものである。さらに、数１２のプログラムでは、プログラムＱにおけるassumeステートメントが、２つのループ文の間の位置から２つのループ文の後の位置に移動している。assumeステートは、変数sum2を使用していないため、この移動はプログラムの意味を変更させない。また、数１２のプログラムでは、プログラムＱにおけるsum2 = sum_middle;の代入ステートメントが、２つのループ文の間の位置から２つのループ文の前の位置に移動している。sum2 = sum_middle;の代入ステートメントは、変数sumを使用していないため、この移動はプログラムの意味を変更させない。したがって、数１２のプログラムは、プログラムＱと等価である。
【００７７】
数１２のプログラムに含まれる２つのループ文は、変数の依存関係がなく、既存のループ融合技術でも融合可能なものとなっている。数１２のプログラムにおける２つのループ文を融合させると、数９に示す変換プログラムとなる。
【００７８】
上記の説明では、実施形態に係るループ融合を具体的なプログラムＰに基づいて説明したが、以下では、実施形態に係るループ融合を一般化して定義する。なお、実施形態に係るループ融合は、上記の説明のように順番に行われる必要はなく、プログラム変換器２０は、以下の定義に従った変換を一括して行うことができる。
【００７９】
まず、オリジナルプログラムＰを以下のように表す。数１３のプログラムＰは、２つの連続するwhileループ文を有し、第１whileループ文は、条件e1が成り立つ間、ループ本体のコマンドP1を実行する。第２whileループ文は、条件e2が成り立つ間、ループ本体のコマンドP2を実行する。
【数１３】
2019113997.tif 000015
【００８０】
このプログラムＰにおける２つのループ文を融合させるコマンドFUSION[P]は、次のように定義される。
【数１４】
2019113997.tif 000016
【００８１】
ここで、Ｖは、プログラムに出現する変数の集合であり、V＝｛x1,x2,…,xn｝である。V’＝｛x1,x2,…,xn｝は、Vと同じサイズで、Vと互いに素である変数の集合である。V’は、変数名が変更された変数の集合に相当する。P’（P2’）は、コマンドP（P2）における変数xiを、V’の変数xi’に置換したコマンドである。e2’は、条件e2における変数xiを、V’の変数xi’に置換した条件である。
【００８２】
V”:= V’（数１４の２行目の代入ステートメント）は、変数の集合V＝｛x1,x2,…,xn｝についての代入コマンドの簡略形であり、x1:=x1’; …; xn:=xn’を示す。assume V= V”（数１４の下から２行目のassumeステートメント）は、assume x1=x1’; …; assume xn=xn’の簡略形を示す。
【００８３】
数１４において、単一のwhileループ文が融合ループ文である。この融合ループ文では、融合前における第１ループ文の条件e1と、第２ループ文の条件e2（ここでは、変数名が変更された条件e2’）のいずれかが成り立つこと（e1 OR e2’）が、融合ループ文のループ繰り返し条件となっている。そして、融合ループ文においては、第１ループ文のループ本体P1は、条件e1が成り立つときにだけ実行され、第２ループ文のループ本体P２（ここでは、変数名が変更されたループ本体P2’）は、条件e2’が成り立つときにだけ実行される。コマンドFUSION[P]では、ループ繰り返し条件e1，e2に関し、このような変換が行われるため、ループ繰り返し条件が異なる複数のループ文であってもループ融合することができる。
【００８４】
数１３のオリジナルプログラムＰと数１４の変換プログラムFUSION[P]が等価であることの説明を図４に示す。図４（ａ）は、オリジナルプログラムＰを示し、図４（ｂ）から図４（ｆ）の順で等価なプログラムに変換されている。図４（ａ）から図４（ｆ）までの各プログラムは全て等価であり、図４（ｆ）は変換プログラムである。
【００８５】
実施形態のループ融合は、融合される複数のループの間に、非ループ文であるコマンドP3が存在していても可能である。そのような場合のループ融合コマンドFUSIONR[P]は、次のように定義される。
【数１５】
2019113997.tif 000017
【数１６】
2019113997.tif 000018
【００８６】
なお、ループ融合の対象であるループ文が３以上ある場合には、２つのループ文のループ融合を繰り返して３以上のループ文を単一の融合ループ文にしてもよいし、FUSION[P]又はFUSIONR[P]の定義を３以上のループ文に拡張し、１回のループ融合で単一の融合ループ文を得てもよい。
【００８７】
［４．３  ループ逆変換（Loop Reversal transformation）］
【００８８】
前述のように、実施形態のプログラム変換器２０は、ループ融合に先立って、ループ逆変換をすることができる。逆実行ループ文は、ループ逆変換前のループ文とは逆の順序で、ループ逆変換前のループ文のループ本体を実行するループ文である。実施形態のプログラム変換器２０が生成する逆実行ループ文は、形式的検証の対象として、ループ逆変換前のループ文と等価である。
【００８９】
実施形態において、ループPの逆実行ループ文を生成するコマンドは、REVERSE[REVERSELOOP[ループ文]]として表される。このコマンドは、REVERSEというコマンドと、REVERSELOOPというコマンドとを有している。
【００９０】
REVERSE[P]は、任意のプログラムＰの実行後の状態（例えば、プログラムP中の変数の実行後の値）が与えられると、プログラムＰの実行前の状態（例えば、プログラムP中の変数の実行前の値）を返すプログラムに、プログラムＰを変換するコマンドである。例えば、プログラムＰが、ｉをインクリメントするものであれば、REVERSE[P]は、ｉをデクリメントするプログラムになる。
【００９１】
実施形態のループ融合で用いられたGuess-and-Assumeスキームは、REVERSE[P]においても用いられる。REVERSE[P]は、次のように定義される。
【数１７】
2019113997.tif 000019
【００９２】
REVERSE[P]は、まず、プログラムＰの最初の状態（プログラムＰ中の変数の値）を推測し（guess）、名前が変更された変数V’に格納され、さらに、V”にバックアップされる。そして、変数名が変更されたプログラムＰ’が実行（順実行）される。そして、assumeステートメントにより、プログラムＰ’の実行完了後の状態V’が、REVERSE[P]に与えられたプログラムＰの実行完了後の状態Vと等しいかどうかチェックされる。等しい場合、プログラムＰの最初の状態の推測値V”が、Vに代入される。例えば、プログラムＰが変数ｉをインクリメントするコード［i++]である場合、REVERSE[P]の定義にしたがって記述された以下のプログラムコードは、変数iをデクリメントするコード[i--]と等価である。
【００９３】
【数１８】
2019113997.tif 000020
【００９４】
REVERSELOOP［ループ文］は、与えられたループ文を、そのループ文の実行順序とは逆の順所で、そのループ文のループ本体ＰについてのREVERSE［P］を実行するコマンドである。ここでは、ループ文は、while e do P doneで表されるwhileループ文とする。ｅは、ループ繰り返し条件であり、Ｐは、ループ本体である。REVERSELOOP［while e do P done］は、次のように定義される。
【数１９】
2019113997.tif 000021
【００９５】
ここで、ｘは、新たに導入された変数であり、ループの繰り返し回数を示す。¬ｅは、ｅの否定を示す。ループ文の実行が完了した場合、繰り返し条件eは成り立たなくなっているはずなので、assume¬eのステートメントはそれを仮定する。Havoc xのステートメントは、ループの繰り返し回数xを推測する。
【００９６】
例えば、while e do P doneが以下のものである場合、
【数２０】
2019113997.tif 000022
REVERSELOOP［while e do P done］により生成されるコードは以下のようになる。なお、以下のコードでは、プログラム本体P{sum += 1; i++;}のREVERSE[P]が、理解の容易のため、等価な表現であるsum -= i; i--;で表されている。
【数２１】
2019113997.tif 000023
【００９７】
REVERSELOOP［while e do P done］は、while e do P doneを、そのwhile e do P doneの実行順序とは逆の順所でREVERSE［P］を実行するコマンドであるから、REVERSE[REVERSELOOP［while e do p done］]は、while e do P doneの実行順序とは逆の順所で実行するものとなる。REVERSE[REVERSELOOP［while e do P done］]は、Guess-and-Assumeアプローチに従いhavocステートメントやassumeステートメントなどを有している。これらのステートメントは、REVERSE[REVERSELOOP［while e do P done］]を、形式的検証の対象として、while e do P doneと等価にする。
【００９８】
［５  実験結果］
【００９９】
実施形態の検証装置１０による検証の実験結果を、表１及び表２に示す。表１は、検証器３０としてCPACHECKERを用いた結果を示し、表２は、検証器３０として、ＳＥＡＨＯＲＮを用いた結果を示している。表１において、CPACHECKERとある列は、ループ融合をせずに検証した結果を示し、表２において、SEAHORNとある列は、ループ融合をせずに検証した結果を示す。表中の数字は、検証に要した時間を示し単位は、秒である。表中において「−」はタイムアウトを示す。タイムアウトは、９００秒以内に検証が完了しなかったことを示す。
【０１００】
表１及び表２において、fusionとある列は図３Ａに示す第１のモード（ループ逆変換なし）でFUSIONR[P]を適用してループ融合をして検証した結果を示し、rev_fusionとある例は図３Ｂに示す第２のモード（ループ逆変換あり）でFUSIONR[P]を適用してループ融合をして検証した結果を示す。
【０１０１】
表１及び表２におけるLevel0,Level1,Lever2は、FUSIONR[P]によって生成される変数V’,V”のうち冗長な変数を削減する程度を示している。Level0は、変数の削減をしない場合である。Level1は、FUSIONR[P]によって生成される変数V’,V”のうち、ループ融合の対象となるループ文に出現しない変数を削除する場合である。Level2は、Level1の削除に加えて、ループ融合の対象となるループ文に出現する変数であるが、その変数への値の代入が行われないもの（例えば、while (i < n) {sum += 1; i++;}における変数n）について、FUSIONR[P]によって生成される変数n’,n”を削除する場合である。
【０１０２】
実験は、loop01からloop05をオリジナルプログラムとして行った。表１及び表２において、各プログラムの検証時間を上下２段で示した。下段の数字は、ループ融合FUSIONRを行って得られた変換プログラムにおいて、havocステートメントと代入ステートメントとを、可能な範囲でプログラムの後ろ側に移動させ、assumeステートメントを、可能な範囲でプログラムの前側に移動させる処理を施してから検証した場合の結果である。上段の数字は、そのような処理を施さない場合の結果である。
【０１０３】
【表１】
2019113997.tif 000024
【表２】
2019113997.tif 000025
【０１０４】
表１及び表２から明らかなように、ループ融合をしない場合、loop01,loop02,loop03,loop04,loop05の検証はいずれもタイムアウトとなった。これに対して、表１において、ループ融合した場合（fusion）、loop05以外は、タイムアウトせずに検証を行うことができた。ループ逆変換とループ融合とをした場合（rev_fusion）Loop05はタイムアウトせずに検証を行うことができた。したがって、ループ逆変換がループ融合の前処理として有効な場合があることがわかる。
【０１０５】
表２において、ループ融合した場合（fusion）、loop03,loop04,loop05以外は、タイムアウトせずに検証を行うことができた。ループ逆変換とループ融合とをした場合（rev_fusion）Loop05はタイムアウトせずに検証を行うことができた場合があった。このことからも、ループ逆変換がループ融合の前処理として有効な場合があることがわかる。
【０１０６】
なお、表１及び表２において、各プログラムの検証時間を上下２段で示した。下段の数字は、ループ融合FUSIONRを行って得られた変換プログラムにおいて、havocステートメントと代入ステートメントとを、可能な範囲でプログラムの後ろ側に移動させ、assumeステートメントを、可能な範囲でプログラムの前側に移動させる処理を施してから検証した場合の結果である。上段の数字は、このような処理を施さない場合の結果である。表１及び表２によれば、このような処理行うことで、処理を行わない場合に比べて検証が早くなる場合があることがわかる。
【０１０７】
実験の対象としたプログラムloop01からloop05は、次のとおりである。
【数２２】
2019113997.tif 000026
【０１０８】
【数２３】
2019113997.tif 000027
【０１０９】
【数２４】
2019113997.tif 000028
【０１１０】
LooP03_falseは、loop03の２つのループの前にあるassume(n >= 0);が省略されている点以外は、loop03と同じプログラムである。
【０１１１】
【数２５】
2019113997.tif 000029
【０１１２】
【数２６】
2019113997.tif 000030
【符号の説明】
【０１１３】
１０  検証装置
１１  プロセッサ
１２  記憶部
２０  プログラム変換器
２１  ループ融合部
２２  ループ逆変換部
３０  検証器
４０  コンピュータ
５０  検証用コンピュータプログラム
１００  検証対象プログラム（オリジナルプログラム）保存領域
２００  変換プログラム保存領域
【図１Ａ】
2019113997.tif 000031
【図１Ｂ】
2019113997.tif 000032
【図２】
2019113997.tif 000033
【図３Ａ】
2019113997.tif 000034
【図３Ｂ】
2019113997.tif 000035
【図４】
2019113997.tif 000036