Theory JVMExec

(*  Title:      HOL/MicroJava/JVM/JVMExec.thy
    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

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))))))"

fun exec :: "jvm_prog × jvm_state => jvm_state option" where -- "single step execution"
  "exec (P, xp, h, []) = None"

| "exec (P, None, h, (stk,loc,C,M,pc)#frs) =
  (let 
     i = instrs_of P C M ! pc;
     (xcpt', h', frs') = exec_instr i P h stk loc C M pc frs
   in Some(case xcpt' of
             None => (None,h',frs')
           | Some a => find_handler P a h ((stk,loc,C,M,pc)#frs)))"

| "exec (P, Some xa, h, frs) = None" 

-- "relational view"
inductive_set
  exec_1 :: "jvm_prog => (jvm_state × jvm_state) set"
  and exec_1' :: "jvm_prog => jvm_state => jvm_state => bool" 
    ("_ \<turnstile>/ _ -jvm->⇣1/ _" [61,61,61] 60)
  for P :: jvm_prog
where
  "P \<turnstile> σ -jvm->⇣1 σ' ≡ (σ,σ') ∈ exec_1 P"
| exec_1I: "exec (P,σ) = Some σ' ==> P \<turnstile> σ -jvm->⇣1 σ'"

-- "reflexive transitive closure:"
definition exec_all :: "jvm_prog => jvm_state => jvm_state => bool"
              ("_ |-/ _ -jvm->/ _" [61,61,61]60) where
(* FIXME exec_all -> exec_star, also in Def.JVM *)
  exec_all_def1: "P |- σ -jvm-> σ' <-> (σ,σ') ∈ (exec_1 P)⇧*"

notation (xsymbols)
  exec_all  ("(_ \<turnstile>/ _ -jvm->/ _)" [61,61,61]60)


lemma exec_1_eq:
  "exec_1 P = {(σ,σ'). exec (P,σ) = Some σ'}"
(*<*)by (auto intro: exec_1I elim: exec_1.cases)(*>*)

lemma exec_1_iff:
  "P \<turnstile> σ -jvm->⇣1 σ' = (exec (P,σ) = Some σ')"
(*<*)by (simp add: exec_1_eq)(*>*)

lemma exec_all_def:
  "P \<turnstile> σ -jvm-> σ' = ((σ,σ') ∈ {(σ,σ'). exec (P,σ) = Some σ'}⇧*)"
(*<*)by (simp add: exec_all_def1 exec_1_eq)(*>*)

lemma jvm_refl[iff]: "P \<turnstile> σ -jvm-> σ"
(*<*)by(simp add: exec_all_def)(*>*)

lemma jvm_trans[trans]:
 "[| P \<turnstile> σ -jvm-> σ'; P \<turnstile> σ' -jvm-> σ'' |] ==> P \<turnstile> σ -jvm-> σ''"
(*<*)by(simp add: exec_all_def)(*>*)

lemma jvm_one_step1[trans]:
 "[| P \<turnstile> σ -jvm->⇣1 σ'; P \<turnstile> σ' -jvm-> σ'' |] ==> P \<turnstile> σ -jvm-> σ''"
(*<*) by (simp add: exec_all_def1) (*>*)

lemma jvm_one_step2[trans]:
 "[| P \<turnstile> σ -jvm-> σ'; P \<turnstile> σ' -jvm->⇣1 σ'' |] ==> P \<turnstile> σ -jvm-> σ''"
(*<*) by (simp add: exec_all_def1) (*>*)

lemma exec_all_conf:
  "[| P \<turnstile> σ -jvm-> σ'; P \<turnstile> σ -jvm-> σ'' |]
  ==> P \<turnstile> σ' -jvm-> σ'' ∨ P \<turnstile> σ'' -jvm-> σ'"
(*<*)by(simp add: exec_all_def single_valued_def single_valued_confluent)(*>*)


lemma exec_all_finalD: "P \<turnstile> (x, h, []) -jvm-> σ ==> σ = (x, h, [])"
(*<*)
apply(simp only: exec_all_def)
apply(erule converse_rtranclE)
 apply simp
apply simp
done
(*>*)

lemma exec_all_deterministic:
  "[| P \<turnstile> σ -jvm-> (x,h,[]); P \<turnstile> σ -jvm-> σ' |] ==> P \<turnstile> σ' -jvm-> (x,h,[])"
(*<*)
apply(drule (1) exec_all_conf)
apply(blast dest!: exec_all_finalD)
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.
*}
definition start_state :: "jvm_prog => cname => mname => jvm_state" where
  "start_state P C M =
  (let (D,Ts,T,mxs,mxl⇣0,b) = method P C M in
    (None, start_heap P, [([], Null # replicate mxl⇣0 undefined, C, M, 0)]))"

end