Theory JVMExecInstr

(*  Title:      JinjaThreads/JVM/JVMExecInstr.thy
    Author:     Cornelia Pusch, Gerwin Klein, Andreas Lochbihler
*)

header {* \isaheader{JVM Instruction Semantics} *}

theory JVMExecInstr
imports JVMInstructions
begin

primrec extRet2JVM :: "nat => heap => val list => val list => cname => mname => pc => frame list => (val + addr) => jvm_state"
where
  "extRet2JVM n h stk loc C M pc frs (Inl v) = (None, h, (v # drop (Suc n) stk, loc, C, M, pc + 1) # frs)"
| "extRet2JVM n h stk loc C M pc frs (Inr a) = (⌊a⌋, h, (stk, loc, C, M, pc) # frs)"

lemma eq_extRet2JVM_conv [simp]:
  "(xcp, h', frs') = extRet2JVM n h stk loc C M pc frs va <-> 
   h' = h ∧ (case va of Inl v => xcp = None ∧ frs' = (v # drop (Suc n) stk, loc, C, M, pc + 1) # frs
                      | Inr a => xcp = ⌊a⌋ ∧ frs' = (stk, loc, C, M, pc) # frs)"
by(cases va) auto

definition extNTA2JVM :: "jvm_prog => (cname × mname × addr) => jvm_thread_state"
where "extNTA2JVM P ≡ (λ(C, M, a). let (D,M',Ts,mxs,mxl0,ins,xt) = method P C M
                                   in (None, [([],Addr a # replicate mxl0 undefined, D, M, 0)]))"

abbreviation extTA2JVM :: "jvm_prog => external_thread_action => jvm_thread_action"
where "extTA2JVM P ≡ convert_extTA (extNTA2JVM P)"

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

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

| exec_instr_Push:
 "exec_instr (Push v) P h stk loc C0 M0 pc frs = 
      [(ε, (None, h, (v # stk, loc, C0, M0, pc+1)#frs) )]"

| exec_instr_New:
 "exec_instr (New C) P h stk loc C0 M0 pc frs = 
  [(ε, (case new_Addr h of
          None =>   (Some (addr_of_sys_xcpt OutOfMemory), h, (stk, loc, C0, M0, pc)#frs)
        | Some a => (None, h(a\<mapsto>blank P C), (Addr a#stk, loc, C0, M0, pc+1)#frs)) )]"

| exec_instr_NewArray:
  "exec_instr (NewArray T) P h stk loc C0 M0 pc frs =
  [(ε, (let si = the_Intg (hd stk)
        in (if (si < 0)
            then (⌊addr_of_sys_xcpt NegativeArraySize⌋, h, (stk, loc, C0, M0, pc) # frs)
            else (case new_Addr h of
                    None => (⌊addr_of_sys_xcpt OutOfMemory⌋, h, (stk, loc, C0, M0, pc) # frs)
                  | ⌊a⌋  => (None, h(a \<mapsto> Arr T (replicate (nat si) (default_val T))), (Addr a # tl stk, loc, C0, M0, pc + 1) # frs)))) )]"

| exec_instr_ALoad:
  "exec_instr ALoad P h stk loc C0 M0 pc frs =
   [(ε, (let i = the_Intg (hd stk);
             va = hd (tl stk);
             (T, el) = the_arr (the (h (the_Addr va)))
         in if va = Null then (⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)
            else if i < 0 ∨ int (length el) ≤ i then (⌊addr_of_sys_xcpt ArrayIndexOutOfBounds⌋, h, (stk, loc, C0, M0, pc) # frs)
            else (None, h, (el ! nat i # tl (tl stk), loc, C0, M0, pc + 1) # frs)) )]"

| exec_instr_AStore:
  "exec_instr AStore P h stk loc C0 M0 pc frs =
  [(ε, (let ve = hd stk;
            vi = hd (tl stk);
            va = hd (tl (tl stk))
        in (if va = Null
            then (⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)
            else (let i = the_Intg vi;
                      (T, el) = the_arr (the (h (the_Addr va)));
                      h' = h((the_Addr va) \<mapsto> Arr T (el[nat i := ve]))
                 in (if i < 0 ∨ int (length el) ≤ i
                     then (⌊addr_of_sys_xcpt ArrayIndexOutOfBounds⌋, h, (stk, loc, C0, M0, pc) # frs)
                     else if cast_ok P T h ve
                          then (None, h', (tl (tl (tl stk)), loc, C0, M0, pc+1) # frs)
                          else (⌊addr_of_sys_xcpt ArrayStore⌋, h, (stk, loc, C0, M0, pc) # frs))))) )]"

| exec_instr_ALength:
  "exec_instr ALength P h stk loc C0 M0 pc frs =
   [(ε, (let va = hd stk
         in if va = Null
            then (⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)
            else let (T, elem) = the_arr (the (h (the_Addr va)))
                 in (None, h, (Intg (int (length elem)) # tl stk, loc, C0, M0, pc+1) # frs)))]"


| "exec_instr (Getfield F C) P h stk loc C0 M0 pc frs = 
  [(ε, (let v      = hd stk;
            (D,fs) = the_obj(the(h(the_Addr v)))
        in if v=Null then (⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)
           else (None, h, (the(fs(F,C))#(tl stk), loc, C0, M0, pc+1)#frs)) )]"

| "exec_instr (Putfield F C) P h stk loc C0 M0 pc frs = 
  [(ε, (let v    = hd stk;
            r    = hd (tl stk);
            a    = the_Addr r;
            (D,fs) = the_obj (the (h a));
            h'  = h(a \<mapsto> (Obj D (fs((F,C) \<mapsto> v))))
        in if r=Null then (⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)
           else (None, h', (tl (tl stk), loc, C0, M0, pc+1)#frs)) )]"

| "exec_instr (Checkcast T) P h stk loc C0 M0 pc frs =
  [(ε, (let v   = hd stk
        in if ¬ cast_ok P T h v then (⌊addr_of_sys_xcpt ClassCast⌋, h, (stk, loc, C0, M0, pc) # frs)
           else (None, h, (stk, loc, C0, M0, pc+1)#frs)) )]"

| exec_instr_Invoke:
 "exec_instr (Invoke M n) P h stk loc C0 M0 pc frs =
  (let ps = rev (take n stk);
       r = stk ! n;
       a = the_Addr r;
       T = the (typeofh (Addr a));
       C = fst(the_obj(the(h a)));
       old_frs = (stk, loc, C0, M0, pc) # frs
   in (if r = Null then [(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, old_frs)]
       else if is_external_call P T M
            then map (λ(ta, va, h). (extTA2JVM P ta, extRet2JVM n h stk loc C0 M0 pc frs va)) (red_external_list P a M ps h)
       else let (D,M',Ts,mxs,mxl0,ins,xt)= method P C M;
                f'  = ([],[r]@ps@(replicate mxl0 undefined),D,M,0)
            in [(ε, None, h, f' # old_frs)]))"


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

| "exec_instr Pop P h stk loc C0 M0 pc frs = 
      [(ε, (None, h, (tl stk, loc, C0, M0, pc+1)#frs) )]"

| "exec_instr (BinOpInstr bop) P h stk loc C0 M0 pc frs =
  [(ε, (None, h, (the (binop bop (hd (tl stk)) (hd stk)) # tl (tl stk), loc, C0, M0, pc + 1) # frs))]"


| "exec_instr (IfFalse i) P h stk loc C0 M0 pc frs =
  [(ε, (let pc' = if hd stk = Bool False then nat(int pc+i) else pc+1
        in (None, h, (tl stk, loc, C0, M0, pc')#frs)) )]"

| exec_instr_Goto:
 "exec_instr (Goto i) P h stk loc C0 M0 pc frs =
      [(ε, (None, h, (stk, loc, C0, M0, nat(int pc+i))#frs) )]"

| "exec_instr ThrowExc P h stk loc C0 M0 pc frs =
  [(ε, (let xp' = if hd stk = Null then ⌊addr_of_sys_xcpt NullPointer⌋ else ⌊the_Addr(hd stk)⌋
        in (xp', h, (stk, loc, C0, M0, pc)#frs)) )]"

| exec_instr_MEnter:
 "exec_instr MEnter P h stk loc C0 M0 pc frs =
  [ let v = hd stk
    in if v = Null
       then (ε, (⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc)#frs))
       else (ε\<lbrace>lLock->the_Addr v\<rbrace>\<lbrace>o Synchronization (the_Addr v)\<rbrace>, (None, h, (tl stk, loc, C0, M0, pc + 1) # frs)) ]"

| exec_instr_MExit:
 "exec_instr MExit P h stk loc C0 M0 pc frs =
  (let v = hd stk
   in if v = Null
      then [(ε, (⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc)#frs) )]
      else [(ε\<lbrace>lUnlock->the_Addr v\<rbrace>\<lbrace>o Synchronization (the_Addr v)\<rbrace>, (None, h, (tl stk, loc, C0, M0, pc + 1) # frs)),
            (ε\<lbrace>lUnlockFail->the_Addr v\<rbrace>, (⌊addr_of_sys_xcpt IllegalMonitorState⌋, h, (stk, loc, C0, M0, pc) # frs)) ])"

lemma exec_instr_not_empty:
  "exec_instr I P h stk loc C0 M0 pc frs ≠ []"
apply(cases I)
apply(auto simp add: split_beta red_external_list_not_Nil)
done

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

lemma exec_instr_NewArray:
  "exec_instr (NewArray T) P h (Intg si # stk) loc C0 M0 pc frs =
   [(ε, (if (si < 0) then (⌊addr_of_sys_xcpt NegativeArraySize⌋, h, (Intg si # stk, loc, C0, M0, pc) # frs)
         else (case new_Addr h of
                 None => (⌊addr_of_sys_xcpt OutOfMemory⌋, h, (Intg si # stk, loc, C0, M0, pc) # frs)
               | ⌊a⌋  => (None, h(a \<mapsto> Arr T (replicate (nat si) (default_val T))), (Addr a # stk, loc, C0, M0, pc + 1) # frs))) )]"
  by simp

lemma exec_instr_ALoad:
  "exec_instr ALoad P h (Intg i # va # stk) loc C0 M0 pc frs =
   [(ε, (let (T, el) = the_arr (the (h (the_Addr va)))
         in if va = Null then (⌊addr_of_sys_xcpt NullPointer⌋, h, (Intg i # va # stk, loc, C0, M0, pc) # frs)
            else if i < 0 ∨ int (length el) ≤ i
                 then (⌊addr_of_sys_xcpt ArrayIndexOutOfBounds⌋, h, (Intg i # va # stk, loc, C0, M0, pc) # frs)
            else (None, h, (el ! nat i # stk, loc, C0, M0, pc + 1) # frs)) )]"
  by(simp add: split_beta)

lemma exec_instr_AStore:
  "exec_instr AStore P h (ve # Intg i # va # stk) loc C0 M0 pc frs =
   [(ε, (if va = Null
         then (⌊addr_of_sys_xcpt NullPointer⌋, h, (ve # Intg i # va # stk, loc, C0, M0, pc) # frs)
         else (let (T, el) = the_arr (the (h (the_Addr va)));
                   h' = h((the_Addr va) \<mapsto> Arr T (el[nat i := ve]))
               in (if i < 0 ∨ int (length el) ≤ i
                   then (⌊addr_of_sys_xcpt ArrayIndexOutOfBounds⌋, h, (ve # Intg i # va # stk, loc, C0, M0, pc) # frs)
                   else if cast_ok P T h ve
                        then (None, h', (stk, loc, C0, M0, pc+1) # frs)
                        else (⌊addr_of_sys_xcpt ArrayStore⌋, h, (ve # Intg i # va # stk, loc, C0, M0, pc) # frs)))) )]"
  by(simp add: exec_instr_AStore split_beta)

lemma exec_instr_ALength:
  "exec_instr ALength P h (va # stk) loc C0 M0 pc frs =
   [(ε, if va = Null
        then (⌊addr_of_sys_xcpt NullPointer⌋, h, (va # stk, loc, C0, M0, pc) # frs)
        else let (T, elem) = the_arr (the (h (the_Addr va)))
             in (None, h, (Intg (int (length elem)) # stk, loc, C0, M0, pc+1) # frs))]"
  by(simp only: exec_instr_ALength Let_def hd.simps tl.simps)


lemma exec_instr_Getfield:
 "exec_instr (Getfield F C) P h (v#stk) loc C0 M0 pc frs = 
  [(ε, let (D,fs) = the_obj(the(h(the_Addr v)))
       in if v=Null then (⌊addr_of_sys_xcpt NullPointer⌋, h, (v # stk, loc, C0, M0, pc) # frs)
          else (None, h, (the(fs(F,C))#stk, loc, C0, M0, pc+1)#frs))]"
  by(simp add: split_beta)

lemma exec_instr_Putfield:
 "exec_instr (Putfield F C) P h (v#r#stk) loc C0 M0 pc frs = 
  [(ε, (let  a    = the_Addr r;
            (D,fs) = the_obj(the (h a));
            h'  = if r=Null then h else h(a \<mapsto> (Obj D (fs((F,C) \<mapsto> v))))
        in if r=Null then (⌊addr_of_sys_xcpt NullPointer⌋, h, (v # r # stk, loc, C0, M0, pc) # frs)
           else (None, h', (stk, loc, C0, M0, pc+1)#frs)))]"
  by(simp add: split_beta)

lemma exec_instr_Checkcast:
 "exec_instr (Checkcast T) P h (v#stk) loc C0 M0 pc frs =
  [(ε, (if ¬ cast_ok P T h v then (⌊addr_of_sys_xcpt ClassCast⌋, h, (v # stk, loc,  C0, M0, pc) # frs)
        else (None, h, (v#stk, loc, C0, M0, pc+1)#frs)) )]"
  by simp

lemma exec_instr_Return:
 "exec_instr Return P h (v#stk0) loc0 C0 M0 pc frs =
  [(ε, (if frs=[] then (None, h, []) else 
       let (stk,loc,C,m,pc) = hd frs;
            n = length (fst (snd (method P C0 M0)))
       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 C0 M0 pc frs = 
      [(ε, (None, h, (stk, loc, C0, M0, pc+1)#frs) )]"
  by simp

lemma exec_instr_IAdd:
 "exec_instr IAdd P h (Intg i2 # Intg i1 # stk) loc C0 M0 pc frs =
      [(ε, (None, h, (Intg (i1+i2)#stk, loc, C0, M0, pc+1)#frs) )]"
  by simp

lemma exec_instr_ISub:
 "exec_instr ISub P h (Intg i2 # Intg i1 # stk) loc C0 M0 pc frs =
      [(ε, (None, h, (Intg (i1-i2)#stk, loc, C0, M0, pc+1)#frs) )]"
  by simp

lemma exec_instr_IMult:
 "exec_instr IMult P h (Intg i2 # Intg i1 # stk) loc C0 M0 pc frs =
      [(ε, (None, h, (Intg (i1*i2)#stk, loc, C0, M0, pc+1)#frs) )]"
  by simp

lemma exec_instr_IMod:
 "exec_instr IMod P h (Intg i2 # Intg i1 # stk) loc C0 M0 pc frs =
      [(ε, (None, h, (Intg (i1 mod i2)#stk, loc, C0, M0, pc+1)#frs) )]"
  by simp

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

lemma exec_instr_CmpEq:
 "exec_instr CmpEq P h (v2#v1#stk) loc C0 M0 pc frs =
  [(ε, (None, h, (Bool (v1=v2) # stk, loc, C0, M0, pc+1)#frs) )]"
  by simp

lemma exec_instr_Throw:
 "exec_instr ThrowExc P h (v#stk) loc C0 M0 pc frs =
  [(ε, (let xp' = if v = Null then ⌊addr_of_sys_xcpt NullPointer⌋ else ⌊the_Addr v⌋
        in (xp', h, (v#stk, loc, C0, M0, pc)#frs)) )]"
  by simp

lemma exec_instr_MEnter:
 "exec_instr MEnter P h (v#stk) loc C0 M0 pc frs =
  [ if v = Null
    then (ε, (⌊addr_of_sys_xcpt NullPointer⌋, h, (v # stk, loc, C0, M0, pc)#frs))
    else (ε\<lbrace>lLock->the_Addr v\<rbrace>\<lbrace>o Synchronization (the_Addr v)\<rbrace>, (None, h, (stk, loc, C0, M0, pc + 1) # frs)) ]"
  by simp

lemma exec_instr_MExit:
 "exec_instr MExit P h (v#stk) loc C0 M0 pc frs =
  (if v = Null
  then [(ε, (⌊addr_of_sys_xcpt NullPointer⌋, h, (v # stk, loc, C0, M0, pc)#frs) )]
  else [(ε\<lbrace>lUnlock->the_Addr v\<rbrace>\<lbrace>o Synchronization (the_Addr v)\<rbrace>, (None, h, (stk, loc, C0, M0, pc + 1) # frs)),
        (ε\<lbrace>lUnlockFail->the_Addr v\<rbrace>, (⌊addr_of_sys_xcpt IllegalMonitorState⌋, h, (v # stk, loc, C0, M0, pc) # frs)) ])"
  by simp

lemma exec_instr_xcp_unchanged:
  "(ta, ⌊xcp⌋, h', frs') ∈ set (exec_instr (ins ! pc) P h stk loc C M pc frs)
  ==> h' = h ∧ frs' = (stk, loc, C, M, pc) # frs"
apply(cases "ins ! pc")
apply(simp_all split: split_if_asm add: split_beta)
apply(auto split: sum.split_asm simp: red_external_list_xcp_heap_unchanged)
done

end