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