src/HOL/MicroJava/BV/JVM.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 22271 51a80e238b29
child 26450 158b924b5153
permissions -rw-r--r--
Name.uu, Name.aT;
kleing@12516
     1
(*  Title:      HOL/MicroJava/BV/JVM.thy
kleing@10592
     2
    ID:         $Id$
kleing@12516
     3
    Author:     Tobias Nipkow, Gerwin Klein
kleing@10592
     4
    Copyright   2000 TUM
kleing@10592
     5
*)
kleing@10592
     6
kleing@12911
     7
header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
kleing@10592
     8
haftmann@16417
     9
theory JVM imports Kildall Typing_Framework_JVM begin
kleing@13066
    10
kleing@10592
    11
kleing@10592
    12
constdefs
kleing@13006
    13
  kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 
kleing@13006
    14
             instr list \<Rightarrow> state list \<Rightarrow> state list"
kleing@12516
    15
  "kiljvm G maxs maxr rT et bs ==
kleing@12516
    16
  kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)"
kleing@10592
    17
kleing@12516
    18
  wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
kleing@12516
    19
             exception_table \<Rightarrow> instr list \<Rightarrow> bool"
kleing@12516
    20
  "wt_kil G C pTs rT mxs mxl et ins ==
kleing@13066
    21
   check_bounded ins et \<and> 0 < size ins \<and> 
kleing@10637
    22
   (let first  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
wenzelm@11701
    23
        start  = OK first#(replicate (size ins - 1) (OK None));
kleing@12516
    24
        result = kiljvm G mxs (1+size pTs+mxl) rT et ins start
kleing@10637
    25
    in \<forall>n < size ins. result!n \<noteq> Err)"
kleing@10637
    26
kleing@13006
    27
  wt_jvm_prog_kildall :: "jvm_prog \<Rightarrow> bool"
kleing@10637
    28
  "wt_jvm_prog_kildall G ==
kleing@12516
    29
  wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"
kleing@10592
    30
kleing@10592
    31
kleing@10592
    32
theorem is_bcv_kiljvm:
kleing@13066
    33
  "\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow>
kleing@12516
    34
      is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
kleing@12516
    35
             (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
kleing@10592
    36
  apply (unfold kiljvm_def sl_triple_conv)
kleing@10592
    37
  apply (rule is_bcv_kildall)
kleing@10592
    38
       apply (simp (no_asm) add: sl_triple_conv [symmetric]) 
streckem@14045
    39
       apply (force intro!: semilat_JVM_slI dest: wf_acyclic 
streckem@14045
    40
	 simp add: symmetric sl_triple_conv)
kleing@10592
    41
      apply (simp (no_asm) add: JVM_le_unfold)
kleing@10592
    42
      apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype
berghofe@22271
    43
                   dest: wf_subcls1 wfP_acyclicP wf_prog_ws_prog)
kleing@10592
    44
     apply (simp add: JVM_le_unfold)
kleing@10592
    45
    apply (erule exec_pres_type)
kleing@13066
    46
   apply assumption
streckem@14045
    47
  apply (drule wf_prog_ws_prog, erule exec_mono, assumption)  
kleing@10592
    48
  done
kleing@10592
    49
kleing@13224
    50
lemma subset_replicate: "set (replicate n x) \<subseteq> {x}"
kleing@13224
    51
  by (induct n) auto
kleing@13224
    52
kleing@13224
    53
lemma in_set_replicate:
kleing@13224
    54
  "x \<in> set (replicate n y) \<Longrightarrow> x = y"
kleing@13224
    55
proof -
kleing@13224
    56
  assume "x \<in> set (replicate n y)"
kleing@13224
    57
  also have "set (replicate n y) \<subseteq> {y}" by (rule subset_replicate)
kleing@13224
    58
  finally have "x \<in> {y}" .
kleing@13224
    59
  thus ?thesis by simp
kleing@13224
    60
qed
kleing@10637
    61
kleing@10637
    62
theorem wt_kil_correct:
kleing@13224
    63
  assumes wf:  "wf_prog wf_mb G"
kleing@13224
    64
  assumes C:   "is_class G C"
kleing@13224
    65
  assumes pTs: "set pTs \<subseteq> types G"
kleing@13224
    66
  
kleing@13224
    67
  assumes wtk: "wt_kil G C pTs rT maxs mxl et bs"
kleing@13224
    68
  
kleing@13224
    69
  shows "\<exists>phi. wt_method G C pTs rT maxs mxl bs et phi"
kleing@10592
    70
