src/HOL/MicroJava/JVM/JVMDefensive.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 16417 9bc16273c2d4
child 35102 cc7a0b9f938c
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/MicroJava/JVM/JVMDefensive.thy
     2     ID:         $Id$
     3     Author:     Gerwin Klein
     4 *)
     5 
     6 header {* \isaheader{A Defensive JVM} *}
     7 
     8 theory JVMDefensive imports JVMExec begin
     9 
    10 text {*
    11   Extend the state space by one element indicating a type error (or
    12   other abnormal termination) *}
    13 datatype 'a type_error = TypeError | Normal 'a
    14 
    15 
    16 syntax "fifth" :: "'a \<times> 'b \<times> 'c \<times> 'd \<times> 'e \<times> 'f \<Rightarrow> 'e"
    17 translations
    18   "fifth x" == "fst(snd(snd(snd(snd x))))"
    19 
    20 
    21 consts isAddr :: "val \<Rightarrow> bool"
    22 recdef isAddr "{}"
    23   "isAddr (Addr loc) = True"
    24   "isAddr v          = False"
    25 
    26 consts isIntg :: "val \<Rightarrow> bool"
    27 recdef isIntg "{}"
    28   "isIntg (Intg i) = True"
    29   "isIntg v        = False"
    30 
    31 constdefs
    32   isRef :: "val \<Rightarrow> bool"
    33   "isRef v \<equiv> v = Null \<or> isAddr v"
    34 
    35 
    36 consts
    37   check_instr :: "[instr, jvm_prog, aheap, opstack, locvars, 
    38                   cname, sig, p_count, nat, frame list] \<Rightarrow> bool"
    39 primrec 
    40   "check_instr (Load idx) G hp stk vars C sig pc mxs frs = 
    41   (idx < length vars \<and> size stk < mxs)"
    42 
    43   "check_instr (Store idx) G hp stk vars Cl sig pc mxs frs = 
    44   (0 < length stk \<and> idx < length vars)"
    45 
    46   "check_instr (LitPush v) G hp stk vars Cl sig pc mxs frs = 
    47   (\<not>isAddr v \<and> size stk < mxs)"
    48 
    49   "check_instr (New C) G hp stk vars Cl sig pc mxs frs = 
    50   (is_class G C \<and> size stk < mxs)"
    51 
    52   "check_instr (Getfield F C) G hp stk vars Cl sig pc mxs frs = 
    53   (0 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> 
    54   (let (C', T) = the (field (G,C) F); ref = hd stk in 
    55     C' = C \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow> 
    56       hp (the_Addr ref) \<noteq> None \<and> 
    57       (let (D,vs) = the (hp (the_Addr ref)) in 
    58         G \<turnstile> D \<preceq>C C \<and> vs (F,C) \<noteq> None \<and> G,hp \<turnstile> the (vs (F,C)) ::\<preceq> T))))" 
    59 
    60   "check_instr (Putfield F C) G hp stk vars Cl sig pc mxs frs = 
    61   (1 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> 
    62   (let (C', T) = the (field (G,C) F); v = hd stk; ref = hd (tl stk) in 
    63     C' = C \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow> 
    64       hp (the_Addr ref) \<noteq> None \<and> 
    65       (let (D,vs) = the (hp (the_Addr ref)) in 
    66         G \<turnstile> D \<preceq>C C \<and> G,hp \<turnstile> v ::\<preceq> T))))" 
    67 
    68   "check_instr (Checkcast C) G hp stk vars Cl sig pc mxs frs =
    69   (0 < length stk \<and> is_class G C \<and> isRef (hd stk))"
    70 
    71   "check_instr (Invoke C mn ps) G hp stk vars Cl sig pc mxs frs =
    72   (length ps < length stk \<and> 
    73   (let n = length ps; v = stk!n in
    74   isRef v \<and> (v \<noteq> Null \<longrightarrow> 
    75     hp (the_Addr v) \<noteq> None \<and>
    76     method (G,cname_of hp v) (mn,ps) \<noteq> None \<and>
    77     list_all2 (\<lambda>v T. G,hp \<turnstile> v ::\<preceq> T) (rev (take n stk)) ps)))"
    78   
    79   "check_instr Return G hp stk0 vars Cl sig0 pc mxs frs =
    80   (0 < length stk0 \<and> (0 < length frs \<longrightarrow> 
    81     method (G,Cl) sig0 \<noteq> None \<and>    
    82     (let v = hd stk0;  (C, rT, body) = the (method (G,Cl) sig0) in
    83     Cl = C \<and> G,hp \<turnstile> v ::\<preceq> rT)))"
    84  
    85   "check_instr Pop G hp stk vars Cl sig pc mxs frs = 
    86   (0 < length stk)"
    87 
    88   "check_instr Dup G hp stk vars Cl sig pc mxs frs = 
    89   (0 < length stk \<and> size stk < mxs)"
    90 
    91   "check_instr Dup_x1 G hp stk vars Cl sig pc mxs frs = 
    92   (1 < length stk \<and> size stk < mxs)"
    93 
    94   "check_instr Dup_x2 G hp stk vars Cl sig pc mxs frs = 
    95   (2 < length stk \<and> size stk < mxs)"
    96 
    97   "check_instr Swap G hp stk vars Cl sig pc mxs frs =
    98   (1 < length stk)"
    99 
   100   "check_instr IAdd G hp stk vars Cl sig pc mxs frs =
   101   (1 < length stk \<and> isIntg (hd stk) \<and> isIntg (hd (tl stk)))"
   102 
   103   "check_instr (Ifcmpeq b) G hp stk vars Cl sig pc mxs frs =
   104   (1 < length stk \<and> 0 \<le> int pc+b)"
   105 
   106   "check_instr (Goto b) G hp stk vars Cl sig pc mxs frs =
   107   (0 \<le> int pc+b)"
   108 
   109   "check_instr Throw G hp stk vars Cl sig pc mxs frs =
   110   (0 < length stk \<and> isRef (hd stk))"
   111 
   112 constdefs
   113   check :: "jvm_prog \<Rightarrow> jvm_state \<Rightarrow> bool"
   114   "check G s \<equiv> let (xcpt, hp, frs) = s in
   115                (case frs of [] \<Rightarrow> True | (stk,loc,C,sig,pc)#frs' \<Rightarrow> 
   116                 (let  (C',rt,mxs,mxl,ins,et) = the (method (G,C) sig); i = ins!pc in
   117                  pc < size ins \<and> 
   118                  check_instr i G hp stk loc C sig pc mxs frs'))"
   119 
   120 
   121   exec_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state option type_error"
   122   "exec_d G s \<equiv> case s of 
   123       TypeError \<Rightarrow> TypeError 
   124     | Normal s' \<Rightarrow> if check G s' then Normal (exec (G, s')) else TypeError"
   125 
   126 
   127 consts
   128   "exec_all_d" :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool" 
   129                    ("_ |- _ -jvmd-> _" [61,61,61]60)
   130 
   131 syntax (xsymbols)
   132   "exec_all_d" :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool" 
   133                    ("_ \<turnstile> _ -jvmd\<rightarrow> _" [61,61,61]60)  
   134  
   135 defs
   136   exec_all_d_def:
   137   "G \<turnstile> s -jvmd\<rightarrow> t \<equiv>
   138          (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union> 
   139                   {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
   140 
   141 
   142 declare split_paired_All [simp del]
   143 declare split_paired_Ex [simp del]
   144 
   145 lemma [dest!]:
   146   "(if P then A else B) \<noteq> B \<Longrightarrow> P"
   147   by (cases P, auto)
   148 
   149 lemma exec_d_no_errorI [intro]:
   150   "check G s \<Longrightarrow> exec_d G (Normal s) \<noteq> TypeError"
   151   by (unfold exec_d_def) simp
   152 
   153 theorem no_type_error_commutes:
   154   "exec_d G (Normal s) \<noteq> TypeError \<Longrightarrow> 
   155   exec_d G (Normal s) = Normal (exec (G, s))"
   156   by (unfold exec_d_def, auto)
   157 
   158 
   159 lemma defensive_imp_aggressive:
   160   "G \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) \<Longrightarrow> G \<turnstile> s -jvm\<rightarrow> t"
   161 proof -
   162   have "\<And>x y. G \<turnstile> x -jvmd\<rightarrow> y \<Longrightarrow> \<forall>s t. x = Normal s \<longrightarrow> y = Normal t \<longrightarrow>  G \<turnstile> s -jvm\<rightarrow> t"
   163     apply (unfold exec_all_d_def)
   164     apply (erule rtrancl_induct)
   165      apply (simp add: exec_all_def)
   166     apply (fold exec_all_d_def)
   167     apply simp
   168     apply (intro allI impI)
   169     apply (erule disjE, simp)
   170     apply (elim exE conjE)
   171     apply (erule allE, erule impE, assumption)
   172     apply (simp add: exec_all_def exec_d_def split: type_error.splits split_if_asm)
   173     apply (rule rtrancl_trans, assumption)
   174     apply blast
   175     done
   176   moreover
   177   assume "G \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t)" 
   178   ultimately
   179   show "G \<turnstile> s -jvm\<rightarrow> t" by blast
   180 qed
   181 
   182 end