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