Quelle  JVMExecInstr.thy

(*  Title:      HOL/MicroJava/JVM/JVMExecInstr.thy

    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹JVM Instruction Semantics›

theory JVMExecInstr
imports JVMInstructions JVMState "../Common/Exceptions"
begin

primrec
  exec_instr :: "[instr, jvm_prog, heap, val list, val list,
                  cname, mname, pc, frame list] => jvm_state"
where
exec_instr_Load:
 "exec_instr (Load n) P h stk loc C₀ M₀ pc frs =
      (None, h, ((loc ! n) # stk, loc, C₀, M₀, pc+1)#frs)"

| "exec_instr (Store n) P h stk loc C₀ M₀ pc frs =
      (None, h, (tl stk, loc[n:=hd stk], C₀, M₀, pc+1)#frs)"

| exec_instr_Push:
 "exec_instr (Push v) P h stk loc C₀ M₀ pc frs =
      (None, h, (v # stk, loc, C₀, M₀, pc+1)#frs)"

| exec_instr_New:
 "exec_instr (New C) P h stk loc C₀ M₀ pc frs =
  (case new_Addr h of
    None ==> (Some (addr_of_sys_xcpt OutOfMemory), h, (stk, loc, C₀, M₀, pc)#frs)
  | Some a ==> (None, h(a↦blank P C), (Addr a#stk, loc, C₀, M₀, pc+1)#frs))"

| "exec_instr (Getfield F C) P h stk loc C₀ M₀ pc frs =
  (let v = hd stk;
       xp' = if v=Null then ⌊addr_of_sys_xcpt NullPointer⌋ else None;
       (D,fs) = the(h(the_Addr v))
   in (xp', h, (the(fs(F,C))#(tl stk), loc, C₀, M₀, pc+1)#frs))"

| "exec_instr (Putfield F C) P h stk loc C₀ M₀ pc frs =
  (let v = hd stk;
       r = hd (tl stk);
       xp' = if r=Null then ⌊addr_of_sys_xcpt NullPointer⌋ else None;
       a = the_Addr r;
       (D,fs) = the (h a);
       h' = h(a ↦ (D, fs((F,C) ↦ v)))
   in (xp', h', (tl (tl stk), loc, C₀, M₀, pc+1)#frs))"

| "exec_instr (Checkcast C) P h stk loc C₀ M₀ pc frs =
  (let v = hd stk;
       xp' = if ¬cast_ok P C h v then ⌊addr_of_sys_xcpt ClassCast⌋ else None
   in (xp', h, (stk, loc, C₀, M₀, pc+1)#frs))"

| exec_instr_Invoke:
 "exec_instr (Invoke M n) P h stk loc C₀ M₀ pc frs =
  (let ps = take n stk;
       r = stk!n;
       xp' = if r=Null then ⌊addr_of_sys_xcpt NullPointer⌋ else None;
       C = fst(the(h(the_Addr r)));
       (D,M',Ts,mxs,mxl₀,ins,xt)= method P C M;
       f' = ([],[r]@(rev ps)@(replicate mxl₀ undefined),D,M,0)
   in (xp', h, f'#(stk, loc, C₀, M₀, pc)#frs))" 

| "exec_instr Return P h stk₀ loc₀ C₀ M₀ pc frs =
  (if frs=[] then (None, h, []) else
   let v = hd stk₀;
       (stk,loc,C,m,pc) = hd frs;
       n = length (fst (snd (method P C₀ M₀)))
   in (None, h, (v#(drop (n+1) stk),loc,C,m,pc+1)#tl frs))"

| "exec_instr Pop P h stk loc C₀ M₀ pc frs =
      (None, h, (tl stk, loc, C₀, M₀, pc+1)#frs)"

| "exec_instr IAdd P h stk loc C₀ M₀ pc frs =
  (let i₂ = the_Intg (hd stk);
       i₁ = the_Intg (hd (tl stk))
   in (None, h, (Intg (i₁+i₂)#(tl (tl stk)), loc, C₀, M₀, pc+1)#frs))"

| "exec_instr (IfFalse i) P h stk loc C₀ M₀ pc frs =
  (let pc' = if hd stk = Bool False then nat(int pc+i) else pc+1
   in (None, h, (tl stk, loc, C₀, M₀, pc')#frs))"

| "exec_instr CmpEq P h stk loc C₀ M₀ pc frs =
  (let v₂ = hd stk;
       v₁ = hd (tl stk)
   in (None, h, (Bool (v₁=v₂) # tl (tl stk), loc, C₀, M₀, pc+1)#frs))"

| exec_instr_Goto:
 "exec_instr (Goto i) P h stk loc C₀ M₀ pc frs =
      (None, h, (stk, loc, C₀, M₀, nat(int pc+i))#frs)"

| "exec_instr Throw P h stk loc C₀ M₀ pc frs =
  (let xp' = if hd stk = Null then ⌊addr_of_sys_xcpt NullPointer⌋ else ⌊the_Addr(hd stk)⌋
   in (xp', h, (stk, loc, C₀, M₀, pc)#frs))"


lemma exec_instr_Store:
  "exec_instr (Store n) P h (v#stk) loc C₀ M₀ pc frs =
  (None, h, (stk, loc[n:=v], C₀, M₀, pc+1)#frs)" 
  by simp

lemma exec_instr_Getfield:
 "exec_instr (Getfield F C) P h (v#stk) loc C₀ M₀ pc frs =
  (let xp' = if v=Null then ⌊addr_of_sys_xcpt NullPointer⌋ else None;
       (D,fs) = the(h(the_Addr v))
   in (xp', h, (the(fs(F,C))#stk, loc, C₀, M₀, pc+1)#frs))"
  by simp

lemma exec_instr_Putfield:
 "exec_instr (Putfield F C) P h (v#r#stk) loc C₀ M₀ pc frs =
  (let xp' = if r=Null then ⌊addr_of_sys_xcpt NullPointer⌋ else None;
       a = the_Addr r;
       (D,fs) = the (h a);
       h' = h(a ↦ (D, fs((F,C) ↦ v)))
   in (xp', h', (stk, loc, C₀, M₀, pc+1)#frs))"
  by simp

lemma exec_instr_Checkcast:
 "exec_instr (Checkcast C) P h (v#stk) loc C₀ M₀ pc frs =
  (let xp' = if ¬cast_ok P C h v then ⌊addr_of_sys_xcpt ClassCast⌋ else None
   in (xp', h, (v#stk, loc, C₀, M₀, pc+1)#frs))"
  by simp

lemma exec_instr_Return:
 "exec_instr Return P h (v#stk₀) loc₀ C₀ M₀ pc frs =
  (if frs=[] then (None, h, []) else
   let (stk,loc,C,m,pc) = hd frs;
       n = length (fst (snd (method P C₀ M₀)))
   in (None, h, (v#(drop (n+1) stk),loc,C,m,pc+1)#tl frs))"
  by simp

lemma exec_instr_IPop:
 "exec_instr Pop P h (v#stk) loc C₀ M₀ pc frs =
      (None, h, (stk, loc, C₀, M₀, pc+1)#frs)"
  by simp

lemma exec_instr_IAdd:
 "exec_instr IAdd P h (Intg i₂ # Intg i₁ # stk) loc C₀ M₀ pc frs =
      (None, h, (Intg (i₁+i₂)#stk, loc, C₀, M₀, pc+1)#frs)"
  by simp

lemma exec_instr_IfFalse:
 "exec_instr (IfFalse i) P h (v#stk) loc C₀ M₀ pc frs =
  (let pc' = if v = Bool False then nat(int pc+i) else pc+1
   in (None, h, (stk, loc, C₀, M₀, pc')#frs))"
  by simp

lemma exec_instr_CmpEq:
 "exec_instr CmpEq P h (v₂#v₁#stk) loc C₀ M₀ pc frs =
  (None, h, (Bool (v₁=v₂) # stk, loc, C₀, M₀, pc+1)#frs)"
  by simp

lemma exec_instr_Throw:
 "exec_instr Throw P h (v#stk) loc C₀ M₀ pc frs =
  (let xp' = if v = Null then ⌊addr_of_sys_xcpt NullPointer⌋ else ⌊the_Addr v⌋
   in (xp', h, (v#stk, loc, C₀, M₀, pc)#frs))"
  by simp

end