int - 米澤研究室

ATTAPL Seminar 10/25
Types for Low-Level Languages (2)
米澤研究室 D1 吉野寿宏
<[email protected]>
前回(4.1～4.2)のおさらい

RISC-like な低級言語 TAL-0 を設計

言語と型システムの定義


mov, add, jump, brz の命令
Control-Flow Safety を満たすことを証明

Progress, Preservation の手法による
今回の概要

TAL-1: Simple Memory Safety (4.3～4.5)




TAL-0 では制御フローの安全性を扱った
TAL-1 ではヒープ・スタック上のデータに関する
安全性を追加
TAL-1 へのコンパイルも考える
その他の言語機構への拡張 (4.6, 4.7)

Object、Closure


Existential Type
Arrays、Arithmetics

Dependent Type の応用
TAL-1:
Simple Memory Safety
TAL-1

データに関するプリミティブサポートを追加

オブジェクトの参照(ポインタ)によるアクセス



ヒープ、スタック
エリアスとの闘い
メモリ安全性を保証する型システムを設計

確保済みのメモリ以外にはアクセスしないこと
型理論的な観点からすると…

データを扱う場合、型の strong update が必要

低級言語では、データの初期化を組み合わせで表現
しなければならない



高級言語では、まとめて初期化するプリミティブを用意できる
レジスタについては TAL-0 で導入済
たとえば以下のようなコードは排除したい
{r1: ptr(code(...))}
r3 := 0;
Mem[r1] := r3;
r4 := Mem[r1];
jump r4

5 行目で r4 == 0 なので control-flow safe でない
型理論的な観点からすると…

しかしエリアシングの問題がある


メモリは 2 箇所以上から同じ場所を参照可能
たとえば次のコードで r1 == r2 だったら？
{r1: ptr(code(...)), r2:...}
r3 := 0;
Mem[r1] := r3;
r4 := Mem[r2];
jump r4


先ほどのスライドと同じ現象になる
しかし r1 と r2 が同じ場所を指していないなら全く
問題はない
エリアスとどう付き合うか

完全なロジックは存在しないが、いくつか静的
解析の理論はある

Alias types


[Smith et al. 2000; Walker et al. 2001; DeLine et al. 2001]
型システムによりリファレンスを追跡
TAL-1 では、ポインタを 2 種類に分類する
アプローチをとる

Shared pointer: エリアスするかもしれないポインタ


型は上書きできない
Unique pointer: エリアスのないポインタ

strong update できるが、ポインタのコピーはできない
TAL-1 Syntax

レジスタ


オペランド



sp (スタックポインタ)レジスタ追加
: コードまたは shared data へのポインタ
uptr(h) : unique data ポインタ
ヒープに割り当てられるオブジェクト

タプル
追加
TAL-1 Syntax

命令セット (追加分)



rd := Mem[rs + n] ロード
Mem[rd + n] := rs ストア
rd := malloc n n ワードを確保


commit rd



割り当てられたポインタは unique pointer になる
shared pointer 化
Unique pointer を shared pointer に coerce
salloc n
sfree n
スタックで n ワード確保
スタックを n ワード解放
TAL-1 Semantics

MOV-1 ルール


MALLOC ルール



RHS が unique pointer でない場合のみ代入を許す
をレジスタに返す
この段階ではまだヒープ(H)は書き換えない
COMMIT ルール


uptr の中身を取り出して H に追加、ラベルを
割り当てる
uptr はスタックにも使われているので、sp レジスタ
はとれない
TAL-1 Semantics

LD-S・LD-U / ST-S・ST-U ルール



ほぼ直感的といえるでしょう
Shared/unique の違いは、ヒープ(H)から取るか
uptr から取り出すかの違い
SALLOC/SFREE ルール


スタックを前のほうに n ワード伸ばす/前から n ワード
切り捨てる
スタック内のオブジェクトへの参照は sp レジスタを
介してのみ可能にするため、uptr を使う
例: malloc を使う

