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