src/HOL/MicroJava/BV/LBVJVM.thy
author haftmann
Tue Nov 24 14:37:23 2009 +0100 (2009-11-24)
changeset 33954 1bc3b688548c
parent 33639 603320b93668
child 34227 33d44b1520c0
permissions -rwxr-xr-x
backported parts of abstract byte code verifier from AFP/Jinja
kleing@13215
     1
(*  Title:      HOL/MicroJava/BV/JVM.thy
kleing@13215
     2
    Author:     Tobias Nipkow, Gerwin Klein
kleing@13215
     3
    Copyright   2000 TUM
kleing@13215
     4
*)
kleing@13215
     5
kleing@13215
     6
header {* \isaheader{LBV for the JVM}\label{sec:JVM} *}
kleing@13215
     7
nipkow@17090
     8
theory LBVJVM
haftmann@33954
     9
imports Typing_Framework_JVM
nipkow@17090
    10
begin
kleing@13215
    11
wenzelm@26450
    12
types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> JVMType.state list"
kleing@13215
    13
kleing@13215
    14
constdefs
wenzelm@26450
    15
  check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool"
kleing@13215
    16
  "check_cert G mxs mxr n cert \<equiv> check_types G mxs mxr cert \<and> length cert = n+1 \<and>
kleing@13215
    17
                                 (\<forall>i<n. cert!i \<noteq> Err) \<and> cert!n = OK None"
kleing@13215
    18
kleing@13215
    19
  lbvjvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 
wenzelm@26450
    20
             JVMType.state list \<Rightarrow> instr list \<Rightarrow> JVMType.state \<Rightarrow> JVMType.state"
kleing@13215
    21
  "lbvjvm G maxs maxr rT et cert bs \<equiv>
kleing@13215
    22
  wtl_inst_list bs cert  (JVMType.sup G maxs maxr) (JVMType.le G maxs maxr) Err (OK None) (exec G maxs rT et bs) 0"
kleing@13215
    23
kleing@13215
    24
  wt_lbv :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
wenzelm@26450
    25
             exception_table \<Rightarrow> JVMType.state list \<Rightarrow> instr list \<Rightarrow> bool"
kleing@13215
    26
  "wt_lbv G C pTs rT mxs mxl et cert ins \<equiv>
kleing@13215
    27
   check_bounded ins et \<and> 
kleing@13215
    28
   check_cert G mxs (1+size pTs+mxl) (length ins) cert \<and>
kleing@13215
    29
   0 < size ins \<and> 
kleing@13215
    30
   (let start  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
kleing@13215
    31
        result = lbvjvm G mxs (1+size pTs+mxl) rT et cert ins (OK start)
kleing@13215
    32
    in result \<noteq> Err)"
kleing@13215
    33
kleing@13215
    34
  wt_jvm_prog_lbv :: "jvm_prog \<Rightarrow> prog_cert \<Rightarrow> bool"
kleing@13215
    35
  "wt_jvm_prog_lbv G cert \<equiv>
kleing@13215
    36
  wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_lbv G C (snd sig) rT maxs maxl et (cert C sig) b) G"
kleing@13215
    37
kleing@13215
    38
  mk_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list 
wenzelm@26450
    39
              \<Rightarrow> method_type \<Rightarrow> JVMType.state list"
kleing@13215
    40
  "mk_cert G maxs rT et bs phi \<equiv> make_cert (exec G maxs rT et bs) (map OK phi) (OK None)"
kleing@13215
    41
kleing@13215
    42
  prg_cert :: "jvm_prog \<Rightarrow> prog_type \<Rightarrow> prog_cert"
kleing@13215
    43
  "prg_cert G phi C sig \<equiv> let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 
kleing@13215
    44
                           mk_cert G maxs rT et ins (phi C sig)"
kleing@13215
    45
 
kleing@13215
    46
  
kleing@13215
    47
lemma wt_method_def2:
kleing@13215
    48
  fixes pTs and mxl and G and mxs and rT and et and bs and phi 
kleing@13215
    49
  defines [simp]: "mxr   \<equiv> 1 + length pTs + mxl"
kleing@13215
    50
  defines [simp]: "r     \<equiv> sup_state_opt G"
kleing@13215
    51
  defines [simp]: "app0  \<equiv> \<lambda>pc. app (bs!pc) G mxs rT pc et"
kleing@13215
    52
  defines [simp]: "step0 \<equiv> \<lambda>pc. eff (bs!pc) G pc et"
kleing@13215
    53
kleing@13215
    54
  shows
