section \<open>Exception handling in the JVM\<close>
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 \<and> pc < end_pc \<and> G\<turnstile> cn \<preceq>C catch_type"
primrec match_exception_table :: "jvm_prog \ cname \ p_count \ exception_table \<Rightarrow> 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)"
primrec find_handler :: "jvm_prog \ val option \ aheap \ frame list \<Rightarrow> jvm_state" where "find_handler G xcpt hp [] = (xcpt, hp, [])"
| "find_handler G xcpt hp (fr#frs) =
(case xcpt of
None \<Rightarrow> (None, hp, fr#frs)
| Some xc \<Rightarrow> 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 \<Rightarrow> find_handler G (Some xc) hp frs
| Some handler_pc \<Rightarrow> (None, hp, ([xc], loc, C, sig, handler_pc)#frs)))"
text\<open>
System exceptions are allocated in all heaps: \<close>
text\<open>
Only program counters that are mentioned in the exception table
can be returned by\<^term>\<open>match_exception_table\<close>: \<close> 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
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
