To Home
mallocの型推論
研究室内部向けの情報です
やること
  1. mallocの引数から推論
  2. mallocの返り値の型から推論
mallocの引数(に渡される式)から推論
  return malloc(sizeof(int))
ならば、intのデータ(1 word)へのポインタ
  return malloc(sizeof(int) * 100)
ならばintの配列と推論する。

mallocの返り値の型から推論

  int size = 4;
  int* ip = (int*)malloc(size);
ならば、外で int* にキャストされて使われているので、 int* 型だと推論する。

それ以外の場合もある (Future work)
void* user_malloc(int size) { somecheck(); return malloc(size); }
この場合は、使う側から型情報をもらう!?

用意されているもの

~/oiwa/work/safeC/parser/test/loadcmds をインタプリタに読み込むと適切なモジュールがロードされる。
使用例
tuba:~oiwa/work/safeC/parser/test> ocaml -I ..
        Objective Caml version 3.06

# #use "loadcmds";;
val print_bigint : Big_int.big_int -> unit = <fun>
...
# read "test2.c";;
- : C_abstree.program =
[{C_abstree.pdecl_t =
...
2003/06/19 現在では、parserディレクトリ内にパーザーに関連するコードを組み込んだ ocaml インタプリタ parser.top が用意されている。

使用例

aki|15:49|~/tmp/safeC/parser> ./parser.top 
        Objective Caml version 3.06

# Test_read.read;;
- : string -> C_abstree.program = <fun>
# Test_read.read "test.c";;
- : C_abstree.program =
[{C_abstree.pdecl_t =
   C_abstree.PdeclFunction
    ([C_abstree.TypeSpec (C_abstree.PtypespecBuiltin C_abstree.Int)],
    C_abstree.PdeclFuncType (C_abstree.PdeclIdent "main",
     [C_abstree.PpdeclConcrete
       ([C_abstree.TypeSpec (C_abstree.PtypespecBuiltin C_abstree.Int)],
       C_abstree.PdeclIdent "argc");
      C_abstree.PpdeclConcrete
       ([C_abstree.TypeSpec (C_abstree.PtypespecBuiltin C_abstree.Char)],
       C_abstree.PdeclPointer ([],
        C_abstree.PdeclArray (C_abstree.PdeclIdent "argv", None)))]),
    [],
    {C_abstree.pstmt_t =
      C_abstree.PstmtCompound ([],
       [{C_abstree.pstmt_t =
          C_abstree.PstmtReturn
           (Some
             {C_abstree.pexp_t =
               C_abstree.PexpConstant (C_abstree.PconstInteger "0");
              C_abstree.pexp_pr = {C_abstree.p_loc = ("", 2)}});
         C_abstree.pstmt_pr = {C_abstree.p_loc = ("", 2)}}]);
     C_abstree.pstmt_pr = {C_abstree.p_loc = ("test.c", 1)}});
  C_abstree.pdecl_pr = {C_abstree.p_loc = ("test.c", 1)}}]

# Test_read.read "kandr_test.c";;
- : C_abstree.program =
[{C_abstree.pdecl_t =
   C_abstree.PdeclFunction
    ([C_abstree.TypeSpec (C_abstree.PtypespecBuiltin C_abstree.Int)],
    C_abstree.PdeclFuncIdent (C_abstree.PdeclIdent "main", ["argc"; "argv"]),
    [{C_abstree.pdecl_t =
       C_abstree.PdeclVariable
        ([C_abstree.TypeSpec (C_abstree.PtypespecBuiltin C_abstree.Int)],
        [C_abstree.PinitDecl (C_abstree.PdeclIdent "argc", None)]);
      C_abstree.pdecl_pr = {C_abstree.p_loc = ("", 1)}};
     {C_abstree.pdecl_t =
       C_abstree.PdeclVariable
        ([C_abstree.TypeSpec (C_abstree.PtypespecBuiltin C_abstree.Char)],
        [C_abstree.PinitDecl
          (C_abstree.PdeclPointer ([],
            C_abstree.PdeclPointer ([], C_abstree.PdeclIdent "argv")),
          None)]);
      C_abstree.pdecl_pr = {C_abstree.p_loc = ("", 2)}}],
    {C_abstree.pstmt_t =
      C_abstree.PstmtCompound ([],
       [{C_abstree.pstmt_t =
          C_abstree.PstmtReturn
           (Some
             {C_abstree.pexp_t =
               C_abstree.PexpConstant (C_abstree.PconstInteger "0");
              C_abstree.pexp_pr = {C_abstree.p_loc = ("", 4)}});
         C_abstree.pstmt_pr = {C_abstree.p_loc = ("", 4)}}]);
     C_abstree.pstmt_pr = {C_abstree.p_loc = ("", 3)}});
  C_abstree.pdecl_pr = {C_abstree.p_loc = ("kandr_test.c", 1)}}]

Abstruct Syntax Treeに関すること

関数呼び出し
C_abstree.PexpInvoke(関数名,引数のリスト)


ソース

int 	foo()
{
    return f(1);
}

AST

# read "/tmp/b.c";;
- : C_abstree.program =
[{C_abstree.pdecl_t =
   C_abstree.PdeclFunction
    ([C_abstree.TypeSpec (C_abstree.PtypespecBuiltin C_abstree.Int)],
    C_abstree.PdeclFuncIdent (C_abstree.PdeclIdent "foo", []), [],
    {C_abstree.pstmt_t =
      C_abstree.PstmtCompound ([],
       [{C_abstree.pstmt_t =
          C_abstree.PstmtReturn
           (Some
             {C_abstree.pexp_t =
               C_abstree.PexpInvoke
                ({C_abstree.pexp_t = C_abstree.PexpVar "f";
                  C_abstree.pexp_pr = {C_abstree.p_loc = ("", 2)}},
                [{C_abstree.pexp_t =
                   C_abstree.PexpConstant (C_abstree.PconstInteger "1");
                  C_abstree.pexp_pr = {C_abstree.p_loc = ("", 2)}}]);
              C_abstree.pexp_pr = {C_abstree.p_loc = ("", 2)}});
         C_abstree.pstmt_pr = {C_abstree.p_loc = ("", 2)}}]);
     C_abstree.pstmt_pr = {C_abstree.p_loc = ("", 1)}});
  C_abstree.pdecl_pr = {C_abstree.p_loc = ("/tmp/b.c", 1)}}]

* sizeofは関数呼び出しではなく、言語に組み込まれている C_abstree.PexpSizeOfType

  C_abstree.PexpSizeOfType
   (C_abstree.Ptypename
     ([C_abstree.TypeSpec
        (C_abstree.PtypespecBuiltin C_abstree.Int)],
     C_abstree.PdeclAnonymous));

詳細は ~oiwa/work/safeC/parser/il.mli 参照

AST を訪問する例
c_pp.ml , c_typing.ml , ctt_printer.ml

素材

parsing の ocamldoc
parsing ないの依存性の図 safeC.png

c_abstree.mlをよんでみた

方針

定数の計算を行わないと型が決まらないことがある (1-1 = 0 = NULL) ので定数の計算は型付けの前に行ってしまいたいが、 定数計算をするとなると sizeof(int) の値も計算しなければならなくなり、 sizeof の引数に入っていた型名の情報が 失われてしまう。よって、整数定数の表現を int * type_name option にする。

絡んでくる場所 c_abstree の PexpSizeOfType , PexpSizeOfExpr。 前者は型をとってくるのは簡単だが、後者は式の 結果の型を保存しなければならない。

メモ

c_abstree (型無し) -> ctt_abstree (型付き)
c_type const / volatile
c_type_descr 組み込み型。ユーザー定義 etc ..
C_abstree.type_name

CTTexpCoerce !?
reduce.ml の reduce_expression

   reduce.ml ないで 定数の計算をしていると思われる。整数同士の演算で
     型情報によってどのように演算するかをきめる必要がある。
      なし なし => なし
      あり なし => ありの方の情報
      あり あり =>
        全く同じ場合
        異なる場合 (これにさらに場合分けあるかも?)
reduce.ml compute_const_ii
c_typing ないの | PexpVar(id) ->

スケジュール

準備
  AST巡り
  mallocのパターン抽出

実装
インターフェイス決定
  呼び出され方
  結果の情報 (型)
11/27ソース解読完了 / 関数のsignature (大岩さんと関口さんと相談) / 実装開始
12/ 4処理の流れを決定 実装中
CTTconstInteger に型情報を付加。 定数演算部分も書く。デバッグ。
12/11version 0.1 完成 / 小さいテスト開始 / デバッグ開始
12/20完成 (来年1月中頃!?)

とりあえず触ってみたところ
Ctt_abstree.CTTconstInteger に型情報 をつけた (CTTconstInteger of big_int * type_name option)
Cttm_abstree.CTTconstInteger って!?

議題
malloc の型付けをどこで行うか?

そもそも、関数呼び出しの時に関数の型を調べているのはどこか? Ctt_abstree , Cttm_abstree の違いは!?

結論
Ctt_constInteger に sizeof 由来の整数定数であるか否かの情報を付加。さらに整数演算のされかた (あとの 解析で変数との演算で同様の処理は行うのだが) で配列であるかどうかを見る。でも、 sizeof(int) * sizeof(float) のように 型情報を持つ整数同士の乗除を行われたときにどうするか考えなければならない。考えられる方法は以下の通り。

後者を採用することにする。ただわからないといっても、型情報のない整数と同じかというとそうではない。
sizeof(int) * sizeof(int) * sizeof(float)
で型情報復活なんてされるのは困る。つまり付加する方は下のようになる
  None    (* 普通の整数 *)
  T       (* sizeof(T) *)
  T[]     (* sizeof(T)*6 など *)
  Invalid (* 型情報同士の演算でinvalidになったもの *)

演算表 (変わるかも)
+, - None T T[]Invalid
None None T T[]Invalid
T T T[] (equivalent type)
Invalid (otherwise)
T[] (equivalent type)
Invalid (otherwise)
Invalid
T[] T[] T[] (equivalent type)
Invalid (otherwise)
T[] (equivalent type)
Invalid (otherwise)
Invalid
InvalidInvalidInvalidInvalidInvalid

sizeof(T) + 8 は、T型のものに適当なバッファを付け加えたもので全体としては型Tであろうと見る。
sizeof(int) + sizeof(float) + sizeof(char) などは Invalid

影響範囲
CTTconstInteger
reduce.ml の 演算部分
  compute_const_ii
  論理演算結果...。
  Coerce!?
  Case文のラベル
  CTT to Ptree ctt_to_ptree.ml (未着手 型情報をそのまま残す必要あり)

* None T T[] Invalid
None None T[] T[] Invalid
T T[] InvalidInvalidInvalid
T[] T[] InvalidInvalidInvalid
InValidInvalidInvalidInvalidInvalid

/ NoneT T[] Invalid
None NoneInvalid?Invalid?Invalid
T T? Invalid?Invalid/None?InvalidInvalid
T[] T[] Invalid/None?Invalid/None?Invalid
InvalidInvalidInvalidInvalidInvalid

また、整数と浮動小数点数との演算が行われる場合は結果はfloatなので型情報が落ちる。整数に復帰することはある!?
intからintへのcoerceは型情報を残す。
Coreceの例が欲しい

単項演算子では型情報は保存

メモ

Reduce.coumpute_const_ff は operator をとるが、それが整数の演算子だったばあいには結果が整数に なるといったことが書いてある。このときの型は!?
想定される変なプログラム
malloc((3.14 == sizeof(int))*10);

(sizeof(int)*10)/2 ハーフサイズの配列

型情報を付与した整数の型と最終的な整数の型との関係
最終的に整数は動的な型情報を持つ型 Tp か 普通の整数 Normal に別れる

relation of type

malloc(sizeof(int)*8*n)
=> malloc( [int[], 32] * n)

いやらしい例

(int)((float)(sizeof(float) * sizeof(int)))*5
sizeof(float) * sizeof(int) で型情報は消える (floatには今は付けていないので 付けるとすればInvalidを付けたい) があとでintにキャストされて NoType に復活。

結論

楽観的に

いまは malloc(exp); の返り値の型は推論できない。
  1. exp がsizeofが絡んだたちのいい定数式であった。
      malloc(sizeof(int));
    ならば int* と型づけできる。
       malloc(4), malloc(sizeof(int)*sizeof(char)) は型づけできないが。
  2. さらに expが
      malloc(sizeof(int)*n);
    の形 (sizeof*変数)でなんらかの方法でnには型情報を伴わない普通の整数が来るとわかったならば int[]と型づけできる
  3. さらに expが
      malloc(n*10);
    の形で何らかの方法でnには型情報を持った整数で、しかも常に同じ型の情報がくると分かれば、そのかたの配列であると型づけできる。
  4. さらに、(!?) expが
      malloc(n*m) で ....

リンク

実装メモ

Author: Takashi Masuyama (tak AT is DOT s DOT u-tokyo DOT ac DOT jp)
Valid HTML 4.0!