kleing@13215
    55
  "wt_method G C pTs rT mxs mxl bs et phi = 
kleing@13215
    56
  (bs \<noteq> [] \<and> 
kleing@13215
    57
   length phi = length bs \<and>
kleing@13215
    58
   check_bounded bs et \<and> 
kleing@13215
    59
   check_types G mxs mxr (map OK phi) \<and>   
kleing@13215
    60
   wt_start G C pTs mxl phi \<and> 
kleing@13215
    61
   wt_app_eff r app0 step0 phi)"
kleing@13215
    62
  by (auto simp add: wt_method_def wt_app_eff_def wt_instr_def lesub_def
kleing@13215
    63
           dest: check_bounded_is_bounded boundedD)
kleing@13215
    64
kleing@13215
    65
kleing@13224
    66
lemma check_certD:
kleing@13224
    67
  "check_cert G mxs mxr n cert \<Longrightarrow> cert_ok cert n Err (OK None) (states G mxs mxr)"
kleing@13224
    68
  apply (unfold cert_ok_def check_cert_def check_types_def)
nipkow@17090
    69
  apply (auto simp add: list_all_iff)
kleing@13224
    70
  done
kleing@13224
    71
kleing@13215
    72
kleing@13215
    73
lemma wt_lbv_wt_step:
kleing@13215
    74
  assumes wf:  "wf_prog wf_mb G"
kleing@13215
    75
  assumes lbv: "wt_lbv G C pTs rT mxs mxl et cert ins"
kleing@13215
    76
  assumes C:   "is_class G C" 
kleing@13215
    77
  assumes pTs: "set pTs \<subseteq> types G"
kleing@13215
    78
  
kleing@13215
    79
  defines [simp]: "mxr \<equiv> 1+length pTs+mxl"
kleing@13215
    80
kleing@13215
    81
  shows "\<exists>ts \<in> list (size ins) (states G mxs mxr). 
kleing@13215
    82
            wt_step (JVMType.le G mxs mxr) Err (exec G mxs rT et ins) ts
kleing@13215
    83
          \<and> OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) <=_(JVMType.le G mxs mxr) ts!0"
kleing@13215
    84
proof -
kleing@13215
    85
  let ?step = "exec G mxs rT et ins"
kleing@13215
    86
  let ?r    = "JVMType.le G mxs mxr"
kleing@13215
    87
  let ?f    = "JVMType.sup G mxs mxr"
kleing@13215
    88
  let ?A    = "states G mxs mxr"
kleing@13215
    89
streckem@14045
    90
  have "semilat (JVMType.sl G mxs mxr)" 
wenzelm@23467
    91
    by (rule semilat_JVM_slI, rule wf_prog_ws_prog, rule wf)
kleing@13215
    92
  hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
kleing@13215
    93
  moreover
kleing@13215
    94
  have "top ?r Err"  by (simp add: JVM_le_unfold)
kleing@13215
    95
  moreover
kleing@13215
    96
  have "Err \<in> ?A" by (simp add: JVM_states_unfold)
kleing@13215
    97
  moreover
kleing@13215
    98
  have "bottom ?r (OK None)" 
kleing@13215
    99
    by (simp add: JVM_le_unfold bottom_def)
kleing@13215
   100
  moreover
kleing@13215
   101
  have "OK None \<in> ?A" by (simp add: JVM_states_unfold)
kleing@13215
   102
  moreover
kleing@13215
   103
  from lbv
kleing@13215
   104
  have "bounded ?step (length ins)" 
kleing@13215
   105
    by (clarsimp simp add: wt_lbv_def exec_def) 
kleing@13215
   106
       (intro bounded_lift check_bounded_is_bounded) 
kleing@13215
   107
  moreover
kleing@13215
   108
  from lbv
kleing@13215
   109
  have "cert_ok cert (length ins) Err (OK None) ?A" 
kleing@13215
   110
    by (unfold wt_lbv_def) (auto dest: check_certD)
kleing@13215
   111
  moreover
wenzelm@23467
   112
  from wf have "pres_type ?step (length ins) ?A" by (rule exec_pres_type)
kleing@13215
   113
  moreover
kleing@13215
   114
  let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))"
kleing@13215
   115
  from lbv
kleing@13215
   116
  have "wtl_inst_list ins cert ?f ?r Err (OK None) ?step 0 ?start \<noteq> Err"
kleing@13215
   117
    by (simp add: wt_lbv_def lbvjvm_def)    
kleing@13215
   118
  moreover
kleing@13215
   119
  from C pTs have "?start \<in> ?A"
