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