15 wt_instr_def step_def |
15 wt_instr_def step_def |
16 |
16 |
17 lemmas [simp del] = split_paired_All |
17 lemmas [simp del] = split_paired_All |
18 |
18 |
19 lemma wt_jvm_prog_impl_wt_instr_cor: |
19 lemma wt_jvm_prog_impl_wt_instr_cor: |
20 "[| wt_jvm_prog G phi;is_class G C; method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
20 "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
21 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
21 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
22 ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" |
22 ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" |
23 apply (unfold correct_state_def Let_def correct_frame_def) |
23 apply (unfold correct_state_def Let_def correct_frame_def) |
24 apply simp |
24 apply simp |
25 apply (blast intro: wt_jvm_prog_impl_wt_instr) |
25 apply (blast intro: wt_jvm_prog_impl_wt_instr) |
212 |
212 |
213 (****** Method Invocation ******) |
213 (****** Method Invocation ******) |
214 |
214 |
215 lemmas [simp del] = split_paired_Ex |
215 lemmas [simp del] = split_paired_Ex |
216 |
216 |
217 lemma Invoke_correct: (* DvO: is_class G C' eingefügt *) |
217 lemma Invoke_correct: |
218 "[| wt_jvm_prog G phi; is_class G C'; |
218 "[| wt_jvm_prog G phi; |
219 method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
219 method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
220 ins ! pc = Invoke C' mn pTs; |
220 ins ! pc = Invoke C' mn pTs; |
221 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
221 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
222 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
222 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
223 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
223 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
224 ==> G,phi \<turnstile>JVM state'\<surd>" |
224 ==> G,phi \<turnstile>JVM state'\<surd>" |
225 proof - |
225 proof - |
226 assume wtprog: "wt_jvm_prog G phi" |
226 assume wtprog: "wt_jvm_prog G phi" |
227 assume is_class: "is_class G C'" |
|
228 assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)" |
227 assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)" |
229 assume ins: "ins ! pc = Invoke C' mn pTs" |
228 assume ins: "ins ! pc = Invoke C' mn pTs" |
230 assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" |
229 assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" |
231 assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" |
230 assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" |
232 assume approx: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>" |
231 assume approx: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>" |
233 |
232 |
234 from wtprog |
233 from wtprog |
235 obtain wfmb where |
234 obtain wfmb where |
236 wfprog: "wf_prog wfmb G" |
235 wfprog: "wf_prog wfmb G" |
237 by (simp add: wt_jvm_prog_def) |
236 by (simp add: wt_jvm_prog_def) |
238 |
237 |
239 from ins method approx |
238 from ins method approx |
240 obtain s where |
239 obtain s where |
241 heap_ok: "G\<turnstile>h hp\<surd>" and |
240 heap_ok: "G\<turnstile>h hp\<surd>" and |
242 phi_pc: "phi C sig!pc = Some s" and |
241 phi_pc: "phi C sig!pc = Some s" and |
|
242 is_class_C: "is_class G C" and |
243 frame: "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and |
243 frame: "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and |
244 frames: "correct_frames G hp phi rT sig frs" |
244 frames: "correct_frames G hp phi rT sig frs" |
245 by (clarsimp simp add: correct_state_def) |
245 by (clarsimp simp add: correct_state_def iff del: not_None_eq) |
246 |
246 |
247 from ins wti phi_pc |
247 from ins wti phi_pc |
248 obtain apTs X ST LT D' rT body where |
248 obtain apTs X ST LT D' rT body where |
249 s: "s = (rev apTs @ X # ST, LT)" and |
249 s: "s = (rev apTs @ X # ST, LT)" and |
250 l: "length apTs = length pTs" and |
250 l: "length apTs = length pTs" and |
|
251 is_class: "is_class G C'" and |
251 X: "G\<turnstile> X \<preceq> Class C'" and |
252 X: "G\<turnstile> X \<preceq> Class C'" and |
252 w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and |
253 w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and |
253 mC': "method (G, C') (mn, pTs) = Some (D', rT, body)" and |
254 mC': "method (G, C') (mn, pTs) = Some (D', rT, body)" and |
254 pc: "Suc pc < length ins" and |
255 pc: "Suc pc < length ins" and |
255 step: "G \<turnstile> step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc" |
256 step: "G \<turnstile> step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc" |
256 by (simp add: wt_instr_def) (elim exE conjE, rule that) |
257 by (simp add: wt_instr_def del: not_None_eq) (elim exE conjE, rule that) |
257 |
258 |
258 from step |
259 from step |
259 obtain ST' LT' where |
260 obtain ST' LT' where |
260 s': "phi C sig ! Suc pc = Some (ST', LT')" |
261 s': "phi C sig ! Suc pc = Some (ST', LT')" |
261 by (simp add: step_def split_paired_Ex) (elim, rule that) |
262 by (simp add: step_def split_paired_Ex) (elim, rule that) |
454 qed |
455 qed |
455 |
456 |
456 lemmas [simp del] = map_append |
457 lemmas [simp del] = map_append |
457 |
458 |
458 lemma Return_correct: |
459 lemma Return_correct: |
459 "[| wt_jvm_prog G phi; |
460 "[| wt_jvm_prog G phi; |
460 method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
461 method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
461 ins ! pc = Return; |
462 ins ! pc = Return; |
462 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
463 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; |
463 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
464 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
464 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
465 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
465 ==> G,phi \<turnstile>JVM state'\<surd>" |
466 ==> G,phi \<turnstile>JVM state'\<surd>" |
466 apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm) |
467 apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm iff del: not_None_eq) |
467 apply (frule wt_jvm_prog_impl_wt_instr) |
468 apply (frule wt_jvm_prog_impl_wt_instr) |
468 sorry |
469 apply (assumption, assumption, erule Suc_lessD) |
469 (* |
|
470 apply (assumption, erule Suc_lessD) |
|
471 apply (unfold wt_jvm_prog_def) |
470 apply (unfold wt_jvm_prog_def) |
472 apply (fastsimp |
471 apply (fastsimp |
473 dest: subcls_widen_methd |
472 dest: subcls_widen_methd |
474 elim: widen_trans [COMP swap_prems_rl] |
473 elim: widen_trans [COMP swap_prems_rl] |
475 intro: conf_widen |
474 intro: conf_widen |
476 simp: approx_val_def append_eq_conv_conj map_eq_Cons defs1) |
475 simp: approx_val_def append_eq_conv_conj map_eq_Cons defs1) |
477 done |
476 done |
478 *) |
|
479 |
477 |
480 lemmas [simp] = map_append |
478 lemmas [simp] = map_append |
481 |
479 |
482 lemma Goto_correct: |
480 lemma Goto_correct: |
483 "[| wf_prog wt G; |
481 "[| wf_prog wt G; |
595 |
593 |
596 |
594 |
597 (** instr correct **) |
595 (** instr correct **) |
598 |
596 |
599 lemma instr_correct: |
597 lemma instr_correct: |
600 "[| wt_jvm_prog G phi; |
598 "[| wt_jvm_prog G phi; |
601 method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
599 method (G,C) sig = Some (C,rT,maxs,maxl,ins); |
602 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
600 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
603 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
601 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
604 ==> G,phi \<turnstile>JVM state'\<surd>" |
602 ==> G,phi \<turnstile>JVM state'\<surd>" |
605 apply (frule wt_jvm_prog_impl_wt_instr_cor) |
603 apply (frule wt_jvm_prog_impl_wt_instr_cor) |
606 sorry |
|
607 (* |
|
608 apply assumption+ |
604 apply assumption+ |
609 apply (cases "ins!pc") |
605 apply (cases "ins!pc") |
610 prefer 9 |
606 prefer 9 |
611 |
607 apply (rule Invoke_correct, assumption+) |
612 apply (blast intro: Invoke_correct) |
|
613 prefer 9 |
608 prefer 9 |
614 apply (blast intro: Return_correct) |
609 apply (rule Return_correct, assumption+) |
|
610 |
615 apply (unfold wt_jvm_prog_def) |
611 apply (unfold wt_jvm_prog_def) |
616 apply (fast intro: |
612 apply (rule Load_correct, assumption+) |
617 Load_correct Store_correct Bipush_correct Aconst_null_correct |
613 apply (rule Store_correct, assumption+) |
618 Checkcast_correct Getfield_correct Putfield_correct New_correct |
614 apply (rule Bipush_correct, assumption+) |
619 Goto_correct Ifcmpeq_correct Pop_correct Dup_correct |
615 apply (rule Aconst_null_correct, assumption+) |
620 Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+ |
616 apply (rule New_correct, assumption+) |
621 done |
617 apply (rule Getfield_correct, assumption+) |
622 *) |
618 apply (rule Putfield_correct, assumption+) |
|
619 apply (rule Checkcast_correct, assumption+) |
|
620 apply (rule Pop_correct, assumption+) |
|
621 apply (rule Dup_correct, assumption+) |
|
622 apply (rule Dup_x1_correct, assumption+) |
|
623 apply (rule Dup_x2_correct, assumption+) |
|
624 apply (rule Swap_correct, assumption+) |
|
625 apply (rule IAdd_correct, assumption+) |
|
626 apply (rule Goto_correct, assumption+) |
|
627 apply (rule Ifcmpeq_correct, assumption+) |
|
628 done |
|
629 |
|
630 |
623 |
631 |
624 (** Main **) |
632 (** Main **) |
625 |
633 |
626 lemma correct_state_impl_Some_method: |
634 lemma correct_state_impl_Some_method: |
627 "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |
635 "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |