Theory JVMExceptions

(*  Title:      JinjaThreads/JVM/JVMExceptions.thy
    Author:     Gerwin Klein, Martin Strecker, Andreas Lochbihler
*)

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

theory JVMExceptions imports JVMInstructions begin

definition matches_ex_entry :: "'m prog => cname => pc => ex_entry => bool"
where
 "matches_ex_entry P C pc xcp ≡
                 let (s, e, C', h, d) = xcp in
                 s ≤ pc ∧ pc < e ∧ (case C' of None => True | ⌊C''⌋ => P \<turnstile> C \<preceq>* C'')"


primrec
  match_ex_table :: "'m prog => cname => pc => ex_table => (pc × nat) option"
where
  "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))))))"

end