kleing@13215
   120
    by (unfold JVM_states_unfold) (auto intro: list_appendI, force)
kleing@13215
   121
  moreover
kleing@13215
   122
  from lbv have "0 < length ins" by (simp add: wt_lbv_def)
kleing@13215
   123
  ultimately
haftmann@27681
   124
  show ?thesis by (rule lbvs.wtl_sound_strong [OF lbvs.intro, OF lbv.intro lbvs_axioms.intro, OF Semilat.intro lbv_axioms.intro])
kleing@13215
   125
qed
kleing@13215
   126
  
kleing@13215
   127
lemma wt_lbv_wt_method:
kleing@13215
   128
  assumes wf:  "wf_prog wf_mb G"
kleing@13215
   129
  assumes lbv: "wt_lbv G C pTs rT mxs mxl et cert ins"
kleing@13215
   130
  assumes C:   "is_class G C" 
kleing@13215
   131
  assumes pTs: "set pTs \<subseteq> types G"
kleing@13215
   132
  
kleing@13215
   133
  shows "\<exists>phi. wt_method G C pTs rT mxs mxl ins et phi"
kleing@13215
   134
proof -
kleing@13215
   135
  let ?mxr   = "1 + length pTs + mxl"
kleing@13215
   136
  let ?step  = "exec G mxs rT et ins"
kleing@13215
   137
  let ?r     = "JVMType.le G mxs ?mxr"
kleing@13215
   138
  let ?f     = "JVMType.sup G mxs ?mxr"
kleing@13215
   139
  let ?A     = "states G mxs ?mxr"
kleing@13215
   140
  let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))"
kleing@13215
   141
  
kleing@13215
   142
  from lbv have l: "ins \<noteq> []" by (simp add: wt_lbv_def)
kleing@13215
   143
  moreover
kleing@13215
   144
  from wf lbv C pTs
kleing@13215
   145
  obtain phi where 
kleing@13215
   146
    list:  "phi \<in> list (length ins) ?A" and
kleing@13215
   147
    step:  "wt_step ?r Err ?step phi" and    
kleing@13215
   148
    start: "?start <=_?r phi!0" 
kleing@13215
   149
    by (blast dest: wt_lbv_wt_step)
kleing@13215
   150
  from list have [simp]: "length phi = length ins" by simp
kleing@13215
   151
  have "length (map ok_val phi) = length ins" by simp  
kleing@13215
   152
  moreover
kleing@13215
   153
  from l have 0: "0 < length phi" by simp
kleing@13215
   154
  with step obtain phi0 where "phi!0 = OK phi0"
kleing@13215
   155
    by (unfold wt_step_def) blast
kleing@13215
   156
  with start 0
kleing@13215
   157
  have "wt_start G C pTs mxl (map ok_val phi)"
kleing@13215
   158
    by (simp add: wt_start_def JVM_le_Err_conv lesub_def)
kleing@13215
   159
  moreover
kleing@13215
   160
  from lbv  have chk_bounded: "check_bounded ins et"
kleing@13215
   161
    by (simp add: wt_lbv_def)
kleing@13215
   162
  moreover {
kleing@13215
   163
    from list
kleing@13215
   164
    have "check_types G mxs ?mxr phi"
kleing@13215
   165
      by (simp add: check_types_def)
kleing@13215
   166
    also from step
kleing@13224
   167
    have [symmetric]: "map OK (map ok_val phi) = phi" 
hoelzl@33639
   168
      by (auto intro!: nth_equalityI simp add: wt_step_def)
kleing@13215
   169
    finally have "check_types G mxs ?mxr (map OK (map ok_val phi))" .
kleing@13215
   170
  }
kleing@13215
   171
  moreover {  
kleing@13215
   172
    let ?app = "\<lambda>pc. app (ins!pc) G mxs rT pc et"
kleing@13215
   173
    let ?eff = "\<lambda>pc. eff (ins!pc) G pc et"
kleing@13215
   174
kleing@13215
   175
    from chk_bounded
kleing@13215
   176
    have "bounded (err_step (length ins) ?app ?eff) (length ins)"
kleing@13215
   177
      by (blast dest: check_bounded_is_bounded boundedD intro: bounded_err_stepI)
kleing@13215
   178
    moreover
kleing@13215
   179
    from step
kleing@13215
   180
    have "wt_err_step (sup_state_opt G) ?step phi"
kleing@13215
   181
      by (simp add: wt_err_step_def JVM_le_Err_conv)
kleing@13215
   182
    ultimately
kleing@13215
   183
    have "wt_app_eff (sup_state_opt G) ?app ?eff (map ok_val phi)"
kleing@13215
   184
      by (auto intro: wt_err_imp_wt_app_eff simp add: exec_def)
kleing@13215
   185
  }    
