Theory JVMExceptions

(*  Title:      HOL/MicroJava/JVM/JVMExceptions.thy
    ID:         $Id: JVMExceptions.thy,v 1.2.2.8 2002/08/07 21:21:59 kleing Exp $
    Author:     Gerwin Klein, Martin Strecker
    Copyright   2001 Technische Universitaet Muenchen
*)

header {* \isaheader{Exception handling in the JVM} *}

theory JVMExceptions
imports JVMInstructions
begin
constdefs
  match_exception_entry :: "jvm_prog => cname => p_count => exception_entry => bool"
  "match_exception_entry G cn pc ee == 
                 let (start_pc, end_pc, handler_pc, catch_type) = ee in
                 start_pc <= pc ∧ pc < end_pc ∧ G\<turnstile> cn \<preceq>C catch_type"


consts
  match_exception_table :: "jvm_prog => cname => p_count => exception_table
                          => p_count option"
primrec
  "match_exception_table G cn pc []     = None"
  "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
                                           then Some (fst (snd (snd e))) 
                                           else match_exception_table G cn pc es)"


consts
  cname_of :: "aheap => val => cname"
  ex_table_of :: "jvm_method => exception_table"

translations
  "cname_of hp v" == "the_Class (obj_ty (the (hp (the_Addr v))))"
  "ex_table_of m" == "snd (snd (snd m))"


consts
  find_handler :: "jvm_prog => val option => sheap => aheap => init_heap => frame list => jvm_state"
primrec
  "find_handler G xcpt shp hp ihp [] = (xcpt,shp, hp, ihp, [])"
  "find_handler G xcpt shp hp ihp (fr#frs) = 
      (case xcpt of
         None => (None, shp,hp, ihp, fr#frs)
       | Some xc => 
       let (stk,loc,C,sig,pc,r) = fr in
       (case match_exception_table G (cname_of hp xc) pc 
              (ex_table_of (snd(snd(the(method (G,C) sig))))) of
          None => find_handler G (Some xc) shp hp ihp frs 
        | Some handler_pc => (None,shp, hp, ihp, ([xc], loc, C, sig, handler_pc, r)#frs)))"


text {*
  Expresses that a value is tagged with an initialized type (only applies 
  to addresses and then only if the heap contains a value for the address)
*}
constdefs
  is_init :: "aheap => init_heap => val => bool"
  "is_init hp ih v ≡ 
  ∀loc. v = Addr loc --> hp loc ≠ None --> (∃t. ih loc = Init t)"


text {*
  System exceptions are allocated in all heaps.
*}
constdefs
  preallocated :: "aheap => init_heap => bool"
  "preallocated hp ihp ≡ ∀x. ∃fs. hp (XcptRef x) = Some (Obj (Xcpt x) fs) ∧ is_init hp ihp (Addr (XcptRef x))"

lemma preallocatedD [simp,dest]:
  "preallocated hp ihp ==> ∃fs. hp (XcptRef x) = Some (Obj (Xcpt x) fs) ∧ is_init hp ihp (Addr (XcptRef x))"
  by (unfold preallocated_def) fast

lemma preallocatedE [elim?]:
  "preallocated hp ihp ==> 
   (!!fs. hp (XcptRef x) = Some (Obj (Xcpt x) fs) ==> is_init hp ihp (Addr (XcptRef x)) ==> P hp ihp)
   ==> P hp ihp"
  by fast

lemma cname_of_xcp:
  "raise_system_xcpt b x = Some xcp ==> preallocated hp ihp
  ==> cname_of hp xcp = Xcpt x"
proof -
  assume "raise_system_xcpt b x = Some xcp"
  hence "xcp = Addr (XcptRef x)"
    by (simp add: raise_system_xcpt_def split: split_if_asm)
  moreover
  assume "preallocated hp ihp" 
  then obtain fs where "hp (XcptRef x) = Some (Obj (Xcpt x) fs)" ..
  ultimately show ?thesis by simp
qed


lemma preallocated_start:
  "preallocated (start_heap G) start_iheap"
  apply (unfold preallocated_def)
  apply (unfold start_heap_def start_iheap_def)
  apply (rule allI)
  apply (case_tac x)
  apply (auto simp add: blank_def is_init_def)
  done


text {*
  Only program counters that are mentioned in the exception table
  can be returned by @{term match_exception_table}:
*}
lemma match_exception_table_in_et:
  "match_exception_table G C pc et = Some pc' ==> ∃e ∈ set et. pc' = fst (snd (snd e))"
  by (induct et) (auto split: split_if_asm)


end