malloc の例: tuple の deep copy
copy:
{r1:ptr(int, int), r2, r3:int}
r2 := malloc 2;
r3 := Mem[r1];
Mem[r2] := r3;
r3 := Mem[r1 + 1];
Mem[r2 + 1] := r3;
commit r2;
{r1: ptr(int,int), r2: ptr(int,int), r3: int}
H
r1
r2
???
r3
int
???
1
???
2
1
2
1
2
Exercise 4.3

4.3.1




push v ≡ salloc 1; Mem[sp] := v
pop rd ≡ rd := Mem[sp]; sfree 1
最適化としては、salloc/sfree をまとめて発行
4.3.2


Semantics の書き換えは straightforward
Unique pointer が share されていないことは、命令
列の長さに関する帰納法で証明可能
TAL-1 Type System

ポインタ型を追加



ptr(σ) : shared pointer type
uptr(σ) : unique pointer type
ヒープ内のデータの型 σ



ε:空
τ : value
σ1,σ2 : 連結


連結は、結合則を満たし ε を単位元とするモノイドになる
⇒ () のつけ・はずしによって変わらない
ρ : allocated type の型変数
TAL-1 Type System
Typing Rules


ヒープ上のデータのルールについては
直観的なので省略
命令列

S-MOV-1 ルール


RHS が uptr 型でないことのチェック追加
S-MALLOC ルール


n ≧ 0 チェック
n 個の int からなる tuple を作成

Semantics での <m1, …, mn> と対応がついている
TAL-1 Type System
Typing Rules

命令列 (cont’d)

S-COMMIT ルール


S-LDS, S-LDU ルール


COMMIT ルールと同様のチェック(sp でないこと)
RHS の型が ptr か uptr かの違い
S-STS, S-STU ルール


S-LDS, S-LDU とほぼ同じ
ただし MOV と同様に、RHS が uptr でないことを
確認する必要がある
TAL-1 Type System
Typing Rules

命令列 (cont’d)

S-SALLOC ルール


スタックの伸張を連結で記述
この型システムではスタックオーバーフローは検出できない


意味論の SALLOC ルールではオーバーフロー防止があった
S-SFREE ルール


先頭 n 要素を削る
オーバーフローとは逆に、アンダーフローは検出
できる

uptr の中身が空になると S-SFREE のルールは失敗
TAL-1 Type System
“Allocated Type Variables”?

メモリのチャンクを変数として扱う



α, β, … といった型変数はワードサイズの値
を表現
Allocated type variables は任意の長さの
データを表現
Allocated type variables は型検査ルール
では消去できない

データ長がわからないので
Exercise 4.4.1
Soundness of TAL-1 Type System

Proof Sketch

Canonical Values, Canonical Operands に
ついて追加された部分を証明




タプルについては長さに関する帰納法で証明
code(Γ), ptr(σ) はに対応
uptr(σ) はヒープにないタプルに対応
その後 TAL-0 と同様の議論を繰り返す

Well-typed になるための条件から、意味論の事前
条件が導出できればよい
Exercise 4.4.1
Soundness of TAL-1 Type System

rd := v; I の場合



commit rd; I の場合




型付け規則の逆と Canonical Values より v = n
または (≠ uptr(h))である
したがって MOV-1 の前提条件が満たされる
(rd) = <...> かつ rd ≠ sp である
したがって COMMIT の事前条件が満たされる
rd := Mem[rs + n]; I の場合
…
Compiling to TAL-1

TAL-1 はコンパイラターゲットとして十分な表現力を
持っている

整数、タプル、レコード、関数ポインタ (closure はまだない)
prod:
int prod(int x, int y)
{
int a = 0;
while(x != 0) {
a = a + y;
x = x – 1;
}
return a;
}
loop:
done:
∀a,b,c,s. {...}
r2 := Mem[sp];
r3 := Mem[sp + 1];
r1 := 0;
jump loop
∀s. {r1,r2,r3: int, sp:uptr(...), ...}
if r2 jump done;
r1 := r1 + r3;
r2 := r2 + (-1);
jump loop
∀s. {r1,r2,r3: int, sp:uptr(...), ...}
sfree 2;
jump r4
Compiling to TAL-1

コーリングシーケンスは以下の通りとする




引数はスタックに積んで渡され、callee が
解放する
戻り先アドレスは r4 に格納されている
関数の返値は r1 に格納される
prod の例でわかるとおり、コードは直観的
Compiling to TAL-1
Type Translation

