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