|
1 (* Title: HOL/MicroJava/BV/BVSpec.thy |
|
2 ID: $Id$ |
|
3 Author: Cornelia Pusch |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 |
|
6 Specification of bytecode verifier |
|
7 *) |
|
8 |
|
9 BVSpec = Convert + |
|
10 |
|
11 types |
|
12 method_type = "state_type list" |
|
13 class_type = "sig \\<Rightarrow> method_type" |
|
14 prog_type = "cname \\<Rightarrow> class_type" |
|
15 |
|
16 consts |
|
17 wt_LS :: "[load_and_store,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" |
|
18 primrec |
|
19 "wt_LS (Load idx) G phi max_pc pc = |
|
20 (let (ST,LT) = phi ! pc |
|
21 in |
|
22 pc+1 < max_pc \\<and> |
|
23 idx < length LT \\<and> |
|
24 (\\<exists>ts. (LT ! idx) = Some ts \\<and> |
|
25 G \\<turnstile> phi ! (pc+1) >>>= (ts # ST , LT)))" |
|
26 |
|
27 "wt_LS (Store idx) G phi max_pc pc = |
|
28 (let (ST,LT) = phi ! pc |
|
29 in |
|
30 pc+1 < max_pc \\<and> |
|
31 idx < length LT \\<and> |
|
32 (\\<exists>ts ST'. ST = ts # ST' \\<and> |
|
33 G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT[idx:=Some ts])))" |
|
34 |
|
35 "wt_LS (Bipush i) G phi max_pc pc = |
|
36 (let (ST,LT) = phi ! pc |
|
37 in |
|
38 pc+1 < max_pc \\<and> |
|
39 G \\<turnstile> phi ! (pc+1) >>>= ((PrimT Integer) # ST , LT))" |
|
40 |
|
41 "wt_LS (Aconst_null) G phi max_pc pc = |
|
42 (let (ST,LT) = phi ! pc |
|
43 in |
|
44 pc+1 < max_pc \\<and> |
|
45 G \\<turnstile> phi ! (pc+1) >>>= (NT # ST , LT))" |
|
46 |
|
47 consts |
|
48 wt_MO :: "[manipulate_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" |
|
49 primrec |
|
50 "wt_MO (Getfield F C) G phi max_pc pc = |
|
51 (let (ST,LT) = phi ! pc |
|
52 in |
|
53 pc+1 < max_pc \\<and> |
|
54 is_class G C \\<and> |
|
55 (\\<exists>T oT ST'. cfield (G,C) F = Some(C,T) \\<and> |
|
56 ST = oT # ST' \\<and> |
|
57 G \\<turnstile> oT \\<preceq> (Class C) \\<and> |
|
58 G \\<turnstile> phi ! (pc+1) >>>= (T # ST' , LT)))" |
|
59 |
|
60 "wt_MO (Putfield F C) G phi max_pc pc = |
|
61 (let (ST,LT) = phi ! pc |
|
62 in |
|
63 pc+1 < max_pc \\<and> |
|
64 is_class G C \\<and> |
|
65 (\\<exists>T vT oT ST'. |
|
66 cfield (G,C) F = Some(C,T) \\<and> |
|
67 ST = vT # oT # ST' \\<and> |
|
68 G \\<turnstile> oT \\<preceq> (Class C) \\<and> |
|
69 G \\<turnstile> vT \\<preceq> T \\<and> |
|
70 G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT)))" |
|
71 |
|
72 |
|
73 consts |
|
74 wt_CO :: "[create_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" |
|
75 primrec |
|
76 "wt_CO (New C) G phi max_pc pc = |
|
77 (let (ST,LT) = phi ! pc |
|
78 in |
|
79 pc+1 < max_pc \\<and> |
|
80 is_class G C \\<and> |
|
81 G \\<turnstile> phi ! (pc+1) >>>= ((Class C) # ST , LT))" |
|
82 |
|
83 consts |
|
84 wt_CH :: "[check_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" |
|
85 primrec |
|
86 "wt_CH (Checkcast C) G phi max_pc pc = |
|
87 (let (ST,LT) = phi ! pc |
|
88 in |
|
89 pc+1 < max_pc \\<and> |
|
90 is_class G C \\<and> |
|
91 (\\<exists>rt ST'. ST = RefT rt # ST' \\<and> |
|
92 G \\<turnstile> phi ! (pc+1) >>>= (Class C # ST' , LT)))" |
|
93 |
|
94 consts |
|
95 wt_OS :: "[op_stack,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" |
|
96 primrec |
|
97 "wt_OS Pop G phi max_pc pc = |
|
98 (let (ST,LT) = phi ! pc |
|
99 in |
|
100 \\<exists>ts ST'. pc+1 < max_pc \\<and> |
|
101 ST = ts # ST' \\<and> |
|
102 G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT))" |
|
103 |
|
104 "wt_OS Dup G phi max_pc pc = |
|
105 (let (ST,LT) = phi ! pc |
|
106 in |
|
107 pc+1 < max_pc \\<and> |
|
108 (\\<exists>ts ST'. ST = ts # ST' \\<and> |
|
109 G \\<turnstile> phi ! (pc+1) >>>= (ts # ts # ST' , LT)))" |
|
110 |
|
111 "wt_OS Dup_x1 G phi max_pc pc = |
|
112 (let (ST,LT) = phi ! pc |
|
113 in |
|
114 pc+1 < max_pc \\<and> |
|
115 (\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and> |
|
116 G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts1 # ST' , LT)))" |
|
117 |
|
118 "wt_OS Dup_x2 G phi max_pc pc = |
|
119 (let (ST,LT) = phi ! pc |
|
120 in |
|
121 pc+1 < max_pc \\<and> |
|
122 (\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and> |
|
123 G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts3 # ts1 # ST' , LT)))" |
|
124 |
|
125 "wt_OS Swap G phi max_pc pc = |
|
126 (let (ST,LT) = phi ! pc |
|
127 in |
|
128 pc+1 < max_pc \\<and> |
|
129 (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and> |
|
130 G \\<turnstile> phi ! (pc+1) >>>= (ts # ts' # ST' , LT)))" |
|
131 |
|
132 consts |
|
133 wt_BR :: "[branch,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" |
|
134 primrec |
|
135 "wt_BR (Ifcmpeq branch) G phi max_pc pc = |
|
136 (let (ST,LT) = phi ! pc |
|
137 in |
|
138 pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and> |
|
139 (\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and> ts = ts' \\<and> |
|
140 G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT) \\<and> |
|
141 G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST' , LT)))" |
|
142 "wt_BR (Goto branch) G phi max_pc pc = |
|
143 (let (ST,LT) = phi ! pc |
|
144 in |
|
145 (nat(int pc+branch)) < max_pc \\<and> |
|
146 G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST , LT))" |
|
147 |
|
148 consts |
|
149 wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" |
|
150 primrec |
|
151 "wt_MI (Invokevirtual mn fpTs) G phi max_pc pc = |
|
152 (let (ST,LT) = phi ! pc |
|
153 in |
|
154 pc+1 < max_pc \\<and> |
|
155 (\\<exists>apTs C ST'. ST = (rev apTs) @ (Class C # ST') \\<and> |
|
156 length apTs = length fpTs \\<and> |
|
157 (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and> |
|
158 (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and> |
|
159 G \\<turnstile> phi ! (pc+1) >>>= (rT # ST' , LT))))" |
|
160 |
|
161 constdefs |
|
162 wt_MR :: "[jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool" |
|
163 "wt_MR G rT phi pc \\<equiv> |
|
164 (let (ST,LT) = phi ! pc |
|
165 in |
|
166 (\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))" |
|
167 |
|
168 |
|
169 constdefs |
|
170 wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count] \\<Rightarrow> bool" |
|
171 "wt_instr instr G rT phi max_pc pc \\<equiv> |
|
172 case instr of |
|
173 LS ins \\<Rightarrow> wt_LS ins G phi max_pc pc |
|
174 | CO ins \\<Rightarrow> wt_CO ins G phi max_pc pc |
|
175 | MO ins \\<Rightarrow> wt_MO ins G phi max_pc pc |
|
176 | CH ins \\<Rightarrow> wt_CH ins G phi max_pc pc |
|
177 | MI ins \\<Rightarrow> wt_MI ins G phi max_pc pc |
|
178 | MR \\<Rightarrow> wt_MR G rT phi pc |
|
179 | OS ins \\<Rightarrow> wt_OS ins G phi max_pc pc |
|
180 | BR ins \\<Rightarrow> wt_BR ins G phi max_pc pc" |
|
181 |
|
182 |
|
183 constdefs |
|
184 wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool" |
|
185 "wt_start G C pTs mxl phi \\<equiv> |
|
186 G \\<turnstile> phi!0 >>>= ([],(Some(Class C))#((map Some pTs))@(replicate mxl None))" |
|
187 |
|
188 |
|
189 wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool" |
|
190 "wt_method G cn pTs rT mxl ins phi \\<equiv> |
|
191 let max_pc = length ins |
|
192 in |
|
193 0 < max_pc \\<and> wt_start G cn pTs mxl phi \\<and> |
|
194 (\\<forall>pc. pc<max_pc \\<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)" |
|
195 |
|
196 wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool" |
|
197 "wt_jvm_prog G phi \\<equiv> |
|
198 wf_prog (\\<lambda>G C (sig,rT,maxl,b). |
|
199 wt_method G C (snd sig) rT maxl b (phi C sig)) G" |
|
200 |
|
201 end |