YARV のバイトコードベリファイアを作ってみた

YARV ベリファイアを試作してみました。製作時間一晩、リファクタリング一晩なので適当です。不正なバイトコードを食わせると例外を投げます。

# encoding: utf-8
# bad_example.rb

require "verifier"

# ヘッダ
header = [
  "YARVInstructionSequence/SimpleDataFormat", 1, 1, 1,
  { :arg_size=>0, :local_size=>1, :stack_max=>3 },
  "<dummy>", "foo.rb", :top, [], 0, []
]

# バイトコード本体 (スタックマシン)
body = [
  [:getlocal, 10000], # 10000 番目のローカル変数を読む
  [:leave]            # 終わり
]

bytecode = header + [body]

# バイトコードをロードする
VM::InstructionSequence.load(bytecode)
   #=> invalid lindex (VM::InstructionSequence::Verifier::IseqVerificationError)

チェックしてること、してないこと

以下のことはチェックしてるつもり。Java のベリファイアとちがって型情報を考える必要がないので、だいぶ簡単です。

  • 各命令を実行するときのスタックの深さが一定であること。かつ、stack overflow や underflow をしないこと。
  • ローカル変数たちへのアクセスが適切なこと (バイトコード実行時にはバウンダリチェックをしないので、不適切なアクセスをすると SEGV する) 。
  • 各命令ごとのパラメータが適切なこと。例えば特殊変数のアクセス命令で、$% みたいな存在しない変数にアクセスしてないかどうかとか。ただし、いい加減です。
  • その他細かいこと。ヘッダ情報の検査とか、ラベルが重複してないかとか。

以下のことはまだチェックしてない。

  • 引数情報 (iseq->arg_*) 。可変長引数とかブロック引数とかのオフセットが、どういう条件を満たすべきか考えるのはちょっとややこしそう。
  • バイトコードを表す配列の中でリフレクションとか == の再定義とか怪しいことをしてないこと。検査不可能?
  • チェックすべきことなのに、僕がそのことに気がついてないこと (たぶんここが一番大きい) 。

実行例

ruby 1.9 のソースにパッチをあてたあと、以下のようにして verifier.rb を生成します。

$ ruby tool/insns2vm.rb verifier.rb

上の例を実行すると、以下のようにベリファイで落ちます。

$ ./ruby bad_example.rb
/home/mame/work/ruby19/ruby/verifier.rb:33:in `error': invalid lindex (VM::InstructionSequence::Verifier::IseqVerificationError)
        from /home/mame/work/ruby19/ruby/verifier.rb:265:in `check_index'
        from /home/mame/work/ruby19/ruby/verifier.rb:327:in `check_insn'
        from /home/mame/work/ruby19/ruby/verifier.rb:218:in `check_bytecode'
        from /home/mame/work/ruby19/ruby/verifier.rb:94:in `check_iseq'
        from /home/mame/work/ruby19/ruby/verifier.rb:25:in `verify'
        from bad_example.rb:22:in `load'
        from bad_example.rb:22:in `<main>'

また、verifier.rb にファイル名を指定して起動することで、ファイルをコンパイルしてできたバイトコードをベリファイします。

$ ./ruby verifier.rb benchmark/other-lang/loop.rb

信憑性

このベリファイアが本当にちゃんとできてるかどうかなんですが、「不正なバイトコードがちゃんと跳ねられる」と「正しいバイトコードがちゃんと通る」の 2 つのテストをする必要があります。
前者の方が圧倒的に重要ですが、すごく面倒で難しいので、すごく適当にしかやってません。なのでバグバグでダメダメです。
後者に関しては、Rubyリポジトリ中の .rb ファイルをそれぞれ YARVコンパイルして、得られたバイトコードを全部ベリファイしてみました*1YARVコンパイラで作ったバイトコードは正しいはずなので、全部ベリファイが通るはずです。

$ for i in `find . -name \*.rb |
  grep -v ./sample/drb/dhasenc.rb |
  grep -v ./sample/mine.rb |
  grep -v ./ext/tk/sample/tcltklib/sample1.rb`; do
  ./ruby verifier.rb $i || break
done

この過程でどうしてもベリファイが通らないところがあったのですが、調べてみると YARVコンパイラのバグでした (ruby-dev:34806 、修正済み) 。

アルゴリズム

自分用のメモなのです。わかるように書いてなくてごめんなさい。ソースを見たほうが早いです。

スタックの深さの推論
  • スタックの深さが確定している命令を洗い出す。具体的には、先頭番地の命令では当然スタックの深さが 0 。あとは例外ハンドラで cont_label の位置の深さが指定されているので、情報を持ってくる。
  • 深さの確定した命令からバイトコードを順方向になめて、命令種別ごとにスタックの深さを更新して、深さが未確定の命令の深さを推論していく。分岐命令があったら分岐先の命令の深さも確定する。
  • スタックの深さが 0 未満になったり stack_max を超えたりしたらエラー。同じ命令に異なるスタック深さが推論された場合もエラー。
  • 推論できるところがなくなったら終了。それでも深さ未確定な命令はデッドコード*2
