7/11 全体ミーティング発表低級言語

7/11 全体ミーティング発表
低級言語のプログラム変換
D1 吉野寿宏
<[email protected]>
Agenda




背景
プログラム変換器の数学的性質
テンプレートによる変換と型システム
変換の正しさの議論に向けて
Agenda




背景
プログラム変換器の数学的性質
テンプレートによる変換と型システム
変換の正しさの議論に向けて
修士論文の概要

低級言語のプログラム検証器を作るための
支援をするフレームワークを作成した

共通言語を固定し、その上で検証ロジックを構築
共通言語に対してプログラム変換してから検証

変換器と検証ロジックとは独立



新しいアーキテクチャに対応する際に検証ロジックは
弄らない
検証ロジックを取り替えるときに変換器を弄らない
研究背景
低級言語向けのプログラム検証器は…
 アーキテクチャへの依存性が強い


種々のアーキテクチャそれぞれに派生言語
検証器を作るたびにモデル化の必要


実装において、大きな負担
実装の移植性が悪いことがしばしば

検証の種類×対応アーキテクチャの種類数の
組み合わせが必要に
アイデア (図)
変換器
共通言語に
変換された
プログラム
低級言語の
プログラム
検証結果
Success
/Fail
検証
ロジック
共通言語の意味論
検証器
問題はどのように解決されるか

言語の意味論の複雑さを削減

低級言語の記述は変換器の中に収める



言語の記述は一度やってしまえば OK
検証ロジックの実装者は変換器を気にする必要
はない
システムの移植性の改善
一度検証ロジックを実装すれば、変換器を取り
替えて他のアーキテクチャにも対応可
⇒ 組み合わせの数が減らせる

共通言語 ADL

ADL: Architecture Description Language

低級言語の意味論を記述するための言語


特定のアーキテクチャに依存しない
低級言語に近いレベルの記述



λ計算のように抽象度の高い記述は変換が手間
レジスタ・メモリに対する操作を明示的に記述
なるべくシンプルな言語構造

基本となる命令数が多いと意味論が複雑化
共通言語
値の定義
Fat Pointer
3 種類の
コンストラクタが
それぞれ対応
Value
a は 1 バイト幅
のデータ
Data
共通言語
言語構文
簡単な例

整数を含む連結リストの要素の総和を求める

ハコは 4 バイト幅のデータと考えてください
start:
%r2 = 0;
goto &loop;
r2
0
6
3
1
1
loop:
r1
if %r1 = &null then
goto &end
else
nop;
%r2 = %r2 + *[4](%r1);
%r1 = *[4](%r1 + 4);
goto &loop;
end:
2
3
null
Agenda


背景
プログラム変換器の数学的性質



正しさとは何か
テンプレートによる変換と型システム
変換の正しさの議論に向けて
プログラム変換と正しさ

別の言語から共通言語に変換


検証したいプログラムは、アセンブリ言語や
機械語で書かれている
検証ロジックは ADL の意味論を用いて定義
⇒ プログラム変換が正しく行われなければ
検証内容が信用できない

変換の正しさってどういうこと？
プログラム変換の正しさ


プログラム = 機械の状態集合上の関数
変換の正しさ =
任意のプログラムに関して、2 つの言語の間での
インタプリタの状態の「対応」が整合的に構成できる
状態
State
変換元の
プログラム
変換後の
プログラム
状態’
State’
手続き型言語の抽象モデル

手続き型言語は、状態(≒変数)を変更
することで実行を進める計算モデル

状態を「インタプリタ」に持たせる


C 言語などコンパイラ型の言語でも、変数全体の
集合を考えることで同じように捉えられる
手続き型言語のプログラムとは状態集合上の
(部分)関数

しかし特に低級言語の場合は、1 命令の実行を
単位として、エラーも状態に含めて考えれば
全関数になることが多い
手続き型言語の抽象モデル

ある言語のインタプリタは
という組
: 状態集合
: 遷移関数 (



)
p はプログラム(パラメータ)であり、p が与えられる
と遷移関数が決まる
S
T
V
U
error
Conservative Simulation

