抽象的解釈

コンピュータサイエンスにおいて、抽象解釈とは、順序集合、特に格子上の単調関数に基づく、コンピュータプログラムの意味論の健全な近似理論である。これは、すべての計算を実行することなく、その意味論（例えば、制御フロー、データフロー）に関する情報を得るコンピュータプログラムの部分的な実行と見なすことができる。

その主な具体的な応用は、形式的な静的解析、つまりコンピュータ プログラムの実行可能性に関する情報の自動抽出です。このような解析には、主に 2 つの用途があります。

• コンパイラ内部で、プログラムを分析して、特定の最適化または変換が適用可能かどうかを判断します。
• デバッグや、バグのクラスに対するプログラムの認証に使用します。

抽象解釈は、 1970年代後半にフランスのコンピュータ科学者の夫婦、パトリック・クゾーとラディア・クゾーによって形式化されました。 ^{[1] [2]}

直感

このセクションでは、現実世界の非コンピューティングの例を使用して抽象的な解釈を説明します。

会議室にいる人々について考えてみましょう。部屋にいる各人には、アメリカの社会保障番号のように、固有の識別子が割り当てられていると仮定します。誰かが出席していないことを証明するには、その人の社会保障番号がリストに載っていないかどうかを確認するだけで済みます。2人の異なる人が同じ番号を持つことはできないため、番号を調べるだけで、参加者が出席しているかどうかを証明または反証できます。

しかし、出席者の名前のみが登録されている可能性もあります。リストに人の名前が見つからない場合、その人は出席していなかったと結論付けることができます。しかし、見つかった場合は、同音異義語の可能性（たとえば、ジョン・スミスという名前の人が 2 人いる）があるため、さらに調査しなければ確実に結論付けることはできません。同音異義語は実際にはまれであるため、この不正確な情報でもほとんどの場合には十分であることに注意してください。ただし、厳密に言って、誰かが部屋にいたと確実に言うことはできません。おそらくここにいたということしか言えません。検索している人物が犯罪者の場合は警報を発しますが、もちろん誤報を発する可能性もあります。同様の現象はプログラムの解析でも発生します。

例えば「部屋に 歳以上の人がいたか？」といった特定の情報だけを知りたい場合は、全員の名前と生年月日をリストにする必要はありません。参加者の年齢のみをリストに残しておけば、正確さを損なうことなく安全に済みます。もしこれだけでも扱いきれないのであれば、最年少と最年長の人の年齢だけをリストに残してもよいでしょう。質問が 歳以上の年齢よりも厳密に低い、または 歳以上の年齢に関するものであれば、そのような参加者はいなかったと安全に答えることができます。そうでない場合は、「わからない」としか言えないかもしれません。 ${\displaystyle n}$ ${\displaystyle m}$ ${\displaystyle M}$ ${\displaystyle m}$ ${\displaystyle M}$

コンピューティングの場合、具体的かつ正確な情報は、一般的に有限の時間とメモリ内では計算できません（ライスの定理と停止問題を参照）。抽象化は、質問に対する一般化された回答を可能にするために使用されます（例えば、私たち（抽象解釈アルゴリズム）が正確な回答を確実に計算できない場合、はい/いいえの質問に対して「たぶん」と答えて「はいまたはいいえ」を意味する）。これにより問題は単純化され、自動解決が可能になります。重要な要件の一つは、問題が扱いやすくなるように十分な曖昧さを加えつつ、重要な質問（「プログラムはクラッシュする可能性があるか？」など）に答えるのに十分な精度を維持することです。

コンピュータプログラムの抽象的解釈

プログラミング言語または仕様記述言語が与えられた場合、抽象解釈は、抽象化の関係で結びついた複数のセマンティクスを与えることから成ります。セマンティクスとは、プログラムの可能な動作を数学的に特徴づけることです。プログラムの実際の実行を非常に厳密に記述する最も正確なセマンティクスは、具体的セマンティクスと呼ばれます。たとえば、命令型プログラミング言語の具体的セマンティクスでは、各プログラムに、それが生成する可能性のある実行トレースのセットを関連付けることがあります。実行トレースは、プログラム実行の可能な連続した状態のシーケンスです。状態は通常、プログラム カウンタの値とメモリの場所 (グローバル、スタック、ヒープ) で構成されます。次に、より抽象的なセマンティクスが導出されます。たとえば、実行における到達可能な状態のセットのみを考慮することができます (これは、有限のトレースの最後の状態を考慮することに相当します)。

