Theory ExternalCall_Execute

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

section ‹Executable semantics for the JVM›

theory ExternalCall_Execute
imports
  "../Common/ExternalCall"
  "../Basic/Set_without_equal"
begin

subsection ‹Translated versions of external calls for the JVM›

locale heap_execute = addr_base +
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id" 
  and thread_id2addr :: "'thread_id ⇒ 'addr" 
  fixes 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 heap_execute < execute: 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 heap_execute begin

definition heap_copy_loc :: "'addr ⇒ 'addr ⇒ addr_loc ⇒ 'heap ⇒ (('addr, 'thread_id) obs_event list × 'heap) set"
where [simp]:
  "heap_copy_loc a a' al h = {(obs, h'). execute.heap_copy_loc a a' al h obs h'}"

lemma heap_copy_loc_code:
  "heap_copy_loc a a' al h =
   (do {
      v ← heap_read h a al;
      h' ← heap_write h a' al v;
      {([ReadMem a al v, WriteMem a' al v], h')}
   })"
by(auto simp add: execute.heap_copy_loc.simps)

definition heap_copies :: "'addr ⇒ 'addr ⇒ addr_loc list ⇒ 'heap ⇒ (('addr, 'thread_id) obs_event list × 'heap) set"
where [simp]: "heap_copies a a' al h = {(obs, h'). execute.heap_copies a a' al h obs h'}"

lemma heap_copies_code:
  shows heap_copies_Nil: 
  "heap_copies a a' [] h = {([], h)}"
  and heap_copies_Cons:
  "heap_copies a a' (al # als) h =
  (do {
     (ob, h') ← heap_copy_loc a a' al h;
     (obs, h'') ← heap_copies a a' als h';
     {(ob @ obs, h'')}
  })"
by(fastforce elim!: execute.heap_copies_cases intro: execute.heap_copies.intros)+

definition heap_clone :: "'m prog ⇒ 'heap ⇒ 'addr ⇒ ('heap × (('addr, 'thread_id) obs_event list × 'addr) option) set"
where [simp]: "heap_clone P h a = {(h', obsa). execute.heap_clone P h a h' obsa}"

lemma heap_clone_code:
  "heap_clone P h a =
  (case typeof_addr h a of
    ⌊Class_type C⌋ ⇒ 
      let HA = allocate h (Class_type C) 
      in if HA = {} then {(h, None)} else do {
          (h', a') ← HA;
          FDTs ← set_of_pred (Fields_i_i_o P C);
          (obs, h'') ← heap_copies a a' (map (λ((F, D), Tfm). CField D F) FDTs) h';
          {(h'', ⌊(NewHeapElem a' (Class_type C) # obs, a')⌋)}
        }
  | ⌊Array_type T n⌋ ⇒ 
      let HA = allocate h (Array_type T n)
      in if HA = {} then {(h, None)} else do {
        (h', a') ← HA;
        FDTs ← set_of_pred (Fields_i_i_o P Object);
        (obs, h'') ← heap_copies a a' (map (λ((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h';
        {(h'', ⌊(NewHeapElem a' (Array_type T n) # obs, a')⌋)}
      }
  | _ ⇒ {})"
  by (auto 4 3 elim!: execute.heap_clone.cases split: ty.splits
  prod.split_asm htype.splits intro: execute.heap_clone.intros
  simp add: eval_Fields_conv split_beta prod_eq_iff)
    (auto simp add: eval_Fields_conv Bex_def)

definition red_external_aggr :: 
  "'m prog ⇒ 'thread_id ⇒ 'addr ⇒ mname ⇒ 'addr val list ⇒ 'heap ⇒ 
  (('addr, 'thread_id, 'heap) external_thread_action × 'addr extCallRet × 'heap) set"
where [simp]:
  "red_external_aggr P t a M vs h = execute.red_external_aggr P t a M vs h"

lemma red_external_aggr_code:
  "red_external_aggr P t a M vs h =
   (if M = wait then
      let ad_t = thread_id2addr t
      in {(⦃Unlock→a, Lock→a, IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄, execute.RetEXC InterruptedException, h),
          (⦃Suspend a, Unlock→a, Lock→a, ReleaseAcquire→a, IsInterrupted t False, SyncUnlock a⦄, RetStaySame, h),
          (⦃UnlockFail→a⦄, execute.RetEXC IllegalMonitorState, h),
          (⦃Notified⦄, RetVal Unit, h),
          (⦃WokenUp, ClearInterrupt t, ObsInterrupted t⦄, execute.RetEXC InterruptedException, h)} ∪
          (if spurious_wakeups then {(⦃Unlock→a, Lock→a, ReleaseAcquire→a, IsInterrupted t False, SyncUnlock a⦄, RetVal Unit, h)} else {})
    else if M = notify then
       {(⦃Notify a, Unlock→a, Lock→a⦄, RetVal Unit, h),
        (⦃UnlockFail→a⦄, execute.RetEXC IllegalMonitorState, h)}
    else if M = notifyAll then 
       {(⦃NotifyAll a, Unlock→a, Lock→a ⦄, RetVal Unit, h),
        (⦃UnlockFail→a⦄, execute.RetEXC IllegalMonitorState, h)}
    else if M = clone then
       do {
         (h', obsa) ← heap_clone P h a;
         {case obsa of None ⇒ (ε, execute.RetEXC OutOfMemory, h')
           | Some (obs, a') ⇒ ((K$ [], [], [], [], [], obs), RetVal (Addr a'), h')}
       }
    else if M = hashcode then {(ε, RetVal (Intg (word_of_int (hash_addr a))), h)}
    else if M = print then {(⦃ExternalCall a M vs Unit⦄, RetVal Unit, h)}
    else if M = currentThread then {(ε, RetVal (Addr (thread_id2addr t)), h)}
    else if M = interrupted then 
      {(⦃IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄, RetVal (Bool True), h),
       (⦃IsInterrupted t False⦄, RetVal (Bool False), h)}
    else if M = yield then {(⦃Yield⦄, RetVal Unit, h)}
    else
      let T = ty_of_htype (the (typeof_addr h a))
      in if P ⊢ T ≤ Class Thread then
        let t_a = addr2thread_id a 
        in if M = start then 
             {(⦃NewThread t_a (the_Class T, run, a) h, ThreadStart t_a⦄, RetVal Unit, h),
              (⦃ThreadExists t_a True⦄, execute.RetEXC IllegalThreadState, h)}
           else if M = join then
             {(⦃Join t_a, IsInterrupted t False, ThreadJoin t_a⦄, RetVal Unit, h),
              (⦃IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄, execute.RetEXC InterruptedException, h)}
           else if M = interrupt then
             {(⦃ThreadExists t_a True, WakeUp t_a, Interrupt t_a, ObsInterrupt t_a⦄, RetVal Unit, h),
              (⦃ThreadExists t_a False⦄, RetVal Unit, h)}
           else if M = isInterrupted then
             {(⦃IsInterrupted t_a False⦄, RetVal (Bool False), h),
              (⦃IsInterrupted t_a True, ObsInterrupted t_a⦄, RetVal (Bool True), h)}
         else {(⦃⦄, undefined)}
    else {(⦃⦄, undefined)})"
by (auto simp add: execute.red_external_aggr_def
  split del: option.splits) auto

end

lemmas [code] =
  heap_execute.heap_copy_loc_code
  heap_execute.heap_copies_code
  heap_execute.heap_clone_code
  heap_execute.red_external_aggr_code

end