src/HOL/MicroJava/BV/BVNoTypeError.thy
author haftmann
Tue Nov 24 14:37:23 2009 +0100 (2009-11-24)
changeset 33954 1bc3b688548c
parent 32960 69916a850301
child 42150 b0c0638c4aad
permissions -rwxr-xr-x
backported parts of abstract byte code verifier from AFP/Jinja
     1 (*  Title:      HOL/MicroJava/BV/BVNoTypeErrors.thy
     2     Author:     Gerwin Klein
     3 *)
     4 
     5 header {* \isaheader{Welltyped Programs produce no Type Errors} *}
     6 
     7 theory BVNoTypeError
     8 imports "../JVM/JVMDefensive" BVSpecTypeSafe
     9 begin
    10 
    11 text {*
    12   Some simple lemmas about the type testing functions of the
    13   defensive JVM:
    14 *}
    15 lemma typeof_NoneD [simp,dest]:
    16   "typeof (\<lambda>v. None) v = Some x \<Longrightarrow> \<not>isAddr v"
    17   by (cases v) auto
    18 
    19 lemma isRef_def2:
    20   "isRef v = (v = Null \<or> (\<exists>loc. v = Addr loc))"
    21   by (cases v) (auto simp add: isRef_def)
    22 
    23 lemma app'Store[simp]:
    24   "app' (Store idx, G, pc, maxs, rT, (ST,LT)) = (\<exists>T ST'. ST = T#ST' \<and> idx < length LT)"
    25   by (cases ST, auto)
    26 
    27 lemma app'GetField[simp]:
    28   "app' (Getfield F C, G, pc, maxs, rT, (ST,LT)) =  
    29   (\<exists>oT vT ST'. ST = oT#ST' \<and> is_class G C \<and>  
    30   field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> Class C)"
    31   by (cases ST, auto)
    32 
    33 lemma app'PutField[simp]:
    34 "app' (Putfield F C, G,  pc, maxs, rT, (ST,LT)) = 
    35  (\<exists>vT vT' oT ST'. ST = vT#oT#ST' \<and> is_class G C \<and> 
    36   field (G,C) F = Some (C, vT') \<and> 
    37   G \<turnstile> oT \<preceq> Class C \<and> G \<turnstile> vT \<preceq> vT')"
    38   apply rule
    39   defer
    40   apply clarsimp
    41   apply (cases ST)
    42   apply simp
    43   apply (cases "tl ST")
    44   apply auto
    45   done
    46 
    47 lemma app'Checkcast[simp]:
    48 "app' (Checkcast C, G, pc, maxs, rT, (ST,LT)) =
    49  (\<exists>rT ST'. ST = RefT rT#ST' \<and> is_class G C)"
    50 apply rule
    51 defer
    52 apply clarsimp
    53 apply (cases ST)
    54 apply simp
    55 apply (cases "hd ST")
    56 defer 
    57 apply simp
    58 apply simp
    59 done
    60 
    61 
    62 lemma app'Pop[simp]: 
    63   "app' (Pop, G, pc, maxs, rT, (ST,LT)) = (\<exists>T ST'. ST = T#ST')"
    64   by (cases ST, auto)
    65 
    66 
    67 lemma app'Dup[simp]:
    68   "app' (Dup, G, pc, maxs, rT, (ST,LT)) =
    69   (\<exists>T ST'. ST = T#ST' \<and> length ST < maxs)"
    70   by (cases ST, auto)
    71  
    72 
    73 lemma app'Dup_x1[simp]:
    74   "app' (Dup_x1, G, pc, maxs, rT, (ST,LT)) = 
    75   (\<exists>T1 T2 ST'. ST = T1#T2#ST' \<and> length ST < maxs)"
    76   by (cases ST, simp, cases "tl ST", auto)
    77 
    78   
    79 lemma app'Dup_x2[simp]:
    80   "app' (Dup_x2, G, pc, maxs, rT, (ST,LT)) = 
    81   (\<exists>T1 T2 T3 ST'. ST = T1#T2#T3#ST' \<and> length ST < maxs)"
    82   by (cases ST, simp, cases "tl ST", simp, cases "tl (tl ST)", auto)
    83 
    84 
    85 lemma app'Swap[simp]:
    86   "app' (Swap, G, pc, maxs, rT, (ST,LT)) = (\<exists>T1 T2 ST'. ST = T1#T2#ST')" 
    87   by (cases ST, simp, cases "tl ST", auto)
    88 
    89   
    90 lemma app'IAdd[simp]:
    91   "app' (IAdd, G, pc, maxs, rT, (ST,LT)) = 
    92   (\<exists>ST'. ST = PrimT Integer#PrimT Integer#ST')"
    93   apply (cases ST)
    94   apply simp
    95   apply simp
    96   apply (case_tac a)
    97   apply auto
    98   apply (case_tac prim_ty)
    99   apply auto
   100   apply (case_tac prim_ty)
   101   apply auto
   102   apply (case_tac list)
   103   apply auto
   104   apply (case_tac a)
   105   apply auto
   106   apply (case_tac prim_ty)
   107   apply auto
   108   done
   109  
   110 
   111 lemma app'Ifcmpeq[simp]:
   112   "app' (Ifcmpeq b, G, pc, maxs, rT, (ST,LT)) =
   113   (\<exists>T1 T2 ST'. ST = T1#T2#ST' \<and> 0 \<le> b + int pc \<and> 
   114   ((\<exists>p. T1 = PrimT p \<and> T1 = T2) \<or> 
   115   (\<exists>r r'. T1 = RefT r \<and> T2 = RefT r')))" 
   116   apply auto
   117   apply (cases ST)
   118   apply simp
   119   apply (cases "tl ST")
   120   apply (case_tac a)
   121   apply auto
   122   done
   123   
   124 
   125 lemma app'Return[simp]:
   126   "app' (Return, G, pc, maxs, rT, (ST,LT)) = 
   127   (\<exists>T ST'. ST = T#ST'\<and> G \<turnstile> T \<preceq> rT)" 
   128   by (cases ST, auto)
   129 
   130 
   131 lemma app'Throw[simp]:
   132   "app' (Throw, G, pc, maxs, rT, (ST,LT)) = 
   133   (\<exists>ST' r. ST = RefT r#ST')"
   134   apply (cases ST, simp)
   135   apply (cases "hd ST")
   136   apply auto
   137   done
   138 
   139   
   140 lemma app'Invoke[simp]:
   141 "app' (Invoke C mn fpTs, G, pc, maxs, rT, ST, LT) = 
   142  (\<exists>apTs X ST' mD' rT' b'.
   143   ST = (rev apTs) @ X # ST' \<and> 
   144   length apTs = length fpTs \<and> is_class G C \<and>
   145   (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and> 
   146   method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> G \<turnstile> X \<preceq> Class C)"
   147   (is "?app ST LT = ?P ST LT")
   148 proof
   149   assume "?P ST LT" thus "?app ST LT" by (auto simp add: list_all2_def)
   150 next  
   151   assume app: "?app ST LT"
   152   hence l: "length fpTs < length ST" by simp
   153   obtain xs ys where xs: "ST = xs @ ys" "length xs = length fpTs"
   154   proof -
   155     have "ST = take (length fpTs) ST @ drop (length fpTs) ST" by simp
   156     moreover from l have "length (take (length fpTs) ST) = length fpTs"
   157       by simp
   158     ultimately show ?thesis ..
   159   qed
   160   obtain apTs where
   161     "ST = (rev apTs) @ ys" and "length apTs = length fpTs"
   162   proof -
   163     from xs(1) have "ST = rev (rev xs) @ ys" by simp
   164     then show thesis by (rule that) (simp add: xs(2))
   165   qed
   166   moreover
   167   from l xs obtain X ST' where "ys = X#ST'" by (auto simp add: neq_Nil_conv)
   168   ultimately
   169   have "ST = (rev apTs) @ X # ST'" "length apTs = length fpTs" by auto
   170   with app
   171   show "?P ST LT"
   172     apply (clarsimp simp add: list_all2_def)
   173     apply ((rule exI)+, (rule conjI)?)+
   174     apply auto
   175     done
   176 qed
   177 
   178 lemma approx_loc_len [simp]:
   179   "approx_loc G hp loc LT \<Longrightarrow> length loc = length LT"
   180   by (simp add: approx_loc_def list_all2_def)
   181 
   182 lemma approx_stk_len [simp]:
   183   "approx_stk G hp stk ST \<Longrightarrow> length stk = length ST"
   184   by (simp add: approx_stk_def)
   185 
   186 lemma isRefI [intro, simp]: "G,hp \<turnstile> v ::\<preceq> RefT T \<Longrightarrow> isRef v"
   187   apply (drule conf_RefTD)
   188   apply (auto simp add: isRef_def)
   189   done
   190 
   191 lemma isIntgI [intro, simp]: "G,hp \<turnstile> v ::\<preceq> PrimT Integer \<Longrightarrow> isIntg v"
   192   apply (unfold conf_def)
   193   apply auto
   194   apply (erule widen.cases)
   195   apply auto
   196   apply (cases v)
   197   apply auto
   198   done
   199 
   200 lemma list_all2_approx:
   201   "\<And>s. list_all2 (approx_val G hp) s (map OK S) = 
   202        list_all2 (conf G hp) s S"
   203   apply (induct S)
   204   apply (auto simp add: list_all2_Cons2 approx_val_def)
   205   done
   206 
   207 lemma list_all2_conf_widen:
   208   "wf_prog mb G \<Longrightarrow>
   209   list_all2 (conf G hp) a b \<Longrightarrow>
   210   list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) b c \<Longrightarrow>
   211   list_all2 (conf G hp) a c"
   212   apply (rule list_all2_trans)
   213   defer
   214   apply assumption
   215   apply assumption
   216   apply (drule conf_widen, assumption+)
   217   done
   218 
   219 
   220 text {*
   221   The main theorem: welltyped programs do not produce type errors if they
   222   are started in a conformant state.
   223 *}
   224 theorem no_type_error:
   225   assumes welltyped: "wt_jvm_prog G Phi" and conforms: "G,Phi \<turnstile>JVM s \<surd>"
   226   shows "exec_d G (Normal s) \<noteq> TypeError"
   227 proof -
   228   from welltyped obtain mb where wf: "wf_prog mb G" by (fast dest: wt_jvm_progD)
   229   
   230   obtain xcp hp frs where s [simp]: "s = (xcp, hp, frs)" by (cases s)
   231 
   232   from conforms have "xcp \<noteq> None \<or> frs = [] \<Longrightarrow> check G s" 
   233     by (unfold correct_state_def check_def) auto
   234   moreover {
   235     assume "\<not>(xcp \<noteq> None \<or> frs = [])"
   236     then obtain stk loc C sig pc frs' where
   237       xcp [simp]: "xcp = None" and
   238       frs [simp]: "frs = (stk,loc,C,sig,pc)#frs'" 
   239       by (clarsimp simp add: neq_Nil_conv) fast
   240 
   241     from conforms obtain  ST LT rT maxs maxl ins et where
   242       hconf:  "G \<turnstile>h hp \<surd>" and
   243       "class":  "is_class G C" and
   244       meth:   "method (G, C) sig = Some (C, rT, maxs, maxl, ins, et)" and
   245       phi:    "Phi C sig ! pc = Some (ST,LT)" and
   246       frame:  "correct_frame G hp (ST,LT) maxl ins (stk,loc,C,sig,pc)" and
   247       frames: "correct_frames G hp Phi rT sig frs'"
   248       by (auto simp add: correct_state_def) (rule that)
   249 
   250     from frame obtain
   251       stk: "approx_stk G hp stk ST" and
   252       loc: "approx_loc G hp loc LT" and
   253       pc:  "pc < length ins" and
   254       len: "length loc = length (snd sig) + maxl + 1"
   255       by (auto simp add: correct_frame_def)
   256 
   257     note approx_val_def [simp]
   258 
   259     from welltyped meth conforms
   260     have "wt_instr (ins!pc) G rT (Phi C sig) maxs (length ins) et pc"
   261       by simp (rule wt_jvm_prog_impl_wt_instr_cor)    
   262     then obtain
   263       app': "app (ins!pc) G maxs rT pc et (Phi C sig!pc) " and
   264       eff: "\<forall>(pc', s')\<in>set (eff (ins ! pc) G pc et (Phi C sig ! pc)). pc' < length ins"
   265       by (simp add: wt_instr_def phi) blast
   266 
   267     from eff 
   268     have pc': "\<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins"
   269       by (simp add: eff_def) blast
   270 
   271     from app' phi
   272     have app:
   273       "xcpt_app (ins!pc) G pc et \<and> app' (ins!pc, G, pc, maxs, rT, (ST,LT))"
   274       by (clarsimp simp add: app_def)
   275 
   276     with eff stk loc pc'
   277     have "check_instr (ins!pc) G hp stk loc C sig pc maxs frs'"
   278     proof (cases "ins!pc")
   279       case (Getfield F C) 
   280       with app stk loc phi obtain v vT stk' where
   281         "class": "is_class G C" and
   282         field: "field (G, C) F = Some (C, vT)" and
   283         stk:   "stk = v # stk'" and
   284         conf:  "G,hp \<turnstile> v ::\<preceq> Class C"
   285         apply clarsimp
   286         apply (blast dest: conf_widen [OF wf])
   287         done
   288       from conf have isRef: "isRef v" ..
   289       moreover {
   290         assume "v \<noteq> Null" 
   291         with conf field isRef wf
   292         have "\<exists>D vs. hp (the_Addr v) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C" 
   293           by (auto dest!: non_np_objD)
   294       }
   295       ultimately show ?thesis using Getfield field "class" stk hconf wf
   296         apply clarsimp
   297         apply (fastsimp intro: wf_prog_ws_prog
   298           dest!: hconfD widen_cfs_fields oconf_objD)
   299         done
   300     next
   301       case (Putfield F C)
   302       with app stk loc phi obtain v ref vT stk' where
   303         "class": "is_class G C" and
   304         field: "field (G, C) F = Some (C, vT)" and
   305         stk:   "stk = v # ref # stk'" and
   306         confv: "G,hp \<turnstile> v ::\<preceq> vT" and
   307         confr: "G,hp \<turnstile> ref ::\<preceq> Class C"
   308         apply clarsimp
   309         apply (blast dest: conf_widen [OF wf])
   310         done
   311       from confr have isRef: "isRef ref" ..
   312       moreover {
   313         assume "ref \<noteq> Null" 
   314         with confr field isRef wf
   315         have "\<exists>D vs. hp (the_Addr ref) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C"
   316           by (auto dest: non_np_objD)
   317       }
   318       ultimately show ?thesis using Putfield field "class" stk confv
   319         by clarsimp
   320     next      
   321       case (Invoke C mn ps)
   322       with app
   323       obtain apTs X ST' where
   324         ST: "ST = rev apTs @ X # ST'" and
   325         ps: "length apTs = length ps" and
   326         w:   "\<forall>(x, y)\<in>set (zip apTs ps). G \<turnstile> x \<preceq> y" and
   327         C:   "G \<turnstile> X \<preceq> Class C" and
   328         mth: "method (G, C) (mn, ps) \<noteq> None"
   329         by (simp del: app'.simps) blast
   330         
   331       from ST stk
   332       obtain aps x stk' where
   333         stk': "stk = aps @ x # stk'" and
   334         aps: "approx_stk G hp aps (rev apTs)" and
   335         x: "G,hp \<turnstile> x ::\<preceq> X" and        
   336         l: "length aps = length apTs"
   337         by (auto dest!: approx_stk_append)
   338       
   339       from stk' l ps 
   340       have [simp]: "stk!length ps = x" by (simp add: nth_append)
   341       from stk' l ps
   342       have [simp]: "take (length ps) stk = aps" by simp
   343       from w ps
   344       have widen: "list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs ps"
   345         by (simp add: list_all2_def) 
   346 
   347       from stk' l ps have "length ps < length stk" by simp
   348       moreover
   349       from wf x C 
   350       have x: "G,hp \<turnstile> x ::\<preceq> Class C" by (rule conf_widen) 
   351       hence "isRef x" by simp
   352       moreover
   353       { assume "x \<noteq> Null"
   354         with x
   355         obtain D fs where
   356           hp: "hp (the_Addr x) = Some (D,fs)" and
   357           D:  "G \<turnstile> D \<preceq>C C"
   358           by - (drule non_npD, assumption, clarsimp, blast)
   359         hence "hp (the_Addr x) \<noteq> None" (is ?P1) by simp
   360         moreover
   361         from wf mth hp D
   362         have "method (G, cname_of hp x) (mn, ps) \<noteq> None" (is ?P2)
   363           by (auto dest: subcls_widen_methd)
   364         moreover
   365         from aps have "list_all2 (conf G hp) aps (rev apTs)"
   366           by (simp add: list_all2_approx approx_stk_def approx_loc_def)        
   367         hence "list_all2 (conf G hp) (rev aps) (rev (rev apTs))"
   368           by (simp only: list_all2_rev)
   369         hence "list_all2 (conf G hp) (rev aps) apTs" by simp
   370         with wf widen        
   371         have "list_all2 (conf G hp) (rev aps) ps" (is ?P3)
   372           by - (rule list_all2_conf_widen) 
   373         ultimately
   374         have "?P1 \<and> ?P2 \<and> ?P3" by blast
   375       }
   376       moreover 
   377       note Invoke
   378       ultimately
   379       show ?thesis by simp
   380     next
   381       case Return with stk app phi meth frames 
   382       show ?thesis        
   383         apply clarsimp
   384         apply (drule conf_widen [OF wf], assumption)
   385         apply (clarsimp simp add: neq_Nil_conv isRef_def2)
   386         done
   387     qed auto
   388     hence "check G s" by (simp add: check_def meth pc)
   389   } ultimately
   390   have "check G s" by blast
   391   thus "exec_d G (Normal s) \<noteq> TypeError" ..
   392 qed
   393 
   394 
   395 text {*
   396   The theorem above tells us that, in welltyped programs, the
   397   defensive machine reaches the same result as the aggressive
   398   one (after arbitrarily many steps).
   399 *}
   400 theorem welltyped_aggressive_imp_defensive:
   401   "wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd> \<Longrightarrow> G \<turnstile> s -jvm\<rightarrow> t 
   402   \<Longrightarrow> G \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t)"
   403   apply (unfold exec_all_def) 
   404   apply (erule rtrancl_induct)
   405    apply (simp add: exec_all_d_def)
   406   apply simp
   407   apply (fold exec_all_def)
   408   apply (frule BV_correct, assumption+)
   409   apply (drule no_type_error, assumption, drule no_type_error_commutes, simp)
   410   apply (simp add: exec_all_d_def)
   411   apply (rule rtrancl_trans, assumption)
   412   apply blast
   413   done
   414 
   415 
   416 lemma neq_TypeError_eq [simp]: "s \<noteq> TypeError = (\<exists>s'. s = Normal s')"
   417   by (cases s, auto)
   418 
   419 theorem no_type_errors:
   420   "wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd>
   421   \<Longrightarrow> G \<turnstile> (Normal s) -jvmd\<rightarrow> t \<Longrightarrow> t \<noteq> TypeError"
   422   apply (unfold exec_all_d_def)   
   423   apply (erule rtrancl_induct)
   424    apply simp
   425   apply (fold exec_all_d_def)
   426   apply (auto dest: defensive_imp_aggressive BV_correct no_type_error)
   427   done
   428 
   429 corollary no_type_errors_initial:
   430   fixes G ("\<Gamma>") and Phi ("\<Phi>")
   431   assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
   432   assumes is_class: "is_class \<Gamma> C"
   433     and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
   434     and m: "m \<noteq> init"
   435   defines start: "s \<equiv> start_state \<Gamma> C m"
   436 
   437   assumes s: "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> t" 
   438   shows "t \<noteq> TypeError"
   439 proof -
   440   from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
   441     unfolding start by (rule BV_correct_initial)
   442   from wt this s show ?thesis by (rule no_type_errors)
   443 qed
   444 
   445 text {*
   446   As corollary we get that the aggressive and the defensive machine
   447   are equivalent for welltyped programs (if started in a conformant
   448   state or in the canonical start state)
   449 *} 
   450 corollary welltyped_commutes:
   451   fixes G ("\<Gamma>") and Phi ("\<Phi>")
   452   assumes wt: "wt_jvm_prog \<Gamma> \<Phi>" and *: "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" 
   453   shows "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s -jvm\<rightarrow> t"
   454   apply rule
   455    apply (erule defensive_imp_aggressive, rule welltyped_aggressive_imp_defensive)
   456     apply (rule wt)
   457    apply (rule *)
   458   apply assumption
   459   done
   460 
   461 corollary welltyped_initial_commutes:
   462   fixes G ("\<Gamma>") and Phi ("\<Phi>")
   463   assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
   464   assumes is_class: "is_class \<Gamma> C"
   465     and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
   466     and m: "m \<noteq> init"
   467   defines start: "s \<equiv> start_state \<Gamma> C m"
   468   shows "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s -jvm\<rightarrow> t"
   469 proof -
   470   from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
   471     unfolding start by (rule BV_correct_initial)
   472   with wt show ?thesis by (rule welltyped_commutes)
   473 qed
   474  
   475 end