OCommand : 型安全な シェルプログラミングのための 領域特化言語の提案 朝倉 泉 増原 英彦 青谷 知幸 東京工業大学 数理・計算科学専攻 OCommand : OCaml上で安全にシェルスクリプトを書くためのDSLを提案

OCommand OCaml上で安全にシェルコマンドを 呼び出すための処理系 コマンド出力へのアクセスに対する 安全性を保証 コマンドの仕様を書くためのDSL コマンドの結果にアクセスする書式を変換する処理系 コマンド出力へのアクセスに対する 安全性を保証 以下の定義を含む

各欄が適切なデータ型に変換されたレコード型として扱いたい lsコマンドを利用するプログラム例 ls -lの出力からサイズの合計が与えられた閾値より小さいファイル集合を求めたい 例 閾値=10000Byte $ ls –l -rw-r----- 1 root admin 2682 Dec 17 20:37 a -rw-r----- 1 root admin 2459 Jan 10 14:54 b -rw-r----- 1 root admin 2397 Jan 10 14:55 c -rw-r--r-- 1 root wheel 607 Jan 16 07:53 d -rw-r----- 1 root admin 12217 Feb 4 17:45 e -rw-r----- 1 root admin 12986 Feb 5 00:02 f ファイルサイズ ファイル名 本発表では次の簡単な問題を解くスクリプトでOCommandの目標を説明する 上から見ていってしきい値を超えないファイル集合を求める 上から順に総和がしきい値を超えない最大のファイル列を求める 多くのシェルコマンドは出力に構造を持つ,　例えば {perm:perm; hard:int; ... ;size:int; ... ;name:string} 各欄が適切なデータ型に変換されたレコード型として扱いたい

lsコマンドを利用するプログラム例 コマンドはオプション集合を引数に取る関数(コマンド関数) コマンド関数の戻り値はレコード(出力行レコード) のリスト let collect_files size = let files = Ls.command (add_l empty) in let rec iter cur_size acc files = match files with | [] -> acc | file :: files -> 　　let cur_size = cur_size + file..size in 　　if cur_size > size then acc 　　else iter cur_size (file..name :: acc) files in iter 0 [] files ;; 指定されているオプションの集合 (オプション集合) OCommandを使うとコマンドはコマンド関数,　... fileはコマンド関数の戻り値のリストの各要素 このあとはこのスクリプトを使って目標を説明する

目標1/5. コマンドの関数化 1. コマンドをオプションを引数に取る関数として扱う let collect_files size = let files = Ls.command (add_l empty) in let rec iter cur_size acc files = match files with | [] -> acc | file :: files -> 　　let cur_size = cur_size + file..size in 　　if cur_size > size then acc 　　else iter cur_size (file..name :: acc) files in iter 0 [] files ;; emptyは空のオプション集合 add_lはオプション集合に lオプションを追加する関数 タイトルに目標とかく

2. コマンド出力が自動的に レコードに変換される 目標2/5. 出力のレコード化 let collect_files size = let files = Ls.command (add_l empty) in let rec iter cur_size acc files = match files with | [] -> acc | file :: files -> 　　let cur_size = cur_size + file..size in 　　if cur_size > size then acc 　　else iter cur_size (file..name :: acc) files in iter 0 [] files ;; ユーザが構文解析等を行う必要はない 2. コマンド出力が自動的に レコードに変換される

目標3/5. レコード型の柔軟な変化 3.オプションが変化すると出力レコードの型も 適切に変化する let collect_files size = let files = Ls.command (add_i (add_l empty)) in let rec iter cur_size acc files = match files with | [] -> acc | file :: files -> 　　let cur_size = cur_size + file..size in 　　if cur_size > size then acc 　　else iter cur_size (file..name :: acc) files in iter 0 [] files ;; iオプションを追加して 出力行レコードにinodeという int型のフィールドを追加 3.オプションが変化すると出力レコードの型も 適切に変化する オプションを誤って-iと書いてしまった場合でも

