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

  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) =
     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›
  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
  "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+

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)

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,mxl0,b) = method P C M in
    (None, start_heap P, [([], Null # replicate mxl0 undefined, C, M, 0)]))"