proof -
kleing@10592
    71
  let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
wenzelm@11701
    72
                #(replicate (size bs - 1) (OK None))"
kleing@10592
    73
kleing@13224
    74
  from wtk obtain maxr r where    
kleing@13066
    75
    bounded: "check_bounded bs et" and
kleing@12516
    76
    result:  "r = kiljvm G maxs maxr rT et bs ?start" and
kleing@10637
    77
    success: "\<forall>n < size bs. r!n \<noteq> Err" and
kleing@10637
    78
    instrs:  "0 < size bs" and
kleing@10637
    79
    maxr:    "maxr = Suc (length pTs + mxl)" 
kleing@10637
    80
    by (unfold wt_kil_def) simp
kleing@10592
    81
kleing@13066
    82
  from bounded have "bounded (exec G maxs rT et bs) (size bs)"
kleing@13066
    83
    by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)
kleing@13066
    84
  with wf have bcv:
kleing@12516
    85
    "is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) 
kleing@13066
    86
    (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
kleing@10592
    87
    by (rule is_bcv_kiljvm)
kleing@13066
    88
    
kleing@13224
    89
  from C pTs instrs maxr
kleing@10592
    90
  have "?start \<in> list (length bs) (states G maxs maxr)"
kleing@13224
    91
    apply (unfold JVM_states_unfold)
kleing@13224
    92
    apply (rule listI)
kleing@13224
    93
    apply (auto intro: list_appendI dest!: in_set_replicate)
kleing@13224
    94
    apply force
kleing@13224
    95
    done    
kleing@13224
    96
kleing@12516
    97
  with bcv success result have 
kleing@10592
    98
    "\<exists>ts\<in>list (length bs) (states G maxs maxr).
kleing@10812
    99
         ?start <=[JVMType.le G maxs maxr] ts \<and>
kleing@12516
   100
         wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) ts"
kleing@10592
   101
    by (unfold is_bcv_def) auto
kleing@10592
   102
  then obtain phi' where
kleing@13214
   103
    phi': "phi' \<in> list (length bs) (states G maxs maxr)" and
kleing@10812
   104
    s: "?start <=[JVMType.le G maxs maxr] phi'" and
kleing@12516
   105
    w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) phi'"
kleing@10592
   106
    by blast
kleing@13066
   107
  hence wt_err_step:
kleing@13066
   108
    "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) phi'"
kleing@13066
   109
    by (simp add: wt_err_step_def exec_def JVM_le_Err_conv)
kleing@10592
   110
kleing@12516
   111
  from s have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)"
kleing@10592
   112
    by (drule_tac p=0 in le_listD) (simp add: lesub_def)+
kleing@10592
   113
kleing@13214
   114
  from phi' have l: "size phi' = size bs" by simp  
kleing@12516
   115
  with instrs w have "phi' ! 0 \<noteq> Err" by (unfold wt_step_def) simp
kleing@12516
   116
  with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
kleing@13214
   117
    by (clarsimp simp add: not_Err_eq)  
kleing@13214
   118
kleing@13214
   119
  from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def)
kleing@13214
   120
  also from w have "phi' = map OK (map ok_val phi')" 
kleing@13224
   121
    apply (clarsimp simp add: wt_step_def not_Err_eq) 
kleing@13214
   122
    apply (rule map_id [symmetric])
kleing@13224
   123
    apply (erule allE, erule impE, assumption)
kleing@13224
   124
    apply clarsimp
kleing@13214
   125
    done    
kleing@13214
   126
  finally 
kleing@13214
   127
  have check_types:
kleing@13214
   128
    "check_types G maxs maxr (map OK (map ok_val phi'))" .
kleing@10592
   129
kleing@12516
   130
  from l bounded 
kleing@13067
   131
  have "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')"
kleing@13066
   132
    by (simp add: exec_def check_bounded_is_bounded)  
kleing@13067
   133
  hence bounded': "bounded (exec G maxs rT et bs) (length bs)"
kleing@13067
   134
    by (auto intro: bounded_lift simp add: exec_def l)
kleing@13066
   135
  with wt_err_step
kleing@13066
   136
  have "wt_app_eff (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) 
kleing@13066
   137
                   (\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')"
kleing@13067
   138
    by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def)
kleing@13214
   139
  with instrs l le bounded bounded' check_types maxr
kleing@12516
   140
  have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')"
kleing@13066
   141
    apply (unfold wt_method_def wt_app_eff_def)
kleing@10592
   142
    apply simp
