POPL ミーティング 6/7 Inside ADL

Presentation on theme: "POPL ミーティング 6/7 Inside ADL"— Presentation transcript:

1 POPL ミーティング 6/7 Inside ADL

2 ADLって何？ ADL: Architecture Description Language
低級言語の意味論を記述するために設計 された言語 修論研究のときに設計しました レジスタ・メモリを扱うことができる Cライクな式の構文を持つ

3 修士論文の概要 低級言語のプログラム検証器を作るための支援をするフレームワークを作成した 共通言語を固定し、その上で検証ロジックを構築
共通言語に対してプログラム変換してから検証 変換器と検証ロジックとは独立 新しいアーキテクチャに対応する際に検証器は 弄らない 検証器を取り替えるときに変換器を弄らない

4 本研究のアイデア (図) 検証器 変換器 検証結果 検証 ロジック 共通言語の意味論 共通言語に 変換された プログラム
低級言語の プログラム 変換器 検証結果 Success /Fail 検証 ロジック 共通言語の意味論

5 問題はどのように解決されるか 言語の意味論の複雑さを削減 システムの移植性の改善 低級言語の記述は変換器の中に収める
言語の記述は一度やってしまえば OK 検証ロジックの実装者は変換器を気にする必要はない システムの移植性の改善 一度検証ロジックを実装すれば、変換器を取り替えて他のアーキテクチャにも対応可 ⇒ 組み合わせの数が減らせる

6 今日のメニュー ADLの設計について プログラム変換器について 型理論・プログラム解析との組み合わせ まとめ

7 今日のメニュー ADLの設計について プログラム変換器について 型理論・プログラム解析との組み合わせ まとめ デザインの着想
構文、意味論の定義 プログラム変換器について 型理論・プログラム解析との組み合わせ まとめ

8 Design Goals 特定のアーキテクチャに依存しない 低級言語に近いレベルの記述 なるべくシンプルな言語構造
種々の低級言語を記述するための言語なので データの幅が 32bit とか 64bit であるとかいう制限は できるだけ排除 低級言語に近いレベルの記述 λ計算のように抽象度の高い記述は変換が手間 レジスタ・メモリに対する操作を明示的に記述できると よいのでは なるべくシンプルな言語構造 基本となる命令数が多いと意味論が複雑化

9 抽象機械の定義 アーキテクチャの記憶域に対応 レジスタ、メモリ プログラムは抽象機械上の操作を記述 ADL 抽象機械 プログラム

10 抽象機械の定義 レジスタ・メモリ 便宜上の目的で一時変数を用意 ADL 抽象機械 … メモリはラベルのつけられたブロックの集合
実際のアーキテクチャには存在しない部分 計算の途中結果を格納し、プログラムを記述しやすくする r1 l1 → <…> l2 → <…> l3 → <…> … x = 1 y = 2 z = &l1 … r2 r3 ADL 抽象機械 …

11 言語の扱う値 整数とポインタがあれば十分 実CPU上のデータには「幅」の概念がある しかし幅は計算を記述する上で障害になる
浮動小数点数などは整数にエンコードできる 実CPU上のデータには「幅」の概念がある 8bitの数(byte)、32bitの数(dword) など 幅によってデータの範囲が制限される しかし幅は計算を記述する上で障害になる 例: 32bit の値と 8bit の値を足すとどうなる？ 普通は 8bit の値を 32bit に coerce するが… MSB を符号として解釈？ それともゼロ拡張？

12 「Value」と「Data」、2 つの世界 記憶域から取り出す・保存するときに「解釈」が はさまると考える
整数全体の集合　 との対応づけ 対応づけはアーキテクチャのパラメータとして与える Data … 記憶領域の上での表現 「幅」の概念を持つ Value … 計算に用いられる値 Dataが「解釈」された値 任意の整数(とかポインタ)を表現可能

13 値の定義 Fat Pointer 3 種類の コンストラクタがそれぞれ対応 a は 1 バイト幅のデータ Value Data