静的解析の目的は、ある時点で計算可能な意味解釈を導き出すことです。例えば、整数変数を操作するプログラムの状態を、変数の実際の値を忘れ、その符号（+、-、または0）のみを保持することで表現することができます。乗算などの基本的な演算では、このような抽象化によって精度が損なわれることはありません。積の符号を得るには、オペランドの符号が分かれば十分です。他の演算では、抽象化によって精度が損なわれる可能性があります。例えば、オペランドがそれぞれ正と負である和の符号を知ることは不可能です。

意味を決定可能にするために、精度を犠牲にする必要がある場合もあります（ライスの定理と停止問題を参照）。一般的に、解析の精度と決定可能性（計算可能性）または扱いやすさ（計算コスト）の間には妥協点があります。

実際には、定義される抽象化は、分析対象となるプログラムの特性と対象プログラム群の両方に合わせて調整されます。抽象解釈を用いたコンピュータプログラムの最初の大規模な自動分析は、 1996年にアリアン5ロケットの初飛行中に発生した事故をきっかけに始まりました^。[3]

形式化

例: 整数集合（赤）から符号集合（緑）への抽象化

を具象集合と呼ばれる順序付き集合とし、を抽象集合と呼ばれる別の順序付き集合とします。これら2つの集合は、要素を一方から他方へ写像する 全関数を定義することで相互に関連しています。${\displaystyle L}$ ${\displaystyle L'}$

関数が具象集合 の要素を抽象集合 の要素に写像する場合、その関数は抽象関数と呼ばれます。つまり、 の要素はの抽象化です。 ${\displaystyle \alpha }$ ${\displaystyle x}$ ${\displaystyle L}$ ${\displaystyle \alpha (x)}$ ${\displaystyle L'}$ ${\displaystyle \alpha (x)}$ ${\displaystyle L'}$ ${\displaystyle x}$ ${\displaystyle L}$

関数が抽象集合 の要素を具象集合 の要素に写像する場合、その関数は具象化関数と呼ばれます。つまり、の要素はの具象化です。 ${\displaystyle \gamma }$ ${\displaystyle x'}$ ${\displaystyle L'}$ ${\displaystyle \gamma (x')}$ ${\displaystyle L}$ ${\displaystyle \gamma (x')}$ ${\displaystyle L}$ ${\displaystyle x'}$ ${\displaystyle L'}$

, , ,を順序付き集合とする。具体的な意味はからへの単調関数である。からへの関数は、内のすべての に対して が成り立つとき、の有効な抽象化であると言われる。 ${\displaystyle L_{1}}$ ${\displaystyle L_{2}}$ ${\displaystyle L'_{1}}$ ${\displaystyle L'_{2}}$ ${\displaystyle f}$ ${\displaystyle L_{1}}$ ${\displaystyle L_{2}}$ ${\displaystyle f'}$ ${\displaystyle L'_{1}}$ ${\displaystyle L'_{2}}$ ${\displaystyle f}$ ${\displaystyle x'}$ ${\displaystyle L'_{1}}$ ${\displaystyle (f\circ \gamma )(x')\leq (\gamma \circ f')(x')}$

プログラムの意味論は、一般的にループや再帰手続きが存在する場合の不動点を用いて記述されます。 が完全格子であり、が からへの単調関数であるとします。すると、のような任意の は、の最小の不動点の抽象化であり、これはクナスター・タルスキー定理によれば存在します。 ${\displaystyle L}$ ${\displaystyle f}$ ${\displaystyle L}$ ${\displaystyle L}$ ${\displaystyle x'}$ ${\displaystyle f(x')\leq x'}$ ${\displaystyle f}$