重要なのは、型がどのように変換されるか
例: prod の型は？
なんでもいい
引数
⇒∀a, b, c, s. code{
r1:a, r2:b, r3:c, sp:uptr(int, int, s),
r4: ∀d, e, f. code{
r1:int, r2:d, r3:e, r4:f, sp:uptr(s)
}
返値
}

Compiling to TAL-1
Type Translation
prod: ∀a, b, c, s. code{
r1:a, r2:b, r3:c, sp:uptr(int, int, s), r4: ∀d, e, f. code{
r1:int, r2:d, r3:e, r4:f, sp:uptr(s)
}
引数なので
}
prod が解放
r1
? int
結果:
r2
?
r3
?
r4
sp
7: int
4: int
?
?
:
コード
s として
抽象化
Compiling to TAL-1
再帰呼び出しの型付け

関数呼び出しの手順



r4、引数をスタックに積み、r4 に戻り先を代入
して関数本体に jump
関数から戻ってきたら r4 を書き戻してスタック
を 1 要素解放
しかしこの呼び出し規約は本質的ではない

例えば戻り先もスタックに積むという方法もとれる
(Exercise 4.5.1)
Exercise 4.5.1

型はひとまず省略
fact:
r1 := Mem[sp];
if r1 jump retn;
r2 := r1 + (-1);
salloc 2
Mem[sp + 1] := cont;
Mem[sp] := r2;
jump fact
cont:
salloc 1;
Mem[sp] := r1;
jump prod // tail call
retn:
r1 := 1;
r4 := Mem[sp + 1];
sfree 2;
jump r4
Exercise 4.5.1

fact の型


∀a,b,c,d,s. code{
r1:a, r2:b, r3:c, r4:d, sp:uptr(int,∀e,f,g. code{
r1:int, r2:e, r3:f, r4:g, sp:uptr(s)
}, s)
}
cont, retn の型


∀b,c,d,s’. code{
r1:int, r2:b, r3:c, r4:d, sp:uptr(int, ∀e,f,g. code{
r1:int, r2:e, r3:f, r4:g, sp:uptr(s’)
}, s’)
}
同じ形になります
Scaling to
Other Language Features
Objects and Closures

Existential Type を導入

∃α.τ … オペランドの抽象化


∃ρ.τ … allocated type の抽象化


S-PACK, S-UNPACK ルール
Operand の existential と同様のルール
α はワードなのに対し、ρ は任意の長さの
タプルを抽象化する、という違い
Objects and Closures
Existential の導入

S-PACK ルール: 型の中の共通している部分
を抽象化する


ptr(code{r1:int, r2:int, ...}, int)
⇒ ∃α.ptr(code{r1:α, r2:int, ...}, α)
S-UNPACK ルール: αが context に存在する
とき ∃ を eliminate する


しかし α は abstract として残される
Context 中の他の型と distinct として扱う
Objects and Closures
オブジェクトの実装
interface Point {
int getX();
int getY();
}
Class C1 implements Point {
int x = 0, y = 0;
int getX() { return x; }
int getY() { return y; }
}
ptr(int,int) → int
Class C2 implements Point {
int x = 0, y = 0, n = 0;
int getX() { n++; return x; }
int getY() { n++; return y; }
}
ptr(int,int,int) → int
Objects and Closures
オブジェクトの実装

getX の型は…？




C1 から ptr(int,int) → int
C2 から ptr(int,int,int) → int
⇒ 左辺を抽象化して∃α. α→int
getY についても同様
したがって Point インターフェイスの型は
∃α.ptr(ptr(α→int, α→int), α)
いわゆる vtable
データフィールド
Objects and Closures
Discussion

Closure はコードポインタと環境を含む
オブジェクトとして実装可能


ML 等の高級言語からコンパイルするときに
必要
もっと実用的に表現するには、再帰型を
導入すればよい[Bruce 1995; 2002]


∃ρ.μα.ptr(ptr(α→int, α→int), ρ)
そのほかにもいくつもの表現手段がある
Objects and Closures
Discussion

再利用可能な型構築子の集合を見つけることが
重要