14 junk ─ 不定値 ADL の枠組みで値が定まらないことを表す
メモリのラベルと整数のマッピングが不明なので アセンブリ言語のプログラムでラベル名を用いることに相当 一部のポインタ 演算等で現れる 詳細は割愛

15 言語構文 (1) 左辺値 左辺値 … レジスタ、メモリ [, ] にはさまれている部分はデータ幅の指定
左辺値 … レジスタ、メモリ [, ] にはさまれている部分はデータ幅の指定 レジスタは一部分のデータをとってくることができる メモリに関しては、オフセットは式の部分で計算するのでデータ幅指定のみでよい 注: 一時変数は Value を格納するのでここには含まれない

16 言語構文 (2) 式 ev: Value に評価される式、eb: Bool 式 中置演算子、括弧などによる記述
四則演算、ビット演算 C, Java などと同等の記述力 レジスタ、メモリを参照するとデコードが発生する

17 言語構文 (3) 文 5 種類のコマンドから構成 レジスタ、メモリへの代入時にはエンコードされる
nop, error, 代入, goto(無条件分岐), 条件実行 goto + 条件実行 = 条件分岐 レジスタ、メモリへの代入時にはエンコードされる 変数は Value を保持するのでエンコードは必要ない

18 ADL のプログラム ADL では、プログラムもメモリに格納 命令ポインタ = ラベル名+命令インデクス
メモリブロック ::= コード列 | データ メモリ :: ラベル → メモリブロック ただしプログラムをデータとしていじることはできません 命令ポインタ = ラベル名+命令インデクス 「この命令は何バイト？」と考えることはナンセンス 分岐はブロックの先頭(つまりラベルのある箇所)にのみ可能 この制限により、メモリブロックがCFGの基本ブロックになる …ので、その後の解析が楽になるかと考えている

19 簡単な例 整数を含む連結リストの要素の総和を求める ハコは 4 バイト幅のデータと考えてください r2 1 6 3 1 r1 2 3
start: %r2 = 0; goto &loop; loop: if %r1 = &null then goto &end else nop; %r2 = %r2 + *[4](%r1); %r1 = *[4](%r1 + 4); goto &loop; end: r2 1 6 3 1 r1 2 3 null

20 今日のメニュー ADLの設計について プログラム変換器について 型理論・プログラム解析との組み合わせ まとめ
変換アルゴリズム、テンプレート言語の設計 変換の正しさに関する定義 型理論・プログラム解析との組み合わせ まとめ

21 プログラム変換器 実際の低級言語から ADL に変換 意味論を保つ変換であることが必要
検証したいプログラムは、実際の CPU 上の アセンブリ言語や機械語で書かれている 検証ロジックは ADL の意味論を用いて定義する 意味論を保つ変換であることが必要 そうでなければ検証が意味を為さない 「意味論を保つとは何か」については後ほど定義

22 アセンブリ言語・機械語の 変換アルゴリズム
これらの言語のプログラムは命令の列 算術演算・論理演算 制御構造としては分岐(無条件・条件)があれば十分 ループや関数呼び出しなどは全てこれらで書ける 基本的には命令単位で順次変換すればよい 各命令はコンテクストを持たない 持っているとすればプロセッサの状態(レジスタ・メモリ)のはず

23 テンプレートによる変換ルールの記述 アセンブリ言語の命令 = 種別 + オペランド たとえば mov 命令(データのコピー)
オペランドによってパラメータ化されている たとえば mov 命令(データのコピー) 命令種別 オペランド 変換ルール！ mov D , S　　⇔　　D = S ; mov %r1, %r2 ⇔　　%r1 = %r2; mov %r3, %r5 ⇔　　%r3 = %r5; mov %r2, %r4 ⇔　　%r2 = %r4;

24 テンプレートによる変換ルールの記述 すべての可能性を列挙する手間が省ける オペランド ::= レジスタ | メモリ | 即値
mov D , S　　⇔　　D = S ; すべての可能性を列挙する手間が省ける オペランド ::= レジスタ | メモリ | 即値 ADL の構文の非終端記号で言うと、l か v ⇒ ev(式) にマップすればカバーできる