目標4/5. フィールドアクセスの検査 $ ls –i 10358 a 305049 b 301392 c 940030 d 61038 e 4.ユーザがアクセスしたフィールドが存在することが検査できる let collect_files size = let files = Ls.command (add_i empty) in let rec iter cur_size acc files = match files with | [] -> acc | file :: files -> 　　let cur_size = cur_size + file..size in 　　if cur_size > size then acc 　　else iter cur_size (file..name :: acc) files in iter 0 [] files ;; $ ls –i 10358 a 305049 b 301392 c 940030 d 61038 e 573013 f 出力にsizeフィールドが無いので コンパイルエラー

目標5/5. オプションの合成 5.オプションを合成可能にすること collect_files add_t size 更新日時順 let collect_files opt size = let files = Ls.command (opt (add_l empty)) in let rec iter cur_size acc files = match files with | [] -> acc | file :: files -> 　　let cur_size = cur_size + file..size in 　　if cur_size > size then acc 　　else iter cur_size (file..name :: acc) file in iter 0 [] files ;; 5.オプションを合成可能にすること ひとつはadd_lとかのように古いオプション集合から新しいオプション集合を作れるようにすること 新しいパラメータoptをとるようにして、-lと合成している -t更新日時順に出力させる -Sサイズ順に出力させる この目標は現在のOCommandでは実現できていない collect_files add_t size collect_files add_S size 更新日時順 サイズ順

目標を実現する方針 DSLによるコマンドの 仕様の記述 1.コマンドの関数化 2.出力のレコード化 4.レコード型の柔軟な変化 オプション集合をsingleton typeで表す 出力行レコードに型レベル関数を用いる 4.レコード型の柔軟な変化 フィールドアクセスが安全であることの証明を 生成 3.フィールドの検査 5.オプションの合成 オプション集合を タプルで表現

目標を実現する方針 DSLによるコマンドの 仕様の記述 1.コマンドの関数化 2.出力のレコード化 4.レコード型の柔軟な変化 オプション集合をsingleton typeで表す 出力行レコードに型レベル関数を用いる 4.レコード型の柔軟な変化 フィールドアクセスが安全であることの証明を 生成 3.フィールドの検査 5.オプションの合成 オプション集合を タプルで表現

提案1/2:OCommand DSL/ 関数と型定義の導出 オプションをコマンドに渡した時に,どのように形式が変化するかを記述 コマンドの記述からコマンドをOCaml上で型安全に扱うための関数,型定義を導出 先ほどあげた４つの貢献を実現するために、このような提案をします

DSLによる形式の定義 コマンドの名前 フィールドの出現順序 COMMAND ls : BEGIN ORDER {inode; owner; group; ...; name} OPTION i : ADD {inode : int} OPTION l : ADD {perm : perm; hard : int; ...} OPTION h : MODIFY {size : hsize} DEFAULT : {name : string} END まず、lsコマンドは何もオプションを指定しないとファイル名のみを出力するので -iオプションをつけるとinode番号を表示するのでADDオプションを用います 各フィールドの出現順序を記述します 出力の形式＝オプションが指定された時に出現するフィールドとその型、変化するフィールドの型 オプションの作用 オプションの作用:オプションが指定された時に出力の形式がどう変化するか

DSLの生成コード DSLで記述されたコマンドの仕様からコマンド関数の定義などが生成される module Ls = struct ... let empty = ... let add_i opt = ... let add_l opt = ... let add_h opt = ... let command opts = ... end オプション集合を操作する関数の定義 このように生成されたモジュール これから残りの目標を実現するためにどのようなプログラムが生成されるかをみる コマンド関数

目標を実現する方針 DSLによるコマンドの仕様の記述 1.コマンドの関数化 2.出力のレコード化 4.レコード型の柔軟な変化 オプション集合をsingleton typeで表す 出力行レコードに型レベル関数を用いる 4.レコード型の柔軟な変化 フィールドアクセスが安全であることの証明を 生成 3.フィールドの検査 オプション型をタプルで表現 5.オプションの合成

