Quelle  JVMExceptions.thy

(*  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 begin

definition match_exception_entry :: "jvm_prog ==> cname ==> p_count ==> exception_entry ==> bool" where
  "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⊨ cn ⪯C catch_type"


primrec match_exception_table :: "jvm_prog ==> cname ==> p_count ==> exception_table
    ==> p_count option"
where
  "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)"

abbreviation
  ex_table_of :: "jvm_method ==> exception_table"
  where "ex_table_of m == snd (snd (snd m))"


primrec find_handler :: "jvm_prog ==> val option ==> aheap ==> frame list
    ==> jvm_state"
where
  "find_handler G xcpt hp [] = (xcpt, hp, [])"
| "find_handler G xcpt hp (fr#frs) =
      (case xcpt of
         None ==> (None, hp, fr#frs)
       | Some xc ==>
       let (stk,loc,C,sig,pc) = 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) hp frs
        | Some handler_pc ==> (None, hp, ([xc], loc, C, sig, handler_pc)#frs)))"


text ‹
  System exceptions are allocated in all heaps:
 ›


text ‹
  Only program counters that are mentioned in the exception table
  can be returned by 🍋‹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: if_split_asm)


end