インタプリタ


が
をシミュレート
下記の性質を満たすように関係
構成できること、と定義
であるときに、
が



そうでない場合
存在し、
ついて
このとき
としたとき列
とnが
かつ n 未満の整数 i に
と書く
Conservative Simulation

Conservative simulation は要するに、

A B のとき、A で実行エラーが起こる場合は B でも
必ずエラー



ただし逆は必ずしも真ならず
この意味において B のほうが「保守的である」という定義
実行エラーが起こらないときは状態の対応が保存
「変換の正しさ」の定義

正しさ =
変換が成功した場合に、変換された
プログラムが元のプログラムに対して
conservative simulation

完全に(エラーになるかどうか等含め)同じ
動作、というわけではない

ただし保守的な(変換後の)ルールでエラーに
ならなければ、元のプログラムもエラーにならない
Agenda



背景
プログラム変換器の数学的性質
テンプレートによる変換と型システム



テンプレートによる変換ルール記述
型の導入による不正テンプレートの検査
変換の正しさの議論に向けて
低級言語の変換アルゴリズム

低級言語のプログラムは基本的に命令列


算術演算・論理演算
制御構造としては分岐のみで十分


ループや関数呼び出しなどは全てこれらで書ける
命令単位で順次変換

各命令はコンテクストを持たない

持っているとすればプロセッサの状態(レジスタ・
メモリ)のはず
テンプレートによる
変換ルールの記述

アセンブリ言語の命令 = 種別+オペランド

オペランドによってパラメータ化されている
命令種別
オペランド
変換ルール！
 たとえば mov 命令(データのコピー)
mov %r1, %r2
mov
mov%r3,
D %r5
,S
mov %r2, %r4
⇔
%r1 = %r2;
⇔⇔ D%r3= =S%r5;
;
⇔
%r2 = %r4;
テンプレートによる
変換ルールの記述
mov D , S
⇔
D = S ;

すべての可能性を列挙する手間が省ける

オペランド ::= レジスタ | メモリ | 即値
ADL の構文の非終端記号で言うと、l か v
⇒ ev (式) にマップすればカバーできる

テンプレート言語

ADL の式(ev)を拡張



テンプレート引数を許容するように
sizeof 演算子(l のデータ幅を返す)の追加
引数で指定できる箇所を ev に変更

代入の左辺、左辺値のデータサイズ指定
テンプレートのインスタンス化


コンテクスト :: 変数 → ev (式)
構文木をほぼそのまま写せばよい


テンプレート変数の部分は「接木」
変数を許すために便宜的に ev を使っている箇
所でダウンキャストが必要



左辺値のデータ幅指定 → 整数へ
代入左辺 → 左辺値または一時変数へ
ダウンキャストできない場合は、変換が失敗する
(変換エラー)
アーキテクチャ記述例
(IA-32、抜粋)
#operand {
eax = %eax;
ax = %eax[0,2];
al = %eax[0,1];
ah = %eax[1,1];
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 = 0
else
%_zf = junk;
...
ebx = %ebx;
...
}
mov(D, S) {
D = S;
}
...
}
テンプレート言語の問題点
しかしこの定義だと…

テンプレート変数に予期しない値が入ってくる
可能性がある
例: mov(D, S) { D = S; } において D = 1 とか

そもそも不正なテンプレートを書ける
例: 引数にない変数を中で参照する可能性
例: 1 = 2; のような式を素で書いてしまう
⇒いずれも変換エラーが発生

「変換器をコンパイルする際に」、ではない
型理論の手法による解決

型を用いることによりこれらの問題を解決

変数に予期しない値が入らないことを検査



これだけだと runtime check と殆どかわらないが
型推論をすることにより、引数の条件を自動的に
求められることには意味がある(?)
不正なテンプレートを静的にチェック

ここで言う「静的」とは、変換器のコンパイル時


