1(* Title: HOL/MicroJava/JVM/JVMExceptions.thy 2 Author: Gerwin Klein, Martin Strecker 3 Copyright 2001 Technische Universitaet Muenchen 4*) 5 6section \<open>Exception handling in the JVM\<close> 7 8theory JVMExceptions imports JVMInstructions begin 9 10definition match_exception_entry :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_entry \<Rightarrow> bool" where 11 "match_exception_entry G cn pc ee == 12 let (start_pc, end_pc, handler_pc, catch_type) = ee in 13 start_pc <= pc \<and> pc < end_pc \<and> G\<turnstile> cn \<preceq>C catch_type" 14 15 16primrec match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table 17 \<Rightarrow> p_count option" 18where 19 "match_exception_table G cn pc [] = None" 20| "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e 21 then Some (fst (snd (snd e))) 22 else match_exception_table G cn pc es)" 23 24abbreviation 25 ex_table_of :: "jvm_method \<Rightarrow> exception_table" 26 where "ex_table_of m == snd (snd (snd m))" 27 28 29primrec find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list 30 \<Rightarrow> jvm_state" 31where 32 "find_handler G xcpt hp [] = (xcpt, hp, [])" 33| "find_handler G xcpt hp (fr#frs) = 34 (case xcpt of 35 None \<Rightarrow> (None, hp, fr#frs) 36 | Some xc \<Rightarrow> 37 let (stk,loc,C,sig,pc) = fr in 38 (case match_exception_table G (cname_of hp xc) pc 39 (ex_table_of (snd(snd(the(method (G,C) sig))))) of 40 None \<Rightarrow> find_handler G (Some xc) hp frs 41 | Some handler_pc \<Rightarrow> (None, hp, ([xc], loc, C, sig, handler_pc)#frs)))" 42 43 44text \<open> 45 System exceptions are allocated in all heaps: 46\<close> 47 48 49text \<open> 50 Only program counters that are mentioned in the exception table 51 can be returned by @{term match_exception_table}: 52\<close> 53lemma match_exception_table_in_et: 54 "match_exception_table G C pc et = Some pc' \<Longrightarrow> \<exists>e \<in> set et. pc' = fst (snd (snd e))" 55 by (induct et) (auto split: if_split_asm) 56 57 58end 59