依存型で型付けされた 副作用のある関数のための 型保存コンパイラ 渡邊 裕貴 コンピュータ科学専攻 米澤研究室

そのコンパイラ、バグってない? 足し算をするプログラムをコンパイルしたら引き算をするアセンブリが出てきた 最適化をかけたら プログラムの動作がおかしくなった

コンパイラの検証 ソースの 意味論 ソース コード 意味論が 一致することを 証明 構文の変換 アセンブリの 意味論 アセンブリ コード

既存研究 Lambda Tamer CompCert … 意味論を扱う証明はとても複雑になりがち A. Chlipala in PLDI 2007 単純型付きラムダ計算のコンパイラの作成・検証 http://ltamer.sourceforge.net/ CompCert X. Leroy in POPL 2006 S. Blazy et al. in FM 2006 C のサブセットから PowerPC アセンブリへのコンパイラの作成・検証 http://compcert.inria.fr/ … 意味論を扱う証明はとても複雑になりがち

本研究のアプローチ コードの挙動を 規定できる型 型保存 コンパイル 挙動 = 意味論

コードの挙動を規定できる型 関数の持つ副作用を表す論理式を 型の中に書く コードの挙動を型でチェック Hoare Type Theory A. Nanevski et al. in ICFP 2006 依存型 R. Burstall and B. Lampson 1984 Separation logic J.C. Reynolds in LICS 2002

コードの挙動を規定できる型の例 コード: λp. v = *p; *p = v + 1; return v 型: Πp:ptr. { ∃x:int. p ↦ x } v:int { p ↦ v ⊸ p ↦ v + 1 } 本研究では簡単な整数演算とメモリの読み書きができる言語を対象とする

型保存コンパイル 型およびその導出木も変換する G. Morrisett et al. 1999 ソース コード 型 型導出木 アセンブリ コード 型 型導出木

本研究での型保存コンパイル 型に含まれる論理式が意味論の一致を保証 ソース コード 型 型導出木 アセンブリ コード 型 型導出木 意味論

実装法 コンパイラは Coq を使って書く 型保存性を Coq で証明 書いた証明が正しいか検証するプログラム http://coq.inria.fr/ 型保存性を Coq で証明

実装の進捗 CPS 変換 クロージャ変換: 未着手 Hoisting: 未着手 レジスタ割当: 未着手 単純型付きラムダ計算: 実装済 依存型: 実装中 Separation logic: 未着手 クロージャ変換: 未着手 Hoisting: 未着手 レジスタ割当: 未着手

まとめ: 型保存コンパイラの作成 目的 手法 進捗 コンパイルの過程でコードの挙動が変わっていないことを保証 意味論の保存の証明をより簡単に コードの挙動を規定できる型 型保存コンパイル 進捗 最初の CPS 変換の部分を実装中

コンパイラの構成 CPS 変換 クロージャ変換 Hoisting レジスタ割当 ソース コード 型 型導出木 アセンブリ コード 型

依存型 コードの挙動を型で規定するための基礎 型の中に論理式を書けるようにする R. Burstall and B. Lampson 1984 型の中に論理式を書けるようにする 恒等関数のコード: λx. x 恒等関数の型: Πx:int. { true } v:int { x = v }

Separation Logic メモリの読み書きに関する挙動を規定 メモリ状態を表す論理式を導入 J.C. Reynolds in LICS 2002 メモリ状態を表す論理式を導入 { true } p1 = malloc(); *p1 = 3; { p1 ↦ 3 } p2 = malloc(); *p2 = 5; { p1 ↦ 3 * p2 ↦ 5 } incr p1; { p1 ↦ 4 * p2 ↦ 5 } incr p2; { p1 ↦ 4 * p2 ↦ 6 } J.C. Reynolds. “Separation logic: a logic for shared mutable data structures.” LICS 2002.

Hoare Type Theory 型付きラムダ計算 + メモリの読み書き 関数の挙動を型の中の論理式で表し検証 A. Nanevski et al. in ICFP 2006 関数の挙動を型の中の論理式で表し検証 依存型 + separation logic インクリメント関数のコード: λp. do v = *p; *p = v + 1; return () インクリメント関数の型: Πp:nat. ∀v:nat. { p ↦nat v } r:unit { p ↦nat v + 1 }

既存研究との比較 本研究 Lambda Tamer CompCert ラムダ計算 + メモリ操作 単純型付きラムダ計算 C のサブセット 仮想アセンブリ PowerPC アセンブリ Coq で証明 型安全 非型安全 型で意味論を規定 型と意味論は無関係

ソースの定義 (仮) t ::= x t t λx. t zero succ t t + t do E 副作用のない項 t ::= x t t λx. t zero succ t t + t do E 副作用のある文 E ::= return t x = eval t; E x = malloc; E x = *t; E *t = t; E 項の型 T ::= nat Πx:T. T {P} x:T {P}

アセンブリの定義 (仮) 命令 I ::= jump v if r jump v move r v add r v v load r r store r r 値 v ::= r レジスタ n 整数リテラル l ラベル 命令の型 T ::= α 型変数 ∀α. T int { rn : Tn | P }

Theorem cps_preserves_typing' : forall (C : sctxt) (t : sterm) (T : stype), C |-s t : T -> forall (C' : cctxt), cctxt_sctxt C C' (vars_in_sterm t) -> forall (t' : cterm), C' |-c t' : cps_type T --> ctbottom -> C' |-c cps t t' : ctbottom. Proof. intros until t; revert C. induction t as [ x | v IH | t1 IH1 t2 IH2 t3 IH3 | t1 IH1 t2 IH2 | b | x t1 IH ] using sterm_ind' with (P2 := fun v => forall (C : sctxt) (T : stype), C |-sv v : T -> cctxt_sctxt C C' (vars_in_sterm v) -> C' |-cv cps_value v : cps_type T). (* case stref *) intros C T H1 C' H2 t' H3. inversion_clear H1 as [ C'' x' T' H' | | | ]. apply (cttapp _ _ _ (cps_type T) _ H3); apply cttref. apply H2. left; reflexivity. assumption.