Up to index of Isabelle/HOL/SafeImp
theory JVMExecInstr(* Title: HOL/MicroJava/JVM/JVMExecInstr.thy
ID: $Id: JVMExecInstr.thy,v 1.8.2.20 2002/08/10 19:58:14 kleing Exp $
Author: Cornelia Pusch, Gerwin Klein
Modified: Delfin Ruperez, June 2008, adding static heap and related
instructions, and tableswitch instruction
Copyright 1999 Technische Universitaet Muenchen
*)
header {* \isaheader{JVM Instruction Semantics} *}
theory JVMExecInstr
imports JVMInstructions
begin
text {* the method name of constructors: *}
consts
init :: mname
text {* replace a by b in l: *}
constdefs
replace :: "'a => 'a => 'a list => 'a list"
"replace a b l == map (λx. if x = a then b else x) l"
text {* some lemmas about replace *}
lemma replace_removes_elem:
"a ≠ b ==> a ∉ set (replace a b l)"
by (unfold replace_def) auto
lemma replace_length [simp]:
"length (replace a b l) = length l" by (simp add: replace_def)
lemma replace_Nil [iff]:
"replace x y [] = []" by (simp add: replace_def)
lemma replace_Cons:
"replace x y (l#ls) = (if l = x then y else l)#(replace x y ls)"
by (simp add: replace_def)
lemma replace_map:
"inj f ==> replace (f x) (f y) (map f l) = map f (replace x y l)"
apply (induct l)
apply (simp add: replace_def)
apply (simp add: replace_def)
apply clarify
apply (drule injD, assumption)
apply simp
done
lemma replace_id:
"x ∉ set l ∨ x = y ==> replace x y l = l"
apply (induct l)
apply (auto simp add: replace_def)
done
text {* single execution step for each instruction: *}
consts
exec_instr :: "[instr, jvm_prog, sheap, aheap, init_heap, opstack, locvars,
cname, sig, p_count, ref_upd, frame list] => jvm_state"
primrec
"exec_instr (Load idx) G shp hp ihp stk vars Cl sig pc z frs =
(None,shp, hp, ihp, ((vars ! idx) # stk, vars, Cl, sig, pc+1, z)#frs)"
"exec_instr (Store idx) G shp hp ihp stk vars Cl sig pc z frs =
(None,shp, hp, ihp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1, z)#frs)"
"exec_instr (LitPush v) G shp hp ihp stk vars Cl sig pc z frs =
(None,shp, hp, ihp, (v # stk, vars, Cl, sig, pc+1, z)#frs)"
"exec_instr (New C) G shp hp ihp stk vars Cl sig pc z frs =
(let (oref,xp') = new_Addr hp;
hp' = if xp'=None then hp(oref \<mapsto> blank G C) else hp;
ihp' = if xp'=None then ihp(oref := UnInit C pc) else ihp;
stk' = if xp'=None then (Addr oref)#stk else stk;
pc' = if xp'=None then pc+1 else pc
in (xp',shp, hp', ihp', (stk', vars, Cl, sig, pc', z)#frs))"
"exec_instr (Getfield F C) G shp hp ihp stk vars Cl sig pc z frs =
(let oref = hd stk;
xp' = raise_system_xcpt (oref=Null) NullPointer;
(oc,fs) = the_obj (the(hp(the_Addr oref)));
stk' = if xp'=None then the(fs(F,C))#(tl stk) else tl stk;
pc' = if xp'=None then pc+1 else pc
in (xp',shp, hp, ihp, (stk', vars, Cl, sig, pc', z)#frs))"
"exec_instr (Putfield F C) G shp hp ihp stk vars Cl sig pc z frs =
(let (fval,oref) = (hd stk, hd(tl stk));
xp' = raise_system_xcpt (oref=Null) NullPointer;
a = the_Addr oref;
(oc,fs) = the_obj (the(hp a));
hp' = if xp'=None then hp(a \<mapsto> Obj oc (fs((F,C) \<mapsto> fval)))
else hp;
pc' = if xp'=None then pc+1 else pc
in (xp',shp, hp', ihp, (tl (tl stk), vars, Cl, sig, pc', z)#frs))"
"exec_instr (Checkcast C) G shp hp ihp stk vars Cl sig pc z frs =
(let oref = hd stk;
xp' = raise_system_xcpt (¬cast_ok G C hp oref) ClassCast;
stk' = if xp'=None then stk else tl stk;
pc' = if xp'=None then pc+1 else pc
in (xp',shp, hp, ihp, (stk', vars, Cl, sig, pc', z)#frs))"
"exec_instr (Invoke C mn ps) G shp hp ihp stk vars Cl sig pc z frs =
(let n = length ps;
args = take n stk;
oref = stk!n;
xp' = raise_system_xcpt (oref=Null) NullPointer;
dynT = the_Class (obj_ty (the(hp (the_Addr oref))));
(dc,mh,mxs,mxl,c) = the (method (G,dynT) (mn,ps));
frs' = (if xp'=None then
[([],oref#(rev args)@(replicate mxl arbitrary),dc,(mn,ps),0,arbitrary)]
else [])
in (xp',shp, hp, ihp, frs'@(stk, vars, Cl, sig, pc, z)#frs))"
-- "Because exception handling needs the pc of the Invoke instruction,"
-- "Invoke doesn't change @{text stk} and @{text pc} yet (@{text Return} does that)."
"exec_instr (Invoke_special C mn ps) G shp hp ihp stk vars Cl sig pc z frs =
(let n = length ps;
args = take n stk;
oref = stk!n;
addr = the_Addr oref;
x' = raise_system_xcpt (oref=Null) NullPointer;
dynT = the_Class (obj_ty (the(hp addr)));
(dc,mh,mxs,mxl,c)= the (method (G,C) (mn,ps));
(addr',x'') = new_Addr hp;
xp' = if x' = None then x'' else x';
hp' = if xp' = None then hp(addr' \<mapsto> blank G dynT) else hp;
ihp' = if C = Object then ihp(addr':= Init (Class dynT))
else ihp(addr' := PartInit C);
ihp'' = if xp' = None then ihp' else ihp;
z' = if C = Object then (Addr addr', Addr addr') else (Addr addr', Null);
frs' = (if xp'=None then
[([],(Addr addr')#(rev args)@(replicate mxl arbitrary),dc,(mn,ps),0,z')]
else [])
in (xp',shp, hp', ihp'', frs'@(stk, vars, Cl, sig, pc, z)#frs))"
(* Return a value from method *)
"exec_instr Return G shp hp ihp stk0 vars Cl sig0 pc z0 frs =
(if frs=[] then (None, shp, hp, ihp, [])
else let
val = hd stk0;
(mn,pt) = sig0;
(stk,loc,C,sig,pc,z) = hd frs;
(b,c) = z0;
(a,c') = z;
n = length pt;
addr = stk!n;
stk' = if mn=init then val#replace addr c stk else val#stk;
loc' = if mn=init then replace addr c loc else loc;
z' = if mn=init ∧ z = (addr,Null) then (a,c) else z
in (None, shp , hp, ihp, (stk',loc',C,sig,pc+1,z')#tl frs))"
-- "Return drops arguments from the caller's stack and increases"
-- "the program counter in the caller"
-- "@{text z} is only updated if we are in a constructor and have initialized the"
-- "same reference as the constructor in the frame above (otherwise we are"
-- "in the last constructor of the init chain)"
(* Return (void) from method *)
"exec_instr Return_Void G shp hp ihp stk0 vars Cl sig0 pc z0 frs =
(if frs=[] then (None, shp, hp, ihp, [])
else let
(mn,pt) = sig0;
(stk,loc,C,sig,pc,z) = hd frs;
(b,c) = z0;
(a,c') = z;
n = length pt;
addr = stk!n;
stk' = if mn=init then replace addr c stk else stk;
loc' = if mn=init then replace addr c loc else loc;
z' = if mn=init ∧ z = (addr,Null) then (a,c) else z
in (None, shp , hp, ihp, (stk',loc',C,sig,pc+1,z')#tl frs))"
-- "All items on the current method's operand stack are discarded"
"exec_instr Pop G shp hp ihp stk vars Cl sig pc z frs =
(None, shp, hp, ihp, (tl stk, vars, Cl, sig, pc+1, z)#frs)"
"exec_instr Dup G shp hp ihp stk vars Cl sig pc z frs =
(None, shp, hp, ihp, (hd stk # stk, vars, Cl, sig, pc+1, z)#frs)"
"exec_instr Dup2 G shp hp ihp stk vars Cl sig pc z frs =
(None, shp, hp, ihp, (hd stk # hd (tl stk) # stk,vars,Cl,sig,pc+1,z)#frs)"
"exec_instr Dup_x1 G shp hp ihp stk vars Cl sig pc z frs =
(None, shp, hp, ihp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)),
vars, Cl, sig, pc+1, z)#frs)"
"exec_instr Dup_x2 G shp hp ihp stk vars Cl sig pc z frs =
(None,shp, hp, ihp,
(hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))),
vars, Cl, sig, pc+1, z)#frs)"
"exec_instr Swap G shp hp ihp stk vars Cl sig pc z frs =
(let (val1,val2) = (hd stk,hd (tl stk))
in (None,shp, hp, ihp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1, z)#frs))"
"exec_instr IAdd G shp hp ihp stk vars Cl sig pc z frs =
(let (val1,val2) = (hd stk,hd (tl stk))
in (None,shp, hp, ihp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)),
vars, Cl, sig, pc+1, z)#frs))"
"exec_instr (Ifcmpeq i) G shp hp ihp stk vars Cl sig pc z frs =
(let (val1,val2) = (hd stk, hd (tl stk));
pc' = if val1 = val2 then nat(int pc+i) else pc+1
in (None,shp, hp, ihp, (tl (tl stk), vars, Cl, sig, pc', z)#frs))"
"exec_instr (Goto i) G shp hp ihp stk vars Cl sig pc z frs =
(None,shp, hp, ihp, (stk, vars, Cl, sig, nat(int pc+i), z)#frs)"
"exec_instr Throw G shp hp ihp stk vars Cl sig pc z frs =
(let xcpt = raise_system_xcpt (hd stk = Null) NullPointer;
xcpt' = if xcpt = None then Some (hd stk) else xcpt
in (xcpt',shp, hp, ihp, (stk, vars, Cl, sig, pc, z)#frs))"
"exec_instr (Jsr i) G shp hp ihp stk vars Cl sig pc z frs =
(None,shp, hp, ihp, (RetAddr (pc+1)#stk, vars, Cl, sig, nat(int pc+i), z)#frs)"
"exec_instr (Ret idx) G shp hp ihp stk vars Cl sig pc z frs =
(None,shp,hp, ihp, (stk, vars, Cl, sig, the_RetAddr (vars!idx), z)#frs)"
"exec_instr (ArrLoad) G shp hp ihp stk vars Cl sig pc z frs =
(let idx = the_Intg (hd stk);
aref = hd (tl stk);
xp'' = raise_system_xcpt (aref=Null) NullPointer;
(T,l,en) = the_arr (the(hp(the_Addr aref)));
xp' = if xp''=None then raise_system_xcpt (int l ≤ idx ∨ idx < 0) ArrayIndexOutOfBounds
else xp'';
stk' = the (en (nat idx)) # (tl (tl stk));
pc' = if xp'=None then pc+1 else pc
in (xp',shp, hp, ihp, (stk', vars, Cl, sig, pc', z)#frs))"
"exec_instr (ArrStore) G shp hp ihp stk vars Cl sig pc z frs =
(let val = hd stk;
idx = the_Intg (hd (tl stk));
aref = hd (tl (tl stk));
xp'' = raise_system_xcpt (aref=Null) NullPointer;
a = the_Addr aref;
(T,l,en) = the_arr (the(hp a));
xp'''= if xp''=None then raise_system_xcpt (int l ≤ idx ∨ idx < 0) ArrayIndexOutOfBounds
else xp'';
xp' = if xp'''=None then raise_system_xcpt ( False) ArrayStore else xp''';
hp' = if xp'=None then hp(a \<mapsto> Arr T l (en(nat idx \<mapsto> val))) else hp;
pc' = if xp'=None then pc+1 else pc
in (xp',shp, hp', ihp, (tl (tl (tl stk)), vars, Cl, sig, pc', z)#frs))"
"exec_instr (ArrLength) G shp hp ihp stk vars Cl sig pc z frs =
(let aref = hd stk;
xp' = raise_system_xcpt (aref=Null) NullPointer;
a = the_Addr aref;
(T,l,en) = the_arr (the(hp a));
pc' = if xp'=None then pc+1 else pc
in (xp', shp, hp, ihp, (Intg (int l)#(tl stk), vars, Cl, sig, pc', z)#frs))"
"exec_instr (ArrNew T) G shp hp ihp stk vars Cl sig pc z frs =
(let len = the_Intg (hd stk);
xp''' = raise_system_xcpt (len < 0) NegativeArraySize;
(aref,xp'') = new_Addr hp;
xp' = if xp'''=None then xp'' else xp''';
hp' = if xp'=None then hp(aref \<mapsto> blank_arr T (nat len)) else hp;
ihp' = if xp'=None then ihp(aref := Init (T.[])) else ihp;
stk' = (Addr aref)#tl stk;
pc' = if xp'=None then pc+1 else pc
in (xp',shp, hp', ihp', (stk', vars, Cl, sig, pc', z)#frs))"
(* Execution Binary Operation *)
"exec_instr (BinOp bop) G shp hp ihp stk vars Cl sig pc z frs =
(let (val2,val1) = (hd stk, hd (tl stk))
in (None,shp, hp, ihp, ((applyBinOp bop val1 val2 )#(tl (tl stk)), vars, Cl, sig, pc + 1, z)#frs))"
(* Execution Invocation static Method *)
"exec_instr(Invoke_static C mn ps) G shp hp ihp stk vars Cl sig pc z frs =
(let n = length ps;
args = take n stk;
(dc,mh,mxs,mxl,c) = the (method (G,C) (mn,ps));
frs' = [([], (rev args)@(replicate mxl arbitrary),dc,(mn,ps),0,arbitrary)]
in (None,shp,hp,ihp,frs'@(stk,vars,Cl,sig,pc,z)#frs))"
(* Execution Tableswitch *)
"exec_instr(Tableswitch n m t) G shp hp ihp stk vars Cl sig pc z frs =
(let val = hd stk;
v = the_Intg val;
pc' = if (v < n) ∨ (v > m) then pc + nat(t!(nat(m - n + 1))) else pc + nat(t!(nat(v - n)))
in (None,shp,hp,ihp,((tl stk),vars,Cl,sig,pc',z)#frs))"
(* Execution Getstatic *)
"exec_instr (Getstatic F C) G shp hp ihp stk vars Cl sig pc z frs =
(let v = the (shp (C,F));
pc' = pc + 1
in (None,shp, hp, ihp, ((v#stk), vars, Cl, sig, pc', z)#frs))"
(* Execution Putstatic *)
"exec_instr (Putstatic F C) G shp hp ihp stk vars Cl sig pc z frs =
(let shp' = shp((C,F) \<mapsto> hd stk );
pc' = pc + 1
in (None, shp', hp, ihp, ((tl stk), vars, Cl, sig, pc', z)#frs))"
(* Execution Ifcmp Generic *)
"exec_instr (Ifcmp bop i) G shp hp ihp stk vars Cl sig pc z frs =
(let (val1,val2) = (hd stk, hd (tl stk));
pc' = if ((applyIf bop val1 val2) = True) then nat(int pc+i) else pc+1
in (None,shp, hp, ihp, (tl (tl stk), vars, Cl, sig, pc', z)#frs))"
end
lemma replace_removes_elem:
a ≠ b ==> a ∉ set (replace a b l)
lemma replace_length:
length (replace a b l) = length l
lemma replace_Nil:
replace x y [] = []
lemma replace_Cons:
replace x y (l # ls) = (if l = x then y else l) # replace x y ls
lemma replace_map:
inj f ==> replace (f x) (f y) (map f l) = map f (replace x y l)
lemma replace_id:
x ∉ set l ∨ x = y ==> replace x y l = l