Up to index of Isabelle/HOL/Jinja/HRB-Slicing
theory JVMCFGheader {*
\isachapter{A Control Flow Graph for Jinja Byte Code}
\isaheader{Formalizing the CFG}
*}
theory JVMCFG imports "../StaticInter/BasicDefs" "../../Jinja/BV/BVExample" begin
declare lesub_list_impl_same_size [simp del]
declare listE_length [simp del]
subsection {* Type definitions *}
subsubsection {* Wellformed Programs *}
definition "wf_jvmprog = {(P, Phi). wf_jvm_prog⇘Phi⇙ P}"
typedef wf_jvmprog = "wf_jvmprog"
proof
show "(E, Phi) ∈ wf_jvmprog"
unfolding wf_jvmprog_def by (auto intro: wf_prog)
qed
hide_const Phi E
abbreviation PROG :: "wf_jvmprog => jvm_prog"
where "PROG P ≡ fst(Rep_wf_jvmprog(P))"
abbreviation TYPING :: "wf_jvmprog => ty⇣P"
where "TYPING P ≡ snd(Rep_wf_jvmprog(P))"
lemma wf_jvmprog_is_wf_typ: "wf_jvm_prog⇘TYPING P⇙ (PROG P)"
using Rep_wf_jvmprog [of P]
by (auto simp: wf_jvmprog_def split_beta)
lemma wf_jvmprog_is_wf: "wf_jvm_prog (PROG P)"
using wf_jvmprog_is_wf_typ unfolding wf_jvm_prog_def
by blast
subsubsection {* Interprocedural CFG *}
type_synonym jvm_method = "wf_jvmprog × cname × mname"
datatype var = Heap | Local "nat" | Stack "nat" | Exception
datatype val = Hp "heap" | Value "Value.val"
type_synonym state = "var \<rightharpoonup> val"
definition valid_state :: "state => bool"
where "valid_state s ≡ (∀val. s Heap ≠ Some (Value val))
∧ (s Exception = None ∨ (∃addr. s Exception = Some (Value (Addr addr))))
∧ (∀var. var ≠ Heap ∧ var ≠ Exception --> (∀h. s var ≠ Some (Hp h)))"
fun the_Heap :: "val => heap"
where "the_Heap (Hp h) = h"
fun the_Value :: "val => Value.val"
where "the_Value (Value v) = v"
abbreviation heap_of :: "state => heap"
where "heap_of s ≡ the_Heap (the (s Heap))"
abbreviation exc_flag :: "state => addr option"
where "exc_flag s ≡ case (s Exception) of None => None
| Some v => Some (THE a. v = Value (Addr a))"
abbreviation stkAt :: "state => nat => Value.val"
where "stkAt s n ≡ the_Value (the (s (Stack n)))"
abbreviation locAt :: "state => nat => Value.val"
where "locAt s n ≡ the_Value (the (s (Local n)))"
datatype nodeType = Enter | Normal | Return | Exceptional "pc option" "nodeType"
type_synonym cfg_node = "cname × mname × pc option × nodeType"
type_synonym
cfg_edge = "cfg_node × (var, val, cname × mname × pc, cname × mname) edge_kind × cfg_node"
definition ClassMain :: "wf_jvmprog => cname"
where "ClassMain P ≡ SOME Name. ¬ is_class (PROG P) Name"
definition MethodMain :: "wf_jvmprog => mname"
where "MethodMain P ≡ SOME Name.
∀C D fs ms. class (PROG P) C = ⌊(D, fs, ms)⌋ --> (∀m ∈ set ms. Name ≠ fst m)"
definition stkLength :: "jvm_method => pc => nat"
where
"stkLength m pc ≡ let (P, C, M) = m in (
if (C = ClassMain P) then 1 else (
length (fst(the(((TYPING P) C M) ! pc)))
))"
definition locLength :: "jvm_method => pc => nat"
where
"locLength m pc ≡ let (P, C, M) = m in (
if (C = ClassMain P) then 1 else (
length (snd(the(((TYPING P) C M) ! pc)))
))"
lemma ex_new_class_name: "∃C. ¬ is_class P C"
proof -
have "¬ finite (UNIV :: cname set)"
by (rule infinite_UNIV_listI)
hence "∃C. C ∉ set (map fst P)"
by -(rule ex_new_if_finite, auto)
then obtain C where "C ∉ set (map fst P)"
by blast
have "¬ is_class P C"
proof
assume "is_class P C"
then obtain D fs ms where "class P C = ⌊(D, fs, ms)⌋"
by auto
with `C ∉ set (map fst P)` show False
by (auto dest: map_of_SomeD intro!: image_eqI simp: class_def)
qed
thus ?thesis
by blast
qed
lemma ClassMain_unique_in_P:
assumes "is_class (PROG P) C"
shows "ClassMain P ≠ C"
proof -
from ex_new_class_name [of "PROG P"] obtain D where "¬ is_class (PROG P) D"
by blast
with `is_class (PROG P) C` show ?thesis
unfolding ClassMain_def
by -(rule someI2, fastforce+)
qed
lemma map_of_fstD: "[| map_of xs a = ⌊b⌋; ∀x ∈ set xs. fst x ≠ a |] ==> False"
by (induct xs, auto)
lemma map_of_fstE: "[| map_of xs a = ⌊b⌋; ∃x ∈ set xs. fst x = a ==> thesis |] ==> thesis"
by (induct xs) (auto split: split_if_asm)
lemma ex_unique_method_name:
"∃Name. ∀C D fs ms. class (PROG P) C = ⌊(D, fs, ms)⌋ --> (∀m∈set ms. Name ≠ fst m)"
proof -
from wf_jvmprog_is_wf [of P]
have "distinct_fst (PROG P)"
by (simp add: wf_jvm_prog_def wf_jvm_prog_phi_def wf_prog_def)
hence "{C. ∃D fs ms. class (PROG P) C = ⌊(D, fs, ms)⌋} = fst ` set (PROG P)"
by (fastforce elim: map_of_fstE simp: class_def intro: map_of_SomeI)
hence "finite {C. ∃D fs ms. class (PROG P) C = ⌊(D, fs, ms)⌋}"
by auto
moreover have "{ms. ∃C D fs. class (PROG P) C = ⌊(D, fs, ms)⌋}
= snd ` snd ` the ` (λC. class (PROG P) C) ` {C. ∃D fs ms. class (PROG P) C = ⌊(D, fs, ms)⌋}"
by (fastforce intro: rev_image_eqI map_of_SomeI simp: class_def)
ultimately have "finite {ms. ∃C D fs. class (PROG P) C = ⌊(D, fs, ms)⌋}"
by auto
moreover have "¬ finite (UNIV :: mname set)"
by (rule infinite_UNIV_listI)
ultimately
have "∃Name. Name ∉ fst ` (\<Union>ms ∈ {ms. ∃C D fs. class (PROG P) C = ⌊(D, fs, ms)⌋}. set ms)"
by -(rule ex_new_if_finite, auto)
thus ?thesis
by fastforce
qed
lemma MethodMain_unique_in_P:
assumes "PROG P \<turnstile> D sees M:Ts->T = mb in C"
shows "MethodMain P ≠ M"
proof -
from ex_unique_method_name [of P] obtain M'
where "!!C D fs ms. class (PROG P) C = ⌊(D, fs, ms)⌋ ==> (∀m ∈ set ms. M' ≠ fst m)"
by blast
with `PROG P \<turnstile> D sees M:Ts->T = mb in C`
show ?thesis
unfolding MethodMain_def
by -(rule someI2_ex, fastforce, fastforce dest!: visible_method_exists elim: map_of_fstE)
qed
lemma ClassMain_is_no_class [dest!]: "is_class (PROG P) (ClassMain P) ==> False"
proof (erule rev_notE)
from ex_new_class_name [of "PROG P"] obtain C where "¬ is_class (PROG P) C"
by blast
thus "¬ is_class (PROG P) (ClassMain P)" unfolding ClassMain_def
by (rule someI)
qed
lemma MethodMain_not_seen [dest!]: "PROG P \<turnstile> C sees (MethodMain P):Ts->T = mb in D ==> False"
by (fastforce dest: MethodMain_unique_in_P)
lemma no_Call_from_ClassMain [dest!]: "PROG P \<turnstile> ClassMain P sees M:Ts->T = mb in C ==> False"
by (fastforce dest: sees_method_is_class)
lemma no_Call_in_ClassMain [dest!]: "PROG P \<turnstile> C sees M:Ts->T = mb in ClassMain P ==> False"
by (fastforce dest: sees_method_idemp)
inductive JVMCFG :: "jvm_method => cfg_node => (var, val, cname × mname × pc, cname × mname) edge_kind => cfg_node => bool" (" _ \<turnstile> _ -_-> _")
and reachable :: "jvm_method => cfg_node => bool" (" _ \<turnstile> =>_")
where
Entry_reachable: "(P, C0, Main) \<turnstile> =>(ClassMain P, MethodMain P, None, Enter)"
| reachable_step: "[| P \<turnstile> =>n; P \<turnstile> n -(e)-> n' |] ==> P \<turnstile> =>n'"
| Main_to_Call: "(P, C0, Main) \<turnstile> =>(ClassMain P, MethodMain P, ⌊0⌋, Enter)
==> (P, C0, Main) \<turnstile> (ClassMain P, MethodMain P, ⌊0⌋, Enter) -\<Up>id-> (ClassMain P, MethodMain P, ⌊0⌋, Normal)"
| Main_Call_LFalse: "(P, C0, Main) \<turnstile> =>(ClassMain P, MethodMain P, ⌊0⌋, Normal)
==> (P, C0, Main) \<turnstile> (ClassMain P, MethodMain P, ⌊0⌋, Normal) -(λs. False)⇣\<surd>-> (ClassMain P, MethodMain P, ⌊0⌋, Return)"
| Main_Call: "[| (P, C0, Main) \<turnstile> =>(ClassMain P, MethodMain P, ⌊0⌋, Normal);
PROG P \<turnstile> C0 sees Main:[]->T = (mxs, mxl⇣0, is, xt) in D;
initParams = [(λs. s Heap),(λs. ⌊Value Null⌋)];
ek = (λ(s, ret). True):(ClassMain P, MethodMain P, 0)\<hookrightarrow>⇘(D, Main)⇙initParams |]
==> (P, C0, Main) \<turnstile> (ClassMain P, MethodMain P, ⌊0⌋, Normal) -(ek)-> (D, Main, None, Enter)"
| Main_Return_to_Exit: "(P, C0, Main) \<turnstile> =>(ClassMain P, MethodMain P, ⌊0⌋, Return)
==> (P, C0, Main) \<turnstile> (ClassMain P, MethodMain P, ⌊0⌋, Return) -(\<Up>id)-> (ClassMain P, MethodMain P, None, Return)"
| Method_LFalse: "(P, C0, Main) \<turnstile> =>(C, M, None, Enter)
==> (P, C0, Main) \<turnstile> (C, M, None, Enter) -(λs. False)⇣\<surd>-> (C, M, None, Return)"
| Method_LTrue: "(P, C0, Main) \<turnstile> =>(C, M, None, Enter)
==> (P, C0, Main) \<turnstile> (C, M, None, Enter) -(λs. True)⇣\<surd>-> (C, M, ⌊0⌋, Enter)"
| CFG_Load: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = Load n;
ek = \<Up>(λs. s(Stack (stkLength (P, C, M) pc) := s (Local n))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊Suc pc⌋, Enter)"
| CFG_Store: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = Store n;
ek = \<Up>(λs. s(Local n := s (Stack (stkLength (P, C, M) pc - 1)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊Suc pc⌋, Enter)"
| CFG_Push: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = Push v;
ek = \<Up>(λs. s(Stack (stkLength (P, C, M) pc) \<mapsto> Value v)) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊Suc pc⌋, Enter)"
| CFG_Pop: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = Pop;
ek = \<Up>id |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊Suc pc⌋, Enter)"
| CFG_IAdd: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = IAdd;
ek = \<Up>(λs. let i1 = the_Intg (stkAt s (stkLength (P, C, M) pc - 1));
i2 = the_Intg (stkAt s (stkLength (P, C, M) pc - 2))
in s(Stack (stkLength (P, C, M) pc - 2) \<mapsto> Value (Intg (i1 + i2)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊Suc pc⌋, Enter)"
| CFG_Goto: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = Goto i |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -((λs. True)⇣\<surd>)-> (C, M, ⌊nat (int pc + i)⌋, Enter)"
| CFG_CmpEq: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter); instrs_of (PROG P) C M ! pc = CmpEq;
ek = \<Up>(λs. let e1 = stkAt s (stkLength (P, C, M) pc - 1);
e2 = stkAt s (stkLength (P, C, M) pc - 2)
in s(Stack (stkLength (P, C, M) pc - 2) \<mapsto> Value (Bool (e1 = e2)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊Suc pc⌋, Enter)"
| CFG_IfFalse_False: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = IfFalse i;
i ≠ 1;
ek = (λs. stkAt s (stkLength(P, C, M) pc - 1) = Bool False)⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊nat (int pc + i)⌋, Enter)"
| CFG_IfFalse_True: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = IfFalse i;
ek = (λs. stkAt s (stkLength(P, C, M) pc - 1) ≠ Bool False ∨ i = 1)⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊Suc pc⌋, Enter)"
| CFG_New_Check_Normal: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = New Cl;
ek = (λs. new_Addr (heap_of s) ≠ None)⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊pc⌋, Normal)"
| CFG_New_Check_Exceptional: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = New Cl;
pc' = (case (match_ex_table (PROG P) OutOfMemory pc (ex_table_of (PROG P) C M)) of
None => None
| Some (pc'', d) => ⌊pc''⌋);
ek = (λs. new_Addr (heap_of s) = None)⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊pc⌋, Exceptional pc' Enter)"
| CFG_New_Update: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Normal);
instrs_of (PROG P) C M ! pc = New Cl;
ek = \<Up>(λs. let a = the (new_Addr (heap_of s))
in s(Heap \<mapsto> Hp ((heap_of s)(a \<mapsto> blank (PROG P) Cl)))
(Stack (stkLength(P, C, M) pc) \<mapsto> Value (Addr a))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Normal) -(ek)-> (C, M, ⌊Suc pc⌋, Enter)"
| CFG_New_Exceptional_prop: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional None Enter);
instrs_of (PROG P) C M ! pc = New Cl;
ek = \<Up>(λs. s(Exception \<mapsto> Value (Addr (addr_of_sys_xcpt OutOfMemory)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Exceptional None Enter) -(ek)-> (C, M, None, Return)"
| CFG_New_Exceptional_handle: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter);
instrs_of (PROG P) C M ! pc = New Cl;
ek = \<Up>(λs. s(Exception := None)
(Stack (stkLength (P, C, M) pc' - 1) \<mapsto> Value (Addr (addr_of_sys_xcpt OutOfMemory)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) -(ek)-> (C, M, ⌊pc'⌋, Enter)"
| CFG_Getfield_Check_Normal: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = Getfield F Cl;
ek = (λs. stkAt s (stkLength (P, C, M) pc - 1) ≠ Null)⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊pc⌋, Normal)"
| CFG_Getfield_Check_Exceptional: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = Getfield F Cl;
pc' = (case (match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M)) of
None => None
| Some (pc'', d) => ⌊pc''⌋);
ek = (λs. stkAt s (stkLength (P, C, M) pc - 1) = Null)⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊pc⌋, Exceptional pc' Enter)"
| CFG_Getfield_Update: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Normal);
instrs_of (PROG P) C M ! pc = Getfield F Cl;
ek = \<Up>(λs. let (D, fs) = the (heap_of s (the_Addr (stkAt s (stkLength (P, C, M) pc - 1))))
in s(Stack (stkLength(P, C, M) pc - 1) \<mapsto> Value (the (fs (F, Cl))))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Normal) -(ek)-> (C, M, ⌊Suc pc⌋, Enter)"
| CFG_Getfield_Exceptional_prop: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional None Enter);
instrs_of (PROG P) C M ! pc = Getfield F Cl;
ek = \<Up>(λs. s(Exception \<mapsto> Value (Addr (addr_of_sys_xcpt NullPointer)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Exceptional None Enter) -(ek)-> (C, M, None, Return)"
| CFG_Getfield_Exceptional_handle: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter);
instrs_of (PROG P) C M ! pc = Getfield F Cl;
ek = \<Up>(λs. s(Exception := None)
(Stack (stkLength (P, C, M) pc' - 1) \<mapsto> Value (Addr (addr_of_sys_xcpt NullPointer)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) -(ek)-> (C, M, ⌊pc'⌋, Enter)"
| CFG_Putfield_Check_Normal: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = Putfield F Cl;
ek = (λs. stkAt s (stkLength (P, C, M) pc - 2) ≠ Null)⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊pc⌋, Normal)"
| CFG_Putfield_Check_Exceptional: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = Putfield F Cl;
pc' = (case (match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M)) of
None => None
| Some (pc'', d) => ⌊pc''⌋);
ek = (λs. stkAt s (stkLength (P, C, M) pc - 2) = Null)⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊pc⌋, Exceptional pc' Enter)"
| CFG_Putfield_Update: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Normal);
instrs_of (PROG P) C M ! pc = Putfield F Cl;
ek = \<Up>(λs. let v = stkAt s (stkLength (P, C, M) pc - 1);
r = stkAt s (stkLength (P, C, M) pc - 2);
a = the_Addr r;
(D, fs) = the (heap_of s a);
h' = (heap_of s)(a \<mapsto> (D, fs((F, Cl) \<mapsto> v)))
in s(Heap \<mapsto> Hp h')) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Normal) -(ek)-> (C, M, ⌊Suc pc⌋, Enter)"
| CFG_Putfield_Exceptional_prop: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional None Enter);
instrs_of (PROG P) C M ! pc = Putfield F Cl;
ek = \<Up>(λs. s(Exception \<mapsto> Value (Addr (addr_of_sys_xcpt NullPointer)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Exceptional None Enter) -(ek)-> (C, M, None, Return)"
| CFG_Putfield_Exceptional_handle: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter);
instrs_of (PROG P) C M ! pc = Putfield F Cl;
ek = \<Up>(λs. s(Exception := None)
(Stack (stkLength (P, C, M) pc' - 1) \<mapsto> Value (Addr (addr_of_sys_xcpt NullPointer)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) -(ek)-> (C, M, ⌊pc'⌋, Enter)"
| CFG_Checkcast_Check_Normal: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = Checkcast Cl;
ek = (λs. cast_ok (PROG P) Cl (heap_of s) (stkAt s (stkLength (P, C, M) pc - 1)))⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊Suc pc⌋, Enter)"
| CFG_Checkcast_Check_Exceptional: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = Checkcast Cl;
pc' = (case (match_ex_table (PROG P) ClassCast pc (ex_table_of (PROG P) C M)) of
None => None
| Some (pc'', d) => ⌊pc''⌋);
ek = (λs. ¬ cast_ok (PROG P) Cl (heap_of s) (stkAt s (stkLength (P, C, M) pc - 1)))⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊pc⌋, Exceptional pc' Enter)"
| CFG_Checkcast_Exceptional_prop: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional None Enter);
instrs_of (PROG P) C M ! pc = Checkcast Cl;
ek = \<Up>(λs. s(Exception \<mapsto> Value (Addr (addr_of_sys_xcpt ClassCast)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Exceptional None Enter) -(ek)-> (C, M, None, Return)"
| CFG_Checkcast_Exceptional_handle: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter);
instrs_of (PROG P) C M ! pc = Checkcast Cl;
ek = \<Up>(λs. s(Exception := None)
(Stack (stkLength (P, C, M) pc' - 1) \<mapsto> Value (Addr (addr_of_sys_xcpt ClassCast)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) -(ek)-> (C, M, ⌊pc'⌋, Enter)"
| CFG_Throw_Check: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = Throw;
pc' = None ∨ match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = ⌊(the pc', d)⌋;
ek = (λs. let v = stkAt s (stkLength (P, C, M) pc - 1);
Cl = if (v = Null) then NullPointer else (cname_of (heap_of s) (the_Addr v))
in case pc' of
None => match_ex_table (PROG P) Cl pc (ex_table_of (PROG P) C M) = None
| Some pc'' => ∃d. match_ex_table (PROG P) Cl pc (ex_table_of (PROG P) C M)
= ⌊(pc'', d)⌋
)⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊pc⌋, Exceptional pc' Enter)"
| CFG_Throw_prop: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional None Enter);
instrs_of (PROG P) C M ! pc = Throw;
ek = \<Up>(λs. s(Exception \<mapsto> Value (stkAt s (stkLength (P, C, M) pc - 1)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Exceptional None Enter) -(ek)-> (C, M, None, Return)"
| CFG_Throw_handle: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter);
pc' ≠ length (instrs_of (PROG P) C M);
instrs_of (PROG P) C M ! pc = Throw;
ek = \<Up>(λs. s(Exception := None)
(Stack (stkLength (P, C, M) pc' - 1) \<mapsto> Value (stkAt s (stkLength (P, C, M) pc - 1)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) -(ek)-> (C, M, ⌊pc'⌋, Enter)"
| CFG_Invoke_Check_NP_Normal: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = Invoke M' n;
ek = (λs. stkAt s (stkLength (P, C, M) pc - Suc n) ≠ Null)⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊pc⌋, Normal)"
| CFG_Invoke_Check_NP_Exceptional: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = Invoke M' n;
pc' = (case (match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M)) of
None => None
| Some (pc'', d) => ⌊pc''⌋);
ek = (λs. stkAt s (stkLength (P, C, M) pc - Suc n) = Null)⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, ⌊pc⌋, Exceptional pc' Enter)"
| CFG_Invoke_NP_prop: "[| C ≠ ClassMain P;
(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional None Enter);
instrs_of (PROG P) C M ! pc = Invoke M' n;
ek = \<Up>(λs. s(Exception \<mapsto> Value (Addr (addr_of_sys_xcpt NullPointer)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Exceptional None Enter) -(ek)-> (C, M, None, Return)"
| CFG_Invoke_NP_handle: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter);
instrs_of (PROG P) C M ! pc = Invoke M' n;
ek = \<Up>(λs. s(Exception := None)
(Stack (stkLength (P, C, M) pc' - 1) \<mapsto> Value (Addr (addr_of_sys_xcpt NullPointer)))) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) -(ek)-> (C, M, ⌊pc'⌋, Enter)"
| CFG_Invoke_Call: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Normal);
instrs_of (PROG P) C M ! pc = Invoke M' n;
TYPING P C M ! pc = ⌊(ST, LT)⌋;
ST ! n = Class D';
PROG P \<turnstile> D' sees M':Ts->T = (mxs, mxl⇣0, is, xt) in D;
Q = (λ(s, ret). let r = stkAt s (stkLength (P, C, M) pc - Suc n);
C' = fst (the (heap_of s (the_Addr r)))
in D = fst (method (PROG P) C' M'));
paramDefs = (λs. s Heap)
# (λs. s (Stack (stkLength (P, C, M) pc - Suc n)))
# (rev (map (λi. (λs. s (Stack (stkLength (P, C, M) pc - Suc i)))) [0..<n]));
ek = Q:(C, M, pc)\<hookrightarrow>⇘(D,M')⇙paramDefs
|]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Normal) -(ek)-> (D, M', None, Enter)"
| CFG_Invoke_False: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Normal);
instrs_of (PROG P) C M ! pc = Invoke M' n;
ek = (λs. False)⇣\<surd>
|]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Normal) -(ek)-> (C, M, ⌊pc⌋, Return)"
| CFG_Invoke_Return_Check_Normal: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Return);
instrs_of (PROG P) C M ! pc = Invoke M' n;
(TYPING P) C M ! pc = ⌊(ST, LT)⌋;
ST ! n ≠ NT;
ek = (λs. s Exception = None)⇣\<surd>
|]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Return) -(ek)-> (C, M, ⌊Suc pc⌋, Enter)"
| CFG_Invoke_Return_Check_Exceptional: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Return);
instrs_of (PROG P) C M ! pc = Invoke M' n;
match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = ⌊(pc', diff)⌋;
pc' ≠ length (instrs_of (PROG P) C M);
ek = (λs. ∃v d. s Exception = ⌊v⌋ ∧
match_ex_table (PROG P) (cname_of (heap_of s) (the_Addr (the_Value v))) pc (ex_table_of (PROG P) C M) = ⌊(pc', d)⌋)⇣\<surd>
|]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Return) -(ek)-> (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Return)"
| CFG_Invoke_Return_Exceptional_handle: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Return);
instrs_of (PROG P) C M ! pc = Invoke M' n;
ek = \<Up>(λs. s(Exception := None,
Stack (stkLength (P, C, M) pc' - 1) := s Exception)) |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Return) -(ek)-> (C, M, ⌊pc'⌋, Enter)"
| CFG_Invoke_Return_Exceptional_prop: "[| C ≠ ClassMain P;
(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Return);
instrs_of (PROG P) C M ! pc = Invoke M' n;
ek = (λs. ∃v. s Exception = ⌊v⌋ ∧
match_ex_table (PROG P) (cname_of (heap_of s) (the_Addr (the_Value v))) pc (ex_table_of (PROG P) C M) = None)⇣\<surd> |]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Return) -(ek)-> (C, M, None, Return)"
| CFG_Return: "[| C ≠ ClassMain P; (P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter);
instrs_of (PROG P) C M ! pc = instr.Return;
ek = \<Up>(λs. s(Stack 0 := s (Stack (stkLength (P, C, M) pc - 1))))
|]
==> (P, C0, Main) \<turnstile> (C, M, ⌊pc⌋, Enter) -(ek)-> (C, M, None, Return)"
| CFG_Return_from_Method: "[| (P, C0, Main) \<turnstile> =>(C, M, None, Return);
(P, C0, Main) \<turnstile> (C', M', ⌊pc'⌋, Normal) -(Q':(C', M', pc')\<hookrightarrow>⇘(C,M)⇙ps)-> (C, M, None, Enter);
Q = (λ(s, ret). ret = (C', M', pc'));
stateUpdate = (λs s'. s'(Heap := s Heap,
Exception := s Exception,
Stack (stkLength (P, C', M') (Suc pc') - 1) := s (Stack 0))
);
ek = Q\<hookleftarrow>⇘(C, M)⇙stateUpdate
|]
==> (P, C0, Main) \<turnstile> (C, M, None, Return) -(ek)-> (C', M', ⌊pc'⌋, Return)"
(* This takes veeeery long *)
lemma JVMCFG_edge_det: "[| P \<turnstile> n -(et)-> n'; P \<turnstile> n -(et')-> n' |] ==> et = et'"
by (erule JVMCFG.cases) (erule JVMCFG.cases, (fastforce dest: sees_method_fun)+)+
lemma sourcenode_reachable: "P \<turnstile> n -(ek)-> n' ==> P \<turnstile> =>n"
by (erule JVMCFG.cases, auto)
lemma targetnode_reachable:
assumes edge: "P \<turnstile> n -(ek)-> n'"
shows "P \<turnstile> =>n'"
proof -
from edge have "P \<turnstile> =>n"
by -(drule sourcenode_reachable)
with edge show ?thesis
by -(rule JVMCFG_reachable.intros)
qed
lemmas JVMCFG_reachable_inducts = JVMCFG_reachable.inducts[split_format (complete)]
lemma ClassMain_imp_MethodMain:
"(P, C0, Main) \<turnstile> (C', M', pc', nt') -ek-> (ClassMain P, M, pc, nt) ==> M = MethodMain P"
"(P, C0, Main) \<turnstile> =>(ClassMain P, M, pc, nt) ==> M = MethodMain P"
proof (induct P=="P" C0≡"C0" Main≡Main C' M' pc' nt' ek C''=="ClassMain P" M pc nt and
P=="P" C0≡"C0" Main≡Main C'=="ClassMain P" M pc nt
rule: JVMCFG_reachable_inducts)
case CFG_Return_from_Method
thus ?case
by (fastforce elim: JVMCFG.cases)
qed auto
lemma ClassMain_no_Call_target [dest!]:
"(P, C0, Main) \<turnstile> (C, M, pc, nt) -Q:(C', M', pc')\<hookrightarrow>⇘(D,M'')⇙paramDefs-> (ClassMain P, M''', pc'', nt')
==> False"
and
"(P, C0, Main) \<turnstile> =>(C, M, pc, nt) ==> True"
by (induct P C0 Main C M pc nt ek=="Q:(C', M', pc')\<hookrightarrow>⇘(D,M'')⇙paramDefs"
C''=="ClassMain P" M''' pc'' nt' and
P C0 Main C M pc nt
rule: JVMCFG_reachable_inducts) auto
lemma method_of_src_and_trg_exists:
"[| (P, C0, Main) \<turnstile> (C', M', pc', nt') -ek-> (C, M, pc, nt); C ≠ ClassMain P; C' ≠ ClassMain P |]
==> (∃Ts T mb. (PROG P) \<turnstile> C sees M:Ts->T = mb in C) ∧
(∃Ts T mb. (PROG P) \<turnstile> C' sees M':Ts->T = mb in C')"
and method_of_reachable_node_exists:
"[| (P, C0, Main) \<turnstile> =>(C, M, pc, nt); C ≠ ClassMain P |]
==> ∃Ts T mb. (PROG P) \<turnstile> C sees M:Ts->T = mb in C"
proof (induct rule: JVMCFG_reachable_inducts)
case CFG_Invoke_Call
thus ?case
by (blast dest: sees_method_idemp)
next
case (reachable_step P C0 Main C M pc nt ek C' M' pc' nt')
show ?case
proof (cases "C = ClassMain P")
case True
with `(P, C0, Main) \<turnstile> (C, M, pc, nt) -ek-> (C', M', pc', nt')` `C' ≠ ClassMain P`
show ?thesis
proof cases
case Main_Call
thus ?thesis
by (blast dest: sees_method_idemp)
qed auto
next
case False
with reachable_step show ?thesis
by simp
qed
qed simp_all
lemma "[| (P, C0, Main) \<turnstile> (C', M', pc', nt') -ek-> (C, M, pc, nt); C ≠ ClassMain P; C' ≠ ClassMain P |]
==> (case pc of None => True |
⌊pc''⌋ => (TYPING P) C M ! pc'' ≠ None ∧ pc'' < length (instrs_of (PROG P) C M)) ∧
(case pc' of None => True |
⌊pc''⌋ => (TYPING P) C' M' ! pc'' ≠ None ∧ pc'' < length (instrs_of (PROG P) C' M'))"
and instr_of_reachable_node_typable: "[| (P, C0, Main) \<turnstile> =>(C, M, pc, nt); C ≠ ClassMain P |]
==> case pc of None => True |
⌊pc''⌋ => (TYPING P) C M ! pc'' ≠ None ∧ pc'' < length (instrs_of (PROG P) C M)"
proof (induct rule: JVMCFG_reachable_inducts)
case (CFG_Load C P C0 Main M pc n ek)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_Load show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (CFG_Store C P C0 Main M pc n ek)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_Store show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (CFG_Push C P C0 Main M pc v ek)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_Push show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (CFG_Pop C P C0 Main M pc ek)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_Pop show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (CFG_IAdd C P C0 Main M pc ek)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_IAdd show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (CFG_Goto C P C0 Main M pc i)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_Goto show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (CFG_CmpEq C P C0 Main M pc ek)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_CmpEq show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (CFG_IfFalse_False C P C0 Main M pc i ek)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_IfFalse_False show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (CFG_IfFalse_True C P C0 Main M pc i ek)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_IfFalse_True show ?case
using [[simproc del: list_to_set_comprehension]] by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (CFG_New_Update C P C0 Main M pc Cl ek)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Normal)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_New_Update show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (CFG_New_Exceptional_handle C P C0 Main M pc pc' Cl ek)
hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
by simp_all
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 where
"PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
by (fastforce dest: method_of_reachable_node_exists)
with `pc < length (instrs_of (PROG P) C M)` `instrs_of (PROG P) C M ! pc = New Cl`
have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
\<turnstile> New Cl,pc :: TYPING P C M"
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)` `C ≠ ClassMain P`
`instrs_of (PROG P) C M ! pc = New Cl` obtain d'
where "match_ex_table (PROG P) OutOfMemory pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
by cases (fastforce elim: JVMCFG.cases)
hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
matches_ex_entry (PROG P) OutOfMemory pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
by -(drule match_ex_table_SomeD)
ultimately show ?case using `instrs_of (PROG P) C M ! pc = New Cl`
by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
case (CFG_Getfield_Update C P C0 Main M pc F Cl ek)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Normal)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_Getfield_Update show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (CFG_Getfield_Exceptional_handle C P C0 Main M pc pc' F Cl ek)
hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
by simp_all
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 where
"PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
by (fastforce dest: method_of_reachable_node_exists)
with `pc < length (instrs_of (PROG P) C M)` `instrs_of (PROG P) C M ! pc = Getfield F Cl`
have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
\<turnstile> Getfield F Cl,pc :: TYPING P C M"
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)` `C ≠ ClassMain P`
`instrs_of (PROG P) C M ! pc = Getfield F Cl` obtain d'
where "match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
by cases (fastforce elim: JVMCFG.cases)
hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
matches_ex_entry (PROG P) NullPointer pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
by -(drule match_ex_table_SomeD)
ultimately show ?case using `instrs_of (PROG P) C M ! pc = Getfield F Cl`
by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
case (CFG_Putfield_Update C P C0 Main M pc F Cl ek)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Normal)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_Putfield_Update show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (CFG_Putfield_Exceptional_handle C P C0 Main M pc pc' F Cl ek)
hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
by simp_all
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 where
"PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
by (fastforce dest: method_of_reachable_node_exists)
with `pc < length (instrs_of (PROG P) C M)` `instrs_of (PROG P) C M ! pc = Putfield F Cl`
have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
\<turnstile> Putfield F Cl,pc :: TYPING P C M"
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)` `C ≠ ClassMain P`
`instrs_of (PROG P) C M ! pc = Putfield F Cl` obtain d'
where "match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
by cases (fastforce elim: JVMCFG.cases)
hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
matches_ex_entry (PROG P) NullPointer pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
by -(drule match_ex_table_SomeD)
ultimately show ?case using `instrs_of (PROG P) C M ! pc = Putfield F Cl`
by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
case (CFG_Checkcast_Check_Normal C P C0 Main M pc Cl ek)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_Checkcast_Check_Normal show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (CFG_Checkcast_Exceptional_handle C P C0 Main M pc pc' Cl ek)
hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
by simp_all
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 where
"PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
by (fastforce dest: method_of_reachable_node_exists)
with `pc < length (instrs_of (PROG P) C M)` `instrs_of (PROG P) C M ! pc = Checkcast Cl`
have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
\<turnstile> Checkcast Cl,pc :: TYPING P C M"
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)` `C ≠ ClassMain P`
`instrs_of (PROG P) C M ! pc = Checkcast Cl` obtain d'
where "match_ex_table (PROG P) ClassCast pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
by cases (fastforce elim: JVMCFG.cases)
hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
matches_ex_entry (PROG P) ClassCast pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
by -(drule match_ex_table_SomeD)
ultimately show ?case using `instrs_of (PROG P) C M ! pc = Checkcast Cl`
by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
case (CFG_Throw_handle C P C0 Main M pc pc' ek)
hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
by simp_all
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 where
"PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
by (fastforce dest: method_of_reachable_node_exists)
with `pc < length (instrs_of (PROG P) C M)` `instrs_of (PROG P) C M ! pc = Throw`
have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
\<turnstile> Throw,pc :: TYPING P C M"
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)` `C ≠ ClassMain P`
`instrs_of (PROG P) C M ! pc = Throw` obtain d' Exc
where "match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
by cases (fastforce elim: JVMCFG.cases)
hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
matches_ex_entry (PROG P) Exc pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
by -(drule match_ex_table_SomeD)
ultimately show ?case using `instrs_of (PROG P) C M ! pc = Throw`
by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
case (CFG_Invoke_NP_handle C P C0 Main M pc pc' M' n ek)
hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
by simp_all
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 where
"PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
by (fastforce dest: method_of_reachable_node_exists)
with `pc < length (instrs_of (PROG P) C M)` `instrs_of (PROG P) C M ! pc = Invoke M' n`
have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
\<turnstile> Invoke M' n,pc :: TYPING P C M"
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)` `C ≠ ClassMain P`
`instrs_of (PROG P) C M ! pc = Invoke M' n` obtain d'
where "match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
by cases (fastforce elim: JVMCFG.cases)
hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
matches_ex_entry (PROG P) NullPointer pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
by -(drule match_ex_table_SomeD)
ultimately show ?case using `instrs_of (PROG P) C M ! pc = Invoke M' n`
by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
case (CFG_Invoke_Return_Exceptional_handle C P C0 Main M pc pc' M' n ek)
hence "TYPING P C M ! pc ≠ None" and "pc < length (instrs_of (PROG P) C M)"
by simp_all
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Return)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 where
"PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, instrs_of (PROG P) C M, ex_table_of (PROG P) C M) in C"
by (fastforce dest: method_of_reachable_node_exists)
with `pc < length (instrs_of (PROG P) C M)` `instrs_of (PROG P) C M ! pc = Invoke M' n`
have "PROG P,T,mxs,length (instrs_of (PROG P) C M),ex_table_of (PROG P) C M
\<turnstile> Invoke M' n,pc :: TYPING P C M"
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
moreover from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Return)` `C ≠ ClassMain P`
`instrs_of (PROG P) C M ! pc = Invoke M' n` obtain d' Exc
where "match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = ⌊(pc', d')⌋"
by cases (fastforce elim: JVMCFG.cases)
hence "∃(f, t, D, h, d)∈set (ex_table_of (PROG P) C M).
matches_ex_entry (PROG P) Exc pc (f, t, D, h, d) ∧ h = pc' ∧ d = d'"
by -(drule match_ex_table_SomeD)
ultimately show ?case using `instrs_of (PROG P) C M ! pc = Invoke M' n`
by (fastforce simp: relevant_entries_def is_relevant_entry_def matches_ex_entry_def)
next
case (CFG_Invoke_Return_Check_Normal C P C0 Main M pc M' n ST LT ek)
from `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, Return)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with CFG_Invoke_Return_Check_Normal show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_instr [OF wf_jvmprog_is_wf_typ])
next
case (Method_LTrue P C0 Main C M)
from `(P, C0, Main) \<turnstile> =>(C, M, None, Enter)` `C ≠ ClassMain P`
obtain Ts T mxs mxl⇣0 "is" xt where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "instrs_of (PROG P) C M = is"
by -(drule method_of_reachable_node_exists, auto)
with Method_LTrue show ?case
by (fastforce dest!: wt_jvm_prog_impl_wt_start [OF wf_jvmprog_is_wf_typ] simp: wt_start_def)
next
case (reachable_step P C0 Main C M opc nt ek C' M' opc' nt')
thus ?case
by (cases "C = ClassMain P") (fastforce elim: JVMCFG.cases, simp)
qed simp_all
lemma reachable_node_impl_wt_instr:
assumes "(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, nt)"
and "C ≠ ClassMain P"
shows "∃T mxs mpc xt. PROG P,T,mxs,mpc,xt \<turnstile> (instrs_of (PROG P) C M ! pc),pc :: TYPING P C M"
proof -
from `C ≠ ClassMain P` `(P, C0, Main) \<turnstile> =>(C, M, ⌊pc⌋, nt)`
method_of_reachable_node_exists [of P C0 Main C M "⌊pc⌋" nt]
instr_of_reachable_node_typable [of P C0 Main C M "⌊pc⌋" nt]
obtain Ts T mxs mxl⇣0 "is" xt
where "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
and "TYPING P C M ! pc ≠ None"
and "pc < length (instrs_of (PROG P) C M)"
by fastforce+
with wf_jvmprog_is_wf_typ [of P]
have "PROG P,T,mxs,length is,xt \<turnstile> instrs_of (PROG P) C M ! pc,pc :: TYPING P C M"
by (fastforce dest!: wt_jvm_prog_impl_wt_instr)
thus ?thesis
by blast
qed
lemma
"[| (P, C0, Main) \<turnstile> (C, M, pc, nt) -ek-> (C', M', pc', nt'); C ≠ ClassMain P ∨ C' ≠ ClassMain P |]
==> ∃T mb D. PROG P \<turnstile> C0 sees Main:[]->T = mb in D"
and reachable_node_impl_Main_ex:
"[| (P, C0, Main) \<turnstile> =>(C, M, pc, nt); C ≠ ClassMain P|]
==> ∃T mb D. PROG P \<turnstile> C0 sees Main:[]->T = mb in D"
by (induct rule: JVMCFG_reachable_inducts) fastforce+
end