Theory JVMExceptions

(*  Title:      HOL/MicroJava/JVM/JVMExceptions.thy
    ID:         $Id: JVMExceptions.thy,v 1.3 2008-06-24 22:23:36 makarius Exp $
    Author:     Gerwin Klein, Martin Strecker
    Copyright   2001 Technische Universitaet Muenchen
*)

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

theory JVMExceptions imports JVMInstructions Exceptions begin

constdefs
  matches_ex_entry :: "'m prog => cname => pc => ex_entry => bool"
 "matches_ex_entry P C pc xcp ≡
                 let (s, e, C', h, d) = xcp in
                 s ≤ pc ∧ pc < e ∧ P \<turnstile> C \<preceq>* C'"


consts
  match_ex_table :: "'m prog => cname => pc => ex_table => (pc × nat) option"
primrec
  "match_ex_table P C pc []     = None"
  "match_ex_table P C pc (e#es) = (if matches_ex_entry P C pc e
                                   then Some (snd(snd(snd e)))
                                   else match_ex_table P C pc es)"

abbreviation
  ex_table_of :: "jvm_prog => cname => mname => ex_table" where
  "ex_table_of P C M == snd (snd (snd (snd (snd (snd(method P C M))))))"


consts
  find_handler :: "jvm_prog => addr => heap => frame list => jvm_state"
primrec
  "find_handler P a h [] = (Some a, h, [])"
  "find_handler P a h (fr#frs) = 
       (let (stk,loc,C,M,pc) = fr in
        case match_ex_table P (cname_of h a) pc (ex_table_of P C M) of
          None => find_handler P a h frs
        | Some pc_d => (None, h, (Addr a # drop (size stk - snd pc_d) stk, loc, C, M, fst pc_d)#frs))"

end