RustとZ3を用いたループフリープログラムの合成 (2020年)

プログラムが与えられた仕様を実装するプログラムを自動的に見つけることをプログラム合成と呼びます。主な困難は、探索空間が非常に大きいことです。サイズnのプログラムの数は指数関数的に増加します。サイズnのプログラムをすべて単純に列挙し、それぞれが仕様を満たすかチェックし、次にサイズn+1のプログラムへと進むという方法はスケールしません。しかし、この分野は、よりスマートな探索技術を使用して探索空間を削減し、SMTソルバーのパフォーマンス向上を活用し、時には問題の範囲を限定することによって進歩してきました。本稿では、現代のプログラム合成のアプローチの1つである、Gulwaniらによる「Synthesis of Loop-Free Programs」で説明されている、コンポーネントベースのループフリープログラムの反例誘導型反復合成について説明します。これらの用語がそれぞれ何を意味するのかを詳しく分析し、Z3ソルバーを使用したRustで書かれた実装例も紹介します。本稿の目的は2つあります。プログラム合成に馴染みのない方々（私もそうでしたが）が、このトピックについて少しでも理解を深め、新しいことを学んでくれることを願っています。多くの例を提供し、論文の密な論理式を小さく、取り組みやすい断片に分解するように努めました。この種のプログラム合成に既に馴染みのある方々が、私が文献で報告されている合成結果を再現できていない実装のパフォーマンス問題の診断に役立ってくれることを願っています。より難しいベンチマーク問題の中には、私の忍耐力が尽きる前に、シンセサイザーが解を見つけることさえ失敗するものがあります。 目次 モチベーション タスクの概要 問題の形式化 SMTソルバーの簡単な紹介 反例誘導型反復合成 コンポーネントを用いたCEGIS コンポーネントベースのプログラムの検証 コンポーネントベースのプログラムの有限合成 実装 プログラム表現 プログラムの構築 コンポーネントの定義 仕様 シンセサイザー 位置マッピング 検証 有限合成 CEGISループ 結果 結論 参考文献 モチベーション なぜ自分で書くのが面倒だからといって、他のプログラムを書くプログラムを書くのでしょうか？単に私が怠惰だからでしょうか？もちろんそうです。しかし、私ほど怠惰ではない人がプログラム合成を利用したいと思うには、多くの正当な理由があります。一部のプログラムは手書きで正確に書くのが非常に難しく、プログラムシンセサイザーがあなたや私では失敗するような場所で成功するかもしれません。速く！3つのビット操作命令だけを使って、単語の最も右にあるゼロビットを分離するにはどうすればよいでしょうか？！ ,--- 最も右のゼロビット。 | V 入力: 011010011 出力: 000000100 ^ | '--- そのビットだけがセットされています。 もう見つけましたか？…さて、答えはこちらです：isolate_rightmost_zero_bit(x): // x = 011010011 a ← not x // a = 100101100 b ← add 1, x // b = 011010100 c ← and a, b // c = 000000100 return c 私たちのプログラムシンセサイザーは、1秒未満で解を見つけ、最小長の解を約1分で見つけます。私が手で同じことをするのに、それよりもずっと時間がかかるでしょう。この問題は、記事の残りの部分で繰り返し取り上げ、実行例として使用します。 プログラムシンセサイザーを使用するもう1つの理由は、手で書く時間よりもはるかに多くのプログラムを書く必要がある場合です。例えば、コンパイラのピープホールオプティマイザを考えてみましょう。これは、命令シーケンスのスライディングウィンドウを考慮し、各シーケンスについて、同等のしかしより高速または小さい命令シーケンスを知っているかどうかをチェックします。より良い命令シーケンスを知っている場合、元の命令をより良いものに置き換えます。ピープホールオプティマイザは通常、最適化されていない命令シーケンスを、それらを置き換える改善された命令シーケンスとペアにしたパターンマッチングルールから構築されます。 新しい PeepholeOptimizer( pattern0 → replacement0 pattern1 → replacement1 pattern2 → replacement2 // ... patternn → replacementn ) 各 replacementi は、小さく最適化されたミニプログラムです。もし私たちがゼロから手で新しいピープホールオプティマイザを書くとしたら、n個の最適化されたミニプログラムを自分で書く必要があります。そして、nは大きくなる可能性があります。LLVMのInstCombineピープホールオプティマイザには、1,000を超えるパターンと置換のペアがあります。その半数でも、私が自分で書きたいと思う量よりずっと多いです。 これらの最適化されたミニプログラムを手書きする代わりに、各元の命令シーケンスを仕様として使用し、プログラムシンセサイザーにフィードして、同じことを行う最適な命令シーケンスを見つけられるかどうかを確認できます。さらに、これらの元の命令シーケンスとそれらに対応する合成された最適な命令シーケンスをすべて、パターンと置換のペアとして使用して、ピープホールオプティマイザを自動的に構築できます！このアイデアは、Bansalらによって「Automatic Generation of Peephole Superoptimizers」で最初に提案されました。編集：John Regehrは、このアイデアがBansalらの論文が発表された2006年よりもはるかに前から存在していたと指摘しました。彼は、Davidsonらによる1980年の「The Design and Application of a Retargetable Peephole Optimizer」を例として挙げましたが、これも初めて登場したわけではないと注意しました。 タスクの概要 プログラム合成とは、仕様を受け取り、それを満たすプログラムを自動的に見つける行為です。問題をより扱いやすくするために、2つの方法で範囲を限定しています。 ループフリー：ループのないプログラムのみを合成します。 コンポーネントベース：与えられたコンポーネントライブラリの構成として表現できるプログラムのみを合成します。 ループフリーという制限は、多くのユースケースではそれほど制限的ではありません。例えば、ピープホールオプティマイザは、ループ境界をまたぐ命令シーケンスを考慮しないことがよくあります。コンポーネントベースの合成とは、ターゲット言語の任意の数の式を任意の組み合わせで使用するプログラムを合成するのではなく、シンセサイザーにコンポーネントライブラリが与えられ、それらの各コンポーネントを正確に1回だけ使用するプログラムを合成することを意味します。シンセサイザーは、仕様を満たす構成を見つけるまで、コンポーネントを並べ替え、入出力を配線し直します。つまり、N個のコンポーネントのライブラリが与えられた場合、それは次のような形式のプログラムを構築します。 synthesized_program(inputs...): temp0 ← component0(params0...) temp1 ← component1(params1...) // ... tempN-1 ← componentN-1(paramsN-1...) return tempN-1 ここで、paramsi の各パラメータは、プログラムの早い段階で定義された tempj 変数か、元の入力のいずれかです。例えば、2つのコンポーネント f(a) と g(a, b) および入力パラメータ x が与えられた場合、シンセサイザーは次のいずれかの候補プログラムを構築できます（暗黙的に最後に定義された変数を返します）。 a ← g(x, x) b ← f(x) または a ← g(x, x) b ← f(a) または a ← f(x) b ← g(x, x) または a ← f(x) b ← g(a, x) または a ← f(x) b ← g(x, a) または a ← f(x) b ← g(a, a) それだけです。これら2つのコンポーネントだけを与えられた場合に構築できるプログラムはすべてです。シンセサイザーは、すべてのコンポーネントを使用しないため、次のプログラムを構築できません。 a ← f(x) そして、シンセサイザーは、fコンポーネントを複数回使用するため、次のプログラムを構築できません。 a ← f(x) b ← f(a) c ← g(b, b) そして最後に、この最後のプログラムは、ライブラリにない関数hを使用するため、構築できません。 a ← f(x) b ← h(a, x) 以下の表は、完全に一般的なプログラム合成と比較して、コンポーネントベースの合成のプロパティのいくつかを説明しています。 一般合成 | コンポーネントベース合成 合成されるプログラムの形状 | ターゲット言語の任意の式の任意の数を使用 | ライブラリのコンポーネントのみを使用 合成されるプログラムのサイズ | 可変 | 各コンポーネントが正確に1回使用されるため、ライブラリのサイズと等しい 私たちのシンセサイザーでは、コンポーネントは固定ビット幅整数（SMTソルバーの用語では「ビットベクトル」とも呼ばれます）上の関数であり、仮想命令セットの単一命令に対応します。