Up to index of Isabelle/HOL/arrays
theory JVMExecInstr = JVMInstructions + JVMState:(* Title: HOL/MicroJava/JVM/JVMExecInstr.thy
ID: $Id: JVMExecInstr.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
Author: Cornelia Pusch, Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
*)
header {* \isaheader{JVM Instruction Semantics} *}
theory JVMExecInstr = JVMInstructions + JVMState:
text {* the method name of constructors: *}
consts
init :: mname
text {* replace a by b in l: *}
constdefs
replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
"replace a b l == map (\<lambda>x. if x = a then b else x) l"
text {* some lemmas about replace *}
lemma replace_removes_elem:
"a \<noteq> b \<Longrightarrow> a \<notin> 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 \<notin> set l \<or> x = y \<Longrightarrow> 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, aheap, init_heap, opstack, locvars,
cname, sig, p_count, ref_upd, frame list] => jvm_state"
primrec
"exec_instr (Load idx) G hp ihp stk vars Cl sig pc z frs =
(None, hp, ihp, ((vars ! idx) # stk, vars, Cl, sig, pc+1, z)#frs)"
"exec_instr (Store idx) G hp ihp stk vars Cl sig pc z frs =
(None, hp, ihp, (tl stk, vars[idx:=hd stk], Cl, sig, pc+1, z)#frs)"
"exec_instr (LitPush v) G hp ihp stk vars Cl sig pc z frs =
(None, hp, ihp, (v # stk, vars, Cl, sig, pc+1, z)#frs)"
"exec_instr (New C) G 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', hp', ihp', (stk', vars, Cl, sig, pc', z)#frs))"
"exec_instr (Getfield F C) G 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', hp, ihp, (stk', vars, Cl, sig, pc', z)#frs))"
"exec_instr (Putfield F C) G 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', hp', ihp, (tl (tl stk), vars, Cl, sig, pc', z)#frs))"
"exec_instr (Checkcast C) G 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', hp, ihp, (stk', vars, Cl, sig, pc', z)#frs))"
"exec_instr (Invoke C mn ps) G 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', 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 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', hp', ihp'', frs'@(stk, vars, Cl, sig, pc, z)#frs))"
"exec_instr Return G hp ihp stk0 vars Cl sig0 pc z0 frs =
(if frs=[] then
(None, 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;
args = take n stk;
addr = stk!n;
drpstk = drop (n+1) stk;
stk' = if mn=init then val#replace addr c drpstk else val#drpstk;
loc' = if mn=init then replace addr c loc else loc;
z' = if mn=init \<and> z = (addr,Null) then (a,c) else z
in
(None, 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)"
"exec_instr Pop G hp ihp stk vars Cl sig pc z frs =
(None, hp, ihp, (tl stk, vars, Cl, sig, pc+1, z)#frs)"
"exec_instr Dup G hp ihp stk vars Cl sig pc z frs =
(None, hp, ihp, (hd stk # stk, vars, Cl, sig, pc+1, z)#frs)"
"exec_instr Dup_x1 G hp ihp stk vars Cl sig pc z frs =
(None, hp, ihp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)),
vars, Cl, sig, pc+1, z)#frs)"
"exec_instr Dup_x2 G hp ihp stk vars Cl sig pc z frs =
(None, 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 hp ihp stk vars Cl sig pc z frs =
(let (val1,val2) = (hd stk,hd (tl stk))
in
(None, hp, ihp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1, z)#frs))"
"exec_instr IAdd G hp ihp stk vars Cl sig pc z frs =
(let (val1,val2) = (hd stk,hd (tl stk))
in
(None, hp, ihp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)),
vars, Cl, sig, pc+1, z)#frs))"
"exec_instr (Ifcmpeq i) G 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, hp, ihp, (tl (tl stk), vars, Cl, sig, pc', z)#frs))"
"exec_instr (Goto i) G hp ihp stk vars Cl sig pc z frs =
(None, hp, ihp, (stk, vars, Cl, sig, nat(int pc+i), z)#frs)"
"exec_instr Throw G 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', hp, ihp, (stk, vars, Cl, sig, pc, z)#frs))"
"exec_instr (Jsr i) G hp ihp stk vars Cl sig pc z frs =
(None, hp, ihp, (RetAddr (pc+1)#stk, vars, Cl, sig, nat(int pc+i), z)#frs)"
"exec_instr (Ret idx) G hp ihp stk vars Cl sig pc z frs =
(None, hp, ihp, (stk, vars, Cl, sig, the_RetAddr (vars!idx), z)#frs)"
"exec_instr (ArrLoad) G 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 \<le> idx \<or> idx < 0) ArrayIndexOutOfBounds else xp'';
stk' = the (en (nat idx)) # (tl (tl stk));
pc' = if xp'=None then pc+1 else pc
in
(xp', hp, ihp, (stk', vars, Cl, sig, pc', z)#frs))"
"exec_instr (ArrStore) G 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 \<le> idx \<or> idx < 0) ArrayIndexOutOfBounds else xp'';
xp' = if xp'''=None then raise_system_xcpt (¬G,hp \<turnstile> val ::\<preceq> T) 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', hp', ihp, (tl (tl (tl stk)), vars, Cl, sig, pc', z)#frs))"
"exec_instr (ArrLength) G 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', hp, ihp, (Intg (int l)#(tl stk), vars, Cl, sig, pc', z)#frs))"
"exec_instr (ArrNew T) G 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', hp', ihp', (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