author | wenzelm |
Sat, 02 Jan 2016 18:48:45 +0100 | |
changeset 62042 | 6c6ccf573479 |
parent 61361 | 8b5f00202e1a |
child 62390 | 842917225d56 |
permissions | -rw-r--r-- |
9376 | 1 |
(* Title: HOL/MicroJava/JVM/JVMExecInstr.thy |
2 |
Author: Cornelia Pusch, Gerwin Klein |
|
3 |
Copyright 1999 Technische Universitaet Muenchen |
|
4 |
*) |
|
5 |
||
10057 | 6 |
|
61361 | 7 |
section \<open>JVM Instruction Semantics\<close> |
10057 | 8 |
|
9 |
||
16417 | 10 |
theory JVMExecInstr imports JVMInstructions JVMState begin |
10057 | 11 |
|
9376 | 12 |
|
39758 | 13 |
primrec exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state" |
14 |
where |
|
9376 | 15 |
"exec_instr (Load idx) G hp stk vars Cl sig pc frs = |
39758 | 16 |
(None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)" | |
9376 | 17 |
|
18 |
"exec_instr (Store idx) G hp stk vars Cl sig pc frs = |
|
39758 | 19 |
(None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)" | |
9376 | 20 |
|
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10591
diff
changeset
|
21 |
"exec_instr (LitPush v) G hp stk vars Cl sig pc frs = |
39758 | 22 |
(None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)" | |
9376 | 23 |
|
24 |
"exec_instr (New C) G hp stk vars Cl sig pc frs = |
|
12519 | 25 |
(let (oref,xp') = new_Addr hp; |
26 |
fs = init_vars (fields(G,C)); |
|
27 |
hp' = if xp'=None then hp(oref \<mapsto> (C,fs)) else hp; |
|
28 |
pc' = if xp'=None then pc+1 else pc |
|
29 |
in |
|
39758 | 30 |
(xp', hp', (Addr oref#stk, vars, Cl, sig, pc')#frs))" | |
9376 | 31 |
|
32 |
"exec_instr (Getfield F C) G hp stk vars Cl sig pc frs = |
|
12519 | 33 |
(let oref = hd stk; |
34 |
xp' = raise_system_xcpt (oref=Null) NullPointer; |
|
35 |
(oc,fs) = the(hp(the_Addr oref)); |
|
36 |
pc' = if xp'=None then pc+1 else pc |
|
37 |
in |
|
39758 | 38 |
(xp', hp, (the(fs(F,C))#(tl stk), vars, Cl, sig, pc')#frs))" | |
9376 | 39 |
|
40 |
"exec_instr (Putfield F C) G hp stk vars Cl sig pc frs = |
|
12519 | 41 |
(let (fval,oref)= (hd stk, hd(tl stk)); |
42 |
xp' = raise_system_xcpt (oref=Null) NullPointer; |
|
43 |
a = the_Addr oref; |
|
44 |
(oc,fs) = the(hp a); |
|
45 |
hp' = if xp'=None then hp(a \<mapsto> (oc, fs((F,C) \<mapsto> fval))) else hp; |
|
46 |
pc' = if xp'=None then pc+1 else pc |
|
47 |
in |
|
39758 | 48 |
(xp', hp', (tl (tl stk), vars, Cl, sig, pc')#frs))" | |
9376 | 49 |
|
50 |
"exec_instr (Checkcast C) G hp stk vars Cl sig pc frs = |
|
12519 | 51 |
(let oref = hd stk; |
52 |
xp' = raise_system_xcpt (\<not> cast_ok G C hp oref) ClassCast; |
|
53 |
stk' = if xp'=None then stk else tl stk; |
|
54 |
pc' = if xp'=None then pc+1 else pc |
|
55 |
in |
|
39758 | 56 |
(xp', hp, (stk', vars, Cl, sig, pc')#frs))" | |
9376 | 57 |
|
9550
19a6d1289f5e
Invoke instruction gets fully qualified method name (class+name+sig) as
kleing
parents:
9376
diff
changeset
|
58 |
"exec_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs = |
12519 | 59 |
(let n = length ps; |
60 |
argsoref = take (n+1) stk; |
|
61 |
oref = last argsoref; |
|
62 |
xp' = raise_system_xcpt (oref=Null) NullPointer; |
|
63 |
dynT = fst(the(hp(the_Addr oref))); |
|
64 |
(dc,mh,mxs,mxl,c)= the (method (G,dynT) (mn,ps)); |
|
65 |
frs' = if xp'=None then |
|
28524 | 66 |
[([],rev argsoref@replicate mxl undefined,dc,(mn,ps),0)] |
12519 | 67 |
else [] |
68 |
in |
|
39758 | 69 |
(xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))" | |
62042 | 70 |
\<comment> "Because exception handling needs the pc of the Invoke instruction," |
71 |
\<comment> "Invoke doesn't change stk and pc yet (\<open>Return\<close> does that)." |
|
9376 | 72 |
|
73 |
"exec_instr Return G hp stk0 vars Cl sig0 pc frs = |
|
12519 | 74 |
(if frs=[] then |
9376 | 75 |
(None, hp, []) |
76 |
else |
|
12519 | 77 |
let val = hd stk0; (stk,loc,C,sig,pc) = hd frs; |
78 |
(mn,pt) = sig0; n = length pt |
|
79 |
in |
|
80 |
(None, hp, (val#(drop (n+1) stk),loc,C,sig,pc+1)#tl frs))" |
|
62042 | 81 |
\<comment> "Return drops arguments from the caller's stack and increases" |
82 |
\<comment> "the program counter in the caller" | |
|
9376 | 83 |
|
84 |
"exec_instr Pop G hp stk vars Cl sig pc frs = |
|
39758 | 85 |
(None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)" | |
9376 | 86 |
|
87 |
"exec_instr Dup G hp stk vars Cl sig pc frs = |
|
39758 | 88 |
(None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)" | |
9376 | 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)), |
39758 | 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))), |
|
39758 | 97 |
vars, Cl, sig, pc+1)#frs)" | |
9376 | 98 |
|
99 |
"exec_instr Swap G hp stk vars Cl sig pc frs = |
|
12519 | 100 |
(let (val1,val2) = (hd stk,hd (tl stk)) |
9376 | 101 |
in |
39758 | 102 |
(None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))" | |
9376 | 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)), |
39758 | 108 |
vars, Cl, sig, pc+1)#frs))" | |
9376 | 109 |
|
110 |
"exec_instr (Ifcmpeq i) G hp stk vars Cl sig pc frs = |
|
12519 | 111 |
(let (val1,val2) = (hd stk, hd (tl stk)); |
9376 | 112 |
pc' = if val1 = val2 then nat(int pc+i) else pc+1 |
12519 | 113 |
in |
39758 | 114 |
(None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))" | |
9376 | 115 |
|
116 |
"exec_instr (Goto i) G hp stk vars Cl sig pc frs = |
|
39758 | 117 |
(None, hp, (stk, vars, Cl, sig, nat(int pc+i))#frs)" | |
9376 | 118 |
|
12519 | 119 |
"exec_instr Throw G hp stk vars Cl sig pc frs = |
120 |
(let xcpt = raise_system_xcpt (hd stk = Null) NullPointer; |
|
121 |
xcpt' = if xcpt = None then Some (hd stk) else xcpt |
|
122 |
in |
|
123 |
(xcpt', hp, (stk, vars, Cl, sig, pc)#frs))" |
|
124 |
||
125 |
end |