Theory JVMExec

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

header {* \isaheader{Program Execution in the JVM} *}

theory JVMExec imports JVMExecInstr JVMExceptions begin

abbreviation instrs_of :: "jvm_prog => cname => mname => instr list"
where "instrs_of P C M == fst(snd(snd(snd(snd(snd(method P C M))))))"


section "single step execution"

fun exception_step :: "jvm_prog => jvm_ta_state => jvm_ta_state"
where
  "exception_step P (ta, ⌊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 => (ta, ⌊a⌋, h, frs)
        | Some (pc', d) => (ta, None, h, (Addr a # drop (size stk - d) stk, loc, C, M, pc') # frs))"
| "exception_step P σ = σ"


lemma exception_step_def_raw:
  "exception_step = 
   (λP (ta, xcp, h, frs).
    case frs of [] => (ta, xcp, h, [])
    | ((stk, loc, C, M, pc) # frs') => (case xcp of None => (ta, xcp, h, frs)
                                                   | ⌊a⌋ => (case match_ex_table P (cname_of h a) pc (ex_table_of P C M) of
                                                                 None => (ta, ⌊a⌋, h, frs')
                                                      | Some (pc', d) => (ta, None, h, (Addr a # drop (size stk - d) stk, loc, C, M, pc') # frs'))))"
by(auto simp add: expand_fun_eq split: list.split)

fun exec :: "jvm_prog => jvm_state => jvm_ta_state list" where
  "exec P (xcp, h, []) = []"
| "exec P (None, h, (stk, loc, C, M, pc) # frs) = exec_instr (instrs_of P C M ! pc) P h stk loc C M pc frs"
| "exec P (⌊a⌋, h, fr # frs) = [exception_step P (ε, ⌊a⌋, h, fr # frs)]"

lemma exec_not_empty:
  "exec P (xcp, h, f # frs) ≠ []"
by(cases f, cases xcp, auto intro: exec_instr_not_empty del: notI)



section "relational view"
inductive
  exec_1 :: "jvm_prog => jvm_state => jvm_thread_action => jvm_state => bool" ("_ \<turnstile>/ _ -_-jvm->/ _" [61,61,0,61] 60)
  for P :: jvm_prog
where
  exec_1I:
  "(ta, σ') ∈ set (exec P σ) ==> P \<turnstile> σ -ta-jvm-> σ'"

section "reflexive transitive closure:"
definition
  exec_star :: "jvm_prog => jvm_state => jvm_thread_action list => jvm_state => bool" ("_ \<turnstile>/ _ -_-jvm->*/ _" [61,61,0,61] 60)
where
  "P \<turnstile> σ -tas-jvm->* σ' ≡ rtrancl3p (exec_1 P) σ tas σ'"

lemma exec_1_iff:
  "P \<turnstile> σ -ta-jvm-> σ' <-> (ta, σ') ∈ set (exec P σ)"
by(auto intro: exec_1I elim: exec_1.cases)

lemma jvm_refl[iff]: "P \<turnstile> σ -[]-jvm->* σ"
by(auto intro: rtrancl3p.intros simp add: exec_star_def)


lemma jvm_trans[trans]:
 "[| P \<turnstile> σ -tas-jvm->* σ'; P \<turnstile> σ' -tas'-jvm->* σ'' |] ==> P \<turnstile> σ -tas@tas'-jvm->* σ''"
  unfolding exec_star_def
  by(rule rtrancl3p_trans)

lemma jvm_one_step1[trans]:
 "[| P \<turnstile> σ -tas-jvm-> σ'; P \<turnstile> σ' -tas'-jvm->* σ'' |] ==> P \<turnstile> σ -tas#tas'-jvm->* σ''"
  unfolding exec_star_def
  by(rule rtrancl3p_step_converse)

lemma jvm_one_step2[trans]:
 "[| P \<turnstile> σ -tas-jvm->* σ'; P \<turnstile> σ' -tas'-jvm-> σ'' |] ==> P \<turnstile> σ -tas@[tas']-jvm->* σ''"
  unfolding exec_star_def
  by(rule rtrancl3p.rtrancl3p_step)

lemma exec_all_finalD: "P \<turnstile> (x, h, []) -tas-jvm->* σ ==> σ = (x, h, []) ∧ tas = []"
apply(simp only: exec_star_def)
apply(erule rtrancl3p_converseE)
apply(auto elim: exec_1.cases)
done


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

constdefs  
  start_state :: "jvm_prog => cname => mname => jvm_state"
  "start_state P C M ≡
  let (D,Ts,T,mxs,mxl0,b) = method P C M in
    (None, start_heap P, [([], Null # replicate mxl0 undefined, C, M, 0)])"

end