Theory JVMExecInstr

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

section ‹JVM Instruction Semantics›

theory JVMExecInstr
imports
  JVMInstructions
  JVMHeap
  "../Common/ExternalCall"
begin

primrec extRet2JVM :: 
  "nat ⇒ 'heap ⇒ 'addr val list ⇒ 'addr val list ⇒ cname ⇒ mname ⇒ pc ⇒ 'addr frame list 
  ⇒ 'addr extCallRet ⇒ ('addr, 'heap) jvm_state"
where
  "extRet2JVM n h stk loc C M pc frs (RetVal v) = (None, h, (v # drop (Suc n) stk, loc, C, M, pc + 1) # frs)"
| "extRet2JVM n h stk loc C M pc frs (RetExc a) = (⌊a⌋, h, (stk, loc, C, M, pc) # frs)"
| "extRet2JVM n h stk loc C M pc frs RetStaySame = (None, 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 RetVal v ⇒ xcp = None ∧ frs' = (v # drop (Suc n) stk, loc, C, M, pc + 1) # frs
                      | RetExc a ⇒ xcp = ⌊a⌋ ∧ frs' = (stk, loc, C, M, pc) # frs
                      | RetStaySame ⇒ xcp = None ∧ frs' = (stk, loc, C, M, pc) # frs)"
by(cases va) auto

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

abbreviation extTA2JVM :: 
  "'addr jvm_prog ⇒ ('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'heap) jvm_thread_action"
where "extTA2JVM P ≡ convert_extTA (extNTA2JVM P)"

context JVM_heap_base begin