kleing@10592
   143
    apply (rule conjI)
kleing@10592
   144
     apply (unfold wt_start_def)
kleing@10592
   145
     apply (rule JVM_le_convert [THEN iffD1])
kleing@10592
   146
     apply (simp (no_asm) add: phi0)
kleing@10592
   147
    apply clarify
kleing@10592
   148
    apply (erule allE, erule impE, assumption)
kleing@10592
   149
    apply (elim conjE)
kleing@10592
   150
    apply (clarsimp simp add: lesub_def wt_instr_def)
kleing@13067
   151
    apply (simp add: exec_def)
kleing@13067
   152
    apply (drule bounded_err_stepD, assumption+)
kleing@13067
   153
    apply blast
kleing@10592
   154
    done
kleing@10592
   155
kleing@10592
   156
  thus ?thesis by blast
kleing@10592
   157
qed
kleing@10592
   158
kleing@10651
   159
kleing@10651
   160
theorem wt_kil_complete:
kleing@13224
   161
  assumes wf:  "wf_prog wf_mb G"  
kleing@13224
   162
  assumes C:   "is_class G C"
kleing@13224
   163
  assumes pTs: "set pTs \<subseteq> types G"
kleing@13224
   164
kleing@13224
   165
  assumes wtm: "wt_method G C pTs rT maxs mxl bs et phi"
kleing@13224
   166
kleing@13224
   167
  shows "wt_kil G C pTs rT maxs mxl et bs"
kleing@10651
   168
proof -
kleing@13214
   169
  let ?mxr = "1+size pTs+mxl"
kleing@13214
   170
  
kleing@13224
   171
  from wtm obtain
kleing@10651
   172
    instrs:   "0 < length bs" and
kleing@13214
   173
    len:      "length phi = length bs" and
kleing@13214
   174
    bounded:  "check_bounded bs et" and
kleing@13214
   175
    ck_types: "check_types G maxs ?mxr (map OK phi)" and
kleing@10651
   176
    wt_start: "wt_start G C pTs mxl phi" and
kleing@10651
   177
    wt_ins:   "\<forall>pc. pc < length bs \<longrightarrow> 
kleing@12516
   178
                    wt_instr (bs ! pc) G rT phi maxs (length bs) et pc"
kleing@10651
   179
    by (unfold wt_method_def) simp
kleing@10651
   180
kleing@13214
   181
  from ck_types len
kleing@13214
   182
  have istype_phi: 
kleing@13214
   183
    "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"
kleing@13214
   184
    by (auto simp add: check_types_def intro!: listI)
kleing@13214
   185
kleing@12516
   186
  let ?eff  = "\<lambda>pc. eff (bs!pc) G pc et"
kleing@12516
   187
  let ?app   = "\<lambda>pc. app (bs!pc) G maxs rT pc et"
kleing@10651
   188
kleing@13066
   189
  from bounded
kleing@13066
   190
  have bounded_exec: "bounded (exec G maxs rT et bs) (size bs)"
kleing@13066
   191
    by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)
kleing@12516
   192
 
kleing@10651
   193
  from wt_ins
kleing@13066
   194
  have "wt_app_eff (sup_state_opt G) ?app ?eff phi"
kleing@13066
   195
    apply (unfold wt_app_eff_def wt_instr_def lesub_def)
kleing@13214
   196
    apply (simp (no_asm) only: len)
kleing@10651
   197
    apply blast
kleing@10651
   198
    done
kleing@13066
   199
  with bounded_exec
kleing@13066
   200
  have "wt_err_step (sup_state_opt G) (err_step (size phi) ?app ?eff) (map OK phi)"
kleing@13214
   201
    by - (erule wt_app_eff_imp_wt_err,simp add: exec_def len)
kleing@13066
   202
  hence wt_err:
kleing@13066
   203
    "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"
kleing@13214
   204
    by (unfold exec_def) (simp add: len)
kleing@10651
   205
 
kleing@12516
   206
  from wf bounded_exec
kleing@10651
   207
  have is_bcv: 
kleing@13224
   208
    "is_bcv (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs) 
kleing@13224
   209
            (size bs) (states G maxs ?mxr) (kiljvm G maxs ?mxr rT et bs)"
kleing@10651
   210
    by (rule is_bcv_kiljvm)
kleing@10651
   211
kleing@10651
   212
  let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
wenzelm@11701
   213
                #(replicate (size bs - 1) (OK None))"
kleing@10651
   214
kleing@13224
   215
  from C pTs instrs
