バイトコード・ベリファイア

それぞれの命令を実行する直前の，オペラントスタックと ローカル変数の(型に関する)状態が， (ループなどを介して何度も違う経路で到達しても) 常に一定かつ適切であることをチェックする

• 上記チェックを通れば， 例えば，int に参照を足してしまうような誤りが起こらないことを， 命令のロード時にチェックできる．
  しかし，もし，ループなどである命令を実行する度に，スタックの型状態 が異なるなら， 必ず問題が起こるとは限らないにしても， その安全性を実行前(=ロード時)にチェックすることは不可能である．

• ベリファイアに正しく通る例(p.121改):

      iconst_3
      istore_1
  Label1:
      iload_1
      ifle Label2
      iinc 1 -1
      goto Label1
  Label2:
      return
  

  この表記に従い フレーム内の動作を記述すると，

  iconst_3
  local=[,  ] stack=[3]
  isotre_1
  local=[, 3] stack=[]
  iload_1
  local=[, 3] stack=[3]
  ifle Label2
  local=[, 3] stack=[]
  iinc 1 -1
  local=[, 2] stack=[]
  goto Label1
  local=[, 2] stack=[]
  iload_1
  local=[, 2] stack=[2]
  ifle Label2
  local=[, 2] stack=[]
  iinc 1 -1
  local=[, 1] stack=[]
  goto Label1
  local=[, 1] stack=[]
  iload_1
  local=[, 1] stack=[1]
  ifle Label2
  local=[, 1] stack=[]
  iinc 1 -1
  local=[, 0] stack=[]
  goto Label1
  local=[, 0] stack=[]
  iload_1
  local=[, 0] stack=[0]
  ifle Label2
  local=[, 0] stack=[]
  return
  

  例えば，もっとも危なそうな Label1の時点での型の状態は，
  local=[, int] stack=[]
  と一定であることがわかる．

• 最も簡単な不適切な例:

  iconst_0
  astore_1
  

  という命令列が変なのは明白である． この表記に従うと，

  iconst_1
  local=[ ] stack=[... 1]
  astore_1
  local=[ ] stack=[... 1] ???? 1は参照じゃないゾ
  

  ってことで誤りなのは，明白である． 要は 参照型に整数を代入しようとしている誤りである．

• 正しそうで，実はJavaベリファイア的にはダメな例 (p.119改)

      iconst_3
      istore_1
  Label1:
      aconst_null
      iinc 1 -1
      iload_1
      ifne Label1
      続く
  

  これも， この表記に従うと，

  iconst_3
  local=[this,  ] stack=[3, , , ]
  istore_1
  local=[this, 3] stack=[, , , ]
  aconst_null
  local=[this, 3] stack=[null, , , ]
  iinc 1 -1
  local=[this, 2] stack=[null, , , ]
  iload_1
  local=[this, 2] stack=[null, 2, , ] 参照, int
  
  ifne Label1
  local=[this, 2] stack=[null, , , ]
  aconst_null
  local=[this, 2] stack=[null, null, , ]
  iinc 1 -1
  local=[this, 1] stack=[null, null, , ]
  iload_1
  local=[this, 1] stack=[null, null, 1, ] 参照, 参照, int
  
  ifne Label1
  local=[this, 1] stack=[null, null, , ]
  aconst_null
  local=[this, 1] stack=[null, null, null, ]
  iinc 1 -1
  local=[this, 0] stack=[null, null, null, ]
  iload_1
  local=[this, 0] stack=[null, null, null, 0] 参照, 参照, 参照, int
  
  ifne Label1
  local=[this, 0] stack=[null, null, null, ]
  続く
  

  上記計算は，単にスタックにnullを3つ積むだけの処理であるが， アルゴリズム的には何の問題もない． しかし，例えば，上記 赤字で示しているifne直前のスタックの型の状態は， 毎回異なっていることがわかる．
  Javaはロード時のベリファイにおいて，このようなコードは門前払いする． (ただし，-verify時のみ)

  ちなみにこれをもっとも安直に書き正す例は，

  aconst_null
  aconst_null
  aconst_null
  

  である(笑)

$Id: ex.html,v 1.2 2000-07-02 20:30:33+09 kaiya Exp kaiya $