久しぶりの論文メモ。今回はプログラム解析のネタ。2 つのプログラムが機能的に同値であるかどうか判定する技術について。プログラムの静的解析は自分の専門だったので、たまに論文読むと里帰りの気分を味わえる。

タイトル

ARDiff: Scaling Program Equivalence Checking via Iterative Abstraction and Refinement of Common Code

ESEC/FSE 2020

ARDiff: scaling program equivalence checking via iterative abstraction and refinement of common code | Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

概要

記号実行を用いて、2 つのプログラムが機能的に同値（functionally equivalent）であるかを検証する手法を提案。特に、以下のコミット前後のプログラムのように、同一のコードを共有する 2 つのプログラムを対象とすることを想定している。ちなみに、この例ではコミット前後の 2 つのプログラムは同値である。

f:id:t-keita:20210501232200p:plain:w400

背景

2 つのプログラムの同値性を検証する手法として、記号実行（Symbolic Execution）を用いたものが提案されている。

記号実行については過去の以下の記事で解説しています。

t-keita.hatenadiary.jp

記号実行の課題のひとつは、対象のコードにループ文が存在したときに繰り返し回数を特定することが難しく、解析が完全（complete）でなくなることである。たとえば、2 つのプログラムが真に同値であるのに、ループの存在によりそれらが同値であると判定できない場合がある。また、プログラム中に SMT ソルバーで表現できないような非線形な操作が存在する場合には unknown として結果を出すしかない。

プログラムの同値性検証の文脈では、このような記号実行の課題を克服するアプローチとして主に以下の 2 つが研究されてきた。

Differential Symbolic Execution (DSE)
Regression verification using impacted summaries (IMP-S)

本研究では、以下の2つの先行手法の課題を克服する手法を提案する。まずは、これら 2 つのアプローチの概要を述べる。

Differential Symbolic Execution

Differential Symbolic Execution (DSE) は、2 つのプログラムのうち構文的に同一の部分を無視してプログラムを比較するやり方である。上記のプログラムの例であれば、2-9 行目や 13-16 行目を "適当な関数" として置換し、記号実行の対象から除外する。以下のオレンジ色の部分を無視することになる。

f:id:t-keita:20210501234923p:plain:w400

これによって、記号実行が苦手とするループ構造の存在を隠蔽しつつ、明らかに同じ意味をもつプログラムの範囲を同値性検証の対象から除外できる。残りの部分の意味の差だけ検証すればよいわけである。

しかし、プログラムの同値性検証に必要な情報が無視してしまった範囲に含まれている場合がある。上記のプログラムの例では、17 行目の変数 acc の定義 acc = 200; はオレンジ色の部分に含まれており、このままではプログラムが同値であると判定できない。これが DSE の課題である。

プログラムの一部を置き換える "適当な関数" に関しては SMTソルバーの uninterpreted function として表現できる。これは、同じ入力に対して同じ出力を返すことだけ保証された関数である。以下の記事でも紹介した SMTLIBv2 の declare-fun 命令を使えばよい。

t-keita.hatenadiary.jp

Regression verification using impacted summaries

Regression verification using impacted summaries (IMP-S) は、変更前後の 2 つのプログラムのうち、変更の影響を受ける部分のみ記号実行で調べるアプローチである。変更の影響を受けない部分は意味が保たれていることが自明なので、意味的に変化した可能性のある部分だけ調べるというわけである。影響範囲の特定には制御フロー（control flow）やデータフロー（data flow）が考慮される。

一方で、このアプローチでは DSE のように 2 つのプログラムの共通部分かどうかを考慮するわけではないので、そこに記号実行が苦手とする処理が含まれていた場合は SMT ソルバーの出力が unknown になってしまう課題がある。

以上の 2 つのアプローチをまとまると、DSE は同値性検証に必要な情報を無視することによって見逃し（false negative）が発生してしまう。一方で IMP-S は、余計な部分を解析対象に含めてしまうことにより unknown を多く出してしまう。提案手法ではこれらの課題を克服することが狙いである。

提案手法

提案手法の ARDIFF は、同値性を示すために必要な部分を解析対象として残しつつ、SMT ソルバーが苦手とする部分を無視する手法である。具体的には、モデル検査などに用いられる Counterexample-Guided Abstraction Refinement （CEGAR）の枠組みによって、2 つのプログラムの共通部分のうち、同値性を示すのに必要な部分のみを徐々に求めてゆくのが特徴である。

提案手法の概要は以下の通りである。

f:id:t-keita:20210502110629p:plain:w500

手順①の Abstraction では、対象のプログラムの一部を抽象化して無視する。一番最初の段階では、DSE のように 2 つのプログラムに共通する部分をすべて無視する。手順②では記号実行を行う。このとき手順①によって捨て去った部分は uninterpreted function として表現される。そして、手順③のプログラムの同値性判定によって等しいこと（EQ）が検出されるまで、必要に応じて解析対象のプログラムを表現した SMT 式を詳細化してゆく（手順④、⑤）。

手順③の同値性の検証では、 2 つのプログラム $M, M'$ が等しいことの否定形を SMT ソルバーで解く。つまり、制約 $\Phi = \neg(M \Leftrightarrow M')$ を解く。これを満たすインスタンスが存在しないということは、同値性を壊すような入力が存在しないということであり、2 つのプログラム $M, M'$ が同値ということである。一方で、制約を満たすインスタンスが存在するからといって「同値でない」ことが示されるわけではない。というのも、SMT ソルバーは、詳細を無視するために導入した uninterpreted function に対して、真の値と異なる値を割り当てる可能性があるからである。そのため、2 つのプログラムが真に同値な場合でも NEQ になる可能性がある。

提案手法の工夫があるのは手順⑤の Refinement の部分であり、独自のヒューリスティックによって、無視していた部分から同値性を示すために必要な情報を集める。要するに、「無視していたがやっぱり考慮したほうがよさそう」な部分を見つけるためのヒューリスティックである。このヒューリスティックの詳細については論文参照のこと。

評価実験

（論文参照のこと。素朴な既存手法 DSE, IMP-S との比較や、導入したヒューリスティックの性能への貢献度が定量的に示されている。）

所感

2 つの既存アプローチを上手く組み合わせた手法。CEGAR によるアプローチの妥当性にも納得感がある。提案手法ではヒューリスティックな部分が重要な役割を果たしており、特に画期的な何かを提案しているという感じではない。solid work。
そんな手法なのに ESEC/FSE に通るだけあって、論文としてプレゼンテーションが抜群に上手い。読みやすいしストーリーも理解しやすい。こういうイントロを書けるようになりたい。
この論文には書かれていないが、プログラムの同値性の検証は記号実行以外にもアプローチがある。プログラム依存グラフ（Program Dependence Graph, PDG）を比較する古典的なやり方や、2 つのプログラムを 1 つのプログラム内に並べた product program を作って、2 つ範囲が常に同じ出力を生成するかをプログラム検証的に調べるやり方などである。いずれもサポートできる構文要素に限りがあったり、recall が十分に高くない印象である。今後の技術の発展に期待。