primrec exec_instr ::
  "'addr instr ⇒ 'addr jvm_prog ⇒ 'thread_id ⇒ 'heap ⇒ 'addr val list ⇒ 'addr val list
  ⇒ cname ⇒ mname ⇒ pc ⇒ 'addr frame list ⇒
    (('addr, 'thread_id, 'heap) jvm_thread_action × ('addr, 'heap) jvm_state) set"
where
exec_instr_Load:
 "exec_instr (Load n) P t h stk loc C⇩0 M⇩0 pc frs = 
      {(ε, (None, h, ((loc ! n) # stk, loc, C⇩0, M⇩0, pc+1)#frs))}"

| "exec_instr (Store n) P t h stk loc C⇩0 M⇩0 pc frs = 
      {(ε, (None, h, (tl stk, loc[n:=hd stk], C⇩0, M⇩0, pc+1)#frs))}"

| exec_instr_Push:
 "exec_instr (Push v) P t h stk loc C⇩0 M⇩0 pc frs = 
      {(ε, (None, h, (v # stk, loc, C⇩0, M⇩0, pc+1)#frs))}"

| exec_instr_New:
 "exec_instr (New C) P t h stk loc C⇩0 M⇩0 pc frs = 
  (let HA = allocate h (Class_type C)
   in if HA = {} then {(ε, ⌊addr_of_sys_xcpt OutOfMemory⌋, h, (stk, loc, C⇩0, M⇩0, pc) # frs)}
      else (λ(h', a). (⦃NewHeapElem a (Class_type C)⦄, None, h', (Addr a # stk, loc, C⇩0, M⇩0, pc + 1)#frs)) ` HA)"

| exec_instr_NewArray:
  "exec_instr (NewArray T) P t h stk loc C0 M0 pc frs =
  (let si = the_Intg (hd stk);
       i = nat (sint si)
   in (if si <s 0
       then {(ε, ⌊addr_of_sys_xcpt NegativeArraySize⌋, h, (stk, loc, C0, M0, pc) # frs)}
        else let HA = allocate h (Array_type T i)
             in if HA = {} then {(ε, ⌊addr_of_sys_xcpt OutOfMemory⌋, h, (stk, loc, C0, M0, pc) # frs)}
                else (λ(h', a). (⦃NewHeapElem a (Array_type T i)⦄, None, h', (Addr a # tl stk, loc, C0, M0, pc + 1) # frs)) ` HA))"

| exec_instr_ALoad:
  "exec_instr ALoad P t h stk loc C0 M0 pc frs =
   (let i = the_Intg (hd stk);
        va = hd (tl stk);
        a = the_Addr va;
        len = alen_of_htype (the (typeof_addr h a))
    in (if va = Null then {(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)}
        else if i <s 0 ∨ int len ≤ sint i then
             {(ε, ⌊addr_of_sys_xcpt ArrayIndexOutOfBounds⌋, h, (stk, loc, C0, M0, pc) # frs)}
        else {(⦃ReadMem a (ACell (nat (sint i))) v⦄, None, h, (v # tl (tl stk), loc, C0, M0, pc + 1) # frs) | v. 
              heap_read h a (ACell (nat (sint i))) v }))"

| exec_instr_AStore:
  "exec_instr AStore P t 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;
                 idx = nat (sint i);
                 a = the_Addr va;
                 hT = the (typeof_addr h a);
                 T = ty_of_htype hT;
                 len = alen_of_htype hT;
                 U = the (typeof⇘h⇙ ve)
             in (if i <s 0 ∨ int len ≤ sint i then
                      {(ε, ⌊addr_of_sys_xcpt ArrayIndexOutOfBounds⌋, h, (stk, loc, C0, M0, pc) # frs)}
                 else if P ⊢ U ≤ the_Array T then 
                      {(⦃WriteMem a (ACell idx) ve⦄, None, h', (tl (tl (tl stk)), loc, C0, M0, pc+1) # frs)
                       | h'. heap_write h a (ACell idx) ve h'}
                 else {(ε, (⌊addr_of_sys_xcpt ArrayStore⌋, h, (stk, loc, C0, M0, pc) # frs))}))))"

| exec_instr_ALength:
  "exec_instr ALength P t 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 (None, h, (Intg (word_of_int (int (alen_of_htype (the (typeof_addr h (the_Addr va)))))) # tl stk, loc, C0, M0, pc+1) # frs)))}"

| "exec_instr (Getfield F C) P t h stk loc C⇩0 M⇩0 pc frs = 
   (let v = hd stk
    in if v = Null then {(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C⇩0, M⇩0, pc) # frs)}
       else let a = the_Addr v
            in {(⦃ReadMem a (CField C F) v'⦄, None, h, (v' # (tl stk), loc, C⇩0, M⇩0, pc + 1) # frs) | v'.
                heap_read h a (CField C F) v'})"

| "exec_instr (Putfield F C) P t h stk loc C⇩0 M⇩0 pc frs = 
  (let v = hd stk;
       r = hd (tl stk)
   in if r = Null then {(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C⇩0, M⇩0, pc) # frs)}
      else let a = the_Addr r
           in {(⦃WriteMem a (CField C F) v⦄, None, h', (tl (tl stk), loc, C⇩0, M⇩0, pc + 1) # frs) | h'.
               heap_write h a (CField C F) v h'})"

| "exec_instr (CAS F C) P t h stk loc C0 M0 pc frs =
  (let v'' = hd stk; v' = hd (tl stk); v = hd (tl (tl stk))
   in if v = Null then {(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)}
      else let a = the_Addr v
           in {(⦃ReadMem a (CField C F) v', WriteMem a (CField C F) v''⦄, None, h', (Bool True # tl (tl (tl stk)), loc, C0, M0, pc + 1) # frs) | h' .
                heap_read h a (CField C F) v' ∧ heap_write h a (CField C F) v'' h'} ∪
              {(⦃ReadMem a (CField C F) v''⦄, None, h, (Bool False # tl (tl (tl stk)), loc, C0, M0, pc + 1) # frs) | v''.
                heap_read h a (CField C F) v'' ∧ v'' ≠ v'})"

| "exec_instr (Checkcast T) P t h stk loc C⇩0 M⇩0 pc frs =
  {(ε, let U = the (typeof⇘h⇙ (hd stk))
       in if P ⊢ U ≤ T then (None, h, (stk, loc, C⇩0, M⇩0, pc + 1) # frs)
          else (⌊addr_of_sys_xcpt ClassCast⌋, h, (stk, loc, C⇩0, M⇩0, pc) # frs))}"

| "exec_instr (Instanceof T) P t h stk loc C⇩0 M⇩0 pc frs =
  {(ε, None, h, (Bool (hd stk ≠ Null ∧ P ⊢ the (typeof⇘h⇙ (hd stk)) ≤ T) # tl stk, loc, C⇩0, M⇩0, pc + 1) # frs)}"

| exec_instr_Invoke:
 "exec_instr (Invoke M n) P t h stk loc C0 M0 pc frs =
  (let ps = rev (take n stk);
       r = stk ! n;
       a = the_Addr r;
       T = the (typeof_addr h a)
   in (if r = Null then {(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)}
       else 
         let C = class_type_of T;
             (D,M',Ts,meth)= method P C M
         in case meth of 
               Native ⇒
               {(extTA2JVM P ta, extRet2JVM n h' stk loc C0 M0 pc frs va) | ta va h'.
                (ta, va, h') ∈ red_external_aggr P t a M ps h}
            | ⌊(mxs,mxl⇩0,ins,xt)⌋ ⇒
              let f' = ([],[r]@ps@(replicate mxl⇩0 undefined_value),D,M,0)
              in {(ε, None, h, f' # (stk, loc, C0, M0, pc) # frs)}))"

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

| "exec_instr Pop P t h stk loc C⇩0 M⇩0 pc frs = 
      {(ε, (None, h, (tl stk, loc, C⇩0, M⇩0, pc+1)#frs) )}"

| "exec_instr Dup P t h stk loc C⇩0 M⇩0 pc frs = 
      {(ε, (None, h, (hd stk # stk, loc, C⇩0, M⇩0, pc+1)#frs) )}"

| "exec_instr Swap P t h stk loc C⇩0 M⇩0 pc frs = 
      {(ε, (None, h, (hd (tl stk) # hd stk # tl (tl stk), loc, C⇩0, M⇩0, pc+1)#frs) )}"

| "exec_instr (BinOpInstr bop) P t h stk loc C0 M0 pc frs =
  {(ε, 
   case the (binop bop (hd (tl stk)) (hd stk)) of
     Inl v ⇒ (None, h, (v # tl (tl stk), loc, C0, M0, pc+1) # frs)
   | Inr a ⇒ (Some a, h, (stk, loc, C0, M0, pc) # frs))}"

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

| exec_instr_Goto:
 "exec_instr (Goto i) P t h stk loc C⇩0 M⇩0 pc frs =
      {(ε, (None, h, (stk, loc, C⇩0, M⇩0, nat(int pc+i))#frs) )}"

| "exec_instr ThrowExc P t h stk loc C⇩0 M⇩0 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⇩0, M⇩0, pc)#frs)) )}"

| exec_instr_MEnter:
 "exec_instr MEnter P t h stk loc C⇩0 M⇩0 pc frs =
  {let v = hd stk
   in if v = Null
      then (ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C⇩0, M⇩0, pc) # frs)
      else (⦃Lock→the_Addr v, SyncLock (the_Addr v)⦄, None, h, (tl stk, loc, C⇩0, M⇩0, pc + 1) # frs)}"

| exec_instr_MExit:
 "exec_instr MExit P t h stk loc C⇩0 M⇩0 pc frs =
  (let v = hd stk
   in if v = Null
      then {(ε, ⌊addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C⇩0, M⇩0, pc)#frs)}
      else {(⦃Unlock→the_Addr v, SyncUnlock (the_Addr v)⦄, None, h, (tl stk, loc, C⇩0, M⇩0, pc + 1) # frs),
            (⦃UnlockFail→the_Addr v⦄, ⌊addr_of_sys_xcpt IllegalMonitorState⌋, h, (stk, loc, C⇩0, M⇩0, pc) # frs)})"

end

end