型推論によるバイトコードベリファイア 24

本章では型推論アルゴリズムを構築する。

バイトコードベリファイアは型システムにおける型チェックに相当する。前章で定義した型システムに よってプログラムの型チェックを行なう場合、次の２点を考慮する必要がある。

• ブロックは一つの型しか持てない

前章で定義した型システムは単相型システムであり,多相型を扱う機構が存在しない.これはサブルー チンの任意の場所から呼び出すことができるという多相的な性質に反する.

• ブロックの型付け規則は他のブロックの型を参照する

このため, ブロックの型チェックを行なうためにはあらかじめそれが参照するラベルの型を推論して おく必要がある.

サブルーチンの多相型を表現するため、JVMのメソッドをMLにおける多相的let式によく似た項とみな して拡張する。この拡張の下ではJVMのバイトコードベリファイアのアルゴリズムは型推論アルゴリズム として記述することが可能になる.

5.1 ^{多相型システム}

定義した型システムでは, サブルーチンはαl//Γ,∆τの形をした唯一の型を持つ.つまり,サブルー チンの呼び出し時のローカル変数およびスタックの状態は必ずそれぞれΓ, ∆を満たさなければならない.

これは, [9]がサブルーチンは内部で使用しないローカル変数については多相的であると指摘したように,サ ブルーチンの持つ多相性に反する. この制限を取り除き,サブルーチンに多相性をもたせるため, 型変数t, ローカル環境変数γ,スタック変数δを導入して,型, ローカル環境,スタック環境を次のように拡張する

τ ::=t| int|void|c| αl | Γ ::=φ|γ |τ·Γ ∆ ::=φ|δ|τ·∆

この拡張の下では,例えば,与えられたスタックの先頭の要素を取り除くサブルーチン,およびスタックの先 頭の整数の和を求めるサブルーチンの型は次のように与えられる.