25 テンプレート言語 ADL の式(ev)を拡張 引数で指定できる箇所を ev に変更 テンプレート引数を許容するように
sizeof 演算子(lvalue のデータ幅を返す)の追加 引数で指定できる箇所を ev に変更 代入の左辺、左辺値のデータサイズ指定

26 テンプレートのインスタンス化 コンテクスト :: 変数 → ev(式) 構文木をほぼそのまま写せばよい
テンプレート変数の部分は「接木」 変数を許すために便宜的に ev を使っている箇所でダウンキャストが必要 左辺値のデータ幅指定 → 整数へ 代入左辺 → 左辺値または一時変数へ ダウンキャストできない場合は、変換が失敗する(エラー)

27 パターンマッチング 使用するテンプレートをどうやって指定する？ ⇒ パターンマッチング パターン言語の文法 を右に示した
Prolog (や O’Caml)にヒント 小さな木のマッチング パターン言語の文法 を右に示した

28 アーキテクチャ記述と 変換アルゴリズム パターン言語と ADL プログラムを関連付け 変換アルゴリズムの概略
命令マッピング パターン { 命令列 } オペランドマッピング パターン = 式 変換アルゴリズムの概略 与えられた項 t をパターンと順にマッチング マッチした場合、変数から項 t への束縛が返るので、 オペランドマッピングを用いて式に変換 変換されたコンテクストを用いてテンプレートコードを インスタンス化