プログラムを実際に与えて変換する時、ではない
何度もコンパイルしてトライ＆エラーする手間が
省ける
型の構造

右図のような subtype
relation を満たす型を導入

lvalue
const
assn
ADLの構文定義の構造を反映


int
const




⇔
⇔
n (整数)
v (Value)
ただし junk を除く
lvalue
assn


int
⇔
⇔
l (左辺値)
l | x (変数)
assignable の意
* (any)
⇔
ev (式)
図では上の方が subtype
* (any)
型付け規則


型環境
式に対する型付け規則 Γ|- ev :τ
型の健全性・完全性

健全性: 型検査に通るテンプレートは(正しい
引数が与えられれば)エラーを起こさない



エラーにならない ⇔ ダウンキャストが成功
ダウンキャストが可能な条件を考えれば自明
完全性: 正しいテンプレートは型検査を通る

ダウンキャストが成功する場合は、型付け規則より
型が整合的につけられることは明らか

Case analysis をすればよい
型を推論する

型付け規則をそのまま使える

(テンプレート)変数の型を全て型変数とおいて
制約を集めて解く



関連付けられているパターンに含まれている変数のみ
注目
「(変数) (型)」という形の制約だけが出てくる
不整合な型が出てきたら推論失敗


X lvalue かつ X int、とか
reg[sizeof(X), X] のような不正な式を静的に除外
さらなる応用

型を細かく定義することにより、細かい制限を
記述することが可能


reg
lvalue などと拡張して、レジスタのみを
受け付けるテンプレートを記述することができる
型を用いた constant folding の補助

現在はデータ幅指定の部分に算術式が書けない



変換時に定数になる「式」を書けると便利？
X:int で reg[sizeof(reg) – X, X]、のような用途を想定
型付け規則を拡張してより細かい型付けを行う
Agenda




背景
プログラム変換器の数学的性質
テンプレートによる変換と型システム
変換の正しさの議論に向けて

中間言語の設計
プログラム変換器の正しさを
保証するには

Conservative Simulation を満たす状態の
対応関係を(機械的に)構築できればよい

しかしポインタと整数値の対応関係など、
考えなければならないことは多い



ADL ではメモリブロックの検証のために、ポインタ
を fat pointer 的な扱いにしている
Junk の扱い
手で全部やるのは結構大変そう

最悪実機を使って全数検査という手段はあるが…
Conservative Simulation
Relation の性質
は半順序になる(はず)



Reflexivity: ≡ = id とすれば自明
Transitivity: 直感的には下図のような感じ
S
≡
S’
～
～
S”
T
≡
T’
～
～
T”
現在考えていること

実際の低級言語と ADL の中間にあたる
言語を定義し、推移律を持ち出せる

そのためにはADL のプログラムを中間言語の
プログラムに正しく変換できる必要
⇒ それを実際に、定理証明系などを用いて
証明できないだろうか？

そのため現在勉強中です…
中間言語

ADL では値が 3 種類ある

整数, ポインタ(ラベル+オフセット), Junk



Junk は ADL の枠組みの中で値が定められない場合に登場
たとえば変なポインタ演算をやると登場
しかし実際の CPU ではポインタは単なる整数

ADL で fat pointer を使っているのは、メモリブロック同士を
切り離し、ポインタ演算を安全にするため
→ 整数だけを扱う言語を考えれば十分(?)
中間言語

値は整数だけ、とすると…


変換器の正しさを
ADL から構文を一部削除証明するには中間
 Conditional by kind が不要になる
言語との間で議論
すれば十分
どうやったら「正しい変換」になるかはまだ
考え中
共通言語に
変換された
プログラム
低級言語の
プログラム
中間言語
プログラム
？
今日のまとめ

低級言語プログラムの意味論を記述する
ための共通言語 ADL を紹介



プログラム変換にまつわる数学的定義
テンプレートによる変換ルールの記述
現在考えていることについて説明


テンプレート言語に型を導入
中間言語の設計・定理証明系を用いた証明

Download Report