Theory JVMExceptions

(*  Title:      HOL/MicroJava/JVM/JVMExceptions.thy
    Author:     Gerwin Klein, Martin Strecker
    Copyright   2001 Technische Universitaet Muenchen
*)

section ‹Exception handling in the JVM›

theory JVMExceptions imports JVMInstructions "../Common/Exceptions" 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 ∧ 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 :: "jvm_prog ⇒ cname ⇒ mname ⇒ ex_table" where
  "ex_table_of P C M == snd (snd (snd (snd (snd (snd(method P C M))))))"


primrec find_handler :: "jvm_prog ⇒ addr ⇒ heap ⇒ frame list ⇒ jvm_state"
where
  "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