Theory JVMExec

(*  Title:      HOL/MicroJava/JVM/JVMExec.thy
    ID:         $Id: JVMExec.thy,v 1.8 2008-10-07 14:07:44 fhaftmann Exp $
    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))))))"


-- "single step execution:"
consts
  exec :: "jvm_prog × jvm_state => jvm_state option"
recdef exec "{}"
  "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" 

(* Needed because recdef splits clauses further up *)
lemma [simp]: "exec (P, x, h, []) = None"
by(cases x) simp+

-- "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:"
consts
  exec_all :: "jvm_prog => jvm_state => jvm_state => bool"
              ("_ |-/ _ -jvm->/ _" [61,61,61]60)
(* FIXME exec_all -> exec_star, also in Def.JVM *)
syntax (xsymbols)
  exec_all :: "jvm_prog => jvm_state => jvm_state => bool"
              ("(_ \<turnstile>/ _ -jvm->/ _)" [61,61,61]60)
defs
  exec_all_def1: "P \<turnstile> σ -jvm-> σ' ≡ (σ,σ') ∈ (exec_1 P)*"


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.
*}
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