(αl=γ, δtin α_l//γ, t·δt) (αl=γ,int·δtin αl//γ,int·int·δt)

これによりサブルーチンを多相型として表現することができるが, JVMでは継承の概念があるために型変 数が持つことのできる型は暗黙的に制約を受けることになる. この制約を表現するために型変数の境界環境 Kを導入する. Kは型変数tからその境界への関数であり,型変数がその境界のサブクラス以外の型は持て ないことを意味する. 境界はクラス名あるいは∗のどちらかであり, ∗はその型変数がなんら制約を受けな いことを表す. この定義の下τがKの下cのサブクラスであることをK τ <:cと書く.

この多相型をもつサブルーチンを型システムに取り込むためにサブルーチンをブロックによって使用さ れる相互に再帰的な関数とみなし,JVM-のプログラム{l¹_b :B1,· · ·, lⁿ_b :Bn | l_s¹:SB1,· · ·, l_s^m:SBm}を次 のように考える.

letrec l¹_s=SB1. . . and l^m_s =SBm in in rec l¹_b =B1. . . and lⁿ_b =Bn end

ここでletrecは多相的let束縛を表し, recは単相的な再帰束縛を表す.この考えの下, メソッドM は M^b ={l_b¹=B1,· · ·, lⁿ_b =Bn}およびM^s={l¹_s:SB1,· · ·, l^m_s :SBm} からなるラムダ計算におけるlet式 に似た項

let M^sin M^b

とみなすことが出来る.この改良に伴い, ラベル環境Lをサブルーチンラベル環境L_sおよびブロックラベ ル環境Lbに分割する. 多相型を持つサブルーチンをブロックから使用するためには,サブルーチンの型を その使用に応じて具体的な型に変換する必要がある. Aが多相型を持つBの型変数に型を代入して得られ る単相型であるとき,AはBの例と呼びA≤Bと書く.またサブルーチン型をσとするとき,σ内の全ての 型変数を∀記号によって限量化することをCls(K, σ)と書く.このとき, 型変数はKが示す境界付きで限量 化されることに注意する.例えばK={t→c}ならば,

Cls(K,α_l//t·γ, α_l·δint) =∀t <:c.∀γ.∀δ.α_l//t·γ, α_l·δint)

以上のJVM-の構文上の拡張により,前章で定義したブロックの型付け規則は全て境界環境Kの下で定義さ

れる.例えばL Γ,∆B:τ なる型判定はK,L Γ,∆B:τとなる. 変更される規則はサブクラス関係 を制約に持つinvoke,putfield, getfieldおよび, サブルーチン呼び出しを行なうjsrのみである. これ らの改良された型付け規則を図5.1に示す.同様の変更はサブルーチンの型付け規則に対しても行なわれる.

L Γ,Θ.c.fields.f·∆B:τ

L Γ, c0·∆getfield(c, f)·B:τ (ifK c0<:c) L Γ,∆B:τ

L Γ, τ0·c0·∆putfield(c, f)·B :τ (ifK c0<:c ∧ K τ0<: Θ.c.fields.f) K,L Γ, τ0·∆B:τ Θ.c1.methods.m={τ₁,· · ·, τ_n}=⇒τ0, τ0=void

K,L Γ, τn· · · · ·τ₁·τ₀·∆invoke(c0, m)·B :τ (ifK τ0<:c0 ∧ K τi<:τ_i for all 1≤i≤n)

K,L Γ,∆B:τ Θ.c1.methods.m={τ₁,· · ·, τ_n}=⇒void K,L Γ, τn· · · · ·τ1·τ0·∆invoke(c0, m)·B:τ (ifK τ0<:c0 ∧ K τi<:τ_i for all 1≤i≤n)

L Γ₁,∆₁jsr(l1, l2):τ

(ifL(l1)≤(αl1= Γ₁,∆₂τ in α_l1//Γ₁, αl1·∆₁τ) ∧ L(l2) = Γ₁,∆₂τ) 図5.1: 拡張された型付け規則

以上の定義を元に,メソッドM に対する型付け規則は次のように改良される.

K M^s:L^s Cls(K,L^s)M^b:L^b K let M^sin M^b:L^b

ここで,Cls(K,L^s)は{l:Cls(K,L^s(l))|l∈dom(L^s)}を表し, K,L^sM^b:L^bは以下のように定義さ れる.

K,L^sM^b:L^b⇐⇒ dom(M^b) =dom(L^b) and

for anyl∈dom(M^b),L^s∪ L^bΓ,∆_l, M{M(l)}τl

5.2 型推論アルゴリズム

前節で拡張したメソッドの型付け規則はラムダ式における多相的let式に対する型付け規則と同じ形をし いるため,同様の手法によってメソッドの型推論アルゴリズムを構築することができる. すなわち,

1. サブルーチンラベル環境を推論して記録する.

2. ブロックラベル環境を推論する.ブロックからサブルーチンラベルを参照するときは,先に得られたサ ブルーチンラベル環境から該当するサブルーチンをインスタンス化して使用する.

5.2.1 単一化アルゴリズム

一般に,型推論アルゴリズムは単一化アルゴリズムを基礎とする. JVMの場合,型変数は境界条件を持つ ためにその単一化アルゴリズムは型変数環境Kの下で定義される.Unifyを単一化アルゴリズムとすると, Unifyは型の組からなる集合Eと型変数環境Kを受け取り,Eの単一化である代入Sを返す.このとき,任 意のt∈dom(K)についてK S(t)<:K(t)を満たさなければならない. 以上の考えより,Unifyは[3]を 拡張して下の変形規則により定義される.

1. (E∪ {(τ, τ)}, S,K) =⇒(E, S,K)

2. (E∪ {(t, c)}, S,K) =⇒([c/t]E,{(t, c)∪[c/t]S,K) (ifc <:K(t) orK(t) =∗) 3. (E∪ {(t1, t2)}, S,K) =⇒

([t2/t1]E,{(t1, t2)∪[t2/t1]S,K) (ifK(t1) =∗orK(t2)<:K(t1)) ([t1/t2]E,{(t2, t1)∪[t1/t2]S,K) (ifK(t2) =∗orK(t1)<:K(t2)) 4. (E∪ {(t, τ)}, S,K) =⇒([τ /t]E,{(t, τ)∪[τ /t]S,K) (ifK(t) =∗)

この変形規則からUnifyは以下の関数として定義できる.

Unify(E,K) =

S ((E, φ,K) =⇒^∗ (φ, S,K)のとき) failure (それ以外)

ここで, 関係=⇒^∗は関係=⇒の反射的推移的閉包である. さらに,JVM-ではローカル変数およびスタック に関しても型変数が存在するため,Unifyはこれらに対しても拡張されるものとする. 例えば,K(t) =∗な らば,int·c·φとt·δの二つのスタックを単一化すると, [int/t]および[c·φ/δ]なる代入が得られる.

5.2.2 メソッドの型推論アルゴリズム WJ

図5.2にメソッドの型推論アルゴリズムWJ を示す. WJ は次のようなアルゴリズムである.

1. 型変数から構成されるサブルーチンラベルの骨格Lsを生成する.

2. サブルーチンラベル環境の型推論アルゴリズムWSを使って,Lsの代入関数を得る.

3. ブロックラベル環境の骨格Lを作成する.このとき,エントリーブロックはΘで示されるメソッドの 型で初期化しておく.

ht

WJ({l₁^s=SB1(entry1), . . . , l_k^s=SBk(entryk);l^b₁=B1, . . . , l_n^b =Bn}) letK=φ

Si = (αentryi =t¹_i1·. . .·t¹_imax·φ;δ¹_i t inαentryi//t²_i1·. . .·t²_imax·φ;δ_i²t) (1≤i≤k)

K=K{t¹_i1 → ∗,· · ·, t¹_imax→ ∗, t²_i1→ ∗,· · ·, t²_imax→ ∗, t→ ∗} (1≤i≤k) L={l₁^s=S1, . . . , l^s_k=Sk}

S0 = the empty substitution

Si =(WS(Si−1(L), Si−1(Si), SBi))◦Si−1 (1≤i≤k) (*サブルーチンラベル環境の推論*) B_entry =τ1·. . .·τ_n·_n+1·. . .·_imax·φ;φt0

(where Θ.c.methods.lentry={τ1, . . ., τn} ⇒τ0) B_i =t¹_i1·. . .·t¹_imax·φ;δ_i¹ti (1≤i≤n)

K=K{ti1 → ∗,· · ·, timax→ ∗, t→ ∗, t0→τ0} (1≤i≤n) L={l^s₁=Cls(K, Sk(S1)), . . . , l_k^s=Cls(K, Sk(Sk));

lentry=B_entry, l^b₁=B₁, . . ., l^b_n=B_n} S₀ = the empty substitution

S_i = (WB(S_i−1 (L), S_i−1 (B_i), Bi))◦S_i−1 (1≤i≤k) (*ブロックラベル環境の推論*) in S_n(L)

図5.2: 型推論アルゴリズムWJ

4. 推論されたLsの下,ブロックラベル環境の型推論アルゴリズムWBによってラベル環境Lbの代入関 数Sを得る.

5. SにL_bを適用することで推論されたラベル環境を得る.

ここでimaxはメソッドで使用されるローカル変数の数を表す.また型変数環境Kはグローバルな環境と し,このアルゴリズムを通して連続的にアクセスができるものとする.

5.2.3 ラベル環境の型推論アルゴリズム WS, WB

一般にプログラムの型推論は,プログラムを構成する個々のプログラムの型を推論し,その型の間の制約 を方程式として記述してそれを単一化アルゴリズムによって求めることによって行なわれる. 同様の考えの 下,ブロックの型推論は図5.3に示すように,

1. ブロックを構成するコード列Aを先頭の命令Iと残りのコード列Bに分割する.

2. Bの型推論を行ない,推論された型とIの間の制約条件を記述しそれを単一化アルゴリズムで求める がその基本的なアルゴリズムである.これは再帰関数によって容易に実現できる. 図5.4,図5.5にサブルー チンブロックおよびベーシックブロックの推論アルゴリズムWS, WBの一部を示す. WSおよびWBは ラベル環境,ブロックの型判定,ブロックのコード列を受け取り, 型変数の代入関数を返す.

return iadd

return A iadd

B I

unification algorithm

infered typing of B

infered typing of A constraints

図 5.3: ブロックの型推論 WS(L,(αl= Γ₁; ∆₁τ in α_l//Γ₂; ∆₂τ),ret(i))

=Unify{(Γ₂(i), αl),(Γ₁,Γ₂),(∆₁,∆₂)}

WS(L,αl//Γ₁; ∆₁τΓ₂; ∆₂τ ,aload(i)·SB) =

letK=K{t→Object}(* any class is a subclass ofObjectclass*) S1 =Unify{(Γ₂(i), t)}

S2 =WS(S1(L), S1(α_l//Γ₁; ∆₁τΓ₂;t·∆₂τ), SB) in S2◦S1

WS(L,α_l//Γ₁; ∆₁τΓ₂; ∆₂τ ,goto l·SB) = let (α_l//αlΓ₂; ∆₂τ) =L(l)

in ifl=l thenUnify{(Γ₂,Γ₂),(∆₂,∆₂)} elsefailure

図5.4: サブルーチンラベル環境の型推論アルゴリズム WB(L,Γ; ∆τ,ireturn) =Unify{(∆,int·δ),(τ,int)}

WB(L,Γ; ∆τ,goto l) = let Γ; ∆τ =L(l)

in Unify{(Γ,Γ),(∆,∆),(τ, τ)} WB(L,Γ; ∆τ,jsr(l1, l2)) =

let (αl1 = Γ₁; ∆₁τ1 inαl1//Γ₂; ∆₂τ2) =F reshInst(L(l1)) Γ; ∆τ=L(l2)

in Unify{(Γ,Γ₂),(αl1·∆,∆₂),(Γ,Γ₁),(∆,∆₁),(τ, τ2),(τ, τ1)} WB(L,Γ,∆τ,getfield(c, f)·B) =

letK=K{t→c}

τ= Θ.c.fields.f S1 =Unify{(∆, t·δ)}

S2 =WB(S1(L), S1(Γ, τ·δτ), B)

in S2◦S1WB(L,Γ; ∆τ,invoke(c, m)·B) =

図5.5: ブロックラベル環境の型推論アルゴリズム