ここで難しいのは、そのような を得ることです。 が有限の高さであるか、少なくとも昇順連鎖条件（すべての昇順列は最終的に定常である）を証明する場合、次のような帰納法で定義される昇順列の定常極限として、そのような を得ることができます。 （ の最小元）および。 ${\displaystyle x'}$ ${\displaystyle L'}$ ${\displaystyle x'}$ ${\displaystyle x'_{n}}$ ${\displaystyle x'_{0}=\bot }$ ${\displaystyle L'}$ ${\displaystyle x'_{n+1}=f'(x'_{n})}$

他の場合には、 （ペア）拡大演算子[ ^4]を通じてそのような演算子を得ることも可能である。拡大演算子は次の条件を満たす 二項演算子として定義される。${\displaystyle x'}$ ${\displaystyle \nabla \colon L\times L\to L}$

1. すべてのおよびに対して、およびが成り立ち、${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle x\leq x\mathbin {\nabla } y}$ ${\displaystyle y\leq x\mathbin {\nabla } y}$
2. 任意の昇順列 に対して、とで定義される列は最終的に定常となる。したがって、 を取ることができる。${\displaystyle (y'_{n})_{n\geq 0}}$ ${\displaystyle x'_{0}:=\bot }$ ${\displaystyle x'_{n+1}:=x'_{n}\mathbin {\nabla } y'_{n}}$ ${\displaystyle y'_{n}=f'(x'_{n})}$

場合によっては、が から、がからであるガロア接続 を用いて抽象化を定義できます。これは最適な抽象化が存在することを前提としていますが、必ずしもそうではありません。例えば、実数の対の集合を凸多面体で囲むことで抽象化する場合、 で定義される円板 に最適な抽象化は存在しません。 ${\displaystyle (\alpha ,\gamma )}$ ${\displaystyle \alpha }$ ${\displaystyle L}$ ${\displaystyle L'}$ ${\displaystyle \gamma }$ ${\displaystyle L'}$ ${\displaystyle L}$ ${\displaystyle (x,y)}$ ${\displaystyle x^{2}+y^{2}\leq 1}$

抽象ドメインの例

数値抽象領域

与えられたプログラムポイントで利用可能な各変数に区間を割り当てることができます。変数 に値を割り当てる状態は、すべての に対してが成り立つ場合、これらの区間の具体化となります。変数およびの区間 および から、それぞれ（つまり、）および（つまり、 ）の区間を簡単に得ることができます。これらは正確な抽象化であることに注意します。なぜなら、例えば の場合の可能な結果の集合は、まさに区間 だからです。乗算、除算などに対してより複雑な式を導き出すことができ、いわゆる区間演算が生成されます。^[5]${\displaystyle x}$ ${\displaystyle [L_{x},H_{x}]}$ ${\displaystyle v(x)}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle v(x)\in [L_{x},H_{x}]}$ ${\displaystyle [L_{x},H_{x}]}$ ${\displaystyle [L_{y},H_{y}]}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle x+y}$ ${\displaystyle [L_{x}+L_{y},H_{x}+H_{y}]}$ ${\displaystyle x-y}$ ${\displaystyle [L_{x}-H_{y},H_{x}-L_{y}]}$ ${\displaystyle x+y}$ ${\displaystyle [L_{x}+L_{y},H_{x}+H_{y}]}$

ここで、次の非常に単純なプログラムを考えてみましょう。

y = x;
z = x - y ;

適切な算術型の場合、zゼロになるはずです。しかし、区間演算をすると×[0, 1]では、z[−1, +1]の範囲にあります。個々の演算は厳密に抽象化されていますが、それらの合成は抽象化されていません。

問題は明らかです。私たちは、×そしてy; 実際には、この区間領域は変数間の関係を一切考慮しないため、非リレーショナル領域です。非リレーショナル領域は実装が高速かつシンプルですが、不正確になる傾向があります。

リレーショナル数値抽象ドメイン の例は次のとおりです。

• 整数の合同関係^{[6] [7]}
• 凸多面体^[8]（左の図参照） – 計算コストがやや高い
• 差分境界行列^[9]
• 「八角形」^{[10] [11] [12]}
• 線形等式^[13]

およびそれらの組み合わせ（還元生成物など、^[2]右図参照）。

抽象ドメインを選択する場合、通常、きめ細かい関係を維持することと高い計算コストの間でバランスを取る必要があります。

機械語の抽象ドメイン

PythonやHaskellなどの高水準言語ではデフォルトで無制限の整数が使用されるのに対し、 C言語やアセンブリ言語などの低水準プログラミング言語では、通常、有限サイズのマシンワード（機械語）上で動作します。マシンワードは、整数を法とするモジュロ${\textstyle 2^{n}}$ （ここでnはマシンワードのビット幅）を使用してより適切にモデル化されます。このような変数の様々な分析に適した抽象領域がいくつかあります。

ビットフィールドドメインは、マシンワード内の各ビットを個別に扱います。つまり、幅nのワードはn個の抽象値の配列として扱われます。抽象値は集合 から取得され、抽象化関数と具体化関数は次のように与えられます。^{[14] [15]}、、、、、、 。これらの抽象値に対するビット演算は、いくつかの3値論理における対応する論理演算と同一です。^[16]${\textstyle \{0,1,\bot \}}$ ${\displaystyle \gamma (0)=\{0\}}$ ${\displaystyle \gamma (1)=\{1\}}$ ${\displaystyle \gamma (\bot )=\{0,1\}}$ ${\displaystyle \alpha (\{0\})=0}$ ${\displaystyle \alpha (\{1\})=1}$ ${\displaystyle \alpha (\{0,1\})=\bot }$ ${\displaystyle \alpha (\{\})=\bot }$

さらに、符号付き区間領域と符号なし区間領域があります。これら3つの領域はすべて、加算、シフト、排他的論理和、乗算といった一般的な演算のための前方および後方抽象演算子をサポートしています。これらの領域は、簡約積を用いて組み合わせることができます。^[17]

参照

• モデル検査
• シンボリックシミュレーション
• シンボリック実行
• 静的コード解析ツールのリスト- 抽象解釈ベース（健全）とアドホック（不健全）の両方のツールが含まれています
• 静的プログラム解析- 抽象解釈を含むがこれに限定されない解析手法の概要
• インタープリター（コンピューティング）

参考文献

1. Cousot, Patrick; Cousot, Radhia (1977). 「抽象解釈：不動点の構築または近似によるプログラムの静的解析のための統一格子モデル」（PDF） .第4回ACMプログラミング言語原理シンポジウム会議記録、米国カリフォルニア州ロサンゼルス、1977年1月. ACM Press. pp.  238– 252. doi :10.1145/512950.512973. S2CID  207614632.
2. Cousot, Patrick; Cousot, Radhia (1979). 「プログラム分析フレームワークの体系的設計」(PDF) .第6回ACMプログラミング言語原理シンポジウム会議記録, 米国テキサス州サンアントニオ, 1979年1月. ACM Press. pp.  269– 282. doi :10.1145/567752.567778. S2CID  1547466.
3. Faure, Christèle. 「PolySpace Technologies History」 . 2010年10月3日閲覧。
4. Cousot, P.; Cousot, R. (1992年8月). 「ガロア接続と抽象解釈への拡張／縮小アプローチの比較」(PDF) . Bruynooghe, Maurice; Wirsing, Martin (編). Proc. 4th Int. Symp. on Programming Language Implementation and Logic Programming (PLILP) . Lecture Notes in Computer Science. Vol. 631. Springer. pp.  269– 296. ISBN 978-0-387-55844-8。
5. Cousot, Patrick; Cousot, Radhia (1976). 「プログラムの動的特性の静的決定」(PDF) .第2回国際プログラミングシンポジウム議事録. パリ、フランス、デュノ. pp.  106– 130.
6. グレンジャー、フィリップ (1989). 「算術合同式の静的解析」.国際コンピュータ数学ジャーナル. 30 ( 3–4 ): 165–190 . doi :10.1080/00207168908803778.
7. Philippe Granger (1991). 「プログラム変数間の線形合同式静的解析」 Abramsky, S.; Maibaum, TSE (編). Proc. Int. J. Conf. on Theory and Practice of Software Development (TAPSOFT) . Lecture Notes in Computer Science. Vol. 493. Springer. pp.  169– 192.
8. Cousot, Patrick; Halbwachs, Nicolas (1978年1月). 「プログラムの変数間の線形制約の自動検出」(PDF) . Conf. Rec. 5th ACM Symp. on Principles of Programming Languages (POPL) . pp.  84– 97.
9. Miné, Antoine (2001). 「差境界行列に基づく新しい数値抽象領域」. Danvy, Olivier; Filinski, Andrzej (編).プログラム・アズ・データ・オブジェクト, 第2回シンポジウム (PADO) . コンピュータサイエンス講義ノート. 第2053巻. Springer. pp.  155– 172. arXiv : cs/0703073 .
10. ミネ、アントワーヌ (2004 年 12 月)。弱い関係の数値抽象ドメイン(PDF) (博士論文)。国立高等情報研究所。
11. Antoine Miné (2006). 「八角形抽象領域」. Higher Order Symbol. Comput . 19 (1): 31– 100. arXiv : cs/0703084 . doi :10.1007/s10990-006-8609-1.
12. Clarisó, Robert; Cortadella, Jordi (2007). 「八面体抽象ドメイン」.コンピュータプログラミングの科学. 64 : 115–139 . doi :10.1016/j.scico.2006.03.009. hdl : 10609/109823 .
13. Michael Karr (1976). 「プログラム変数間のアフィン関係」. Acta Informatica . 6 (2): 133– 151. doi :10.1007/BF00268497. S2CID  376574.
14. Miné, Antoine (2012年6月). 「ビットレベルマシン整数演算および浮動小数点演算のための抽象領域」. WING'12 - 第4回不変式生成に関する国際ワークショップ. マンチェスター、イギリス: 16.
15. Regehr, John; Duongsaa, Usit (2006年6月). 「組み込みソフトウェア解析のための抽象伝達関数の導出」.組み込みシステムのための言語、コンパイラ、ツールサポートに関する2006年ACM SIGPLAN/SIGBED会議議事録. LCTES '06. ニューヨーク州ニューヨーク: Association for Computing Machinery. pp.  34– 43. doi :10.1145/1134650.1134657. ISBN 978-1-59593-362-1. S2CID  13221224。
16. Reps, T.; Loginov, A.; Sagiv, M. (2002年7月). 「3値命題式の意味的最小化」. Proceedings 17th Annual IEEE Symposium on Logic in Computer Science . pp.  40– 51. doi :10.1109/LICS.2002.1029816. ISBN 0-7695-1483-9. S2CID  8451238。
17. Yoon, Yongho; Lee, Woosuk; Yi, Kwangkeun (2023-06-06). 「反復的な前方後方抽象解釈による帰納的プログラム合成」. Proceedings of the ACM on Programming Languages . 7 (PLDI): 174:1657–174:1681. arXiv : 2304.10768 . doi : 10.1145/3591288 .

外部リンク

• パトリック・クーゾットが管理する抽象解釈に関するウェブページ
• Roberto Bagnara 氏の論文では、C のようなプログラミング言語に抽象解釈ベースの静的解析ツールを実装する方法が示されています。
• 静的解析シンポジウム、Springer LNCSシリーズに掲載されている議事録
• POPL会議に所属する検証、モデル検査、抽象解釈に関する会議（VMCAI）、Springer LNCSシリーズに掲載されている議事録

講義ノート

• 抽象解釈。パトリック・クーゾ。MIT。
• デビッド・シュミットの抽象解釈に関する講義ノート
• モーラーとシュワルツバッハの静的プログラム解析に関する講義ノート
• アゴスティーノ・コルテシのプログラム分析と検証に関する講義ノート
• Grégoire Sutre によるスライドでは、抽象解釈のすべてのステップを多くの例とともに説明し、ガロア接続も紹介しています。