1 (* Title: HOL/MicroJava/BV/BVSpec.thy |
1 (* Title: HOL/MicroJava/BV/BVSpec.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Cornelia Pusch |
3 Author: Cornelia Pusch, Gerwin Klein |
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 header "The Bytecode Verifier" |
8 header "The Bytecode Verifier" |
9 |
9 |
10 theory BVSpec = Step: |
10 theory BVSpec = Effect: |
|
11 |
|
12 text {* |
|
13 This theory contains a specification of the BV. The specification |
|
14 describes correct typings of method bodies; it corresponds |
|
15 to type \emph{checking}. |
|
16 *} |
11 |
17 |
12 constdefs |
18 constdefs |
13 wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,p_count] => bool" |
19 wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count, |
14 "wt_instr i G rT phi mxs max_pc pc == |
20 exception_table,p_count] => bool" |
15 app i G mxs rT (phi!pc) \<and> |
21 "wt_instr i G rT phi mxs max_pc et pc == |
16 (\<forall> pc' \<in> set (succs i pc). pc' < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!pc'))" |
22 app i G mxs rT pc et (phi!pc) \<and> |
|
23 (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')" |
17 |
24 |
18 wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool" |
25 wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool" |
19 "wt_start G C pTs mxl phi == |
26 "wt_start G C pTs mxl phi == |
20 G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0" |
27 G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0" |
21 |
28 |
|
29 wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list, |
|
30 exception_table,method_type] => bool" |
|
31 "wt_method G C pTs rT mxs mxl ins et phi == |
|
32 let max_pc = length ins in |
|
33 0 < max_pc \<and> wt_start G C pTs mxl phi \<and> |
|
34 (\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc et pc)" |
22 |
35 |
23 wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,method_type] => bool" |
36 wt_jvm_prog :: "[jvm_prog,prog_type] => bool" |
24 "wt_method G C pTs rT mxs mxl ins phi == |
37 "wt_jvm_prog G phi == |
25 let max_pc = length ins |
38 wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). |
26 in |
39 wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G" |
27 0 < max_pc \<and> wt_start G C pTs mxl phi \<and> |
|
28 (\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc pc)" |
|
29 |
|
30 wt_jvm_prog :: "[jvm_prog,prog_type] => bool" |
|
31 "wt_jvm_prog G phi == |
|
32 wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b)). |
|
33 wt_method G C (snd sig) rT maxs maxl b (phi C sig)) G" |
|
34 |
|
35 |
40 |
36 |
41 |
37 lemma wt_jvm_progD: |
42 lemma wt_jvm_progD: |
38 "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)" |
43 "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)" |
39 by (unfold wt_jvm_prog_def, blast) |
44 by (unfold wt_jvm_prog_def, blast) |
40 |
45 |
41 lemma wt_jvm_prog_impl_wt_instr: |
46 lemma wt_jvm_prog_impl_wt_instr: |
42 "[| wt_jvm_prog G phi; is_class G C; |
47 "[| wt_jvm_prog G phi; is_class G C; |
43 method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] |
48 method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins |] |
44 ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"; |
49 ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"; |
45 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, |
50 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, |
46 simp, simp, simp add: wf_mdecl_def wt_method_def) |
51 simp, simp, simp add: wf_mdecl_def wt_method_def) |
47 |
52 |
48 lemma wt_jvm_prog_impl_wt_start: |
53 lemma wt_jvm_prog_impl_wt_start: |
49 "[| wt_jvm_prog G phi; is_class G C; |
54 "[| wt_jvm_prog G phi; is_class G C; |
50 method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> |
55 method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) |] ==> |
51 0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)" |
56 0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)" |
52 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, |
57 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, |
53 simp, simp, simp add: wf_mdecl_def wt_method_def) |
58 simp, simp, simp add: wf_mdecl_def wt_method_def) |
54 |
|
55 text {* for most instructions wt\_instr collapses: *} |
|
56 lemma |
|
57 "succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc = |
|
58 (app i G mxs rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))" |
|
59 by (simp add: wt_instr_def) |
|
60 |
59 |
61 end |
60 end |
62 |
|
63 |
|