1 (* Title: HOL/MicroJava/J/JTypeSafe.thy |
1 (* Title: HOL/MicroJava/J/JTypeSafe.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: David von Oheimb |
3 Author: David von Oheimb |
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 |
5 |
6 Type Safety of Java |
6 Type Safety Proof for MicroJava |
7 *) |
7 *) |
8 |
8 |
9 JTypeSafe = Eval + Conform |
9 theory JTypeSafe = Eval + Conform: |
|
10 |
|
11 declare split_beta [simp] |
|
12 |
|
13 lemma NewC_conforms: |
|
14 "[|h a = None; (h, l)::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==> |
|
15 (h(a\<mapsto>(C,(init_vars (fields (G,C))))), l)::\<preceq>(G, lT)" |
|
16 apply( erule conforms_upd_obj) |
|
17 apply( unfold oconf_def) |
|
18 apply( auto dest!: fields_is_type) |
|
19 done |
|
20 |
|
21 lemma Cast_conf: |
|
22 "[| wf_prog wf_mb G; G,h\<turnstile>v::\<preceq>Class C; G\<turnstile>C\<preceq>? D; cast_ok G D h v|] |
|
23 ==> G,h\<turnstile>v::\<preceq>Class D" |
|
24 apply (unfold cast_ok_def) |
|
25 apply( case_tac "v = Null") |
|
26 apply( simp) |
|
27 apply( drule widen_RefT) |
|
28 apply( clarify) |
|
29 apply( drule (1) non_npD) |
|
30 apply( auto intro!: conf_AddrI simp add: obj_ty_def) |
|
31 done |
|
32 |
|
33 lemma FAcc_type_sound: |
|
34 "[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)::\<preceq>(G,lT); |
|
35 x' = None --> G,h\<turnstile>a'::\<preceq> Class C; np a' x' = None |] ==> |
|
36 G,h\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\<preceq>ft" |
|
37 apply( drule np_NoneD) |
|
38 apply( erule conjE) |
|
39 apply( erule (1) notE impE) |
|
40 apply( drule non_np_objD) |
|
41 apply auto |
|
42 apply( drule conforms_heapD [THEN hconfD]) |
|
43 apply( assumption) |
|
44 apply( drule (2) widen_cfs_fields) |
|
45 apply( drule (1) oconf_objD) |
|
46 apply auto |
|
47 done |
|
48 |
|
49 lemma FAss_type_sound: |
|
50 "[| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); |
|
51 (G, lT)\<turnstile>v::T'; G\<turnstile>T'\<preceq>ft; |
|
52 (G, lT)\<turnstile>aa::Class C; |
|
53 field (G,C) fn = Some (fd, ft); h''\<le>|h'; |
|
54 x' = None --> G,h'\<turnstile>a'::\<preceq> Class C; h'\<le>|h; |
|
55 (h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None|] ==> |
|
56 h''\<le>|h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))) \<and> |
|
57 (h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) \<and> |
|
58 G,h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x))))\<turnstile>x::\<preceq>T'" |
|
59 apply( drule np_NoneD) |
|
60 apply( erule conjE) |
|
61 apply( simp) |
|
62 apply( drule non_np_objD) |
|
63 apply( assumption) |
|
64 apply( force) |
|
65 apply( clarify) |
|
66 apply( simp (no_asm_use)) |
|
67 apply( frule (1) hext_objD) |
|
68 apply( erule exE) |
|
69 apply( simp) |
|
70 apply( clarify) |
|
71 apply( rule conjI) |
|
72 apply( fast elim: hext_trans hext_upd_obj) |
|
73 apply( rule conjI) |
|
74 prefer 2 |
|
75 apply( fast elim: conf_upd_obj [THEN iffD2]) |
|
76 |
|
77 apply( rule conforms_upd_obj) |
|
78 apply auto |
|
79 apply( rule_tac [2] hextI) |
|
80 prefer 2 |
|
81 apply( force) |
|
82 apply( rule oconf_hext) |
|
83 apply( erule_tac [2] hext_upd_obj) |
|
84 apply( drule (2) widen_cfs_fields) |
|
85 apply( rule oconf_obj [THEN iffD2]) |
|
86 apply( simp (no_asm)) |
|
87 apply( intro strip) |
|
88 apply( case_tac "(aaa, b) = (fn, fd)") |
|
89 apply( simp) |
|
90 apply( fast intro: conf_widen) |
|
91 apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD) |
|
92 done |
|
93 |
|
94 lemma Call_lemma2: "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs; |
|
95 list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT; |
|
96 length pTs' = length pns; nodups pns; |
|
97 Ball (set lvars) (split (\<lambda>vn. is_type G)) |
|
98 |] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')" |
|
99 apply (unfold wf_mhead_def) |
|
100 apply( clarsimp) |
|
101 apply( rule lconf_ext_list) |
|
102 apply( rule Ball_set_table [THEN lconf_init_vars]) |
|
103 apply( force) |
|
104 apply( assumption) |
|
105 apply( assumption) |
|
106 apply( erule (2) conf_list_gext_widen) |
|
107 done |
|
108 |
|
109 lemma Call_type_sound: |
|
110 "[| wf_java_prog G; a' \<noteq> Null; (h, l)::\<preceq>(G, lT); class G C = Some y; |
|
111 max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\<le>|xh; xh\<le>|h; |
|
112 list_all2 (conf G h) pvs pTsa; |
|
113 (md, rT, pns, lvars, blk, res) = |
|
114 the (method (G,fst (the (h (the_Addr a')))) (mn, pTs')); |
|
115 \<forall>lT. (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) --> |
|
116 (G, lT)\<turnstile>blk\<surd> --> h\<le>|xi \<and> (xi, xl)::\<preceq>(G, lT); |
|
117 \<forall>lT. (xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T --> |
|
118 xi\<le>|h' \<and> (h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T)); |
|
119 G,xh\<turnstile>a'::\<preceq> Class C |] ==> |
|
120 xc\<le>|h' \<and> (h', l)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)" |
|
121 apply (unfold wf_java_prog_def) |
|
122 apply( drule max_spec2mheads) |
|
123 apply( clarify) |
|
124 apply( drule (2) non_np_objD') |
|
125 apply( clarsimp) |
|
126 apply( clarsimp) |
|
127 apply( frule (1) hext_objD) |
|
128 apply( clarsimp) |
|
129 apply( drule (3) Call_lemma) |
|
130 apply( clarsimp simp add: wf_java_mdecl_def) |
|
131 apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl) |
|
132 apply( drule spec, erule impE) |
|
133 apply( erule_tac [2] notE impE, tactic "assume_tac 2") |
|
134 apply( rule conformsI) |
|
135 apply( erule conforms_heapD) |
|
136 apply( rule lconf_ext) |
|
137 apply( force elim!: Call_lemma2) |
|
138 apply( erule conf_hext, erule (1) conf_obj_AddrI) |
|
139 apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl) |
|
140 apply( erule conjE) |
|
141 apply( drule spec, erule (1) impE) |
|
142 apply( drule spec, erule (1) impE) |
|
143 apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl) |
|
144 apply( clarify) |
|
145 apply( rule conjI) |
|
146 apply( fast intro: hext_trans) |
|
147 apply( rule conjI) |
|
148 apply( rule_tac [2] impI) |
|
149 apply( erule_tac [2] notE impE, tactic "assume_tac 2") |
|
150 apply( frule_tac [2] conf_widen) |
|
151 apply( tactic "assume_tac 4") |
|
152 apply( tactic "assume_tac 2") |
|
153 prefer 2 |
|
154 apply( fast elim!: widen_trans) |
|
155 apply( erule conforms_hext) |
|
156 apply( erule (1) hext_trans) |
|
157 apply( erule conforms_heapD) |
|
158 done |
|
159 |
|
160 declare split_if [split del] |
|
161 declare fun_upd_apply [simp del] |
|
162 declare fun_upd_same [simp] |
|
163 ML{* |
|
164 val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac, |
|
165 (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)])) |
|
166 *} |
|
167 ML{* |
|
168 Unify.search_bound := 40; |
|
169 Unify.trace_bound := 40 |
|
170 *} |
|
171 theorem eval_evals_exec_type_sound: |
|
172 "wf_java_prog G ==> |
|
173 (G\<turnstile>(x,(h,l)) -e \<succ>v -> (x', (h',l')) --> |
|
174 (\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e :: T --> |
|
175 h\<le>|h' \<and> (h',l')::\<preceq>(G,lT) \<and> (x'=None --> G,h'\<turnstile>v ::\<preceq> T )))) \<and> |
|
176 (G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) --> |
|
177 (\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts --> |
|
178 h\<le>|h' \<and> (h',l')::\<preceq>(G,lT) \<and> (x'=None --> list_all2 (\<lambda>v T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) \<and> |
|
179 (G\<turnstile>(x,(h,l)) -c -> (x', (h',l')) --> |
|
180 (\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (G,lT)\<turnstile>c \<surd> --> |
|
181 h\<le>|h' \<and> (h',l')::\<preceq>(G,lT)))" |
|
182 apply( rule eval_evals_exec_induct) |
|
183 apply( unfold c_hupd_def) |
|
184 |
|
185 (* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *) |
|
186 apply( simp_all) |
|
187 apply( tactic "ALLGOALS strip_tac") |
|
188 apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) *}) |
|
189 apply( tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])") |
|
190 apply( unfold wf_java_prog_def) |
|
191 |
|
192 (* Level 7 *) |
|
193 |
|
194 (* 15 NewC *) |
|
195 apply( drule new_AddrD) |
|
196 apply( erule disjE) |
|
197 prefer 2 |
|
198 apply( simp (no_asm_simp)) |
|
199 apply( clarsimp) |
|
200 apply( rule conjI) |
|
201 apply( force elim!: NewC_conforms) |
|
202 apply( rule conf_obj_AddrI) |
|
203 apply( rule_tac [2] rtrancl_refl) |
|
204 apply( simp (no_asm)) |
|
205 |
|
206 (* for Cast *) |
|
207 defer 1 |
|
208 |
|
209 (* 14 Lit *) |
|
210 apply( erule conf_litval) |
|
211 |
|
212 (* 13 BinOp *) |
|
213 apply (tactic "forward_hyp_tac") |
|
214 apply (tactic "forward_hyp_tac") |
|
215 apply( rule conjI, erule (1) hext_trans) |
|
216 apply( erule conjI) |
|
217 apply( clarsimp) |
|
218 apply( drule eval_no_xcpt) |
|
219 apply( simp split add: binop.split) |
|
220 |
|
221 (* 12 LAcc *) |
|
222 apply( fast elim: conforms_localD [THEN lconfD]) |
|
223 |
|
224 (* for FAss *) |
|
225 apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*}) |
|
226 |
|
227 (* for if *) |
|
228 apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8*}) |
|
229 |
|
230 apply (tactic "forward_hyp_tac") |
|
231 |
|
232 (* 11+1 if *) |
|
233 prefer 8 |
|
234 apply( fast intro: hext_trans) |
|
235 prefer 8 |
|
236 apply( fast intro: hext_trans) |
|
237 |
|
238 (* 10 Expr *) |
|
239 prefer 6 |
|
240 apply( fast) |
|
241 |
|
242 (* 9 ??? *) |
|
243 apply( simp_all) |
|
244 |
|
245 (* 8 Cast *) |
|
246 prefer 8 |
|
247 apply (rule impI) |
|
248 apply (drule raise_if_NoneD) |
|
249 apply (clarsimp) |
|
250 apply (fast elim: Cast_conf) |
|
251 |
|
252 (* 7 LAss *) |
|
253 apply (fold fun_upd_def) |
|
254 apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) 1 *}) |
|
255 apply( blast intro: conforms_upd_local conf_widen) |
|
256 |
|
257 (* 6 FAcc *) |
|
258 apply( fast elim!: FAcc_type_sound) |
|
259 |
|
260 (* 5 While *) |
|
261 prefer 5 |
|
262 apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl) |
|
263 apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop) |
|
264 apply(force elim: hext_trans) |
|
265 |
|
266 apply (tactic "forward_hyp_tac") |
|
267 |
|
268 (* 4 Cons *) |
|
269 prefer 3 |
|
270 apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) |
|
271 |
|
272 (* 3 ;; *) |
|
273 prefer 3 |
|
274 apply( fast intro: hext_trans) |
|
275 |
|
276 (* 2 FAss *) |
|
277 apply( case_tac "x2 = None") |
|
278 prefer 2 |
|
279 apply( simp (no_asm_simp)) |
|
280 apply( fast intro: hext_trans) |
|
281 apply( simp) |
|
282 apply( drule eval_no_xcpt) |
|
283 apply( erule FAss_type_sound, simp (no_asm) (*###rule refl*), assumption+) |
|
284 |
|
285 apply( tactic prune_params_tac) |
|
286 (* Level 52 *) |
|
287 |
|
288 (* 1 Call *) |
|
289 apply( case_tac "x") |
|
290 prefer 2 |
|
291 apply( clarsimp) |
|
292 apply( drule exec_xcpt) |
|
293 apply( simp) |
|
294 apply( drule_tac eval_xcpt) |
|
295 apply( simp) |
|
296 apply( fast elim: hext_trans) |
|
297 apply( clarify) |
|
298 apply( drule evals_no_xcpt) |
|
299 apply( simp) |
|
300 apply( case_tac "a' = Null") |
|
301 apply( simp) |
|
302 apply( drule exec_xcpt) |
|
303 apply( simp) |
|
304 apply( drule eval_xcpt) |
|
305 apply( simp) |
|
306 apply( fast elim: hext_trans) |
|
307 apply( drule (1) ty_expr_is_type) |
|
308 apply(clarsimp) |
|
309 apply(unfold is_class_def) |
|
310 apply(clarsimp) |
|
311 apply(rule Call_type_sound [unfolded wf_java_prog_def]); |
|
312 prefer 11 |
|
313 apply blast |
|
314 apply (simp (no_asm_simp))+ |
|
315 done |
|
316 ML{* |
|
317 Unify.search_bound := 20; |
|
318 Unify.trace_bound := 20 |
|
319 *} |
|
320 |
|
321 lemma eval_type_sound: "!!E s s'. |
|
322 [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); s::\<preceq>E; E\<turnstile>e::T |] |
|
323 ==> s'::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T)" |
|
324 apply( simp (no_asm_simp) only: split_tupled_all) |
|
325 apply (drule eval_evals_exec_type_sound |
|
326 [THEN conjunct1, THEN mp, THEN spec, THEN mp]) |
|
327 apply auto |
|
328 done |
|
329 |
|
330 lemma exec_type_sound: "!!E s s'. |
|
331 [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); s::\<preceq>E; E\<turnstile>s0\<surd> |] |
|
332 ==> s'::\<preceq>E" |
|
333 apply( simp (no_asm_simp) only: split_tupled_all) |
|
334 apply (drule eval_evals_exec_type_sound |
|
335 [THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp]) |
|
336 apply auto |
|
337 done |
|
338 |
|
339 theorem all_methods_understood: |
|
340 "[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null; |
|
341 s::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==> |
|
342 method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None" |
|
343 apply( drule (4) eval_type_sound) |
|
344 apply(clarsimp) |
|
345 apply(unfold wf_java_prog_def) |
|
346 apply( frule widen_methd) |
|
347 apply( assumption) |
|
348 prefer 2 |
|
349 apply( fast) |
|
350 apply( drule non_npD) |
|
351 apply auto |
|
352 done |
|
353 |
|
354 declare split_beta [simp del] |
|
355 declare fun_upd_apply [simp] |
|
356 |
|
357 end |
|
358 |
|
359 |