変数アクセスの検査
  • ブロックを再帰的に辿って、各フレームでのローカル変数の数を調べる。definemethod と defineclass ではスコープが切れることに注意する。
  • ローカル変数やダイナミック変数のアクセス命令を探す。その命令がアクセスするフレーム (ローカル変数なら一番遠いフレーム、ダイナミック変数なら指示されたフレーム) の変数の数をみて、その数より大きいインデックスを指定していないことを確認する。
細かいこと
  • ヘッダ (マジック、バージョン、フォーマットタイプ) を適当にチェックする。
  • 引数やローカル変数の数を適当にチェックする (固定長でない引数のチェックは未実装) 。
  • ラベルが重複して現れないことをチェックする。
  • 例外ハンドラに存在しないラベルが指示されていないことをチェックする。
  • 例外ハンドラの start_label が end_label より先に来ることをチェックする。
  • 行番号が負にならない。

既知の問題

  • 現状の YARVコンパイラが、while や until で break に対して怪しい catch table を入れるので、スタック推論が通らない。この catch table は過去の残骸で、今ではもう意味がないので、はずしてしまえば OK 。
  • break の throw がキャッチされないようなバイトコードがチェックを通る。でも実行すると core を吐く。静的なベリファイで検出するのは無理そう。rb_bug でなく unexcepted break (LocalJumpError) にしてしまおう。
  • VM::InstructionSequence::Verifier.verify を再定義すればベリファイを無効にできてしまう。C で作り直せば解決する予定。
  • (適宜追加されるかも)

ソースコード

以下ソース (既知の問題の対策を含みます) 。ダウンロードしたい人は yarv-verifier-20080523.patchYARV が好きな人はぜひ遊んでみてください。そんでバグを見つけて教えてください (問題があるバイトコードなのに load できてしまって core を吐くとか) 。
さっそくバグがあったので差し替え。yarv-verifier-20080523-2.patch

Index: iseq.c
===================================================================
--- iseq.c	(revision 16559)
+++ iseq.c	(working copy)
@@ -419,6 +419,11 @@
     VALUE data, opt=Qnil;
     rb_scan_args(argc, argv, "11", &data, &opt);
 
+    if (rb_const_defined(rb_cISeq, rb_intern("Verifier"))) {
+	VALUE rb_cVerifier = rb_const_get(rb_cISeq, rb_intern("Verifier"));
+	rb_funcall(rb_cVerifier, rb_intern("verify"), 1, data);
+    }
+
     return iseq_load(self, data, 0, opt);
 }
 
@@ -1299,7 +1304,7 @@
     rb_define_method(rb_cISeq, "eval", iseq_eval, 0);
 
     /* disable this feature because there is no verifier. */
-    /* rb_define_singleton_method(rb_cISeq, "load", iseq_s_load, -1); */
+    rb_define_singleton_method(rb_cISeq, "load", iseq_s_load, -1);
 
     rb_define_singleton_method(rb_cISeq, "compile", iseq_s_compile, -1);
     rb_define_singleton_method(rb_cISeq, "new", iseq_s_compile, -1);
Index: compile.c
===================================================================
--- compile.c	(revision 16559)
+++ compile.c	(working copy)
@@ -1317,8 +1317,7 @@
 	    /* TODO: Dirty Hack!  Fix me */
 	    if (entry->type == CATCH_TYPE_RESCUE ||
 		entry->type == CATCH_TYPE_BREAK ||
-		(((ptr[0] & 0x10000) == 0)
-		 && entry->type == CATCH_TYPE_NEXT)) {
+		entry->type == CATCH_TYPE_NEXT) {
 		entry->sp--;
 	    }
 	}
@@ -2978,13 +2977,6 @@
 	    ADD_INSN(ret, nd_line(node), pop);
 	}
 
-	ADD_CATCH_ENTRY(CATCH_TYPE_BREAK, redo_label, break_label,
-			0, break_label);
-	ADD_CATCH_ENTRY(CATCH_TYPE_NEXT | 0x10000, redo_label,
-			break_label, 0, iseq->compile_data->start_label);
-	ADD_CATCH_ENTRY(CATCH_TYPE_REDO, redo_label, break_label, 0,
-			iseq->compile_data->redo_label);
-
 	iseq->compile_data->start_label = prev_start_label;
 	iseq->compile_data->end_label = prev_end_label;
 	iseq->compile_data->redo_label = prev_redo_label;
@@ -5002,7 +4994,7 @@
 
     iseq->local_table_size = opt + RARRAY_LEN(locals);
     iseq->local_table = tbl = (ID *)ALLOC_N(ID *, iseq->local_table_size);
-    iseq->local_size = opt + iseq->local_table_size;
+    iseq->local_size = iseq->local_table_size - opt + 1;
 
     for (i=0; i<RARRAY_LEN(locals); i++) {
 	VALUE lv = RARRAY_PTR(locals)[i];
Index: vm_insnhelper.c
===================================================================
--- vm_insnhelper.c	(revision 16559)
+++ vm_insnhelper.c	(working copy)
@@ -1229,7 +1229,7 @@
 			}
 			cfp++;
 		    }