kleing@13215
   186
  ultimately
kleing@13215
   187
  have "wt_method G C pTs rT mxs mxl ins et (map ok_val phi)"
kleing@13215
   188
    by - (rule wt_method_def2 [THEN iffD2], simp)
kleing@13215
   189
  thus ?thesis ..
kleing@13215
   190
qed
kleing@13215
   191
kleing@13215
   192
kleing@13215
   193
lemma wt_method_wt_lbv:
kleing@13215
   194
  assumes wf:  "wf_prog wf_mb G"
kleing@13215
   195
  assumes wt:  "wt_method G C pTs rT mxs mxl ins et phi"
kleing@13215
   196
  assumes C:   "is_class G C" 
kleing@13215
   197
  assumes pTs: "set pTs \<subseteq> types G"
kleing@13215
   198
  
kleing@13215
   199
  defines [simp]: "cert \<equiv> mk_cert G mxs rT et ins phi"
kleing@13215
   200
kleing@13215
   201
  shows "wt_lbv G C pTs rT mxs mxl et cert ins"
kleing@13215
   202
proof -
kleing@13215
   203
  let ?mxr  = "1 + length pTs + mxl"
kleing@13215
   204
  let ?step = "exec G mxs rT et ins"
kleing@13215
   205
  let ?app  = "\<lambda>pc. app (ins!pc) G mxs rT pc et"
kleing@13215
   206
  let ?eff  = "\<lambda>pc. eff (ins!pc) G pc et"
kleing@13215
   207
  let ?r    = "JVMType.le G mxs ?mxr"
kleing@13215
   208
  let ?f    = "JVMType.sup G mxs ?mxr"
kleing@13215
   209
  let ?A    = "states G mxs ?mxr"
kleing@13215
   210
  let ?phi  = "map OK phi"
kleing@13215
   211
  let ?cert = "make_cert ?step ?phi (OK None)"
kleing@13215
   212
kleing@13215
   213
  from wt obtain 
kleing@13215
   214
    0:          "0 < length ins" and
kleing@13215
   215
    length:     "length ins = length ?phi" and
kleing@13215
   216
    ck_bounded: "check_bounded ins et" and
kleing@13215
   217
    ck_types:   "check_types G mxs ?mxr ?phi" and
kleing@13215
   218
    wt_start:   "wt_start G C pTs mxl phi" and
kleing@13215
   219
    app_eff:    "wt_app_eff (sup_state_opt G) ?app ?eff phi"
berghofe@13601
   220
    by (simp (asm_lr) add: wt_method_def2)
kleing@13215
   221
  
streckem@14045
   222
  have "semilat (JVMType.sl G mxs ?mxr)" 
wenzelm@23467
   223
    by (rule semilat_JVM_slI) (rule wf_prog_ws_prog [OF wf])
kleing@13215
   224
  hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
kleing@13215
   225
  moreover
kleing@13215
   226
  have "top ?r Err"  by (simp add: JVM_le_unfold)
kleing@13215
   227
  moreover
kleing@13215
   228
  have "Err \<in> ?A" by (simp add: JVM_states_unfold)
kleing@13215
   229
  moreover
kleing@13215
   230
  have "bottom ?r (OK None)" 
kleing@13215
   231
    by (simp add: JVM_le_unfold bottom_def)
kleing@13215
   232
  moreover
kleing@13215
   233
  have "OK None \<in> ?A" by (simp add: JVM_states_unfold)
kleing@13215
   234
  moreover
kleing@13215
   235
  from ck_bounded
kleing@13215
   236
  have bounded: "bounded ?step (length ins)" 
kleing@13215
   237
    by (clarsimp simp add: exec_def) 
kleing@13215
   238
       (intro bounded_lift check_bounded_is_bounded)
kleing@13215
   239
  with wf
streckem@14045
   240
  have "mono ?r ?step (length ins) ?A"
streckem@14045
   241
    by (rule wf_prog_ws_prog [THEN exec_mono])
kleing@13215
   242
  hence "mono ?r ?step (length ?phi) ?A" by (simp add: length)
kleing@13215
   243
  moreover
wenzelm@23467
   244
  from wf have "pres_type ?step (length ins) ?A" by (rule exec_pres_type)
kleing@13215
   245
  hence "pres_type ?step (length ?phi) ?A" by (simp add: length)
kleing@13215
   246
  moreover
kleing@13215
   247
  from ck_types
