author | nipkow |
Fri, 26 Nov 1999 08:46:59 +0100 | |
changeset 8034 | 6fc37b5c5e98 |
parent 8032 | 1eaae1a2f8ff |
child 8048 | b7f7e18eb584 |
permissions | -rw-r--r-- |
8011 | 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> |
|
8023 | 25 |
G \\<turnstile> (ts # ST , LT) <=s phi ! (pc+1)))" |
8011 | 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> |
|
8023 | 33 |
G \\<turnstile> (ST' , LT[idx:=Some ts]) <=s phi ! (pc+1)))" |
8011 | 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> |
|
8023 | 39 |
G \\<turnstile> ((PrimT Integer) # ST , LT) <=s phi ! (pc+1))" |
8011 | 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> |
|
8023 | 45 |
G \\<turnstile> (NT # ST , LT) <=s phi ! (pc+1))" |
8011 | 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> |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
55 |
(\\<exists>T oT ST'. field (G,C) F = Some(C,T) \\<and> |
8011 | 56 |
ST = oT # ST' \\<and> |
57 |
G \\<turnstile> oT \\<preceq> (Class C) \\<and> |
|
8023 | 58 |
G \\<turnstile> (T # ST' , LT) <=s phi ! (pc+1)))" |
8011 | 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'. |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
66 |
field (G,C) F = Some(C,T) \\<and> |
8011 | 67 |
ST = vT # oT # ST' \\<and> |
68 |
G \\<turnstile> oT \\<preceq> (Class C) \\<and> |
|
69 |
G \\<turnstile> vT \\<preceq> T \\<and> |
|
8023 | 70 |
G \\<turnstile> (ST' , LT) <=s phi ! (pc+1)))" |
8011 | 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> |
|
8023 | 81 |
G \\<turnstile> ((Class C) # ST , LT) <=s phi ! (pc+1))" |
8011 | 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> |
|
8023 | 92 |
G \\<turnstile> (Class C # ST' , LT) <=s phi ! (pc+1)))" |
8011 | 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> |
|
8023 | 102 |
G \\<turnstile> (ST' , LT) <=s phi ! (pc+1))" |
8011 | 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> |
|
8023 | 109 |
G \\<turnstile> (ts # ts # ST' , LT) <=s phi ! (pc+1)))" |
8011 | 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> |
|
8023 | 116 |
G \\<turnstile> (ts1 # ts2 # ts1 # ST' , LT) <=s phi ! (pc+1)))" |
8011 | 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> |
|
8023 | 123 |
G \\<turnstile> (ts1 # ts2 # ts3 # ts1 # ST' , LT) <=s phi ! (pc+1)))" |
8011 | 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> |
|
8023 | 130 |
G \\<turnstile> (ts # ts' # ST' , LT) <=s phi ! (pc+1)))" |
8011 | 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> |
|
8023 | 140 |
G \\<turnstile> (ST' , LT) <=s phi ! (pc+1) \\<and> |
141 |
G \\<turnstile> (ST' , LT) <=s phi ! (nat(int pc+branch))))" |
|
8011 | 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> |
|
8023 | 146 |
G \\<turnstile> (ST , LT) <=s phi ! (nat(int pc+branch)))" |
8011 | 147 |
|
148 |
consts |
|
149 |
wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" |
|
150 |
primrec |
|
8032 | 151 |
"wt_MI (Invoke mn fpTs) G phi max_pc pc = |
8011 | 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> |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
158 |
(\\<exists>D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\<and> |
8023 | 159 |
G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))" |
8011 | 160 |
|
8032 | 161 |
consts |
162 |
wt_MR :: "[meth_ret,jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool" |
|
163 |
primrec |
|
164 |
"wt_MR Return G rT phi pc = |
|
8011 | 165 |
(let (ST,LT) = phi ! pc |
166 |
in |
|
167 |
(\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))" |
|
168 |
||
169 |
||
170 |
constdefs |
|
171 |
wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count] \\<Rightarrow> bool" |
|
172 |
"wt_instr instr G rT phi max_pc pc \\<equiv> |
|
173 |
case instr of |
|
174 |
LS ins \\<Rightarrow> wt_LS ins G phi max_pc pc |
|
175 |
| CO ins \\<Rightarrow> wt_CO ins G phi max_pc pc |
|
176 |
| MO ins \\<Rightarrow> wt_MO ins G phi max_pc pc |
|
177 |
| CH ins \\<Rightarrow> wt_CH ins G phi max_pc pc |
|
178 |
| MI ins \\<Rightarrow> wt_MI ins G phi max_pc pc |
|
8032 | 179 |
| MR ins \\<Rightarrow> wt_MR ins G rT phi pc |
8011 | 180 |
| OS ins \\<Rightarrow> wt_OS ins G phi max_pc pc |
181 |
| BR ins \\<Rightarrow> wt_BR ins G phi max_pc pc" |
|
182 |
||
183 |
||
184 |
constdefs |
|
185 |
wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool" |
|
186 |
"wt_start G C pTs mxl phi \\<equiv> |
|
8023 | 187 |
G \\<turnstile> ([],(Some(Class C))#((map Some pTs))@(replicate mxl None)) <=s phi!0" |
8011 | 188 |
|
189 |
||
190 |
wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool" |
|
191 |
"wt_method G cn pTs rT mxl ins phi \\<equiv> |
|
192 |
let max_pc = length ins |
|
193 |
in |
|
194 |
0 < max_pc \\<and> wt_start G cn pTs mxl phi \\<and> |
|
195 |
(\\<forall>pc. pc<max_pc \\<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)" |
|
196 |
||
197 |
wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool" |
|
198 |
"wt_jvm_prog G phi \\<equiv> |
|
199 |
wf_prog (\\<lambda>G C (sig,rT,maxl,b). |
|
200 |
wt_method G C (snd sig) rT maxl b (phi C sig)) G" |
|
201 |
||
202 |
end |