Theory JVMExec

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

section ‹Program Execution in the JVM›

theory JVMExec
imports
  JVMExecInstr
  JVMExceptions
  "../Common/StartConfig"
begin

abbreviation instrs_of :: "'addr jvm_prog ⇒ cname ⇒ mname ⇒ 'addr instr list"
where "instrs_of P C M == fst(snd(snd(the(snd(snd(snd(method P C M)))))))"

subsection "single step execution"

context JVM_heap_base begin

fun exception_step :: "'addr jvm_prog ⇒ 'addr ⇒ 'heap ⇒ 'addr frame ⇒ 'addr frame list ⇒ ('addr, 'heap) jvm_state"
where
  "exception_step P a h (stk, loc, C, M, pc) frs = 
   (case match_ex_table P (cname_of h a) pc (ex_table_of P C M) of
          None ⇒ (⌊a⌋, h, frs)
        | Some (pc', d) ⇒ (None, h, (Addr a # drop (size stk - d) stk, loc, C, M, pc') # frs))"

lemma exception_step_def_raw:
  "exception_step = 
   (λP a h (stk, loc, C, M, pc) frs.
    case match_ex_table P (cname_of h a) pc (ex_table_of P C M) of
      None ⇒ (⌊a⌋, h, frs)
    | Some (pc', d) ⇒ (None, h, (Addr a # drop (size stk - d) stk, loc, C, M, pc') # frs))"
by(intro ext) auto

fun exec :: "'addr jvm_prog ⇒ 'thread_id ⇒ ('addr, 'heap) jvm_state ⇒ ('addr, 'thread_id, 'heap) jvm_ta_state set" where
  "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) = {(ε, exception_step P a h fr frs)}"

subsection "relational view"

inductive exec_1 :: 
  "'addr jvm_prog ⇒ 'thread_id ⇒ ('addr, 'heap) jvm_state
  ⇒ ('addr, 'thread_id, 'heap) jvm_thread_action ⇒ ('addr, 'heap) jvm_state ⇒ bool"
  (‹_,_ ⊢/ _ -_-jvm→/ _› [61,0,61,0,61] 60)
  for P :: "'addr jvm_prog" and t :: 'thread_id
where
  exec_1I:
  "(ta, σ') ∈ exec P t σ ⟹ P,t ⊢ σ -ta-jvm→ σ'"

lemma exec_1_iff:
  "P,t ⊢ σ -ta-jvm→ σ' ⟷ (ta, σ') ∈ exec P t σ"
by(auto intro: exec_1I elim: exec_1.cases)

end

text ‹
  The start configuration of the JVM: in the start heap, we call a 
  method ‹m› of class ‹C› in program ‹P› with parameters @{term "vs"}. The 
  ‹this› pointer of the frame is set to ‹Null› to simulate
  a static method invokation.
›

abbreviation JVM_local_start ::
  "cname ⇒ mname ⇒ ty list ⇒ ty ⇒ 'addr jvm_method ⇒ 'addr val list
  ⇒ 'addr jvm_thread_state"
where
  "JVM_local_start ≡ 
   λC M Ts T (mxs, mxl0, b) vs. 
   (None, [([], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])"

context JVM_heap_base begin

abbreviation JVM_start_state :: 
  "'addr jvm_prog ⇒ cname ⇒ mname ⇒ 'addr val list ⇒ ('addr,'thread_id,'addr jvm_thread_state,'heap,'addr) state"
where
  "JVM_start_state ≡ start_state JVM_local_start"

definition JVM_start_state' :: "'addr jvm_prog ⇒ cname ⇒ mname ⇒ 'addr val list ⇒ ('addr, 'heap) jvm_state"
where
  "JVM_start_state' P C M vs ≡
   let (D, Ts, T, meth) = method P C M;
       (mxs, mxl0, ins, xt) = the meth
   in (None, start_heap, [([], Null # vs @ replicate mxl0 undefined_value, D, M, 0)])"

end

end