Theory JVMExec

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

section ‹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" 
    (‹_ ⊢/ _ -jvm→⇩1/ _› [61,61,61] 60)
  for P :: jvm_prog
where
  "P ⊢ σ -jvm→⇩1 σ' ≡ (σ,σ') ∈ exec_1 P"
| exec_1I: "exec (P,σ) = Some σ' ⟹ P ⊢ σ -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 (ASCII)
  exec_all  (‹_ |-/ _ -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 ⊢ σ -jvm→⇩1 σ' = (exec (P,σ) = Some σ')"
(*<*)by (simp add: exec_1_eq)(*>*)

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

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

lemma jvm_trans[trans]:
 "⟦ P ⊢ σ -jvm→ σ'; P ⊢ σ' -jvm→ σ'' ⟧ ⟹ P ⊢ σ -jvm→ σ''"
(*<*)by(simp add: exec_all_def)(*>*)

lemma jvm_one_step1[trans]:
 "⟦ P ⊢ σ -jvm→⇩1 σ'; P ⊢ σ' -jvm→ σ'' ⟧ ⟹ P ⊢ σ -jvm→ σ''"
(*<*) by (simp add: exec_all_def1) (*>*)

lemma jvm_one_step2[trans]:
 "⟦ P ⊢ σ -jvm→ σ'; P ⊢ σ' -jvm→⇩1 σ'' ⟧ ⟹ P ⊢ σ -jvm→ σ''"
(*<*) by (simp add: exec_all_def1) (*>*)

lemma exec_all_conf:
  "⟦ P ⊢ σ -jvm→ σ'; P ⊢ σ -jvm→ σ'' ⟧
  ⟹ P ⊢ σ' -jvm→ σ'' ∨ P ⊢ σ'' -jvm→ σ'"
(*<*)by(simp add: exec_all_def single_valued_def single_valued_confluent)(*>*)


lemma exec_all_finalD: "P ⊢ (x, h, []) -jvm→ σ ⟹ σ = (x, h, [])"
(*<*)
proof -
  assume "P ⊢ (x, h, []) -jvm→ σ"
  then have "((x, h, []), σ) ∈ {(σ, σ'). exec (P, σ) = ⌊σ'⌋}⇧*"
    by(simp only: exec_all_def)
  then show ?thesis proof(rule converse_rtranclE) qed simp+
qed
(*>*)

lemma exec_all_deterministic:
  "⟦ P ⊢ σ -jvm→ (x,h,[]); P ⊢ σ -jvm→ σ' ⟧ ⟹ P ⊢ σ' -jvm→ (x,h,[])"
(*<*)
proof -
  assume assms: "P ⊢ σ -jvm→ (x,h,[])" "P ⊢ σ -jvm→ σ'"
  show ?thesis using exec_all_conf[OF assms]
    by(blast dest!: exec_all_finalD)
qed
(*>*)


text ‹
  The start configuration of the JVM: in the start heap, we call a 
  method ‹m› of class ‹C› in program ‹P›. The 
  ‹this› pointer of the frame is set to ‹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