適切な型検査 コマンド関数は引数のオプション集合に よって出力行レコード型が異なる # Ls.command empty 引数の値毎に異なる レコード型を返す # Ls.command empty - : {name : string} list # Ls.command (add_i empty) - : {inode : int; name : string} list アニメいらない # Ls.command (add_i (add_l empty)) - : {inode : int; perm : …; name : string} list

提案2/2:型レベル関数を用いた コマンド関数のエンコード オプション集合をGADTsによってsingleton typeにする 出力行レコードに型レベル関数を用いる コマンド関数 : オプション集合型 出力行レコード型 → 一対一対応 (singleton type) 型レベル関数 オプション集合値 依存

提案2/2:型レベル関数を用いた コマンド関数のエンコード オプション集合をGADTsによってsingleton typeにする 出力行レコードに型レベル関数を用いる レコードをタプルで表現 perm, size, name等が型レベル関数 ('i opt_i * 'l opt_l * 'h opt_h) (('i, 'l, 'h) perm * ... * ('i, 'l, 'h) size * ... * ('i, 'l, 'h) name)) list command : →

オプション指定型 オプションが指定されているかどうかを表す型 GADTsを用いて定義 (* on, offは抽象型 *) type 'i opt_i = I_On : on opt_i | I_Off : off opt_i let empty = (I_Off, L_Off, H_Off) let add_i (_, l, h) = (I_On, l, h) let add_l (i, _, h) = (i, L_On, h) let add_h (i, l, _) = (i, l, H_On)

提案2/2:型レベル関数を用いた コマンド関数のエンコード オプション集合をGADTsによってsingleton typeにする 出力行レコードに型レベル関数を用いる レコードをタプルで表現 perm, size, name等が型レベル関数 ('i opt_i * 'l opt_l * 'h opt_h) (('i, 'l, 'h) perm * ... * ('i, 'l, 'h) size * ... * ('i, 'l, 'h) name)) list command : →

フィールド型 各オプション指定型からフィールド出現型への型レベル関数 フィールド出現型:フィールドが存在して その型がτであることを表す型τ preと フィールドが存在しないことを表すabs OCamlは型レベル関数を直接サポートしていないので何らかのエンコードが必要 'i 'l 'h size (off, on, off) = int pre size (off, on, on) = string pre size (off, off, off) = abs