kleing@13224
   216
  have start: "?start \<in> list (length bs) (states G maxs ?mxr)"
kleing@13224
   217
    apply (unfold JVM_states_unfold)
kleing@13224
   218
    apply (rule listI)
kleing@13224
   219
    apply (auto intro!: list_appendI dest!: in_set_replicate)
kleing@13224
   220
    apply force
kleing@13224
   221
    done    
kleing@10651
   222
kleing@12516
   223
  let ?phi = "map OK phi"  
kleing@13224
   224
  have less_phi: "?start <=[JVMType.le G maxs ?mxr] ?phi"
kleing@10657
   225
  proof -
kleing@13214
   226
    from len instrs
kleing@12516
   227
    have "length ?start = length (map OK phi)" by simp
kleing@12516
   228
    moreover
kleing@10657
   229
    { fix n
kleing@10657
   230
      from wt_start
kleing@10657
   231
      have "G \<turnstile> ok_val (?start!0) <=' phi!0"
kleing@10657
   232
        by (simp add: wt_start_def)
kleing@10657
   233
      moreover
kleing@13214
   234
      from instrs len
kleing@10657
   235
      have "0 < length phi" by simp
kleing@10657
   236
      ultimately
kleing@13224
   237
      have "JVMType.le G maxs ?mxr (?start!0) (?phi!0)"
kleing@10657
   238
        by (simp add: JVM_le_Err_conv Err.le_def lesub_def)
kleing@10657
   239
      moreover
kleing@10657
   240
      { fix n'
kleing@13224
   241
        have "JVMType.le G maxs ?mxr (OK None) (?phi!n)"
kleing@10657
   242
          by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def 
kleing@10657
   243
            split: err.splits)        
kleing@13006
   244
        hence "\<lbrakk> n = Suc n'; n < length ?start \<rbrakk> 
kleing@13224
   245
          \<Longrightarrow> JVMType.le G maxs ?mxr (?start!n) (?phi!n)"
kleing@10657
   246
          by simp
kleing@10657
   247
      }
kleing@10657
   248
      ultimately
kleing@13224
   249
      have "n < length ?start \<Longrightarrow> (?start!n) <=_(JVMType.le G maxs ?mxr) (?phi!n)"
kleing@12516
   250
        by (unfold lesub_def) (cases n, blast+)
kleing@12516
   251
    } 
kleing@12516
   252
    ultimately show ?thesis by (rule le_listI)
kleing@10657
   253
  qed         
kleing@10651
   254
kleing@13066
   255
  from wt_err
kleing@13224
   256
  have "wt_step (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs) ?phi"
kleing@13066
   257
    by (simp add: wt_err_step_def JVM_le_Err_conv)  
kleing@12516
   258
  with start istype_phi less_phi is_bcv
kleing@13224
   259
  have "\<forall>p. p < length bs \<longrightarrow> kiljvm G maxs ?mxr rT et bs ?start ! p \<noteq> Err"
kleing@12516
   260
    by (unfold is_bcv_def) auto
kleing@13066
   261
  with bounded instrs
kleing@12516
   262
  show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp
kleing@12516
   263
qed
kleing@10651
   264
kleing@10637
   265
kleing@13214
   266
theorem jvm_kildall_sound_complete:
kleing@13214
   267
  "wt_jvm_prog_kildall G = (\<exists>Phi. wt_jvm_prog G Phi)"
kleing@13214
   268
proof 
kleing@12516
   269
  let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 
kleing@12516
   270
              SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"
kleing@13224
   271
  
kleing@13224
   272
  assume "wt_jvm_prog_kildall G"
kleing@13224
   273
  hence "wt_jvm_prog G ?Phi"
kleing@13224
   274
    apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)
kleing@13224
   275
    apply (erule jvm_prog_lift)
kleing@13224
   276
    apply (auto dest!: wt_kil_correct intro: someI)
kleing@10637
   277
    done
kleing@13224
   278
  thus "\<exists>Phi. wt_jvm_prog G Phi" by fast
kleing@13214
   279
next
kleing@13214
   280
  assume "\<exists>Phi. wt_jvm_prog G Phi"
kleing@13224
   281
  thus "wt_jvm_prog_kildall G"
kleing@13224
   282
    apply (clarify)
kleing@13224
   283
    apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)
kleing@13224
   284
    apply (erule jvm_prog_lift)
kleing@13224
   285
    apply (auto intro: wt_kil_complete)
kleing@13214
   286
    done
kleing@10637
   287
qed
kleing@10637
   288
kleing@10592
   289
end