29 アーキテクチャ記述例 (IA-32、抜粋) #operand { eax = %eax; ax = %eax[0,2];
al = %eax[0,1]; ah = %eax[1,1]; ebx = %ebx; ... } mov(D, S) { D = S; add(D, S) { // calculate result D = D + S; // ZF if D : int then if D == 0 then %_zf = 1 else %_zf = 0 else if (D - &null) : int then if (D - &null) == 0 then %_zf = 1 else %_zf = junk; ... } この画面で実際にマッピングを黒板で説明したほうがいいと思う

30 プログラム変換の正しさ プログラム = 機械の状態集合上の関数
変換の正しさ = 実機械状態と ADL 抽象機械の状態の「対応」 が任意のプログラムに関して保存 状態 State 変換元の プログラム 変換後の プログラム 状態’ State’

31 状態の対応関係 レジスタ、 メモリ、 一時変数 レジスタの状態, メモリの中身 変換器(ルール)の実装者が定義
実機械の状態集合が、抽象機械の状態集合に埋め込まれるのがポイント 抽象機械の状態の集合から実機械の状態の集合へ total な surjection が定義できればよい 実機械では値として整数値しか用いないことを考えれば直観的に明らか 変数の生存期間が局所的(ある一命令に対応するコード内で完結している)ならば変数については忘れてよい

32 変換の正しさを検査する 今のところ、変換器の実装者に委ねている (半)自動的に保証することは future work
いくつかの入力例について出力が等しくなることを確かめればある程度の確証を得るのでは？ (半)自動的に保証することは future work パターンが決まっているし、プリミティブなループを含まないので、なんとかならないか？ その前段として、ADL の意味論を定理証明器に載せるべく現在勉強中

33 今日のメニュー ADLの設計について プログラム変換器について 型理論・プログラム解析との組み合わせ まとめ テンプレート言語の問題点
テンプレート言語に対する型判定、型推論 プログラム解析の手法の適用 さらなる応用 まとめ

34 テンプレート言語の問題点 テンプレート変数に予期しない値が入ってくる 不正なテンプレートを書ける ⇒いずれも「変換時に」エラーが発生
これまでの定義では… テンプレート変数に予期しない値が入ってくる 例: mov(D, S) { D = S; } に対して D = 1 などを 与えると… 不正なテンプレートを書ける 例: 引数にない変数を中で参照する可能性 例: 1 = 2; のような式を許容してしまう ⇒いずれも「変換時に」エラーが発生 「変換器をコンパイルする際に」、ではない

35 型理論の手法による解決 型を用いることにより、これらの問題を解決 変数に予期しない値が入ってこないように検査
これは runtime check とほぼ変わらないが 逆に、型推論を行うことで引数にどういった条件が 必要かがわかる 不正なテンプレートを静的にチェックできる ここで言う「静的」とは、変換器のコンパイル時のこと プログラムを実際に与えて変換する時、ではない 何度もコンパイルしてトライ&エラーする手間が省ける

36 型の構造 右図のような subtype relation を満たす型を導入 ADLの構文定義の構造を反映 図では上の方が subtype
int ⇔ n (整数) const ⇔ v (Value) ただし junk を除く lvalue ⇔ l (左辺値) assn ⇔ l | x (変数) assignable の意 * (any) ⇔ ev (式) 図では上の方が subtype * (any) const assn int lvalue

37 型付け規則 型環境 式に対する型付け規則 Γ|- ev :τ

38 型付け規則 Bool 式に対する型付け規則 Γ|-eb : bool 文に対する型付け規則 Γ|- c
ほぼ自明なので割愛します 文に対する型付け規則 Γ|- c コード列に対する型付け規則 Γ|- <c;…> これもほぼ自明なので割愛します

39 型の健全性・完全性 健全性: 型検査に通るテンプレートは(正しい引数が与えられれば)エラーを起こさない
エラーにならない ⇔ ダウンキャストが成功 ダウンキャストが可能な条件を考えれば自明 完全性: 正しいテンプレートは型検査を通る ダウンキャストが成功する場合は、型付け規則 より型が整合的につけられることは明らか case analysis をすればよい

40 型検査の一例 型環境 Γ= D : lvalue, S : * のもとで、文 D = S + 1 を型付け * const assn int

41 型を推論する 型付け規則をそのまま使える (テンプレート)変数の型を全て型変数とおいて 制約を集めて解く 不整合な型が出てきたら推論失敗
関連付けられているパターンに含まれている変数のみ注目 「(変数) 　 (型)」という形の制約だけが出てくる 不整合な型が出てきたら推論失敗 X　 lvalue かつ X　 int、とか reg[sizeof(X), X] のような不正な式を静的に除外

42 さらなる応用 型を細かく定義することにより、細かい言語の制限を記述することが可能 型を用いた constant folding の補助
reg 　 lvalue などとして、レジスタのみを受け 付けるテンプレートを記述することができる 型を用いた constant folding の補助 現在はデータ幅指定の部分に算術式が書けない 変換時に定数になる「式」を書けると便利？ X:int で reg[sizeof(reg) – X, X]、のような用途を想定 型付け規則を拡張してより細かい型付けを行う

43 ほかの問題点 ありえない instantiation がなされる可能性 変数使用の局所性を保証できない
例: 「レジスタのみ受け付ける」などが表現できない ⇒ あり得る組み合わせが全て正しく変換されていれば 問題はないはず 変数使用の局所性を保証できない 同一テンプレートの外で定義されている(一時)変数を 参照していないか 手で確かめるのは容易だが、変数の生存解析により自動で検査できる

44 しかし大きな障害が… 実際のところ、純粋にテンプレート言語だけで書けるアーキテクチャは少ない(or, ない)
call は次命令のアドレスを知らなければできない Delayed branch をする場合、変換途中で後続命令を変換することが必要 対応するために、式の部分を拡張して任意のコードを書けるようにする必要 ⇒ たとえば Java の意味論を知らないと型が求められない?

45 今日のメニュー ADLの設計について プログラム変換器について 型理論・プログラム解析との組み合わせ まとめ

46 まとめ 低級言語の意味論を記述するための言語 ADL の設計について述べた プログラム変換器の実装について述べた
ルールベースの記述 変換ルールに対して型理論やプログラム 解析の手法を応用できることを説明した おかしなテンプレート、instantiation をはじく 細かく型をつけることでいろいろな応用ができそう