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