Theory JVMExecInstr

Up to index of Isabelle/HOL/jsr

theory JVMExecInstr = JVMInstructions + JVMState:
(*  Title:      HOL/MicroJava/JVM/JVMExecInstr.thy
    ID:         $Id: JVMExecInstr.html,v 1.1 2002/11/28 14:17:20 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(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(hp a);
             hp'        = if xp'=None then hp(a \<mapsto> (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       = fst(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       = fst(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)"


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