author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
parent 39758 | b8a53e3a0ee2 |
child 58886 | 8a6cac7c7247 |
permissions | -rw-r--r-- |
12519 | 1 |
(* Title: HOL/MicroJava/JVM/JVMExceptions.thy |
2 |
Author: Gerwin Klein, Martin Strecker |
|
3 |
Copyright 2001 Technische Universitaet Muenchen |
|
4 |
*) |
|
5 |
||
12911 | 6 |
header {* \isaheader{Exception handling in the JVM} *} |
12519 | 7 |
|
16417 | 8 |
theory JVMExceptions imports JVMInstructions begin |
12519 | 9 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
10 |
definition match_exception_entry :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_entry \<Rightarrow> bool" where |
12519 | 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 |
||
39758 | 16 |
primrec match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table |
17 |
\<Rightarrow> p_count option" |
|
18 |
where |
|
12519 | 19 |
"match_exception_table G cn pc [] = None" |
39758 | 20 |
| "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e |
12519 | 21 |
then Some (fst (snd (snd e))) |
22 |
else match_exception_table G cn pc es)" |
|
23 |
||
35102 | 24 |
abbreviation |
12519 | 25 |
ex_table_of :: "jvm_method \<Rightarrow> exception_table" |
35102 | 26 |
where "ex_table_of m == snd (snd (snd m))" |
12519 | 27 |
|
28 |
||
39758 | 29 |
primrec find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list |
30 |
\<Rightarrow> jvm_state" |
|
31 |
where |
|
12519 | 32 |
"find_handler G xcpt hp [] = (xcpt, hp, [])" |
39758 | 33 |
| "find_handler G xcpt hp (fr#frs) = |
12519 | 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 |
||
12545
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12519
diff
changeset
|
44 |
text {* |
13052 | 45 |
System exceptions are allocated in all heaps: |
12545
7319d384d0d3
removed preallocated heaps axiom (now in type safety invariant)
kleing
parents:
12519
diff
changeset
|
46 |
*} |
13052 | 47 |
|
13065 | 48 |
|
49 |
text {* |
|
50 |
Only program counters that are mentioned in the exception table |
|
51 |
can be returned by @{term match_exception_table}: |
|
52 |
*} |
|
53 |
lemma 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: split_if_asm) |
|
56 |
||
57 |
||
12519 | 58 |
end |