1(*  Title:      HOL/MicroJava/JVM/JVMExecInstr.thy
2    Author:     Cornelia Pusch, Gerwin Klein
3    Copyright   1999 Technische Universitaet Muenchen
4*)
5
6
7section \<open>JVM Instruction Semantics\<close>
8
9
10theory JVMExecInstr imports JVMInstructions JVMState begin
11
12
13primrec exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state"
14where
15 "exec_instr (Load idx) G hp stk vars Cl sig pc frs = 
16      (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)" |
17
18 "exec_instr (Store idx) G hp stk vars Cl sig pc frs = 
19      (None, hp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1)#frs)" |
20
21 "exec_instr (LitPush v) G hp stk vars Cl sig pc frs = 
22      (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)" |
23
24 "exec_instr (New C) G hp stk vars Cl sig pc frs = 
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 
30      (xp', hp', (Addr oref#stk, vars, Cl, sig, pc')#frs))" |
31
32 "exec_instr (Getfield F C) G hp stk vars Cl sig pc frs = 
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
38      (xp', hp, (the(fs(F,C))#(tl stk), vars, Cl, sig, pc')#frs))" |
39
40 "exec_instr (Putfield F C) G hp stk vars Cl sig pc frs = 
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
48      (xp', hp', (tl (tl stk), vars, Cl, sig, pc')#frs))" |
49
50 "exec_instr (Checkcast C) G hp stk vars Cl sig pc frs =
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
56      (xp', hp, (stk', vars, Cl, sig, pc')#frs))" |
57
58 "exec_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs =
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 
66                [([],rev argsoref@replicate mxl undefined,dc,(mn,ps),0)]
67              else []
68   in 
69      (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))" |
70  \<comment> \<open>Because exception handling needs the pc of the Invoke instruction,\<close>
71  \<comment> \<open>Invoke doesn't change stk and pc yet (\<open>Return\<close> does that).\<close>
72
73 "exec_instr Return G hp stk0 vars Cl sig0 pc frs =
74  (if frs=[] then 
75     (None, hp, [])
76   else 
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))"
81  \<comment> \<open>Return drops arguments from the caller's stack and increases\<close>
82  \<comment> \<open>the program counter in the caller\<close> |
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 = 
91      (None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)), 
92                  vars, Cl, sig, pc+1)#frs)" |
93
94 "exec_instr Dup_x2 G hp stk vars Cl sig pc frs = 
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)" |
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
107      (None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), 
108       vars, Cl, sig, pc+1)#frs))" |
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 "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
125end
126