author | kleing |
Fri, 22 Sep 2000 13:12:19 +0200 | |
changeset 10057 | 8c8d2d0d3ef8 |
parent 10056 | 9f84ffa4a8d0 |
child 10591 | 6d6cb845e841 |
permissions | -rw-r--r-- |
9376 | 1 |
(* Title: HOL/MicroJava/JVM/JVMExecInstr.thy |
2 |
ID: $Id$ |
|
3 |
Author: Cornelia Pusch, Gerwin Klein |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
5 |
*) |
|
6 |
||
10057 | 7 |
|
8 |
header {* JVM Instruction Semantics *} |
|
9 |
||
10 |
||
11 |
theory JVMExecInstr = JVMInstructions + JVMState: |
|
12 |
||
9376 | 13 |
|
14 |
consts |
|
10056 | 15 |
exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, |
16 |
cname, sig, p_count, frame list] => jvm_state" |
|
9376 | 17 |
primrec |
18 |
"exec_instr (Load idx) G hp stk vars Cl sig pc frs = |
|
19 |
(None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)" |
|
20 |
||
21 |
"exec_instr (Store idx) G hp stk vars Cl sig pc frs = |
|
22 |
(None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)" |
|
23 |
||
24 |
"exec_instr (Bipush ival) G hp stk vars Cl sig pc frs = |
|
25 |
(None, hp, (Intg ival # stk, vars, Cl, sig, pc+1)#frs)" |
|
26 |
||
27 |
"exec_instr Aconst_null G hp stk vars Cl sig pc frs = |
|
28 |
(None, hp, (Null # stk, vars, Cl, sig, pc+1)#frs)" |
|
29 |
||
30 |
"exec_instr (New C) G hp stk vars Cl sig pc frs = |
|
10057 | 31 |
(let xp' = raise_xcpt (\<forall>x. hp x \<noteq> None) OutOfMemory; |
9376 | 32 |
oref = newref hp; |
33 |
fs = init_vars (fields(G,C)); |
|
10057 | 34 |
hp' = if xp'=None then hp(oref \<mapsto> (C,fs)) else hp; |
9376 | 35 |
stk' = if xp'=None then (Addr oref)#stk else stk |
36 |
in |
|
37 |
(xp', hp', (stk', vars, Cl, sig, pc+1)#frs))" |
|
38 |
||
39 |
"exec_instr (Getfield F C) G hp stk vars Cl sig pc frs = |
|
40 |
(let oref = hd stk; |
|
41 |
xp' = raise_xcpt (oref=Null) NullPointer; |
|
42 |
(oc,fs) = the(hp(the_Addr oref)); |
|
43 |
stk' = if xp'=None then the(fs(F,C))#(tl stk) else tl stk |
|
44 |
in |
|
45 |
(xp', hp, (stk', vars, Cl, sig, pc+1)#frs))" |
|
46 |
||
47 |
"exec_instr (Putfield F C) G hp stk vars Cl sig pc frs = |
|
48 |
(let (fval,oref)= (hd stk, hd(tl stk)); |
|
49 |
xp' = raise_xcpt (oref=Null) NullPointer; |
|
50 |
a = the_Addr oref; |
|
51 |
(oc,fs) = the(hp a); |
|
10057 | 52 |
hp' = if xp'=None then hp(a \<mapsto> (oc, fs((F,C) \<mapsto> fval))) else hp |
9376 | 53 |
in |
54 |
(xp', hp', (tl (tl stk), vars, Cl, sig, pc+1)#frs))" |
|
55 |
||
56 |
"exec_instr (Checkcast C) G hp stk vars Cl sig pc frs = |
|
57 |
(let oref = hd stk; |
|
10057 | 58 |
xp' = raise_xcpt (\<not> cast_ok G C hp oref) ClassCast; |
9376 | 59 |
stk' = if xp'=None then stk else tl stk |
60 |
in |
|
61 |
(xp', hp, (stk', vars, Cl, sig, pc+1)#frs))" |
|
62 |
||
9550
19a6d1289f5e
Invoke instruction gets fully qualified method name (class+name+sig) as
kleing
parents:
9376
diff
changeset
|
63 |
"exec_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs = |
9376 | 64 |
(let n = length ps; |
65 |
argsoref = take (n+1) stk; |
|
66 |
oref = last argsoref; |
|
67 |
xp' = raise_xcpt (oref=Null) NullPointer; |
|
68 |
dynT = fst(the(hp(the_Addr oref))); |
|
69 |
(dc,mh,mxl,c)= the (method (G,dynT) (mn,ps)); |
|
10056 | 70 |
frs' = if xp'=None then |
71 |
[([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)] |
|
72 |
else [] |
|
9376 | 73 |
in |
74 |
(xp', hp, frs'@(drop (n+1) stk, vars, Cl, sig, pc+1)#frs))" |
|
75 |
||
76 |
"exec_instr Return G hp stk0 vars Cl sig0 pc frs = |
|
77 |
(if frs=[] then |
|
78 |
(None, hp, []) |
|
79 |
else |
|
80 |
let val = hd stk0; (stk,loc,C,sig,pc) = hd frs |
|
81 |
in |
|
82 |
(None, hp, (val#stk,loc,C,sig,pc)#tl frs))" |
|
83 |
||
84 |
"exec_instr Pop G hp stk vars Cl sig pc frs = |
|
85 |
(None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)" |
|
86 |
||
87 |
"exec_instr Dup G hp stk vars Cl sig pc frs = |
|
88 |
(None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)" |
|
89 |
||
90 |
"exec_instr Dup_x1 G hp stk vars Cl sig pc frs = |
|
10056 | 91 |
(None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)), |
92 |
vars, Cl, sig, pc+1)#frs)" |
|
9376 | 93 |
|
94 |
"exec_instr Dup_x2 G hp stk vars Cl sig pc frs = |
|
10056 | 95 |
(None, hp, |
96 |
(hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))), |
|
97 |
vars, Cl, sig, pc+1)#frs)" |
|
9376 | 98 |
|
99 |
"exec_instr Swap G hp stk vars Cl sig pc frs = |
|
100 |
(let (val1,val2) = (hd stk,hd (tl stk)) |
|
101 |
in |
|
102 |
(None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))" |
|
103 |
||
104 |
"exec_instr IAdd G hp stk vars Cl sig pc frs = |
|
105 |
(let (val1,val2) = (hd stk,hd (tl stk)) |
|
106 |
in |
|
10056 | 107 |
(None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), |
108 |
vars, Cl, sig, pc+1)#frs))" |
|
9376 | 109 |
|
110 |
"exec_instr (Ifcmpeq i) G hp stk vars Cl sig pc frs = |
|
111 |
(let (val1,val2) = (hd stk, hd (tl stk)); |
|
112 |
pc' = if val1 = val2 then nat(int pc+i) else pc+1 |
|
113 |
in |
|
114 |
(None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))" |
|
115 |
||
116 |
"exec_instr (Goto i) G hp stk vars Cl sig pc frs = |
|
117 |
(None, hp, (stk, vars, Cl, sig, nat(int pc+i))#frs)" |
|
118 |
||
119 |
end |