F-bounded existential など
それによって、多くのオブジェクトモデルを表現できる
ようになる


CLI, JVML はオブジェクトモデルを固定しており、対象とする
以外の言語へのサポートは貧困
しかしダウンキャストは問題になる


動的に型検査を行う必要がある
表現型を応用できる[Crary et al. 1998]が、重い上に
実用的なオブジェクトの表現をサポートしない
配列


TAL-1 では固定長のデータしかとれない
配列をサポートするには？


CISC 風のアプローチ
Dependent Type を用いるアプローチ
[Xi, Harper 2001]
 実際に TALx86 に実装されている
配列
CISC 風アプローチ

CISC 風のアプローチ
≡ プリミティブを増やす



rd := newarray(ri, rs)
rd := ldarr(rs, ri) / starr(rs, rd, ri)
範囲外アクセスをしないようにすることが重要


サイズを最初の要素に持たせたタプルを配列として扱う等
範囲外をアクセスしようとしたら例外ハンドラに飛ばす
配列
CISC 風アプローチ

利点


型システムの設計が単純
欠点



配列のアクセス範囲内チェックを動的にやる
必要がある
サイズが静的に定まる場合でも必ず実行時に
サイズを管理しなければならない
コード最適化との相性が悪い
配列
Dependent Type によるアプローチ

Compile time expression の導入


整数値、算術式(加減算・乗算)、変数から成る
型がこれらの式を含むことを許す

arr(τ, 30+12) ≡ arr(τ, 42)


int(36)


「36」という値を表す型 (singleton integer)
∃i. int(i * 2)


42 要素からなるτ型の配列
偶数
∀i1,i2. code{r1:int(i1), r2:arr(T,i1), r3:int(i2)}


r2 は T 型の配列、r1 はその要素数を格納
r3 はまた別の整数
配列
Dependent Type によるアプローチ

算術式から変数の間の大小関係を静的に
求めれば配列の境界チェックを消せる
sub:
if
rt
if
rd


…
r3
:=
rt
:=
< 0 jump L;
r3 - r1;
>= 0 jump L;
ldarr(r2, r3)
範囲チェック済み
なので ldarr での
検査は必要ない
教科書のコードにはミスあり (3行目 RHS)
コンテクストに変数の制約を追加して計算

if 文で分岐しない場合の条件を求める
配列
Dependent Type によるアプローチ

どういった制約がかけるか？

DTAL では型付けを decidable にするために
制約は linear なものに限られている


配列くらいならばこれでなんとかなる
実際にはコード生成側が proof をつければ
任意の制約を扱える


Proof-Carrying Code Framework を作れる
型システムの設計者側で、sound な inference
rule のみ受け付けるようにする必要は残る
Exercise 4.6.1

意味論

例外ルール
Exercise 4.6.1

型システム


τに arr(τ) を追加
型付け規則

境界チェックは例外生成
Some Real World Issues

メモリ領域に対して読み込み・書き込みの
アクセス制限をかける


領域の型に対してフラグをつけることで可能
Subtyping の追加



σの連結に関する subtyping
rw-access <: ro-access, wo-access
...
Some Real World Issues

スタックの型を拡張する

中を指すポインタを作れるようにする



Intersection type の応用


TALT [Crary, 2003]
free 命令の追加


Nested procedure にも対応できる
STAL [Morrisett et al. 2002]
ヒープオブジェクトの解放
Capability types

Region のサポートを追加することができる
[Walker et al. 2000]
Some Real World Issues

これらの拡張は型システムの肥大化を招く

健全性の証明を手でやるのは非常に大変

定理証明系の応用



TALT [Crary 2003]
Coq を利用した例 [Hamid et al. 2002]
もうひとつのアプローチとして「Foundational
×××」の世界がある[Appel, Felty 2000]

高階論理を用いて型をつくる
4 章まとめ
まとめ

低級言語のための型システムは面白い

型情報を生成・処理するのが機械のため、
人的要因をある程度排除できる



高級言語の設計においてはこのあたりが心配
もちろん型システム自体の健全性は(定理証明系
などによって)証明しておくべき
メモリ操作のための型システムなどは高級
言語では必要ない

Download Report