author | nipkow |
Sat, 02 Jan 2010 22:57:19 +0100 | |
changeset 34227 | 33d44b1520c0 |
parent 33954 | 1bc3b688548c |
child 35416 | d8d7d1b785af |
permissions | -rwxr-xr-x |
13215 | 1 |
(* Title: HOL/MicroJava/BV/JVM.thy |
2 |
Author: Tobias Nipkow, Gerwin Klein |
|
3 |
Copyright 2000 TUM |
|
4 |
*) |
|
5 |
||
6 |
header {* \isaheader{LBV for the JVM}\label{sec:JVM} *} |
|
7 |
||
17090 | 8 |
theory LBVJVM |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33639
diff
changeset
|
9 |
imports Typing_Framework_JVM |
17090 | 10 |
begin |
13215 | 11 |
|
26450 | 12 |
types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> JVMType.state list" |
13215 | 13 |
|
14 |
constdefs |
|
26450 | 15 |
check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool" |
13215 | 16 |
"check_cert G mxs mxr n cert \<equiv> check_types G mxs mxr cert \<and> length cert = n+1 \<and> |
17 |
(\<forall>i<n. cert!i \<noteq> Err) \<and> cert!n = OK None" |
|
18 |
||
19 |
lbvjvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> |
|
26450 | 20 |
JVMType.state list \<Rightarrow> instr list \<Rightarrow> JVMType.state \<Rightarrow> JVMType.state" |
13215 | 21 |
"lbvjvm G maxs maxr rT et cert bs \<equiv> |
22 |
wtl_inst_list bs cert (JVMType.sup G maxs maxr) (JVMType.le G maxs maxr) Err (OK None) (exec G maxs rT et bs) 0" |
|
23 |
||
24 |
wt_lbv :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> |
|
26450 | 25 |
exception_table \<Rightarrow> JVMType.state list \<Rightarrow> instr list \<Rightarrow> bool" |
13215 | 26 |
"wt_lbv G C pTs rT mxs mxl et cert ins \<equiv> |
27 |
check_bounded ins et \<and> |
|
28 |
check_cert G mxs (1+size pTs+mxl) (length ins) cert \<and> |
|
29 |
0 < size ins \<and> |
|
30 |
(let start = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)); |
|
31 |
result = lbvjvm G mxs (1+size pTs+mxl) rT et cert ins (OK start) |
|
32 |
in result \<noteq> Err)" |
|
33 |
||
34 |
wt_jvm_prog_lbv :: "jvm_prog \<Rightarrow> prog_cert \<Rightarrow> bool" |
|
35 |
"wt_jvm_prog_lbv G cert \<equiv> |
|
36 |
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_lbv G C (snd sig) rT maxs maxl et (cert C sig) b) G" |
|
37 |
||
38 |
mk_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list |
|
26450 | 39 |
\<Rightarrow> method_type \<Rightarrow> JVMType.state list" |
13215 | 40 |
"mk_cert G maxs rT et bs phi \<equiv> make_cert (exec G maxs rT et bs) (map OK phi) (OK None)" |
41 |
||
42 |
prg_cert :: "jvm_prog \<Rightarrow> prog_type \<Rightarrow> prog_cert" |
|
43 |
"prg_cert G phi C sig \<equiv> let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in |
|
44 |
mk_cert G maxs rT et ins (phi C sig)" |
|
45 |
||
46 |
||
47 |
lemma wt_method_def2: |
|
48 |
fixes pTs and mxl and G and mxs and rT and et and bs and phi |
|
49 |
defines [simp]: "mxr \<equiv> 1 + length pTs + mxl" |
|
50 |
defines [simp]: "r \<equiv> sup_state_opt G" |
|
51 |
defines [simp]: "app0 \<equiv> \<lambda>pc. app (bs!pc) G mxs rT pc et" |
|
52 |
defines [simp]: "step0 \<equiv> \<lambda>pc. eff (bs!pc) G pc et" |
|
53 |
||
54 |
shows |
|
55 |
"wt_method G C pTs rT mxs mxl bs et phi = |
|
56 |
(bs \<noteq> [] \<and> |
|
57 |
length phi = length bs \<and> |
|
58 |
check_bounded bs et \<and> |
|
59 |
check_types G mxs mxr (map OK phi) \<and> |
|
60 |
wt_start G C pTs mxl phi \<and> |
|
61 |
wt_app_eff r app0 step0 phi)" |
|
62 |
by (auto simp add: wt_method_def wt_app_eff_def wt_instr_def lesub_def |
|
63 |
dest: check_bounded_is_bounded boundedD) |
|
64 |
||
65 |
||
13224 | 66 |
lemma check_certD: |
67 |
"check_cert G mxs mxr n cert \<Longrightarrow> cert_ok cert n Err (OK None) (states G mxs mxr)" |
|
68 |
apply (unfold cert_ok_def check_cert_def check_types_def) |
|
17090 | 69 |
apply (auto simp add: list_all_iff) |
13224 | 70 |
done |
71 |
||
13215 | 72 |
|
73 |
lemma wt_lbv_wt_step: |
|
74 |
assumes wf: "wf_prog wf_mb G" |
|
75 |
assumes lbv: "wt_lbv G C pTs rT mxs mxl et cert ins" |
|
76 |
assumes C: "is_class G C" |
|
77 |
assumes pTs: "set pTs \<subseteq> types G" |
|
78 |
||
79 |
defines [simp]: "mxr \<equiv> 1+length pTs+mxl" |
|
80 |
||
81 |
shows "\<exists>ts \<in> list (size ins) (states G mxs mxr). |
|
82 |
wt_step (JVMType.le G mxs mxr) Err (exec G mxs rT et ins) ts |
|
83 |
\<and> OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) <=_(JVMType.le G mxs mxr) ts!0" |
|
84 |
proof - |
|
85 |
let ?step = "exec G mxs rT et ins" |
|
86 |
let ?r = "JVMType.le G mxs mxr" |
|
87 |
let ?f = "JVMType.sup G mxs mxr" |
|
88 |
let ?A = "states G mxs mxr" |
|
89 |
||
14045 | 90 |
have "semilat (JVMType.sl G mxs mxr)" |
23467 | 91 |
by (rule semilat_JVM_slI, rule wf_prog_ws_prog, rule wf) |
13215 | 92 |
hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv) |
93 |
moreover |
|
94 |
have "top ?r Err" by (simp add: JVM_le_unfold) |
|
95 |
moreover |
|
96 |
have "Err \<in> ?A" by (simp add: JVM_states_unfold) |
|
97 |
moreover |
|
98 |
have "bottom ?r (OK None)" |
|
99 |
by (simp add: JVM_le_unfold bottom_def) |
|
100 |
moreover |
|
101 |
have "OK None \<in> ?A" by (simp add: JVM_states_unfold) |
|
102 |
moreover |
|
103 |
from lbv |
|
104 |
have "bounded ?step (length ins)" |
|
105 |
by (clarsimp simp add: wt_lbv_def exec_def) |
|
106 |
(intro bounded_lift check_bounded_is_bounded) |
|
107 |
moreover |
|
108 |
from lbv |
|
109 |
have "cert_ok cert (length ins) Err (OK None) ?A" |
|
110 |
by (unfold wt_lbv_def) (auto dest: check_certD) |
|
111 |
moreover |
|
23467 | 112 |
from wf have "pres_type ?step (length ins) ?A" by (rule exec_pres_type) |
13215 | 113 |
moreover |
114 |
let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))" |
|
115 |
from lbv |
|
116 |
have "wtl_inst_list ins cert ?f ?r Err (OK None) ?step 0 ?start \<noteq> Err" |
|
117 |
by (simp add: wt_lbv_def lbvjvm_def) |
|
118 |
moreover |
|
119 |
from C pTs have "?start \<in> ?A" |
|
120 |
by (unfold JVM_states_unfold) (auto intro: list_appendI, force) |
|
121 |
moreover |
|
122 |
from lbv have "0 < length ins" by (simp add: wt_lbv_def) |
|
123 |
ultimately |
|
27681 | 124 |
show ?thesis by (rule lbvs.wtl_sound_strong [OF lbvs.intro, OF lbv.intro lbvs_axioms.intro, OF Semilat.intro lbv_axioms.intro]) |
13215 | 125 |
qed |
126 |
||
127 |
lemma wt_lbv_wt_method: |
|
128 |
assumes wf: "wf_prog wf_mb G" |
|
129 |
assumes lbv: "wt_lbv G C pTs rT mxs mxl et cert ins" |
|
130 |
assumes C: "is_class G C" |
|
131 |
assumes pTs: "set pTs \<subseteq> types G" |
|
132 |
||
133 |
shows "\<exists>phi. wt_method G C pTs rT mxs mxl ins et phi" |
|
134 |
proof - |
|
135 |
let ?mxr = "1 + length pTs + mxl" |
|
136 |
let ?step = "exec G mxs rT et ins" |
|
137 |
let ?r = "JVMType.le G mxs ?mxr" |
|
138 |
let ?f = "JVMType.sup G mxs ?mxr" |
|
139 |
let ?A = "states G mxs ?mxr" |
|
140 |
let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))" |
|
141 |
||
142 |
from lbv have l: "ins \<noteq> []" by (simp add: wt_lbv_def) |
|
143 |
moreover |
|
144 |
from wf lbv C pTs |
|
145 |
obtain phi where |
|
146 |
list: "phi \<in> list (length ins) ?A" and |
|
147 |
step: "wt_step ?r Err ?step phi" and |
|
148 |
start: "?start <=_?r phi!0" |
|
149 |
by (blast dest: wt_lbv_wt_step) |
|
150 |
from list have [simp]: "length phi = length ins" by simp |
|
151 |
have "length (map ok_val phi) = length ins" by simp |
|
152 |
moreover |
|
153 |
from l have 0: "0 < length phi" by simp |
|
154 |
with step obtain phi0 where "phi!0 = OK phi0" |
|
155 |
by (unfold wt_step_def) blast |
|
156 |
with start 0 |
|
157 |
have "wt_start G C pTs mxl (map ok_val phi)" |
|
158 |
by (simp add: wt_start_def JVM_le_Err_conv lesub_def) |
|
159 |
moreover |
|
160 |
from lbv have chk_bounded: "check_bounded ins et" |
|
161 |
by (simp add: wt_lbv_def) |
|
162 |
moreover { |
|
163 |
from list |
|
164 |
have "check_types G mxs ?mxr phi" |
|
165 |
by (simp add: check_types_def) |
|
166 |
also from step |
|
13224 | 167 |
have [symmetric]: "map OK (map ok_val phi) = phi" |
33639
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
27681
diff
changeset
|
168 |
by (auto intro!: nth_equalityI simp add: wt_step_def) |
13215 | 169 |
finally have "check_types G mxs ?mxr (map OK (map ok_val phi))" . |
170 |
} |
|
171 |
moreover { |
|
172 |
let ?app = "\<lambda>pc. app (ins!pc) G mxs rT pc et" |
|
173 |
let ?eff = "\<lambda>pc. eff (ins!pc) G pc et" |
|
174 |
||
175 |
from chk_bounded |
|
176 |
have "bounded (err_step (length ins) ?app ?eff) (length ins)" |
|
177 |
by (blast dest: check_bounded_is_bounded boundedD intro: bounded_err_stepI) |
|
178 |
moreover |
|
179 |
from step |
|
180 |
have "wt_err_step (sup_state_opt G) ?step phi" |
|
181 |
by (simp add: wt_err_step_def JVM_le_Err_conv) |
|
182 |
ultimately |
|
183 |
have "wt_app_eff (sup_state_opt G) ?app ?eff (map ok_val phi)" |
|
184 |
by (auto intro: wt_err_imp_wt_app_eff simp add: exec_def) |
|
185 |
} |
|
186 |
ultimately |
|
187 |
have "wt_method G C pTs rT mxs mxl ins et (map ok_val phi)" |
|
188 |
by - (rule wt_method_def2 [THEN iffD2], simp) |
|
189 |
thus ?thesis .. |
|
190 |
qed |
|
191 |
||
192 |
||
193 |
lemma wt_method_wt_lbv: |
|
194 |
assumes wf: "wf_prog wf_mb G" |
|
195 |
assumes wt: "wt_method G C pTs rT mxs mxl ins et phi" |
|
196 |
assumes C: "is_class G C" |
|
197 |
assumes pTs: "set pTs \<subseteq> types G" |
|
198 |
||
199 |
defines [simp]: "cert \<equiv> mk_cert G mxs rT et ins phi" |
|
200 |
||
201 |
shows "wt_lbv G C pTs rT mxs mxl et cert ins" |
|
202 |
proof - |
|
203 |
let ?mxr = "1 + length pTs + mxl" |
|
204 |
let ?step = "exec G mxs rT et ins" |
|
205 |
let ?app = "\<lambda>pc. app (ins!pc) G mxs rT pc et" |
|
206 |
let ?eff = "\<lambda>pc. eff (ins!pc) G pc et" |
|
207 |
let ?r = "JVMType.le G mxs ?mxr" |
|
208 |
let ?f = "JVMType.sup G mxs ?mxr" |
|
209 |
let ?A = "states G mxs ?mxr" |
|
210 |
let ?phi = "map OK phi" |
|
211 |
let ?cert = "make_cert ?step ?phi (OK None)" |
|
212 |
||
34227 | 213 |
from wt have |
13215 | 214 |
0: "0 < length ins" and |
215 |
length: "length ins = length ?phi" and |
|
216 |
ck_bounded: "check_bounded ins et" and |
|
217 |
ck_types: "check_types G mxs ?mxr ?phi" and |
|
218 |
wt_start: "wt_start G C pTs mxl phi" and |
|
219 |
app_eff: "wt_app_eff (sup_state_opt G) ?app ?eff phi" |
|
34227 | 220 |
by (simp_all add: wt_method_def2) |
13215 | 221 |
|
14045 | 222 |
have "semilat (JVMType.sl G mxs ?mxr)" |
23467 | 223 |
by (rule semilat_JVM_slI) (rule wf_prog_ws_prog [OF wf]) |
13215 | 224 |
hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv) |
225 |
moreover |
|
226 |
have "top ?r Err" by (simp add: JVM_le_unfold) |
|
227 |
moreover |
|
228 |
have "Err \<in> ?A" by (simp add: JVM_states_unfold) |
|
229 |
moreover |
|
230 |
have "bottom ?r (OK None)" |
|
231 |
by (simp add: JVM_le_unfold bottom_def) |
|
232 |
moreover |
|
233 |
have "OK None \<in> ?A" by (simp add: JVM_states_unfold) |
|
234 |
moreover |
|
235 |
from ck_bounded |
|
236 |
have bounded: "bounded ?step (length ins)" |
|
237 |
by (clarsimp simp add: exec_def) |
|
238 |
(intro bounded_lift check_bounded_is_bounded) |
|
239 |
with wf |
|
14045 | 240 |
have "mono ?r ?step (length ins) ?A" |
241 |
by (rule wf_prog_ws_prog [THEN exec_mono]) |
|
13215 | 242 |
hence "mono ?r ?step (length ?phi) ?A" by (simp add: length) |
243 |
moreover |
|
23467 | 244 |
from wf have "pres_type ?step (length ins) ?A" by (rule exec_pres_type) |
13215 | 245 |
hence "pres_type ?step (length ?phi) ?A" by (simp add: length) |
246 |
moreover |
|
247 |
from ck_types |
|
248 |
have "set ?phi \<subseteq> ?A" by (simp add: check_types_def) |
|
249 |
hence "\<forall>pc. pc < length ?phi \<longrightarrow> ?phi!pc \<in> ?A \<and> ?phi!pc \<noteq> Err" by auto |
|
250 |
moreover |
|
251 |
from bounded |
|
252 |
have "bounded (exec G mxs rT et ins) (length ?phi)" by (simp add: length) |
|
253 |
moreover |
|
254 |
have "OK None \<noteq> Err" by simp |
|
255 |
moreover |
|
256 |
from bounded length app_eff |
|
257 |
have "wt_err_step (sup_state_opt G) ?step ?phi" |
|
258 |
by (auto intro: wt_app_eff_imp_wt_err simp add: exec_def) |
|
259 |
hence "wt_step ?r Err ?step ?phi" |
|
260 |
by (simp add: wt_err_step_def JVM_le_Err_conv) |
|
261 |
moreover |
|
262 |
let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))" |
|
263 |
from 0 length have "0 < length phi" by auto |
|
264 |
hence "?phi!0 = OK (phi!0)" by simp |
|
265 |
with wt_start have "?start <=_?r ?phi!0" |
|
266 |
by (clarsimp simp add: wt_start_def lesub_def JVM_le_Err_conv) |
|
267 |
moreover |
|
268 |
from C pTs have "?start \<in> ?A" |
|
269 |
by (unfold JVM_states_unfold) (auto intro: list_appendI, force) |
|
270 |
moreover |
|
271 |
have "?start \<noteq> Err" by simp |
|
272 |
moreover |
|
273 |
note length |
|
274 |
ultimately |
|
275 |
have "wtl_inst_list ins ?cert ?f ?r Err (OK None) ?step 0 ?start \<noteq> Err" |
|
27681 | 276 |
by (rule lbvc.wtl_complete [OF lbvc.intro, OF lbv.intro lbvc_axioms.intro, OF Semilat.intro lbv_axioms.intro]) |
13215 | 277 |
moreover |
278 |
from 0 length have "phi \<noteq> []" by auto |
|
279 |
moreover |
|
280 |
from ck_types |
|
281 |
have "check_types G mxs ?mxr ?cert" |
|
282 |
by (auto simp add: make_cert_def check_types_def JVM_states_unfold) |
|
283 |
moreover |
|
284 |
note ck_bounded 0 length |
|
285 |
ultimately |
|
286 |
show ?thesis |
|
287 |
by (simp add: wt_lbv_def lbvjvm_def mk_cert_def |
|
288 |
check_cert_def make_cert_def nth_append) |
|
289 |
qed |
|
290 |
||
291 |
||
13224 | 292 |
|
293 |
theorem jvm_lbv_correct: |
|
294 |
"wt_jvm_prog_lbv G Cert \<Longrightarrow> \<exists>Phi. wt_jvm_prog G Phi" |
|
295 |
proof - |
|
296 |
let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in |
|
297 |
SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi" |
|
298 |
||
299 |
assume "wt_jvm_prog_lbv G Cert" |
|
300 |
hence "wt_jvm_prog G ?Phi" |
|
301 |
apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def) |
|
302 |
apply (erule jvm_prog_lift) |
|
303 |
apply (auto dest: wt_lbv_wt_method intro: someI) |
|
304 |
done |
|
305 |
thus ?thesis by blast |
|
306 |
qed |
|
307 |
||
13215 | 308 |
theorem jvm_lbv_complete: |
309 |
"wt_jvm_prog G Phi \<Longrightarrow> wt_jvm_prog_lbv G (prg_cert G Phi)" |
|
13224 | 310 |
apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def) |
311 |
apply (erule jvm_prog_lift) |
|
19437 | 312 |
apply (auto simp add: prg_cert_def intro: wt_method_wt_lbv) |
13224 | 313 |
done |
13215 | 314 |
|
315 |
end |