Theory JVMExec_Execute

(*  Title:      JinjaThreads/Execute/JVMExec_Execute.thy
    Author:     Andreas Lochbihler
*)

theory JVMExec_Execute
imports
  "../JVM/JVMExec"
  ExternalCall_Execute
begin

subsection ‹Manual translation of the JVM to use sets instead of predicates›

locale JVM_heap_execute = heap_execute +
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id" 
  and thread_id2addr :: "'thread_id ⇒ 'addr" 
  and spurious_wakeups :: bool
  and empty_heap :: "'heap" 
  and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set" 
  and typeof_addr :: "'heap ⇒ 'addr ⇒ htype option" 
  and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val set" 
  and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap set"

sublocale JVM_heap_execute < execute: JVM_heap_base
  addr2thread_id thread_id2addr 
  spurious_wakeups
  empty_heap allocate typeof_addr
  "λh a ad v. v ∈ heap_read h a ad" "λh a ad v h'. h' ∈ heap_write h a ad v"
.

context JVM_heap_execute begin

definition 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 [simp]: "exec_instr = execute.exec_instr"

lemma exec_instr_code [code]:
  "exec_instr (Load n) P t h stk loc C0 M0 pc frs = 
   {(ε, (None, h, ((loc ! n) # stk, loc, C0, M0, pc+1)#frs))}"
  "exec_instr (Store n) P t h stk loc C0 M0 pc frs = 
   {(ε, (None, h, (tl stk, loc[n:=hd stk], C0, M0, pc+1)#frs))}"
  "exec_instr (Push v) P t h stk loc C0 M0 pc frs = 
   {(ε, (None, h, (v # stk, loc, C0, M0, pc+1)#frs))}"
  "exec_instr (New C) P t h stk loc C0 M0 pc frs = 
   (let HA = allocate h (Class_type C) in
    if HA = {} then {(ε, ⌊execute.addr_of_sys_xcpt OutOfMemory⌋, h, (stk, loc, C0, M0, pc) # frs)}
    else do { (h', a) ← HA; {(⦃NewHeapElem a (Class_type C)⦄, None, h', (Addr a # stk, loc, C0, M0, pc + 1)#frs)} })"
  "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 {(ε, ⌊execute.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 {(ε, ⌊execute.addr_of_sys_xcpt OutOfMemory⌋, h, (stk, loc, C0, M0, pc) # frs)}
         else do { (h', a) ← HA; {(⦃NewHeapElem a (Array_type T i)⦄, None, h', (Addr a # tl stk, loc, C0, M0, pc + 1) # frs)}})"
  "exec_instr ALoad P t h stk loc C0 M0 pc frs =
   (let va = hd (tl stk)
    in (if va = Null then {(ε, ⌊execute.addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)}
        else 
          let i = the_Intg (hd stk);
              a = the_Addr va;
              len = alen_of_htype (the (typeof_addr h a))
          in if i <s 0 ∨ int len ≤ sint i then
               {(ε, ⌊execute.addr_of_sys_xcpt ArrayIndexOutOfBounds⌋, h, (stk, loc, C0, M0, pc) # frs)}
             else do {
                 v ← heap_read h a (ACell (nat (sint i)));
                 {(⦃ReadMem a (ACell (nat (sint i))) v⦄, None, h, (v # tl (tl stk), loc, C0, M0, pc + 1) # frs)}
               }))"
  "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 {(ε, ⌊execute.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 (execute.typeof_h h ve)
             in (if i <s 0 ∨ int len ≤ sint i then
                      {(ε, ⌊execute.addr_of_sys_xcpt ArrayIndexOutOfBounds⌋, h, (stk, loc, C0, M0, pc) # frs)}
                 else if P ⊢ U ≤ the_Array T then 
                      do {
                         h' ← heap_write h a (ACell idx) ve;
                         {(⦃WriteMem a (ACell idx) ve⦄, None, h', (tl (tl (tl stk)), loc, C0, M0, pc+1) # frs)}
                      }
                 else {(ε, (⌊execute.addr_of_sys_xcpt ArrayStore⌋, h, (stk, loc, C0, M0, pc) # frs))}))))"
  "exec_instr ALength P t h stk loc C0 M0 pc frs =
   {(ε, (let va = hd stk
         in if va = Null
            then (⌊execute.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 C0 M0 pc frs = 
   (let v = hd stk
    in if v = Null then {(ε, ⌊execute.addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)}
       else let a = the_Addr v
            in do {
               v' ← heap_read h a (CField C F);
               {(⦃ReadMem a (CField C F) v'⦄, None, h, (v' # (tl stk), loc, C0, M0, pc + 1) # frs)}
            })"
  "exec_instr (Putfield F C) P t h stk loc C0 M0 pc frs = 
  (let v = hd stk;
       r = hd (tl stk)
   in if r = Null then {(ε, ⌊execute.addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)}
      else let a = the_Addr r
           in do {
                h' ← heap_write h a (CField C F) v;
                {(⦃WriteMem a (CField C F) v⦄, None, h', (tl (tl stk), loc, C0, M0, pc + 1) # frs)}
              })"
 "exec_instr (Checkcast T) P t h stk loc C0 M0 pc frs =
  {(ε, let U = the (typeof⇘h⇙ (hd stk))
       in if P ⊢ U ≤ T then (None, h, (stk, loc, C0, M0, pc + 1) # frs)
          else (⌊execute.addr_of_sys_xcpt ClassCast⌋, h, (stk, loc, C0, M0, pc) # frs))}"
  "exec_instr (Instanceof T) P t h stk loc C0 M0 pc frs =
   {(ε, None, h, (Bool (hd stk ≠ Null ∧ P ⊢ the (typeof⇘h⇙ (hd stk)) ≤ T) # tl stk, loc, C0, M0, pc + 1) # frs)}"
  "exec_instr (Invoke M n) P t h stk loc C0 M0 pc frs =
   (let r = stk ! n
    in (if r = Null then {(ε, ⌊execute.addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)}
        else (let ps = rev (take n stk);
                  a = the_Addr r;
                  T = the (typeof_addr h a);
                  (D,M',Ts,meth)= method P (class_type_of T) M
         in case meth of 
               Native ⇒
                      do {
                        (ta, va, h') ← red_external_aggr P t a M ps h;
                        {(extTA2JVM P ta, extRet2JVM n h' stk loc C0 M0 pc frs va)}
                      }
            | ⌊(mxs,mxl0,ins,xt)⌋ ⇒
              let f' = ([],[r]@ps@(replicate mxl0 undefined_value),D,M,0)
              in {(ε, None, h, f' # (stk, loc, C0, M0, pc) # frs)})))"
  "exec_instr Return P t 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 t h stk loc C0 M0 pc frs = {(ε, (None, h, (tl stk, loc, C0, M0, pc+1)#frs))}"
  "exec_instr Dup P t h stk loc C0 M0 pc frs = {(ε, (None, h, (hd stk # stk, loc, C0, M0, pc+1)#frs))}"
  "exec_instr Swap P t h stk loc C0 M0 pc frs = {(ε, (None, h, (hd (tl stk) # hd stk # tl (tl stk), loc, C0, M0, pc+1)#frs))}"
  "exec_instr (BinOpInstr bop) P t h stk loc C0 M0 pc frs =
   {(ε, 
     case the (execute.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 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 i) P t h stk loc C0 M0 pc frs = {(ε, (None, h, (stk, loc, C0, M0, nat(int pc+i))#frs))}"
  "exec_instr ThrowExc P t h stk loc C0 M0 pc frs =
   {(ε, (let xp' = if hd stk = Null then ⌊execute.addr_of_sys_xcpt NullPointer⌋ else ⌊the_Addr(hd stk)⌋
         in (xp', h, (stk, loc, C0, M0, pc)#frs)))}"
  "exec_instr MEnter P t h stk loc C0 M0 pc frs =
   {(let v = hd stk
     in if v = Null
        then (ε, ⌊execute.addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)
        else (⦃Lock→the_Addr v, SyncLock (the_Addr v)⦄, None, h, (tl stk, loc, C0, M0, pc + 1) # frs))}"
  "exec_instr MExit P t h stk loc C0 M0 pc frs =
   (let v = hd stk
    in if v = Null
       then {(ε, ⌊execute.addr_of_sys_xcpt NullPointer⌋, h, (stk, loc, C0, M0, pc) # frs)}
       else {(⦃Unlock→the_Addr v, SyncUnlock (the_Addr v)⦄, None, h, (tl stk, loc, C0, M0, pc + 1) # frs),
             (⦃UnlockFail→the_Addr v⦄, ⌊execute.addr_of_sys_xcpt IllegalMonitorState⌋, h, (stk, loc, C0, M0, pc) # frs)})"
by(auto 4 4 intro: rev_bexI)

definition exec :: "'addr jvm_prog ⇒ 'thread_id ⇒ ('addr, 'heap) jvm_state ⇒ ('addr, 'thread_id, 'heap) jvm_ta_state set"
where "exec = execute.exec"

lemma exec_code:
  "exec P t (xcp, h, []) = {}"
  "exec P t (None, h, (stk, loc, C, M, pc) # frs) = exec_instr (instrs_of P C M ! pc) P t h stk loc C M pc frs"
  "exec P t (⌊a⌋, h, fr # frs) = {(ε, execute.exception_step P a h fr frs)}"
by(simp_all add: exec_def)

definition exec_1 ::
  "'addr jvm_prog ⇒ 'thread_id ⇒ ('addr, 'heap) jvm_state
   ⇒ (('addr, 'thread_id, 'heap) jvm_thread_action × ('addr, 'heap) jvm_state) Predicate.pred"
where "exec_1 P t σ = pred_of_set (exec P t σ)"

lemma exec_1I: "execute.exec_1 P t σ ta σ' ⟹ Predicate.eval (exec_1 P t σ) (ta, σ')"
by(erule execute.exec_1.cases)(simp add: exec_1_def exec_def)

lemma exec_1E:
  assumes "Predicate.eval (exec_1 P t σ) (ta, σ')"
  obtains "execute.exec_1 P t σ ta σ'"
using assms
by(auto simp add: exec_1_def exec_def intro: execute.exec_1.intros)

lemma exec_1_eq [simp]:
  "Predicate.eval (exec_1 P t σ) (ta, σ') ⟷ execute.exec_1 P t σ ta σ'"
by(auto intro: exec_1I elim: exec_1E)

lemma exec_1_eq':
  "Predicate.eval (exec_1 P t σ) = (λ(ta, σ'). execute.exec_1 P t σ ta σ')"
by(rule ext)(simp split: prod.split)

end

lemmas [code] = 
  JVM_heap_execute.exec_instr_code
  JVM_heap_base.exception_step.simps
  JVM_heap_execute.exec_code
  JVM_heap_execute.exec_1_def

end