8245
|
1 |
(* Title: HOL/MicroJava/BV/BVLightSpec.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gerwin Klein
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
5 |
|
|
6 |
Specification of a lightweight bytecode verifier
|
|
7 |
*)
|
|
8 |
|
8390
|
9 |
LBVSpec = BVSpec +
|
8245
|
10 |
|
|
11 |
types
|
|
12 |
certificate = "state_type option list"
|
|
13 |
class_certificate = "sig \\<Rightarrow> certificate"
|
|
14 |
prog_certificate = "cname \\<Rightarrow> class_certificate"
|
|
15 |
|
|
16 |
consts
|
|
17 |
wtl_LS :: "[load_and_store,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
|
|
18 |
primrec
|
|
19 |
"wtl_LS (Load idx) s s' max_pc pc =
|
|
20 |
(let (ST,LT) = s
|
|
21 |
in
|
|
22 |
pc+1 < max_pc \\<and>
|
|
23 |
idx < length LT \\<and>
|
|
24 |
(\\<exists>ts. (LT ! idx) = Some ts \\<and>
|
|
25 |
(ts # ST , LT) = s'))"
|
|
26 |
|
|
27 |
"wtl_LS (Store idx) s s' max_pc pc =
|
|
28 |
(let (ST,LT) = s
|
|
29 |
in
|
|
30 |
pc+1 < max_pc \\<and>
|
|
31 |
idx < length LT \\<and>
|
|
32 |
(\\<exists>ts ST'. ST = ts # ST' \\<and>
|
|
33 |
(ST' , LT[idx:=Some ts]) = s'))"
|
|
34 |
|
|
35 |
"wtl_LS (Bipush i) s s' max_pc pc =
|
|
36 |
(let (ST,LT) = s
|
|
37 |
in
|
|
38 |
pc+1 < max_pc \\<and>
|
|
39 |
((PrimT Integer) # ST , LT) = s')"
|
|
40 |
|
|
41 |
"wtl_LS (Aconst_null) s s' max_pc pc =
|
|
42 |
(let (ST,LT) = s
|
|
43 |
in
|
|
44 |
pc+1 < max_pc \\<and>
|
|
45 |
(NT # ST , LT) = s')"
|
|
46 |
|
|
47 |
consts
|
|
48 |
wtl_MO :: "[manipulate_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
|
|
49 |
primrec
|
|
50 |
"wtl_MO (Getfield F C) G s s' max_pc pc =
|
|
51 |
(let (ST,LT) = s
|
|
52 |
in
|
|
53 |
pc+1 < max_pc \\<and>
|
|
54 |
is_class G C \\<and>
|
|
55 |
(\\<exists>T oT ST'. field (G,C) F = Some(C,T) \\<and>
|
8390
|
56 |
ST = oT # ST' \\<and>
|
|
57 |
G \\<turnstile> oT \\<preceq> (Class C) \\<and>
|
|
58 |
(T # ST' , LT) = s'))"
|
8245
|
59 |
|
|
60 |
"wtl_MO (Putfield F C) G s s' max_pc pc =
|
|
61 |
(let (ST,LT) = s
|
|
62 |
in
|
|
63 |
pc+1 < max_pc \\<and>
|
|
64 |
is_class G C \\<and>
|
|
65 |
(\\<exists>T vT oT ST'.
|
|
66 |
field (G,C) F = Some(C,T) \\<and>
|
|
67 |
ST = vT # oT # ST' \\<and>
|
|
68 |
G \\<turnstile> oT \\<preceq> (Class C) \\<and>
|
8390
|
69 |
G \\<turnstile> vT \\<preceq> T \\<and>
|
8245
|
70 |
(ST' , LT) = s'))"
|
|
71 |
|
|
72 |
|
|
73 |
consts
|
|
74 |
wtl_CO :: "[create_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
|
|
75 |
primrec
|
|
76 |
"wtl_CO (New C) G s s' max_pc pc =
|
|
77 |
(let (ST,LT) = s
|
|
78 |
in
|
|
79 |
pc+1 < max_pc \\<and>
|
|
80 |
is_class G C \\<and>
|
|
81 |
((Class C) # ST , LT) = s')"
|
|
82 |
|
|
83 |
consts
|
|
84 |
wtl_CH :: "[check_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
|
|
85 |
primrec
|
|
86 |
"wtl_CH (Checkcast C) G s s' max_pc pc =
|
|
87 |
(let (ST,LT) = s
|
|
88 |
in
|
|
89 |
pc+1 < max_pc \\<and>
|
|
90 |
is_class G C \\<and>
|
|
91 |
(\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
|
|
92 |
(Class C # ST' , LT) = s'))"
|
|
93 |
|
|
94 |
consts
|
|
95 |
wtl_OS :: "[op_stack,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
|
|
96 |
primrec
|
|
97 |
"wtl_OS Pop s s' max_pc pc =
|
|
98 |
(let (ST,LT) = s
|
|
99 |
in
|
|
100 |
\\<exists>ts ST'. pc+1 < max_pc \\<and>
|
|
101 |
ST = ts # ST' \\<and>
|
|
102 |
(ST' , LT) = s')"
|
|
103 |
|
|
104 |
"wtl_OS Dup s s' max_pc pc =
|
|
105 |
(let (ST,LT) = s
|
|
106 |
in
|
|
107 |
pc+1 < max_pc \\<and>
|
|
108 |
(\\<exists>ts ST'. ST = ts # ST' \\<and>
|
|
109 |
(ts # ts # ST' , LT) = s'))"
|
|
110 |
|
|
111 |
"wtl_OS Dup_x1 s s' max_pc pc =
|
|
112 |
(let (ST,LT) = s
|
|
113 |
in
|
|
114 |
pc+1 < max_pc \\<and>
|
|
115 |
(\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and>
|
|
116 |
(ts1 # ts2 # ts1 # ST' , LT) = s'))"
|
|
117 |
|
|
118 |
"wtl_OS Dup_x2 s s' max_pc pc =
|
|
119 |
(let (ST,LT) = s
|
|
120 |
in
|
|
121 |
pc+1 < max_pc \\<and>
|
|
122 |
(\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and>
|
|
123 |
(ts1 # ts2 # ts3 # ts1 # ST' , LT) = s'))"
|
|
124 |
|
|
125 |
"wtl_OS Swap s s' max_pc pc =
|
|
126 |
(let (ST,LT) = s
|
|
127 |
in
|
|
128 |
pc+1 < max_pc \\<and>
|
|
129 |
(\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and>
|
|
130 |
(ts # ts' # ST' , LT) = s'))"
|
|
131 |
|
|
132 |
consts
|
|
133 |
wtl_BR :: "[branch,jvm_prog,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
|
|
134 |
primrec
|
|
135 |
"wtl_BR (Ifcmpeq branch) G s s' cert max_pc pc =
|
|
136 |
(let (ST,LT) = s
|
|
137 |
in
|
|
138 |
pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and>
|
8390
|
139 |
(\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and>
|
|
140 |
((\\<exists>p. ts = PrimT p \\<and> ts' = PrimT p) \\<or>
|
|
141 |
(\\<exists>r r'. ts = RefT r \\<and> ts' = RefT r')) \\<and>
|
8245
|
142 |
((ST' , LT) = s') \\<and>
|
|
143 |
cert ! (nat(int pc+branch)) \\<noteq> None \\<and>
|
|
144 |
G \\<turnstile> (ST' , LT) <=s the (cert ! (nat(int pc+branch)))))"
|
|
145 |
|
|
146 |
"wtl_BR (Goto branch) G s s' cert max_pc pc =
|
|
147 |
((let (ST,LT) = s
|
|
148 |
in
|
|
149 |
(nat(int pc+branch)) < max_pc \\<and> cert ! (nat(int pc+branch)) \\<noteq> None \\<and>
|
|
150 |
G \\<turnstile> (ST , LT) <=s the (cert ! (nat(int pc+branch)))) \\<and>
|
|
151 |
(cert ! (pc+1) = Some s'))"
|
|
152 |
|
|
153 |
consts
|
8390
|
154 |
wtl_MI :: "[meth_inv,jvm_prog,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
|
8245
|
155 |
primrec
|
8390
|
156 |
"wtl_MI (Invoke mn fpTs) G s s' cert max_pc pc =
|
8245
|
157 |
(let (ST,LT) = s
|
|
158 |
in
|
|
159 |
pc+1 < max_pc \\<and>
|
8390
|
160 |
(\\<exists>apTs X ST'. ST = (rev apTs) @ (X # ST') \\<and>
|
8245
|
161 |
length apTs = length fpTs \\<and>
|
8390
|
162 |
(\\<exists>s''. cert ! (pc+1) = Some s'' \\<and>
|
|
163 |
((s'' = s' \\<and> X = NT) \\<or>
|
|
164 |
((G \\<turnstile> s' <=s s'') \\<and> (\\<exists>C. X = Class C \\<and>
|
|
165 |
(\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
|
|
166 |
(\\<exists>D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
|
|
167 |
(rT # ST' , LT) = s')))))))"
|
8245
|
168 |
|
|
169 |
consts
|
|
170 |
wtl_MR :: "[meth_ret,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
|
|
171 |
primrec
|
|
172 |
"wtl_MR Return G rT s s' cert max_pc pc =
|
|
173 |
((let (ST,LT) = s
|
|
174 |
in
|
|
175 |
(\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT)) \\<and>
|
|
176 |
(cert ! (pc+1) = Some s'))"
|
|
177 |
|
|
178 |
|
|
179 |
consts
|
|
180 |
wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
|
|
181 |
primrec
|
|
182 |
"wtl_inst (LS ins) G rT s s' cert max_pc pc = wtl_LS ins s s' max_pc pc"
|
|
183 |
"wtl_inst (CO ins) G rT s s' cert max_pc pc = wtl_CO ins G s s' max_pc pc"
|
|
184 |
"wtl_inst (MO ins) G rT s s' cert max_pc pc = wtl_MO ins G s s' max_pc pc"
|
|
185 |
"wtl_inst (CH ins) G rT s s' cert max_pc pc = wtl_CH ins G s s' max_pc pc"
|
8390
|
186 |
"wtl_inst (MI ins) G rT s s' cert max_pc pc = wtl_MI ins G s s' cert max_pc pc"
|
8245
|
187 |
"wtl_inst (MR ins) G rT s s' cert max_pc pc = wtl_MR ins G rT s s' cert max_pc pc"
|
|
188 |
"wtl_inst (OS ins) G rT s s' cert max_pc pc = wtl_OS ins s s' max_pc pc"
|
|
189 |
"wtl_inst (BR ins) G rT s s' cert max_pc pc = wtl_BR ins G s s' cert max_pc pc"
|
|
190 |
|
|
191 |
|
|
192 |
constdefs
|
|
193 |
wtl_inst_option :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
|
|
194 |
"wtl_inst_option i G rT s0 s1 cert max_pc pc \\<equiv>
|
|
195 |
(case cert!pc of
|
|
196 |
None \\<Rightarrow> wtl_inst i G rT s0 s1 cert max_pc pc
|
|
197 |
| Some s0' \\<Rightarrow> (G \\<turnstile> s0 <=s s0') \\<and>
|
|
198 |
wtl_inst i G rT s0' s1 cert max_pc pc)"
|
|
199 |
|
|
200 |
consts
|
|
201 |
wtl_inst_list :: "[instr list,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
|
|
202 |
primrec
|
|
203 |
"wtl_inst_list [] G rT s0 s2 cert max_pc pc = (s0 = s2)"
|
|
204 |
|
|
205 |
"wtl_inst_list (instr#is) G rT s0 s2 cert max_pc pc =
|
|
206 |
(\\<exists>s1. wtl_inst_option instr G rT s0 s1 cert max_pc pc \\<and>
|
|
207 |
wtl_inst_list is G rT s1 s2 cert max_pc (pc+1))"
|
|
208 |
|
|
209 |
constdefs
|
|
210 |
wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \\<Rightarrow> bool"
|
|
211 |
"wtl_method G C pTs rT mxl ins cert \\<equiv>
|
|
212 |
let max_pc = length ins
|
|
213 |
in
|
|
214 |
0 < max_pc \\<and>
|
|
215 |
(\\<exists>s2. wtl_inst_list ins G rT
|
|
216 |
([],(Some(Class C))#((map Some pTs))@(replicate mxl None))
|
|
217 |
s2 cert max_pc 0)"
|
|
218 |
|
|
219 |
wtl_jvm_prog :: "[jvm_prog,prog_certificate] \\<Rightarrow> bool"
|
|
220 |
"wtl_jvm_prog G cert \\<equiv>
|
|
221 |
wf_prog (\\<lambda>G C (sig,rT,maxl,b).
|
|
222 |
wtl_method G C (snd sig) rT maxl b (cert C sig)) G"
|
|
223 |
|
|
224 |
end
|