フィールド型 type ('i, 'l, 'h) size = | Size : 'fld field * ('i, 'l, 'h, 'fld) rel_size 型引数'fldは存在量化されて外から隠されている 'fld fieldは'fldがpreの時のみ値を持つ型(GADTs) type 'fld field = | FPre : 'a -> 'a pre field | FAbs : abs field rel_sizeは型レベル関数size('i,'l,'h)='fldである証明

フィールド型 type ('i, 'l, 'h) size = | Size : 'fld field * ('i, 'l, 'h, 'fld) rel_size ∃x:(i, l, h, fld)rel_size ⇔ size(i,l,h)=fld type ('i, 'l, 'h, 'fld) rel_size = | Rel_size_0 : (off, off, off, abs) rel_size | Rel_size_1 : (off, off, on, abs) rel_size | Rel_size_2 : (off, on, off, int pre) rel_size | Rel_size_3 : (off, on, on, string pre) rel_size (* other 4 combinations of options *) size(i,l,h)=fldである証明を一緒に持たせておく

フィールド型 type ('i, 'l, 'h) size = | Size : 'fld field * ('i, 'l, 'h, 'fld) rel_size x0 : (off, off, off) size ⇒ x0 = (FAbs * Rel_size0) x1 : (off, on, off) size ⇒ x1 = (FPre (int型の値) * Rel_size2 型引数毎に'fldの型が変化している

目標を実現する方針 DSLによるコマンドの仕様の記述 1.コマンドの関数化 2.出力のレコード化 4.レコード型の柔軟な変化 オプション集合をsingleton typeで表す 出力行レコードに型レベル関数を用いる 4.レコード型の柔軟な変化 フィールドアクセスが安全であることの証明を生成 3.フィールドの検査 5.オプションの合成 オプション集合を タプルで表現

存在量化されたresの型がエスケープするので型エラー フィールドアクセス≠パターンマッチ 型を無視するとパターンマッチで取り出せば良い file..size match file with | (..., Size (Fpre res, _), ...) -> res 存在量化されたresの型がエスケープするので型エラー

フィールドアクセス=パターンマッチ+証明 存在型が具体的なフィールド出現型に等しいことを証明して取り出す file..size (off, on, off, ?) rel_size -> (?, int pre) eq match file with | (..., Size (x, rel), ...) -> let eq = eq_rel_size_off_on_off rel in let FPre res = apply_eq eq x in res (?, int pre) eq -> ? field -> int pre field

実装 合計1000行程度のシステムになった コマンドを使うスクリプト DSLで記述された コマンドの形式 ダミープログラムの生成(100行) コマンドモジュールの生成(600行) 型情報を得るための ダミーコード フィールド出現型を証明する関数 ocaml コンパイラ Camlp4というOCamlのためのプリプロセッサシステムを用いました コード生成に型情報を利用しているので,OCamlコンパイラのオプションを使って取得しました スクリプトの変換(200行) 型/関数定義 型情報 (.annot) 合計1000行程度のシステムになった 証明付きの スクリプト

事例研究 lsコマンドの他に,df,psコマンドを本研究が提案するDSLで扱えることを確かめた フィールド数:7 対応したオプション:T,h COMMAND ps : BEGIN ORDER : {f; s; uid; pid; ppid; c; pri; ni; addr; sz; wchan; stime; tty; time; cmd;} ;; OPTION e : ADD {} OPTION f : ADD {uid : string; ppid : int; c : int; stime : time} ;; OPTION l : ADD {f : int; s : string; uid : int; ppid : int; c : int; pri : int; ni : int; addr : string; sz : int; wchan : string} DEFAULT : {uid : int; tty : string; time : string; cmd : string with delim = ""} END;; COMMAND df : BEGIN ORDER : {filesystem; type; size; used; available; use; mounted_on} ;; OPTION T : ADD {type : string};; OPTION h : MODIFY {size : hint; use : hint; avail : hint} ;; DEFAULT : {filesystem : string; size : int; used : int; available : int; use : int; mouted_on : string} END;; フィールド数:7 対応したオプション:T,h フィールド数:15 対応したオプション:e,f,l

関連研究 : Caml-Shcaml [Heller, A. and Tov, J. A., ML2008] 手法 コマンドの形式をモジュールで記述 モジュールをファンクターに渡すことでコマンド関数等を生成 本研究との相違点 オプションの合成等は扱っていない 出力行レコードへのアクセスに対する型安全性はない

課題: 多相なオプションへの対応 引数のオプションに対する制約はHaskellの type classと関数従属性を用いて表現できる let sum_size opt size = let files = Ls.command (opt (add_l empty)) in List.fold files ~init:0 ~f:(fun acc file -> acc + file..size) ;; この時,　optには “lオプションと組み合わせた時の出力行レコードには sizeというint型のフィールドが存在する”ような任意の型 という型が付いてほしい OCommandエンコードでは表現できない 引数のオプションに対する制約はHaskellの type classと関数従属性を用いて表現できる

結論 コマンドの仕様を記述し、コマンドを OCaml上で呼び出すためのコードを 生成するためのDSLを提案 オプションを指定した時にどのように出力を 変化させるかを記述 コンパイル時にフィールドアクセスが安全であることを検査するためのOCaml上での型の表現を与えた GADTsを用いて表現 ls,ps,dfが扱えることを確かめた 多相なオプションをどう扱うかは今後の課題