kleing@13215
   248
  have "set ?phi \<subseteq> ?A" by (simp add: check_types_def) 
kleing@13215
   249
  hence "\<forall>pc. pc < length ?phi \<longrightarrow> ?phi!pc \<in> ?A \<and> ?phi!pc \<noteq> Err" by auto
kleing@13215
   250
  moreover 
kleing@13215
   251
  from bounded 
kleing@13215
   252
  have "bounded (exec G mxs rT et ins) (length ?phi)" by (simp add: length)
kleing@13215
   253
  moreover
kleing@13215
   254
  have "OK None \<noteq> Err" by simp
kleing@13215
   255
  moreover
kleing@13215
   256
  from bounded length app_eff
kleing@13215
   257
  have "wt_err_step (sup_state_opt G) ?step ?phi"
kleing@13215
   258
    by (auto intro: wt_app_eff_imp_wt_err simp add: exec_def)
kleing@13215
   259
  hence "wt_step ?r Err ?step ?phi"
kleing@13215
   260
    by (simp add: wt_err_step_def JVM_le_Err_conv)
kleing@13215
   261
  moreover 
kleing@13215
   262
  let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))"  
kleing@13215
   263
  from 0 length have "0 < length phi" by auto
kleing@13215
   264
  hence "?phi!0 = OK (phi!0)" by simp
kleing@13215
   265
  with wt_start have "?start <=_?r ?phi!0"
kleing@13215
   266
    by (clarsimp simp add: wt_start_def lesub_def JVM_le_Err_conv)
kleing@13215
   267
  moreover
kleing@13215
   268
  from C pTs have "?start \<in> ?A"
kleing@13215
   269
    by (unfold JVM_states_unfold) (auto intro: list_appendI, force)
kleing@13215
   270
  moreover
kleing@13215
   271
  have "?start \<noteq> Err" by simp
kleing@13215
   272
  moreover
kleing@13215
   273
  note length 
kleing@13215
   274
  ultimately
kleing@13215
   275
  have "wtl_inst_list ins ?cert ?f ?r Err (OK None) ?step 0 ?start \<noteq> Err"
haftmann@27681
   276
    by (rule lbvc.wtl_complete [OF lbvc.intro, OF lbv.intro lbvc_axioms.intro, OF Semilat.intro lbv_axioms.intro])
kleing@13215
   277
  moreover
kleing@13215
   278
  from 0 length have "phi \<noteq> []" by auto
kleing@13215
   279
  moreover
kleing@13215
   280
  from ck_types
kleing@13215
   281
  have "check_types G mxs ?mxr ?cert"
kleing@13215
   282
    by (auto simp add: make_cert_def check_types_def JVM_states_unfold)
kleing@13215
   283
  moreover
kleing@13215
   284
  note ck_bounded 0 length
kleing@13215
   285
  ultimately 
kleing@13215
   286
  show ?thesis 
kleing@13215
   287
    by (simp add: wt_lbv_def lbvjvm_def mk_cert_def 
kleing@13215
   288
      check_cert_def make_cert_def nth_append)
kleing@13215
   289
qed  
kleing@13215
   290
kleing@13215
   291
kleing@13224
   292
kleing@13224
   293
theorem jvm_lbv_correct:
kleing@13224
   294
  "wt_jvm_prog_lbv G Cert \<Longrightarrow> \<exists>Phi. wt_jvm_prog G Phi"
kleing@13224
   295
proof -  
kleing@13224
   296
  let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 
kleing@13224
   297
              SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"
kleing@13224
   298
    
kleing@13224
   299
  assume "wt_jvm_prog_lbv G Cert"
kleing@13224
   300
  hence "wt_jvm_prog G ?Phi"
kleing@13224
   301
    apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def)
kleing@13224
   302
    apply (erule jvm_prog_lift)
kleing@13224
   303
    apply (auto dest: wt_lbv_wt_method intro: someI)
kleing@13224
   304
    done
kleing@13224
   305
  thus ?thesis by blast
kleing@13224
   306
qed
kleing@13224
   307
kleing@13215
   308
theorem jvm_lbv_complete:
kleing@13215
   309
  "wt_jvm_prog G Phi \<Longrightarrow> wt_jvm_prog_lbv G (prg_cert G Phi)"
kleing@13224
   310
  apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def)
kleing@13224
   311
  apply (erule jvm_prog_lift)
wenzelm@19437
   312
  apply (auto simp add: prg_cert_def intro: wt_method_wt_lbv)
kleing@13224
   313
  done  
kleing@13215
   314
kleing@13215
   315
end