-		    rb_bug("VM (throw): can't find break base.");
+		    vm_localjump_error("unexpected break", throwobj, TAG_BREAK);
 		}
 
 		if (VM_FRAME_TYPE(cfp) == FRAME_MAGIC_LAMBDA) {
Index: tool/instruction.rb
===================================================================
--- tool/instruction.rb	(revision 16559)
+++ tool/instruction.rb	(working copy)
@@ -84,6 +84,35 @@
         "return depth + #{rets.size - pops.size};"
       end
     end
+
+    def sp_increase_ruby_expr
+      if(pops.any?{|t, v| v == '...'} ||
+         rets.any?{|t, v| v == '...'})
+        # user definision
+        raise "no sp increase definition" if @sp_inc.nil?
+        ret = "inc = 0; "
+
+        @opes.each_with_index{|(t, v), i|
+          if t == 'rb_num_t'
+            ret << "#{v} = rands[#{i}]; "
+          end
+        }
+        @defopes.each_with_index{|((t, var), val), i|
+          if t == 'rb_num_t' && val != '*'
+            ret << "#{var} = #{val}; "
+          end
+        }
+
+        # use a fragment of C as Ruby
+        inc = @sp_inc.gsub("?", "!= 0 ?")
+        inc = inc.gsub("VM_CALL_ARGS_BLOCKARG_BIT", "4")
+
+        ret << inc << "; inc"
+        "(#{ ret })"
+      else
+        "#{rets.size - pops.size}"
+      end
+    end
     
     def inspect
       "#<Instruction:#{@name}>"
@@ -1010,6 +1039,28 @@
   end
 
   ###################################################################
+  # verifier.rb
+  class VerifierRbGenerator < InsnsInfoIncGenerator
+    def generate
+      verifier_rb
+    end
+
+    ###
+    private
+
+    # verifier.rb
+    def verifier_rb
+      insn_handlers = []
+      @insns.each do |insn|
+        opes = insn.opes.map {|type, var| op2typesig(type)[3..-1].downcase }
+        insn_handlers << [insn.name, insn.sp_increase_ruby_expr, opes]
+      end
+
+      ERB.new(vpath.read('template/verifier.rb.tmpl'), nil, ">").result(binding)
+    end
+  end
+
+  ###################################################################
   # insns.inc
   class InsnsIncGenerator < SourceCodeGenerator
     def generate
@@ -1308,6 +1359,7 @@
       'vmtc.inc'       => VmTCIncGenerator,
       'insns.inc'      => InsnsIncGenerator,
       'insns_info.inc' => InsnsInfoIncGenerator,
+      'verifier.rb'    => VerifierRbGenerator,
     # 'minsns.inc'     => MInsnsIncGenerator,
       'optinsn.inc'    => OptInsnIncGenerator,
       'optunifs.inc'   => OptUnifsIncGenerator,
Index: test/ruby/test_verifier.rb
===================================================================
--- test/ruby/test_verifier.rb	(revision 0)
+++ test/ruby/test_verifier.rb	(revision 0)
@@ -0,0 +1,201 @@
+require "verifier"
+require 'test/unit'
+
+def test_ruby_test_verifier(*r)
+#  p r
+end
+
+class TestVerifier < Test::Unit::TestCase
+  def accept(&b)
+    assert_nothing_raised { accept_exec(&b) }
+  end
+
+  def accept_exec
+    bytecode = yield
+    VM::InstructionSequence::Verifier.verify(bytecode)
+    iseq = VM::InstructionSequence.load(bytecode)
+    iseq.eval
+  end
+
+  def reject(&b)
+    assert_raise(VM::InstructionSequence::Verifier::IseqVerificationError) do
+      reject_exec(&b)
+    end
+  end
+
+  def reject_exec
+    begin
+      bytecode = yield
+      VM::InstructionSequence::Verifier.verify(bytecode)
+      iseq = VM::InstructionSequence.load(bytecode)
+    rescue VM::InstructionSequence::Verifier::IseqVerificationError
+      raise
+    else
+      puts "attack!"
+      iseq.eval
+    end
+  end
+
+  def test_getdynamic_ok
+    accept do
+      ["YARVInstructionSequence/SimpleDataFormat", 1, 1, 1,
+       {:arg_size=>0, :local_size=>2, :stack_max=>1},
+       "<compiled>", "<compiled>", :top, [:x], 0,
+       [[:break, nil, :label_4, :label_12, :label_12, 0]],
+       [1,
+        [:putobject, 1],
+        [:setlocal, 2],
+        :label_4,
+        2,
+        [:putobject, 1],
+        [:send,
+         :times,
+         0,
+         ["YARVInstructionSequence/SimpleDataFormat", 1, 1, 1,
+          {:arg_size=>0, :local_size=>2, :stack_max=>1},
+          "block in <compiled>", "<compiled>", :block, [:y], 0,
+          [[:break, nil, :label_5, :label_13, :label_13, 0],
+           [:redo, nil, :label_0, :label_13, :label_0, 0],
+           [:next, nil, :label_0, :label_13, :label_13, 0]],
+          [:label_0,
+           3,
+           [:putobject, 1],
+           [:setdynamic, 2, 0],
+           :label_5,
+           4,
+           [:putobject, 1],
+           [:send,
+            :times,
+            0,
+            ["YARVInstructionSequence/SimpleDataFormat", 1, 1, 1,
+             {:arg_size=>0, :local_size=>2, :stack_max=>4},
+             "block (2 levels) in <compiled>", "<compiled>", :block, [:z], 0,
+             [[:redo, nil, :label_0, :label_21, :label_0, 0],
+              [:next, nil, :label_0, :label_21, :label_21, 0]],
+             [:label_0,
+              5,
+              [:putobject, 1],
+              [:setdynamic, 2, 0],
+              6,
+              [:putnil],
+              [:getdynamic, 2, 2],
+              [:getdynamic, 2, 1],
+              [:getdynamic, 2, 0],
+              [:send, :test_ruby_test_verifier, 3, nil, 8, nil],
+              :label_21,
+              [:leave]]],
+            0,
+            nil],
+           :label_13,
+           [:leave]]],
+         0,
+         nil],
+        :label_12,
+        [:leave]]]
+    end
+  end
+
+  def test_getdynamic_ng
+    reject do
+      ["YARVInstructionSequence/SimpleDataFormat", 1, 1, 1,
+       {:arg_size=>0, :local_size=>1, :stack_max=>1},
+       "<compiled>", "<compiled>", :top, [], 0, [],
+       [1, [:getdynamic, 0, 0], [:leave]]]
+    end
+
+    reject do
+      ["YARVInstructionSequence/SimpleDataFormat", 1, 1, 1,
+       {:arg_size=>0, :local_size=>1, :stack_max=>1},
+       "<compiled>", "<compiled>", :top, [], 0, [],
+       [1, [:getdynamic, 0, 1], [:leave]]]
+    end
+  end
+
+  def test_uncaught_break
+    assert_raise(LocalJumpError) do
+      accept_exec do
+        ["YARVInstructionSequence/SimpleDataFormat", 1, 1, 1,
+         {:arg_size=>0, :local_size=>1, :stack_max=>1},
+         "<compiled>", "<compiled>", :top, [], 0, [],
+         [1, [:putnil], [:throw, 2], [:leave]]]
+      end
+    end
+  end
+
+  def test_getspecial_ok
+    # test_ruby_test_verifier $&
+    accept do
+      ["YARVInstructionSequence/SimpleDataFormat", 1, 1, 1,
+       {:arg_size=>0, :local_size=>1, :stack_max=>2},
+       "<compiled>", "<compiled>", :top, [], 0, [],
+       [1,
+        [:putnil],
+        [:getspecial, 1, ?&.ord << 1 | 1], # $&
+        [:send, :test_ruby_test_verifier, 1, nil, 8, nil],
+        [:leave]]]
+    end
+
+    # $_ = "...foo..."
+    # test_ruby_test_verifier $_ if /foo/
+    accept do
+      ["YARVInstructionSequence/SimpleDataFormat", 1, 1, 1,
+       {:arg_size=>0, :local_size=>1, :stack_max=>2},
+       "<compiled>", "<compiled>", :top, [], 0, [],
+        [1,
+         [:putstring, "...foo..."],
+         [:setglobal, :$_],
+         2,
+         [:putobject, /foo/],
+         [:getspecial, 0, 0],
+         [:opt_regexpmatch2],
+         [:branchunless, :label_23],
+         [:putnil],
+         [:getglobal, :$_],
+         [:send, :test_ruby_test_verifier, 1, nil, 8, nil],
+         [:leave],
+         [:pop],
+         :label_23,
+         [:putnil],
+         [:leave]]]
+    end
+  end
+
+  def test_getspecial_ng
+    # test_ruby_test_verifier $%  ???
+    reject do
+      ["YARVInstructionSequence/SimpleDataFormat", 1, 1, 1,
+       {:arg_size=>0, :local_size=>1, :stack_max=>2},
+       "<compiled>", "<compiled>", :top, [], 0, [],
+       [1,
+        [:putnil],
+        [:getspecial, 1, ?%.ord << 1 | 1], # $%
+        [:send, :test_ruby_test_verifier, 1, nil, 8, nil],
+        [:leave]]]
+    end
+
+    # $_ = "...foo..."
+    # test_ruby_test_verifier $_ if /foo/
+    reject do
+      ["YARVInstructionSequence/SimpleDataFormat", 1, 1, 1,
+       {:arg_size=>0, :local_size=>1, :stack_max=>2},
+       "<compiled>", "<compiled>", :top, [], 0, [],
+       [1,
+        [:putnil],
+        [:getspecial, nil, 0],
+        [:send, :test_ruby_test_verifier, 1, nil, 8, nil],
+        [:leave]]]
+    end
+
+    # $_ = "...foo..."
+    # test_ruby_test_verifier $_ if /foo/
+    reject do
+      ["YARVInstructionSequence/SimpleDataFormat", 1, 1, 1,
+       {:arg_size=>0, :local_size=>1, :stack_max=>2},
+       "<compiled>", "<compiled>", :top, [], 0, [],
+       [1,
+        [:getspecial, 1, 0],
+        [:send, :test_ruby_test_verifier, 1, nil, 8, nil],
+        [:leave]]]
+    end
+  end
+end

Property changes on: test/ruby/test_verifier.rb
___________________________________________________________________
Name: svn:eol-style
   + LF

Index: template/verifier.rb.tmpl
===================================================================
--- template/verifier.rb.tmpl	(revision 0)
+++ template/verifier.rb.tmpl	(revision 0)
@@ -0,0 +1,582 @@
+# -*-ruby-*-
+#  This file is a verifier for YARV bytecode.
+#  
+#  ----
+#  This file is auto generated by insns2vm.rb
+#  DO NOT TOUCH!
+#  
+#  If you want to fix something, you must edit 'template/verifier.rb.tmpl'
+#  or insns2vm.rb
+
+$debug = false
+
+class VM::InstructionSequence
+  def verify
+    VM::InstructionSequence::Verifier.verify(self)
+  end
+end
+
+module VM::InstructionSequence::Verifier
+  module_function
+
+  def verify(iseq)
+    iseq = iseq.to_a if iseq.is_a?(VM::InstructionSequence)
+    check_iseq(iseq, [])
+  end
+
+
+  class IseqVerificationError < ScriptError
+  end
+
+  def error(msg, *r)
+    raise(IseqVerificationError, msg % r)
+  end
+
+  SUPPORTED_MAGICS      = %w(YARVInstructionSequence/SimpleDataFormat)
+  SUPPORTED_VERSION     = [1, 1]
+  SUPPORTED_FORMAT_TYPE = 1
+
+  ISEQ_TYPES = [:top, :method, :block, :class, :rescue, :ensure, :eval, :defined_guard]
+  CATCH_TABLE_TYPES = [:rescue, :ensure, :retry, :break, :redo, :next]
+  CATCH_TABLE_SP_INC_TYPES = [:rescue, :break, :next]
+<%   BREAK_INSNS = ["leave", "jump", "opt_case_dispatch"] %>
+  INSN_ID_TYPES = {
+    :getinstancevariable => :instance,
+    :setinstancevariable => :instance,
+    :getclassvariable => :class,
+    :setclassvariable => :class,
+    :getconstant => :constant,
+    :setconstant => :constant,
+  }
+
+  def check_iseq(iseq, dvars_stack)
+    return unless iseq
+
+    # parse iseq
+    magic, major_version, minor_version, format_type, *iseq = iseq
+    misc, name, filename, type, locals, args, catch_table, bytecode = iseq
+    arg_size, local_size, stack_max =
+      [:arg_size, :local_size, :stack_max].map {|s| misc[s] }
+
+    # check whether the bytecode is supported
+    check_header(magic, major_version, minor_version, format_type, type)
+
+    # check whether the numbers of arguments and local variables is valid
+    check_args_and_locals(type, args, arg_size, local_size, locals)
+
+    # make label table (label -> index to the bytecode)
+    label_table = make_label_table(bytecode)
+
+    # extend dvars_stack
+    # (dvars_stack represents the number of local variables in each frame)
+    dvars_stack = [local_size] + dvars_stack
+
+    # check whether catch_table is valid
+    check_catch_table(catch_table, label_table, dvars_stack)
+
+    # make inference queue
+    # (inference queue means a list of pairs of index and stack depth)
+    # stack depth is 0 at the start of the bytecode
+    queue = [[0, 0]]
+    # catch_table specifies stack depth at cont_label
+    queue += make_sp_inference_queue(catch_table, label_table)
+
+    if $debug
+      require "pp"
+      puts "======== iseq ========"
+      pp catch_table
+      pp bytecode
+      puts "======== iseq end ========"
+      puts
+    end
+
+    # check bytecode
+    check_bytecode(bytecode, label_table, queue, dvars_stack, stack_max)
+  end
+
+  def check_header(magic, major_version, minor_version, format_type, type)
+    # check magic
+    unless SUPPORTED_MAGICS.any? {|m| m == magic }
+      error("unsupported magic: `%s'", magic)
+    end
+
+    # check version
+    unless ([major_version, minor_version] <=> SUPPORTED_VERSION) >= 0
+      error("unsupported version: %d.%d", major_version, minor_version)
+    end
+
+    # check format type
+    unless format_type == SUPPORTED_FORMAT_TYPE
+      error("unknown format_type: %d", format_type)
+    end
+
+    # check type
+    unless ISEQ_TYPES.include?(type)
+      error("unknown type: `%s'", type)
+    end
+  end
+
+  def check_args_and_locals(type, args, arg_size, local_size, locals)
+    if type != :defined_guard
+      unless arg_size <= local_size - 1
+        error("arg_size must be less than local_size: " +
+              "%d in %d", arg_size, local_size - 1)
+      end
+      unless locals.size <= local_size - 1
+        error("local variables exist more than local_size: " +
+              "%d in %d", locals.size, local_size - 1)
+      end
+      case args
+      when Fixnum
+        argc = args
+      when Array
+        argc, opt_labels, post_len, post_start, rest, block, simple = args
+        # todo: check the format of arguments
+      end
+    else
+      # if the type is defined_guard, arg_size and local_size have no sense.
+      error("arg_size must be 0 in defined_guard") unless arg_size == 0
+      error("local_size must be 0 in defined_guard") unless local_size == 0
+    end
+  end
+
+  def make_label_table(bytecode)
+    label_table = {}
+
+    bytecode.each_with_index do |ent, idx|
+      next unless ent.is_a?(Symbol)
+      error("duplicate label: `%s'", ent) if label_table[ent]
+      label_table[ent] = idx
+    end
+
+    label_table
+  end
+
+  def check_catch_table(catch_table, label_table, dvars_stack)
+    catch_table.each do |type, iseq, start_label, end_label, cont_label, sp|
+      unless CATCH_TABLE_TYPES.include?(type)
+        error("unknown type of catch table: `%s'", type)
+      end
+
+      check_iseq(iseq, dvars_stack)
+
+      [start_label, end_label, cont_label].each do |label|
+        unless label_table.include?(label)
+          error "unknown label: #{ start_label }"
+        end
+      end
+
+      unless label_table[start_label] <= label_table[end_label]
+        error("end_label `%s' exists before start_label `%s'",
+              end_label, start_label)
+      end
+    end
+  end
+
+  def make_sp_inference_queue(catch_table, label_table)
+    queue = []
+    catch_table.each do |type, iseq, start_label, end_label, cont_label, sp|
+      sp = CATCH_TABLE_SP_INC_TYPES.include?(type) ? sp + 1 : sp
+      queue << [label_table[cont_label], sp]
+    end
+    queue
+  end
+
+  def check_bytecode(bytecode, label_table, queue, dvars_stack, stack_max)
+    # stack depth table (index -> stack depth)
+    sp_table = [nil] * bytecode.size
+
+    # iterate until inference queue is empty
+    until queue.empty?
+      idx, sp = queue.shift
+
+      p [:start, idx, sp, queue] if $debug
+
+      while bytecode[idx] && sp
+        if sp_table[idx]
+          # stack depth of this insn is already inferred
+          break if sp_table[idx] == sp
+          error("stack consistency error")
+        end
+        sp_table[idx] = sp
+
+        # check stack overflow/underflow
+        unless sp <= stack_max
+          error("stack depth exceeds stack_max: %d over %d", sp, stack_max)
+        end
+        error("stack underflow") unless sp >= 0
+
+        p [sp, idx, bytecode[idx]] if $debug
+
+        case bytecode[idx]
+        when Fixnum  # line number
+          unless bytecode[idx] >= 0
+            error("negative line number: %d", bytecode[idx])
+          end
+        when Symbol  # label
+        when Array   # insn
+          sp = check_insn(*bytecode[idx], sp, dvars_stack, label_table, sp_table, queue)
+        else
+          error("unknown object")
+        end
+        idx += 1
+      end
+    end
+
+    if $debug
+      puts
+      puts "======== result ========"
+      sp_table.zip(bytecode) do |sp, ent|
+        p [sp, ent]
+      end
+      puts "======== end ========"
+    end
+
+    #error("dead code exists") if sp_table.include?(nil)
+  end
+
+
+  def check_operands_size(rands, size)
+    unless rands.size == size
+      error("wrong number of operands: %d for %d", rands.size, size)
+    end
+  end
+
+  def check_offset(label, sp, label_table, sp_table, queue)
+    error("offset must be symbol") unless label.is_a?(Symbol)
+
+    error("unknown label: `%s'", label) unless label_table[label]
+
+    if sp_table[label_table[label]] && sp_table[label_table[label]] != sp
+      error("stack consistency error")
+    end
+
+    queue << [label_table[label], sp]
+  end
+
+  def check_num(num, insn)
+    error("id must be fixnum") unless num.is_a?(Fixnum)
+  end
+
+  def check_index(index, dvars, msg)
+    error("invalid %s", msg) unless dvars && 1 <= index && index <= dvars
+  end
+
+  def check_value(value, insn)
+  end
+
+  def determine_id_type(id)  # slapdash
+    case id.to_s
+    when /^[a-z_]/ then :local
+    when /^[A-Z]/ then :constant
+    when /^@@/ then :class
+    when /^@/ then :instance
+    when /^\$/ then :global
+    when "==", "===", "!=", "<=>", "<", ">", "<=", "=>", "[]", "[]=",
+         "~", "&", "|", "^", "!", "=~", "!~", "+@", "-@",
+         "+", "-", "*", "/", "%", "**", "`", ">>", "<<"
+      :method
+    else
+      error("invalid id: `%s'", id)
+    end
+  end
+
+  def check_id(id, insn)
+    error("id must be symbol") unless id.is_a?(Symbol)
+    id_type = determine_id_type(id)
+    unless !INSN_ID_TYPES[insn] || id_type == INSN_ID_TYPES[insn]
+      error("%s must have %s variable identifier but does %s",
+            insn, INSN_ID_TYPES[insn], id_type)
+    end
+  end
+
+  def check_gentry(gentry)
+    error("gentry must be symbol") unless gentry.is_a?(Symbol)
+    unless determine_id_type(gentry) == :global
+      error("gentry must be global variable identifier")
+    end
+  end
+
+  def check_ic(ic)
+    error("ic must be nil") unless ic == nil
+  end
+
+  def check_cdhash(cdhash, sp, label_table, sp_table, queue)
+    cdhash.each_with_index do |label, idx|
+      next if idx % 2 == 0
+      check_offset(label, sp, label_table, sp_table, queue)
+    end
+  end
+
+  def check_insn(insn, *rands, sp, dvars_stack, label_table, sp_table, queue)
+    case insn
+<% insn_handlers.each do |insn, inc, opes| %>
+    when :<%= insn %>  # sig: [<%= opes.map {|type, var| type }.join(", ") %>]
+      # update sp
+      sp += <%= inc %>
+
+      # check operands
+      check_operands_size(rands, <%= opes.size %>)
+<%   opes.each_with_index do |(type, var), idx| %>
+<%     var = "rands[#{ idx }]" %>
+<% %>
+<% %>
+<%     case type %>
+<% %>
+<% %>
+<%     when "offset" %>
+<%       if insn != "setinlinecache" %>
+      check_offset(<%= var %>, sp, label_table, sp_table, queue)
+<%       end %>
+<% %>
+<% %>
+<%     when "num" %>
+      check_num(<%= var %>, :<%= insn %>)
+<% %>
+<% %>
+<%     when "lindex" %>
+      check_index(<%= var %>, dvars_stack.last, "lindex")
+<% %>
+<% %>
+<%     when "dindex" %>
+      check_index(<%= var %>, dvars_stack[rands[<%= idx + 1 %>]], "dindex")
+<% %>
+<% %>
+<%     when "value" %>
+      check_value(<%= var %>, :<%= insn %>)
+<% %>
+<% %>
+<%     when "id" %>
+      check_id(<%= var %>, :<%= insn %>)
+<% %>
+<% %>
+<%     when "gentry" %>
+      check_gentry(<%= var %>)
+<% %>
+<% %>
+<%     when "ic" %>
+      check_ic(<%= var %>)
+<% %>
+<% %>
+<%     when "iseq" %>
+<%       if insn == "definemethod" || insn == "defineclass" %>
+      check_iseq(<%= var %>, [])  # new scope
+<%       else %>
+      check_iseq(<%= var %>, dvars_stack)
+<%       end %>
+<% %>
+<% %>
+<%     when "cdhash" %>
+      check_cdhash(<%= var %>, sp, label_table, sp_table, queue)
+<% %>
+<% %>
+<%     else %>
+      error("<%= type %> unsupported")
+<% %>
+<% %>
+<%     end %>
+<%   end %>
+<% %>
+<% %>
+
+<%   case insn %>
+<%   when "getspecial" %>
+      if rands[1] == 0
+        unless rands[0] == 0 || rands[0].is_a?(String)
+          error("invalid special variable")
+        end
+      elsif rands[1] & 1 == 1
+        unless %w(& ` ' +).include?((rands[1] >> 1).chr)
+          error("invalid back-ref")
+        end
+      end
+
+<%   when "setspecial" %>
+      unless rands[0].is_a?(String)
+        error("invalid special variable")
+      end
+
+<%   when "putobject" %>
+      # todo: check the object
+
+<%   when "putstring" %>
+      unless rands[0].is_a?(String)
+        error("putstring must have a String")
+      end
+
+<%   when "concatstrings" %>
+      unless rands[0] > 0
+        error("concatstrings must have a positive number")
+      end
+
+<%   when "toregexp" %>
+      # todo: check the 1st operand (regexp option)
+      unless rands[1] >= 0
+        error("toregexp must have a nonnegative number")
+      end
+
+<%   when "newarray" %>
+      unless rands[0] >= 0
+        error("newarray must have a nonnegative number")
+      end
+
+<%   when "expandarray" %>
+      unless rands[0] >= 0
+        error("expandarray must have a nonnegative number")
+      end
+      unless 0 <= rands[1] && rands[1] < 4
+        error("expandarray flag must be a 2 bit number")
+      end
+
+<%   when "splatarray" %>
+      unless rands[0] == false
+        error("splatarray flag must be a boolean")
+      end
+
+<%   when "checkincludearray" %>
+      unless rands[0] == true || rands[0] == false
+        error("checkincludearray flag must be a boolean")
+      end
+
+<%   when "newhash" %>
+      unless rands[0] >= 0
+        error("newhash must have a nonnegative number")
+      end
+
+<%   when "newrange" %>
+      unless rands[0] == 0 || rands[0] == 1
+        error("newrange must have zero or one: %d", rands[0])
+      end
+
+<%   when "dupn" %>
+      unless rands[0] >= 0
+        error("dupn must have a nonnegative number")
+      end
+
+<%   when "topn" %>
+      unless rands[0] >= 0
+        error("topn must have a nonnegative number")
+      end
+
+<%   when "topn" %>
+      unless rands[0] >= 0
+        error("topn must have a nonnegative number")
+      end
+
+<%   when "setn" %>
+      unless rands[0] >= 0
+        error("setn must have a nonnegative number")
+      end
+
+<%   when "adjuststack" %>
+      unless rands[0] >= 0
+        error("adjuststack must have a nonnegative number")
+      end
+
+<%   when "definemethod" %>
+      unless rands[2] == 0 || rands[2] == 1
+        error("definemethod must have zero or one: %d", rands[0])
+      end
+
+<%   when "alias" %>
+      unless rands[0] == true || rands[0] == false
+        error("alias flag must be a boolean")
+      end
+
+<%   when "defined" %>
+      type = {
+         3 => "IVAR"  ,  5 => "IVAR2" ,  7 => "GVAR" ,  9 => "CVAR",
+        11 => "CONST" , 13 => "METHOD", 15 => "YIELD", 17 => "REF" ,
+        19 => "ZSUPER", 21 => "FUNC"
+      }[rands[0]]
+      case type
+      when "IVAR", "CVAR", "CONST", "METHOD", "FUNC"
+        unless rands[1].is_a?(Symbol)
+          error("defined %s must have a Symbol", type)
+        end
+      when "GVAR"
+        unless rands[1].is_a?(Fixnum)
+          error("defined %s must have a Fixnum", type)
+        end
+      when "REF"
+        unless rands[1].is_a?(Fixnum)
+          error("defined %s must have a Fixnum", type)
+        end
+        if rands[1] & 1 == 1
+          unless %w(& ` ' +).include?((rands[1] >> 1).chr)
+            error("invalid back-ref")
+          end
+        end
+      when "YIELD", "ZSUPER"
+        unless rands[1] == false
+          error("defined %s must have zero: %p", type, rands[1])
+        end
+      end
+
+<%   when "trace" %>
+      a = [0, 1, 2, 4, 8, 0x10, 0x20, 0x40, 0x80, 0xff, 0x100, 0x200]
+      unless a.include?(rands[0])
+        error("trace nf must be a RUBY_EVENT_*")
+      end
+
+<%   when "defineclass" %>
+      unless 0 <= rands[2] && rands[2] <= 2
+        error("defineclass define_type must be 0, 1 or 2")
+      end
+
+<%   when "send" %>
+      unless rands[1] >= 0
+        error("send op_argc must be a nonnegative number")
+      end
+
+<%   when "invokesuper" %>
+      unless rands[0] >= 0
+        error("invokesuper op_argc must be a nonnegative number")
+      end
+
+<%   when "invokeblock" %>
+      unless rands[0] >= 0
+        error("invokeblock num must be a nonnegative number")
+      end
+
+<%   when "leave" %>
+      # stack depth must be 1 when executing leave
+      error "stack consistency error" unless sp == 1
+
+<%   when "throw" %>
+      if [2, 3, 5].include?(rands[0] & 0xf)
+        unless rands[0] & 0x3ff0 == 0
+          error("throw flag is invalid: 0x%x", rands[0])
+        end
+      elsif [0, 1, 4].include?(rands[0])
+      else
+        error("throw flag is invalid: 0x%x", rands[0])
+      end
+
+<%   when "opt_regexpmatch1" %>
+      unless rands[0].is_a?(Regexp)
+        error("opt_regexpmatch1 must have a Regexp")
+      end
+
+<%   # todo: need more check %>
+<%   end %>
+<%   if BREAK_INSNS.include?(insn) %>
+      # after <%= insn %>, execution never follows to next insn
+      return
+
+<%   end %>
+<% end %>
+    end
+
+    sp
+  end
+end
+
+
+
+if $0 == __FILE__ && ARGV[0]
+
+iseq = VM::InstructionSequence.compile_file(ARGV[0]).to_a
+VM::InstructionSequence::Verifier.verify(iseq)
+
+end

Property changes on: template/verifier.rb.tmpl
___________________________________________________________________
Name: svn:eol-style
   + LF

*1:./sample/drb/dhasenc.rb とかを飛ばしてますが、これらは encoding の指定なしに日本語を含んでるため、元々動きません。

*2:ただしエラーにはしない。現状の YARV は、コンパイラの実装の都合上、デッドコードを意図的に埋め込むので。