Theory JinjaDCI.JVMExceptions
section ‹ Exception handling in the JVM ›
theory JVMExceptions imports "../Common/Exceptions" JVMInstructions
begin
definition matches_ex_entry :: "'m prog ⇒ cname ⇒ pc ⇒ ex_entry ⇒ bool"
where
"matches_ex_entry P C pc xcp ≡
let (s, e, C', h, d) = xcp in
s ≤ pc ∧ pc < e ∧ P ⊢ C ≼⇧* C'"
primrec match_ex_table :: "'m prog ⇒ cname ⇒ pc ⇒ ex_table ⇒ (pc × nat) option"
where
"match_ex_table P C pc [] = None"
| "match_ex_table P C pc (e#es) = (if matches_ex_entry P C pc e
then Some (snd(snd(snd e)))
else match_ex_table P C pc es)"
abbreviation
ex_table_of :: "jvm_prog ⇒ cname ⇒ mname ⇒ ex_table" where
"ex_table_of P C M == snd (snd (snd (snd (snd (snd (snd (method P C M)))))))"
fun find_handler :: "jvm_prog ⇒ addr ⇒ heap ⇒ frame list ⇒ sheap ⇒ jvm_state"
where
"find_handler P a h [] sh = (Some a, h, [], sh)"
| "find_handler P a h (fr#frs) sh =
(let (stk,loc,C,M,pc,ics) = fr in
case match_ex_table P (cname_of h a) pc (ex_table_of P C M) of
None ⇒
(case M = clinit of
True ⇒ (case frs of (stk',loc',C',M',pc',ics')#frs'
⇒ (case ics' of Called Cs ⇒ (None, h, (stk',loc',C',M',pc',Throwing (C#Cs) a)#frs', sh)
| _ ⇒ (None, h, (stk',loc',C',M',pc',ics')#frs', sh)
)
| [] ⇒ (Some a, h, [], sh)
)
| _ ⇒ find_handler P a h frs sh
)
| Some pc_d ⇒ (None, h, (Addr a # drop (size stk - snd pc_d) stk, loc, C, M, fst pc_d, No_ics)#frs, sh))"
lemma find_handler_cases:
"find_handler P a h frs sh = js
⟹ (∃frs'. frs' ≠ [] ∧ js = (None, h, frs', sh)) ∨ (js = (Some a, h, [], sh))"
proof(induct P a h frs sh rule: find_handler.induct)
case 1 then show ?case by clarsimp
next
case (2 P a h fr frs sh) then show ?case
by(cases fr, auto split: bool.splits list.splits init_call_status.splits)
qed
lemma find_handler_heap[simp]:
"find_handler P a h frs sh = (xp',h',frs',sh') ⟹ h' = h"
by(auto dest: find_handler_cases)
lemma find_handler_sheap[simp]:
"find_handler P a h frs sh = (xp',h',frs',sh') ⟹ sh' = sh"
by(auto dest: find_handler_cases)
lemma find_handler_frames[simp]:
"find_handler P a h frs sh = (xp',h',frs',sh') ⟹ length frs' ≤ length frs"
proof(induct frs)
case Nil then show ?case by simp
next
case (Cons a frs) then show ?case
by(auto simp: split_beta split: bool.splits list.splits init_call_status.splits)
qed
lemma find_handler_None:
"find_handler P a h frs sh = (None, h, frs', sh') ⟹ frs' ≠ []"
by (drule find_handler_cases, clarsimp)
lemma find_handler_Some:
"find_handler P a h frs sh = (Some x, h, frs', sh') ⟹ frs' = []"
by (drule find_handler_cases, clarsimp)
lemma find_handler_Some_same_error_same_heap[simp]:
"find_handler P a h frs sh = (Some x, h', frs', sh') ⟹ x = a ∧ h = h' ∧ sh = sh'"
by(auto dest: find_handler_cases)
lemma find_handler_prealloc_pres:
assumes "preallocated h"
and fh: "find_handler P a h frs sh = (xp',h',frs',sh')"
shows "preallocated h'"
using assms find_handler_heap[OF fh] by simp
lemma find_handler_frs_tl_neq:
"ics_of f ≠ No_ics
⟹ (xp, h, f#frs, sh) ≠ find_handler P xa h' (f' # frs) sh'"
proof(induct frs arbitrary: f f')
case Nil then show ?case by(auto simp: split_beta split: bool.splits)
next
case (Cons a frs)
obtain xp1 h1 frs1 sh1 where fh: "find_handler P xa h' (a # frs) sh' = (xp1,h1,frs1,sh1)"
by(cases "find_handler P xa h' (a # frs) sh'")
then have "length frs1 ≤ length (a#frs)"
by(rule find_handler_frames[where P=P and a=xa and h=h' and frs="a#frs" and sh=sh'])
then have neq: "f#a#frs ≠ frs1" by(clarsimp dest: impossible_Cons)
then show ?case
proof(cases "find_handler P xa h' (f' # a # frs) sh' = find_handler P xa h' (a # frs) sh'")
case True then show ?thesis using neq fh by simp
next
case False then show ?thesis using Cons.prems
by(fastforce simp: split_beta split: bool.splits init_call_status.splits list.splits)
qed
qed
end