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