Theory JVMExceptions

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

section ‹Exception handling in the JVM›

theory JVMExceptions
imports
  JVMInstructions
begin

abbreviation Any :: "cname option"
where "Any ≡ None"

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 ⊢ C ≼⇧* 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 :: "'addr jvm_prog ⇒ cname ⇒ mname ⇒ ex_table"
where "ex_table_of P C M == snd (snd (snd (the (snd (snd (snd(method P C M)))))))"

lemma match_ex_table_SomeD:
  "match_ex_table P C pc xt = Some (pc',d') ⟹ 
  ∃(f,t,D,h,d) ∈ set xt. matches_ex_entry P C pc (f,t,D,h,d) ∧ h = pc' ∧ d=d'"
  by (induct xt) (auto split: if_split_asm)

end