author | kleing |
Mon, 17 Jul 2000 14:00:53 +0200 | |
changeset 9376 | c32c5696ec2a |
parent 9271 | c26964691975 |
child 9549 | 40d64cb4f4e6 |
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 |
|
9376 | 17 |
wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count] \\<Rightarrow> bool" |
18 |
||
8011 | 19 |
primrec |
9376 | 20 |
"wt_instr (Load idx) G rT phi max_pc pc = |
8011 | 21 |
(let (ST,LT) = phi ! pc |
22 |
in |
|
23 |
pc+1 < max_pc \\<and> |
|
24 |
idx < length LT \\<and> |
|
25 |
(\\<exists>ts. (LT ! idx) = Some ts \\<and> |
|
8023 | 26 |
G \\<turnstile> (ts # ST , LT) <=s phi ! (pc+1)))" |
8011 | 27 |
|
9376 | 28 |
"wt_instr (Store idx) G rT phi max_pc pc = |
8011 | 29 |
(let (ST,LT) = phi ! pc |
30 |
in |
|
31 |
pc+1 < max_pc \\<and> |
|
32 |
idx < length LT \\<and> |
|
33 |
(\\<exists>ts ST'. ST = ts # ST' \\<and> |
|
8023 | 34 |
G \\<turnstile> (ST' , LT[idx:=Some ts]) <=s phi ! (pc+1)))" |
8011 | 35 |
|
9376 | 36 |
"wt_instr (Bipush i) G rT phi max_pc pc = |
8011 | 37 |
(let (ST,LT) = phi ! pc |
38 |
in |
|
39 |
pc+1 < max_pc \\<and> |
|
8023 | 40 |
G \\<turnstile> ((PrimT Integer) # ST , LT) <=s phi ! (pc+1))" |
8011 | 41 |
|
9376 | 42 |
"wt_instr (Aconst_null) G rT phi max_pc pc = |
8011 | 43 |
(let (ST,LT) = phi ! pc |
44 |
in |
|
45 |
pc+1 < max_pc \\<and> |
|
8023 | 46 |
G \\<turnstile> (NT # ST , LT) <=s phi ! (pc+1))" |
8011 | 47 |
|
9376 | 48 |
"wt_instr (Getfield F C) G rT phi max_pc pc = |
8011 | 49 |
(let (ST,LT) = phi ! pc |
50 |
in |
|
51 |
pc+1 < max_pc \\<and> |
|
52 |
is_class G C \\<and> |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
53 |
(\\<exists>T oT ST'. field (G,C) F = Some(C,T) \\<and> |
8011 | 54 |
ST = oT # ST' \\<and> |
55 |
G \\<turnstile> oT \\<preceq> (Class C) \\<and> |
|
8023 | 56 |
G \\<turnstile> (T # ST' , LT) <=s phi ! (pc+1)))" |
8011 | 57 |
|
9376 | 58 |
"wt_instr (Putfield F C) G rT phi max_pc pc = |
8011 | 59 |
(let (ST,LT) = phi ! pc |
60 |
in |
|
61 |
pc+1 < max_pc \\<and> |
|
62 |
is_class G C \\<and> |
|
63 |
(\\<exists>T vT oT ST'. |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8032
diff
changeset
|
64 |
field (G,C) F = Some(C,T) \\<and> |
8011 | 65 |
ST = vT # oT # ST' \\<and> |
66 |
G \\<turnstile> oT \\<preceq> (Class C) \\<and> |
|
67 |
G \\<turnstile> vT \\<preceq> T \\<and> |
|
8023 | 68 |
G \\<turnstile> (ST' , LT) <=s phi ! (pc+1)))" |
8011 | 69 |
|
9376 | 70 |
"wt_instr (New C) G rT phi max_pc pc = |
8011 | 71 |
(let (ST,LT) = phi ! pc |
72 |
in |
|
73 |
pc+1 < max_pc \\<and> |
|
74 |
is_class G C \\<and> |
|
8023 | 75 |
G \\<turnstile> ((Class C) # ST , LT) <=s phi ! (pc+1))" |
8011 | 76 |
|
9376 | 77 |
"wt_instr (Checkcast C) G rT phi max_pc pc = |
8011 | 78 |
(let (ST,LT) = phi ! pc |
79 |
in |
|
80 |
pc+1 < max_pc \\<and> |
|
81 |
is_class G C \\<and> |
|
82 |
(\\<exists>rt ST'. ST = RefT rt # ST' \\<and> |
|
8023 | 83 |
G \\<turnstile> (Class C # ST' , LT) <=s phi ! (pc+1)))" |
8011 | 84 |
|
9376 | 85 |
"wt_instr Pop G rT phi max_pc pc = |
8011 | 86 |
(let (ST,LT) = phi ! pc |
87 |
in |
|
88 |
\\<exists>ts ST'. pc+1 < max_pc \\<and> |
|
89 |
ST = ts # ST' \\<and> |
|
8023 | 90 |
G \\<turnstile> (ST' , LT) <=s phi ! (pc+1))" |
8011 | 91 |
|
9376 | 92 |
"wt_instr Dup G rT phi max_pc pc = |
8011 | 93 |
(let (ST,LT) = phi ! pc |
94 |
in |
|
95 |
pc+1 < max_pc \\<and> |
|
96 |
(\\<exists>ts ST'. ST = ts # ST' \\<and> |
|
8023 | 97 |
G \\<turnstile> (ts # ts # ST' , LT) <=s phi ! (pc+1)))" |
8011 | 98 |
|
9376 | 99 |
"wt_instr Dup_x1 G rT phi max_pc pc = |
8011 | 100 |
(let (ST,LT) = phi ! pc |
101 |
in |
|
102 |
pc+1 < max_pc \\<and> |
|
103 |
(\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and> |
|
8023 | 104 |
G \\<turnstile> (ts1 # ts2 # ts1 # ST' , LT) <=s phi ! (pc+1)))" |
8011 | 105 |
|
9376 | 106 |
"wt_instr Dup_x2 G rT phi max_pc pc = |
8011 | 107 |
(let (ST,LT) = phi ! pc |
108 |
in |
|
109 |
pc+1 < max_pc \\<and> |
|
110 |
(\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and> |
|
8023 | 111 |
G \\<turnstile> (ts1 # ts2 # ts3 # ts1 # ST' , LT) <=s phi ! (pc+1)))" |
8011 | 112 |
|
9376 | 113 |
"wt_instr Swap G rT phi max_pc pc = |
8011 | 114 |
(let (ST,LT) = phi ! pc |
115 |
in |
|
116 |
pc+1 < max_pc \\<and> |
|
117 |
(\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and> |
|
8023 | 118 |
G \\<turnstile> (ts # ts' # ST' , LT) <=s phi ! (pc+1)))" |
8011 | 119 |
|
9376 | 120 |
"wt_instr IAdd G rT phi max_pc pc = |
9260 | 121 |
(let (ST,LT) = phi ! pc |
122 |
in |
|
123 |
pc+1 < max_pc \\<and> |
|
124 |
(\\<exists>ST'. ST = (PrimT Integer) # (PrimT Integer) # ST' \\<and> |
|
125 |
G \\<turnstile> ((PrimT Integer) # ST' , LT) <=s phi ! (pc+1)))" |
|
126 |
||
9376 | 127 |
"wt_instr (Ifcmpeq branch) G rT phi max_pc pc = |
8011 | 128 |
(let (ST,LT) = phi ! pc |
129 |
in |
|
130 |
pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and> |
|
8386
3e56677d3b98
minor adjustments in branch and method invocation for completeness of LBV
kleing
parents:
8200
diff
changeset
|
131 |
(\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and> |
3e56677d3b98
minor adjustments in branch and method invocation for completeness of LBV
kleing
parents:
8200
diff
changeset
|
132 |
((\\<exists>p. ts = PrimT p \\<and> ts' = PrimT p) \\<or> |
3e56677d3b98
minor adjustments in branch and method invocation for completeness of LBV
kleing
parents:
8200
diff
changeset
|
133 |
(\\<exists>r r'. ts = RefT r \\<and> ts' = RefT r')) \\<and> |
8023 | 134 |
G \\<turnstile> (ST' , LT) <=s phi ! (pc+1) \\<and> |
135 |
G \\<turnstile> (ST' , LT) <=s phi ! (nat(int pc+branch))))" |
|
8200
700067a98634
Branch: top elements of stack only need to be convertible (not equal)
kleing
parents:
8048
diff
changeset
|
136 |
|
9376 | 137 |
"wt_instr (Goto branch) G rT phi max_pc pc = |
8011 | 138 |
(let (ST,LT) = phi ! pc |
139 |
in |
|
140 |
(nat(int pc+branch)) < max_pc \\<and> |
|
8023 | 141 |
G \\<turnstile> (ST , LT) <=s phi ! (nat(int pc+branch)))" |
8011 | 142 |
|
9376 | 143 |
"wt_instr (Invoke mn fpTs) G rT phi max_pc pc = |
8011 | 144 |
(let (ST,LT) = phi ! pc |
8386
3e56677d3b98
minor adjustments in branch and method invocation for completeness of LBV
kleing
parents:
8200
diff
changeset
|
145 |
in |
8011 | 146 |
pc+1 < max_pc \\<and> |
8386
3e56677d3b98
minor adjustments in branch and method invocation for completeness of LBV
kleing
parents:
8200
diff
changeset
|
147 |
(\\<exists>apTs X ST'. ST = (rev apTs) @ (X # ST') \\<and> |
8011 | 148 |
length apTs = length fpTs \\<and> |
8386
3e56677d3b98
minor adjustments in branch and method invocation for completeness of LBV
kleing
parents:
8200
diff
changeset
|
149 |
(X = NT \\<or> (\\<exists>C. X = Class C \\<and> |
8011 | 150 |
(\\<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
|
151 |
(\\<exists>D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\<and> |
8386
3e56677d3b98
minor adjustments in branch and method invocation for completeness of LBV
kleing
parents:
8200
diff
changeset
|
152 |
G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))))" |
8011 | 153 |
|
9376 | 154 |
"wt_instr Return G rT phi max_pc pc = |
8011 | 155 |
(let (ST,LT) = phi ! pc |
156 |
in |
|
157 |
(\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))" |
|
158 |
||
159 |
||
160 |
constdefs |
|
161 |
wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool" |
|
162 |
"wt_start G C pTs mxl phi \\<equiv> |
|
8023 | 163 |
G \\<turnstile> ([],(Some(Class C))#((map Some pTs))@(replicate mxl None)) <=s phi!0" |
8011 | 164 |
|
165 |
||
166 |
wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool" |
|
8048 | 167 |
"wt_method G C pTs rT mxl ins phi \\<equiv> |
8011 | 168 |
let max_pc = length ins |
169 |
in |
|
8386
3e56677d3b98
minor adjustments in branch and method invocation for completeness of LBV
kleing
parents:
8200
diff
changeset
|
170 |
length ins < length phi \\<and> 0 < max_pc \\<and> wt_start G C pTs mxl phi \\<and> |
8011 | 171 |
(\\<forall>pc. pc<max_pc \\<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)" |
172 |
||
173 |
wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool" |
|
174 |
"wt_jvm_prog G phi \\<equiv> |
|
175 |
wf_prog (\\<lambda>G C (sig,rT,maxl,b). |
|
176 |
wt_method G C (snd sig) rT maxl b (phi C sig)) G" |
|
177 |
||
178 |
end |