Theory JVMPostdomination
theory JVMPostdomination imports JVMInterpretation "../StaticInter/Postdomination" begin
context CFG begin
lemma vp_snocI:
"⟦n -as→⇩√* n'; n' -[a]→* n''; ∀Q p ret fs. kind a ≠ Q↩⇘p⇙ret ⟧ ⟹ n -as @ [a]→⇩√* n''"
by (cases "kind a") (auto intro: path_Append valid_path_aux_Append simp: vp_def valid_path_def)
lemma valid_node_cases' [case_names Source Target, consumes 1]:
"⟦ valid_node n; ⋀e. ⟦ valid_edge e; sourcenode e = n ⟧ ⟹ thesis;
⋀e. ⟦ valid_edge e; targetnode e = n ⟧ ⟹ thesis ⟧
⟹ thesis"
by (auto simp: valid_node_def)
end
lemma disjE_strong: "⟦P ∨ Q; P ⟹ R; ⟦Q; ¬ P⟧ ⟹ R⟧ ⟹ R"
by auto
lemmas path_intros [intro] = JVMCFG_Interpret.path.Cons_path JVMCFG_Interpret.path.empty_path
declare JVMCFG_Interpret.vp_snocI [intro]
declare JVMCFG_Interpret.valid_node_def [simp add]
valid_edge_def [simp add]
JVMCFG_Interpret.intra_path_def [simp add]
abbreviation vp_snoc :: "wf_jvmprog ⇒ cname ⇒ mname ⇒ cfg_edge list ⇒ cfg_node
⇒ (var, val, cname × mname × pc, cname × mname) edge_kind ⇒ cfg_node ⇒ bool"
where "vp_snoc P C0 Main as n ek n'
≡ JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) (as @ [(n,ek,n')]) n'"
lemma
"(P, C0, Main) ⊢ (C, M, pc, nt) -ek→ (C', M', pc', nt')
⟹ (∃as. CFG.valid_path' sourcenode targetnode kind (valid_edge (P, C0, Main))
(get_return_edges P) (ClassMain P, MethodMain P, None, Enter) as (C, M, pc, nt)) ∧
(∃as. CFG.valid_path' sourcenode targetnode kind (valid_edge (P, C0, Main))
(get_return_edges P) (ClassMain P, MethodMain P, None, Enter) as (C', M', pc', nt'))"
and valid_Entry_path: "(P, C0, Main) ⊢ ⇒(C, M, pc, nt)
⟹ ∃as. CFG.valid_path' sourcenode targetnode kind (valid_edge (P, C0, Main))
(get_return_edges P) (ClassMain P, MethodMain P, None, Enter) as (C, M, pc, nt)"
proof (induct rule: JVMCFG_reachable_inducts)
case (Entry_reachable P C0 Main)
hence "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) [] (ClassMain P, MethodMain P, None, Enter)"
by (fastforce intro: JVMCFG_Interpret.intra_path_vp Method_LTrue
JVMCFG_reachable.Entry_reachable)
thus ?case by blast
next
case (reachable_step P C0 Main C M pc nt ek C' M' pc' nt')
thus ?case by simp
next
case (Main_to_Call P C0 Main)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (ClassMain P, MethodMain P, ⌊0⌋, Enter)"
by blast
moreover with ‹(P, C0, Main) ⊢ ⇒(ClassMain P, MethodMain P, ⌊0⌋, Enter)›
have "vp_snoc P C0 Main as (ClassMain P, MethodMain P, ⌊0⌋, Enter) ⇑id
(ClassMain P, MethodMain P, ⌊0⌋, Normal)"
by (fastforce intro: JVMCFG_reachable.Main_to_Call)
ultimately show ?case by blast
next
case (Main_Call_LFalse P C0 Main)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (ClassMain P, MethodMain P, ⌊0⌋, Normal)"
by blast
moreover with ‹(P, C0, Main) ⊢ ⇒(ClassMain P, MethodMain P, ⌊0⌋, Normal)›
have "vp_snoc P C0 Main as (ClassMain P, MethodMain P, ⌊0⌋, Normal) (λs. False)⇩√
(ClassMain P, MethodMain P, ⌊0⌋, Return)"
by (fastforce intro: JVMCFG_reachable.Main_Call_LFalse)
ultimately show ?case by blast
next
case (Main_Call P C0 Main T mxs mxl⇩0 "is" xt D initParams ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (ClassMain P, MethodMain P, ⌊0⌋, Normal)"
by blast
moreover with ‹(P, C0, Main) ⊢ ⇒(ClassMain P, MethodMain P, ⌊0⌋, Normal)›
‹PROG P ⊢ 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)↪⇘(D, Main)⇙initParams›
have "vp_snoc P C0 Main as (ClassMain P, MethodMain P, ⌊0⌋, Normal)
((λ(s, ret). True):(ClassMain P, MethodMain P, 0)↪⇘(D, Main)⇙[(λs. s Heap),(λs. ⌊Value Null⌋)])
(D, Main, None, Enter)"
by (fastforce intro: JVMCFG_reachable.Main_Call)
ultimately show ?case by blast
next
case (Main_Return_to_Exit P C0 Main)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (ClassMain P, MethodMain P, ⌊0⌋, nodeType.Return)"
by blast
moreover with ‹(P, C0, Main) ⊢ ⇒(ClassMain P, MethodMain P, ⌊0⌋, nodeType.Return)›
have "vp_snoc P C0 Main as (ClassMain P, MethodMain P, ⌊0⌋, nodeType.Return) ⇑id
(ClassMain P, MethodMain P, None, nodeType.Return)"
by (fastforce intro: JVMCFG_reachable.Main_Return_to_Exit)
ultimately show ?case by blast
next
case (Method_LFalse P C0 Main C M)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, None, Enter)"
by blast
moreover with ‹(P, C0, Main) ⊢ ⇒(C, M, None, Enter)›
have "vp_snoc P C0 Main as (C, M, None, Enter) (λs. False)⇩√ (C, M, None, Return)"
by (fastforce intro: JVMCFG_reachable.Method_LFalse)
ultimately show ?case by blast
next
case (Method_LTrue P C0 Main C M)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, None, Enter)"
by blast
moreover with ‹(P, C0, Main) ⊢ ⇒(C, M, None, Enter)›
have "vp_snoc P C0 Main as (C, M, None, Enter) (λs. True)⇩√ (C, M, ⌊0⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.Method_LTrue)
ultimately show ?case by blast
next
case (CFG_Load C P C0 Main M pc n ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)›
‹instrs_of (PROG P) C M ! pc = Load n›
‹ek = ⇑λs. s(Stack (stkLength (P, C, M) pc) := s (Local n))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊Suc pc⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Load)
ultimately show ?case by blast
next
case (CFG_Store C P C0 Main M pc n ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)›
‹instrs_of (PROG P) C M ! pc = Store n›
‹ek = ⇑λs. s(Local n := s (Stack (stkLength (P, C, M) pc - 1)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊Suc pc⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Store)
ultimately show ?case by blast
next
case (CFG_Push C P C0 Main M pc v ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)›
‹instrs_of (PROG P) C M ! pc = Push v›
‹ek = ⇑λs. s(Stack (stkLength (P, C, M) pc) ↦ Value v)›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊Suc pc⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Push)
ultimately show ?case by blast
next
case (CFG_Pop C P C0 Main M pc ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)›
‹instrs_of (PROG P) C M ! pc = Pop› ‹ek = ⇑id›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊Suc pc⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Pop)
ultimately show ?case by blast
next
case (CFG_IAdd C P C0 Main M pc ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)›
‹instrs_of (PROG P) C M ! pc = IAdd›
‹ek = ⇑λ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) ↦ Value (Intg (i1 + i2)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊Suc pc⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_IAdd)
ultimately show ?case by blast
next
case (CFG_Goto C P C0 Main M pc i)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)›
‹instrs_of (PROG P) C M ! pc = Goto i›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) (λs. True)⇩√ (C, M, ⌊nat (int pc + i)⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Goto)
ultimately show ?case by blast
next
case (CFG_CmpEq C P C0 Main M pc ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)›
‹instrs_of (PROG P) C M ! pc = CmpEq›
‹ek = ⇑λ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) ↦ Value (Bool (e1 = e2)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊Suc pc⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_CmpEq)
ultimately show ?case by blast
next
case (CFG_IfFalse_False C P C0 Main M pc i ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(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)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊nat (int pc + i)⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_IfFalse_False)
ultimately show ?case by blast
next
case (CFG_IfFalse_True C P C0 Main M pc i ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(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)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊Suc pc⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_IfFalse_True)
ultimately show ?case by blast
next
case (CFG_New_Check_Normal C P C0 Main M pc Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)›
‹instrs_of (PROG P) C M ! pc = New Cl› ‹ek = (λs. new_Addr (heap_of s) ≠ None)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊pc⌋, Normal)"
by (fastforce intro: JVMCFG_reachable.CFG_New_Check_Normal)
ultimately show ?case by blast
next
case (CFG_New_Check_Exceptional C P C0 Main M pc Cl pc' ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(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
| ⌊(pc'', d)⌋ ⇒ ⌊pc''⌋)› ‹ek = (λs. new_Addr (heap_of s) = None)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊pc⌋, Exceptional pc' Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_New_Check_Exceptional)
ultimately show ?case by blast
next
case (CFG_New_Update C P C0 Main M pc Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Normal)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Normal)›
‹ instrs_of (PROG P) C M ! pc = New Cl›
‹ ek = ⇑λs. let a = the (new_Addr (heap_of s)) in
s(Heap ↦ Hp ((heap_of s)(a ↦ blank (PROG P) Cl)),
Stack (stkLength (P, C, M) pc) ↦ Value (Addr a))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Normal) ek (C, M, ⌊Suc pc⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_New_Update)
ultimately show ?case by blast
next
case (CFG_New_Exceptional_prop C P C0 Main M pc Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Exceptional None Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional None Enter)›
‹instrs_of (PROG P) C M ! pc = New Cl›
‹ek = ⇑λs. s(Exception ↦ Value (Addr (addr_of_sys_xcpt OutOfMemory)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Exceptional None Enter) ek (C, M, None, Return)"
by (fastforce intro: JVMCFG_reachable.CFG_New_Exceptional_prop)
ultimately show ?case by blast
next
case (CFG_New_Exceptional_handle C P C0 Main M pc pc' Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)›
‹instrs_of (PROG P) C M ! pc = New Cl›
‹ek = ⇑λs. (s(Exception := None))(Stack (stkLength (P, C, M) pc' - 1) ↦
Value (Addr (addr_of_sys_xcpt OutOfMemory)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) ek (C, M, ⌊pc'⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_New_Exceptional_handle)
ultimately show ?case by blast
next
case (CFG_Getfield_Check_Normal C P C0 Main M pc F Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(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)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊pc⌋, Normal)"
by (fastforce intro: JVMCFG_reachable.CFG_Getfield_Check_Normal)
ultimately show ?case by blast
next
case (CFG_Getfield_Check_Exceptional C P C0 Main M pc F Cl pc' ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(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
| ⌊(pc'', d)⌋ ⇒ ⌊pc''⌋)› ‹ek = (λs. stkAt s (stkLength (P, C, M) pc - 1) = Null)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊pc⌋, Exceptional pc' Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Getfield_Check_Exceptional)
ultimately show ?case by blast
next
case (CFG_Getfield_Update C P C0 Main M pc F Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Normal)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Normal)›
‹instrs_of (PROG P) C M ! pc = Getfield F Cl›
‹ek = ⇑λ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) ↦ Value (the (fs (F, Cl))))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Normal) ek (C, M, ⌊Suc pc⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Getfield_Update)
ultimately show ?case by blast
next
case (CFG_Getfield_Exceptional_prop C P C0 Main M pc F Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Exceptional None Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional None Enter)›
‹instrs_of (PROG P) C M ! pc = Getfield F Cl›
‹ek = ⇑λs. s(Exception ↦ Value (Addr (addr_of_sys_xcpt NullPointer)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Exceptional None Enter) ek (C, M, None, Return)"
by (fastforce intro: JVMCFG_reachable.CFG_Getfield_Exceptional_prop)
ultimately show ?case by blast
next
case (CFG_Getfield_Exceptional_handle C P C0 Main M pc pc' F Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)›
‹instrs_of (PROG P) C M ! pc = Getfield F Cl›
‹ek = ⇑λs. (s(Exception := None))(Stack (stkLength (P, C, M) pc' - 1) ↦
Value (Addr (addr_of_sys_xcpt NullPointer)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) ek (C, M, ⌊pc'⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Getfield_Exceptional_handle)
ultimately show ?case by blast
next
case (CFG_Putfield_Check_Normal C P C0 Main M pc F Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(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)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊pc⌋, Normal)"
by (fastforce intro: JVMCFG_reachable.CFG_Putfield_Check_Normal)
ultimately show ?case by blast
next
case (CFG_Putfield_Check_Exceptional C P C0 Main M pc F Cl pc' ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(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
| ⌊(pc'', d)⌋ ⇒ ⌊pc''⌋)› ‹ek = (λs. stkAt s (stkLength (P, C, M) pc - 2) = Null)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊pc⌋, Exceptional pc' Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Putfield_Check_Exceptional)
ultimately show ?case by blast
next
case (CFG_Putfield_Update C P C0 Main M pc F Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Normal)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Normal)›
‹instrs_of (PROG P) C M ! pc = Putfield F Cl›
‹ek = ⇑λ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 ↦ (D, fs((F, Cl) ↦ v)))
in s(Heap ↦ Hp h')›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Normal) ek (C, M, ⌊Suc pc⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Putfield_Update)
ultimately show ?case by blast
next
case (CFG_Putfield_Exceptional_prop C P C0 Main M pc F Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Exceptional None Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional None Enter)›
‹instrs_of (PROG P) C M ! pc = Putfield F Cl›
‹ek = ⇑λs. s(Exception ↦ Value (Addr (addr_of_sys_xcpt NullPointer)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Exceptional None Enter) ek (C, M, None, Return)"
by (fastforce intro: JVMCFG_reachable.CFG_Putfield_Exceptional_prop)
ultimately show ?case by blast
next
case (CFG_Putfield_Exceptional_handle C P C0 Main M pc pc' F Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)›
‹instrs_of (PROG P) C M ! pc = Putfield F Cl›
‹ek = ⇑λs. (s(Exception := None))(Stack (stkLength (P, C, M) pc' - 1) ↦
Value (Addr (addr_of_sys_xcpt NullPointer)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) ek (C, M, ⌊pc'⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Putfield_Exceptional_handle)
ultimately show ?case by blast
next
case (CFG_Checkcast_Check_Normal C P C0 Main M pc Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(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)))⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊Suc pc⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Checkcast_Check_Normal)
ultimately show ?case by blast
next
case (CFG_Checkcast_Check_Exceptional C P C0 Main M pc Cl pc' ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(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
| ⌊(pc'', d)⌋ ⇒ ⌊pc''⌋)›
‹ek = (λs. ¬ cast_ok (PROG P) Cl (heap_of s) (stkAt s (stkLength (P, C, M) pc - 1)))⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊pc⌋, Exceptional pc' Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Checkcast_Check_Exceptional)
ultimately show ?case by blast
next
case (CFG_Checkcast_Exceptional_prop C P C0 Main M pc Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Exceptional None Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional None Enter)›
‹instrs_of (PROG P) C M ! pc = Checkcast Cl›
‹ek = ⇑λs. s(Exception ↦ Value (Addr (addr_of_sys_xcpt ClassCast)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Exceptional None Enter) ek (C, M, None, Return)"
by (fastforce intro: JVMCFG_reachable.CFG_Checkcast_Exceptional_prop)
ultimately show ?case by blast
next
case (CFG_Checkcast_Exceptional_handle C P C0 Main M pc pc' Cl ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)›
‹instrs_of (PROG P) C M ! pc = Checkcast Cl›
‹ek = ⇑λs. (s(Exception := None))(Stack (stkLength (P, C, M) pc' - 1) ↦
Value (Addr (addr_of_sys_xcpt ClassCast)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) ek (C, M, ⌊pc'⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Checkcast_Exceptional_handle)
ultimately show ?case by blast
next
case (CFG_Throw_Check C P C0 Main M pc pc' Exc d ek)
then obtain as where path_src: "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
from ‹pc' = None ∨ match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = ⌊(the pc', d)⌋›
show ?case
proof (elim disjE_strong)
assume "pc' = None"
with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)›
‹instrs_of (PROG P) C M ! pc = Throw›
‹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
| ⌊pc''⌋ ⇒
∃d. match_ex_table (PROG P) Cl pc (ex_table_of (PROG P) C M) = ⌊(pc'', d)⌋)⇩√›
have "(P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -
(λs. (stkAt s (stkLength (P, C, M) pc - Suc 0) = Null ⟶
match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M) = None) ∧
(stkAt s (stkLength (P, C, M) pc - Suc 0) ≠ Null ⟶
match_ex_table (PROG P) (cname_of (heap_of s)
(the_Addr (stkAt s (stkLength (P, C, M) pc - Suc 0)))) pc (ex_table_of (PROG P) C M) =
None))⇩√→ (C, M, ⌊pc⌋, Exceptional None Enter)"
by -(erule JVMCFG_reachable.CFG_Throw_Check, simp_all)
with path_src ‹pc' = None› ‹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
| ⌊pc''⌋ ⇒
∃d. match_ex_table (PROG P) Cl pc (ex_table_of (PROG P) C M) = ⌊(pc'', d)⌋)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊pc⌋, Exceptional None Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Throw_Check)
with path_src ‹pc' = None› show ?thesis by blast
next
assume met: "match_ex_table (PROG P) Exc pc (ex_table_of (PROG P) C M) = ⌊(the pc', d)⌋"
and pc': "pc' ≠ None"
with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)›
‹instrs_of (PROG P) C M ! pc = Throw›
‹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
| ⌊pc''⌋ ⇒
∃d. match_ex_table (PROG P) Cl pc (ex_table_of (PROG P) C M) = ⌊(pc'', d)⌋)⇩√›
have "(P, C0, Main) ⊢ (C, M, ⌊pc⌋, Enter) -
(λs. (stkAt s (stkLength (P, C, M) pc - Suc 0) = Null ⟶
(∃d. match_ex_table (PROG P) NullPointer pc
(ex_table_of (PROG P) C M) =
⌊(the pc', d)⌋)) ∧
(stkAt s (stkLength (P, C, M) pc - Suc 0) ≠ Null ⟶
(∃d. match_ex_table (PROG P)
(cname_of (heap_of s)
(the_Addr
(stkAt s (stkLength (P, C, M) pc - Suc 0))))
pc (ex_table_of (PROG P) C M) =
⌊(the pc', d)⌋)))⇩√→
(C, M, ⌊pc⌋, Exceptional ⌊the pc'⌋ Enter)"
by -(rule JVMCFG_reachable.CFG_Throw_Check, simp_all)
with met pc' path_src ‹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
| ⌊pc''⌋ ⇒
∃d. match_ex_table (PROG P) Cl pc (ex_table_of (PROG P) C M) = ⌊(pc'', d)⌋)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊pc⌋, Exceptional pc' Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Throw_Check)
with path_src show ?thesis by blast
qed
next
case (CFG_Throw_prop C P C0 Main M pc ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Exceptional None Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional None Enter)›
‹instrs_of (PROG P) C M ! pc = Throw›
‹ek = ⇑λs. s(Exception ↦ Value (stkAt s (stkLength (P, C, M) pc - 1)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Exceptional None Enter) ek (C, M, None, nodeType.Return)"
by (fastforce intro: JVMCFG_reachable.CFG_Throw_prop)
ultimately show ?case by blast
next
case (CFG_Throw_handle C P C0 Main M pc pc' ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)›
‹pc' ≠ length (instrs_of (PROG P) C M)› ‹instrs_of (PROG P) C M ! pc = Throw›
‹ek = ⇑λs. (s(Exception := None))(Stack (stkLength (P, C, M) pc' - 1) ↦
Value (stkAt s (stkLength (P, C, M) pc - 1)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) ek (C, M, ⌊pc'⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Throw_handle)
ultimately show ?case by blast
next
case (CFG_Invoke_Check_NP_Normal C P C0 Main M pc M' n ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(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)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊pc⌋, Normal)"
by (fastforce intro: JVMCFG_reachable.CFG_Invoke_Check_NP_Normal)
ultimately show ?case by blast
next
case (CFG_Invoke_Check_NP_Exceptional C P C0 Main M pc M' n pc' ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(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
| ⌊(pc'', d)⌋ ⇒ ⌊pc''⌋)›
‹ek = (λs. stkAt s (stkLength (P, C, M) pc - Suc n) = Null)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, ⌊pc⌋, Exceptional pc' Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Invoke_Check_NP_Exceptional)
ultimately show ?case by blast
next
case (CFG_Invoke_NP_prop C P C0 Main M pc M' n ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Exceptional None Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional None Enter)›
‹instrs_of (PROG P) C M ! pc = Invoke M' n›
‹ek = ⇑λs. s(Exception ↦ Value (Addr (addr_of_sys_xcpt NullPointer)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Exceptional None Enter) ek (C, M, None, Return)"
by (fastforce intro: JVMCFG_reachable.CFG_Invoke_NP_prop)
ultimately show ?case by blast
next
case (CFG_Invoke_NP_handle C P C0 Main M pc pc' M' n ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)›
‹instrs_of (PROG P) C M ! pc = Invoke M' n›
‹ek = ⇑λs. (s(Exception := None))(Stack (stkLength (P, C, M) pc' - 1) ↦
Value (Addr (addr_of_sys_xcpt NullPointer)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter) ek (C, M, ⌊pc'⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Invoke_NP_handle)
ultimately show ?case by blast
next
case (CFG_Invoke_Call C P C0 Main M pc M' n ST LT D' Ts T mxs mxl⇩0 "is" xt D Q paramDefs ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Normal)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(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 ⊢ 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' = cname_of (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)↪⇘(D, M')⇙paramDefs›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Normal) ek (D, M', None, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Invoke_Call)
ultimately show ?case by blast
next
case (CFG_Invoke_False C P C0 Main M pc M' n ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Normal)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Normal)›
‹instrs_of (PROG P) C M ! pc = Invoke M' n› ‹ek = (λs. False)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Normal) ek (C, M, ⌊pc⌋, Return)"
by (fastforce intro: JVMCFG_reachable.CFG_Invoke_False)
ultimately show ?case by blast
next
case (CFG_Invoke_Return_Check_Normal C P C0 Main M pc M' n ST LT ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, nodeType.Return)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, nodeType.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)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Return) ek (C, M, ⌊Suc pc⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Invoke_Return_Check_Normal)
ultimately show ?case by blast
next
case (CFG_Invoke_Return_Check_Exceptional C P C0 Main M pc M' n Exc pc' diff ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, nodeType.Return)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, nodeType.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)⌋)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Return) ek (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Return)"
by (fastforce intro: JVMCFG_reachable.CFG_Invoke_Return_Check_Exceptional)
ultimately show ?case by blast
next
case (CFG_Invoke_Return_Exceptional_handle C P C0 Main M pc pc' M' n ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ nodeType.Return)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ nodeType.Return)›
‹instrs_of (PROG P) C M ! pc = Invoke M' n›
‹ek = ⇑λs. s(Exception := None, Stack (stkLength (P, C, M) pc' - 1) := s Exception)›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Return) ek (C, M, ⌊pc'⌋, Enter)"
by (fastforce intro: JVMCFG_reachable.CFG_Invoke_Return_Exceptional_handle)
ultimately show ?case by blast
next
case (CFG_Invoke_Return_Exceptional_prop C P C0 Main M pc M' n ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, nodeType.Return)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, nodeType.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)⇩√›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Return) ek (C, M, None, Return)"
by (fastforce intro: JVMCFG_reachable.CFG_Invoke_Return_Exceptional_prop)
ultimately show ?case by blast
next
case (CFG_Return C P C0 Main M pc ek)
then obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C, M, ⌊pc⌋, Enter)"
by blast
moreover with ‹C ≠ ClassMain P› ‹(P, C0, Main) ⊢ ⇒(C, M, ⌊pc⌋, Enter)›
‹instrs_of (PROG P) C M ! pc = instr.Return›
‹ek = ⇑λs. s(Stack 0 := s (Stack (stkLength (P, C, M) pc - 1)))›
have "vp_snoc P C0 Main as (C, M, ⌊pc⌋, Enter) ek (C, M, None, Return)"
by (fastforce intro: JVMCFG_reachable.CFG_Return)
ultimately show ?case by blast
next
case (CFG_Return_from_Method P C0 Main C M C' M' pc' Q' ps Q stateUpdate ek)
from ‹(P, C0, Main) ⊢ (C', M', ⌊pc'⌋, Normal) -Q':(C', M', pc')↪⇘(C, M)⇙ps→ (C, M, None, Enter)›
show ?case
proof cases
case Main_Call
with CFG_Return_from_Method obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (ClassMain P, MethodMain P, ⌊0⌋, Normal)"
by blast
moreover with Main_Call have "vp_snoc P C0 Main as (ClassMain P, MethodMain P, ⌊0⌋, Normal)
(λs. False)⇩√ (ClassMain P, MethodMain P, ⌊0⌋, Return)"
by (fastforce intro: Main_Call_LFalse)
ultimately show ?thesis using Main_Call CFG_Return_from_Method by blast
next
case CFG_Invoke_Call
with CFG_Return_from_Method obtain as where "JVMCFG_Interpret.valid_path' P C0 Main
(ClassMain P, MethodMain P, None, Enter) as (C', M', ⌊pc'⌋, Normal)"
by blast
moreover with CFG_Invoke_Call
have "vp_snoc P C0 Main as (C', M', ⌊pc'⌋, Normal) (λs. False)⇩√ (C', M', ⌊pc'⌋, Return)"
by (fastforce intro: CFG_Invoke_False)
ultimately show ?thesis using CFG_Invoke_Call CFG_Return_from_Method by blast
qed
qed
declare JVMCFG_Interpret.vp_snocI []
declare JVMCFG_Interpret.valid_node_def [simp del]
valid_edge_def [simp del]
JVMCFG_Interpret.intra_path_def [simp del]
definition EP :: jvm_prog
where "EP = (''C'', Object, [],
[(''M'', [], Void, 1::nat, 0::nat, [Push Unit, instr.Return], [])]) # SystemClasses"
definition Phi_EP :: ty⇩P
where "Phi_EP C M = (if C = ''C'' ∧ M = ''M''
then [⌊([],[OK (Class ''C'')])⌋,⌊([Void],[OK (Class ''C'')])⌋] else [])"
lemma distinct_classes'':
"''C'' ≠ Object"
"''C'' ≠ NullPointer"
"''C'' ≠ OutOfMemory"
"''C'' ≠ ClassCast"
by (simp_all add: Object_def NullPointer_def OutOfMemory_def ClassCast_def)
lemmas distinct_classes =
distinct_classes distinct_classes'' distinct_classes'' [symmetric]
declare distinct_classes [simp add]
lemma i_max_2D: "i < Suc (Suc 0) ⟹ i = 0 ∨ i = 1" by auto
lemma EP_wf: "wf_jvm_prog⇘Phi_EP⇙ EP"
unfolding wf_jvm_prog_phi_def wf_prog_def
proof
show "wf_syscls EP"
by (simp add: EP_def wf_syscls_def SystemClasses_def sys_xcpts_def
ObjectC_def NullPointerC_def OutOfMemoryC_def ClassCastC_def)
next
have distinct_EP: "distinct_fst EP"
by (auto simp: EP_def SystemClasses_def ObjectC_def NullPointerC_def OutOfMemoryC_def
ClassCastC_def)
moreover have classes_wf:
"∀c∈set EP. wf_cdecl
(λP C (M, Ts, T⇩r, mxs, mxl⇩0, is, xt). wt_method P C Ts T⇩r mxs mxl⇩0 is xt (Phi_EP C M)) EP c"
proof
fix C
assume C_in_EP: "C ∈ set EP"
show "wf_cdecl
(λP C (M, Ts, T⇩r, mxs, mxl⇩0, is, xt). wt_method P C Ts T⇩r mxs mxl⇩0 is xt (Phi_EP C M)) EP C"
proof (cases "C ∈ set SystemClasses")
case True
thus ?thesis
by (auto simp: wf_cdecl_def SystemClasses_def ObjectC_def NullPointerC_def
OutOfMemoryC_def ClassCastC_def EP_def class_def)
next
case False
with C_in_EP have "C = (''C'', the (class EP ''C''))"
by (auto simp: EP_def SystemClasses_def class_def)
thus ?thesis
by (auto dest!: i_max_2D elim: Methods.cases
simp: wf_cdecl_def class_def EP_def wf_mdecl_def wt_method_def Phi_EP_def
wt_start_def check_types_def states_def JVM_SemiType.sl_def SystemClasses_def
stk_esl_def upto_esl_def loc_sl_def SemiType.esl_def ObjectC_def
SemiType.sup_def Err.sl_def Err.le_def err_def Listn.sl_def Method_def
Err.esl_def Opt.esl_def Product.esl_def relevant_entries_def)
qed
qed
ultimately show "(∀c∈set EP. wf_cdecl
(λP C (M, Ts, T⇩r, mxs, mxl⇩0, is, xt). wt_method P C Ts T⇩r mxs mxl⇩0 is xt (Phi_EP C M)) EP c) ∧
distinct_fst EP"
by simp
qed
lemma [simp]: "PROG (Abs_wf_jvmprog (EP, Phi_EP)) = EP"
proof (cases "(EP, Phi_EP) ∈ wf_jvmprog")
case True thus ?thesis by (simp add: Abs_wf_jvmprog_inverse)
next
case False with EP_wf show ?thesis by (simp add: wf_jvmprog_def)
qed
lemma [simp]: "TYPING (Abs_wf_jvmprog (EP, Phi_EP)) = Phi_EP"
proof (cases "(EP, Phi_EP) ∈ wf_jvmprog")
case True thus ?thesis by (simp add: Abs_wf_jvmprog_inverse)
next
case False with EP_wf show ?thesis by (simp add: wf_jvmprog_def)
qed
lemma method_in_EP_is_M:
"EP ⊢ C sees M: Ts→T = (mxs, mxl, is, xt) in D
⟹ C = ''C'' ∧ M = ''M'' ∧ Ts = [] ∧ T = Void ∧ mxs = 1 ∧ mxl = 0 ∧
is = [Push Unit, instr.Return] ∧ xt = [] ∧ D = ''C''"
by (fastforce elim: Methods.cases
simp: class_def SystemClasses_def ObjectC_def NullPointerC_def OutOfMemoryC_def ClassCastC_def
if_split_eq1 EP_def Method_def)
lemma [simp]:
"∃T Ts mxs mxl is. (∃xt. EP ⊢ ''C'' sees ''M'': Ts→T = (mxs, mxl, is, xt) in ''C'') ∧ is ≠ []"
using EP_wf
by (fastforce dest: mdecl_visible simp: wf_jvm_prog_phi_def EP_def)
lemma [simp]:
"∃T Ts mxs mxl is. (∃xt. EP ⊢ ''C'' sees ''M'': Ts→T = (mxs, mxl, is, xt) in ''C'') ∧
Suc 0 < length is"
using EP_wf
by (fastforce dest: mdecl_visible simp: wf_jvm_prog_phi_def EP_def)
lemma C_sees_M_in_EP [simp]:
"EP ⊢ ''C'' sees ''M'': []→Void = (Suc 0, 0, [Push Unit, instr.Return], []) in ''C''"
proof -
have "EP ⊢ ''C'' sees_methods [''M'' ↦ (([], Void, 1, 0, [Push Unit, instr.Return], []), ''C'')]"
by (fastforce intro: Methods.intros simp: class_def SystemClasses_def ObjectC_def EP_def)
thus ?thesis by (fastforce simp: Method_def)
qed
lemma instrs_of_EP_C_M [simp]:
"instrs_of EP ''C'' ''M'' = [Push Unit, instr.Return]"
unfolding method_def
by (rule theI2 [where P = "λ(D, Ts, T, m). EP ⊢ ''C'' sees ''M'': Ts→T = m in D"])
(auto dest: method_in_EP_is_M)
lemma ClassMain_not_C [simp]: "ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) ≠ ''C''"
by (fastforce intro: no_Call_in_ClassMain [where P="Abs_wf_jvmprog (EP, Phi_EP)"] C_sees_M_in_EP)
lemma method_entry [dest!]: "(Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ⊢ ⇒(C, M, None, Enter)
⟹ (C = ClassMain (Abs_wf_jvmprog (EP, Phi_EP)) ∧ M = MethodMain (Abs_wf_jvmprog (EP, Phi_EP)))
∨ (C = ''C'' ∧ M = ''M'')"
by (fastforce elim: reachable.cases elim!: JVMCFG.cases dest!: method_in_EP_is_M)
lemma valid_node_in_EP_D:
assumes vn: "JVMCFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP)) ''C'' ''M'' n"
shows "n ∈ {
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter),
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Return),
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), ⌊0⌋, Enter),
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), ⌊0⌋, Normal),
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), ⌊0⌋, Return),
(''C'', ''M'', None, Enter),
(''C'', ''M'', ⌊0⌋, Enter),
(''C'', ''M'', ⌊1⌋, Enter),
(''C'', ''M'', None, Return)
}"
using vn
proof (cases rule: JVMCFG_Interpret.valid_node_cases')
let ?prog = "Abs_wf_jvmprog (EP, Phi_EP)"
case (Source e)
then obtain C M pc nt ek C' M' pc' nt'
where [simp]: "e = ((C, M, pc, nt), ek, (C', M', pc', nt'))"
and [simp]: "n = (C, M, pc, nt)"
and edge: "(?prog, ''C'', ''M'') ⊢ (C, M, pc, nt) -ek→ (C', M', pc', nt')"
by (cases e) (fastforce simp: valid_edge_def)
from edge have src_reachable: "(?prog, ''C'', ''M'') ⊢ ⇒(C, M, pc, nt)"
by -(drule sourcenode_reachable)
show ?thesis
proof (cases "C = ClassMain ?prog")
case True
with src_reachable have "M = MethodMain ?prog"
by (fastforce dest: ClassMain_imp_MethodMain)
with True edge show ?thesis
by clarsimp (erule JVMCFG.cases, simp_all)
next
case False
with src_reachable obtain T Ts mb where "EP ⊢ C sees M:Ts→T = mb in C"
by (fastforce dest: method_of_reachable_node_exists)
hence [simp]: "C = ''C''"
and [simp]: "M = ''M''"
and [simp]: "Ts = []"
and [simp]: "T = Void"
and [simp]: "mb = (1, 0, [Push Unit, instr.Return], [])"
by (cases mb, fastforce dest: method_in_EP_is_M)+
from src_reachable False have "pc ∈ {None, ⌊0⌋, ⌊1⌋}"
by (fastforce dest: instr_of_reachable_node_typable)
show ?thesis
proof (cases pc)
case None
with edge False show ?thesis
by clarsimp (erule JVMCFG.cases, simp_all)
next
case (Some pc')
show ?thesis
proof (cases pc')
case 0
with Some False edge show ?thesis
by clarsimp (erule JVMCFG.cases, fastforce+)
next
case (Suc n)
with ‹pc ∈ {None, ⌊0⌋, ⌊1⌋}› Some have "pc = ⌊1⌋"
by simp
with False edge show ?thesis
by clarsimp (erule JVMCFG.cases, fastforce+)
qed
qed
qed
next
let ?prog = "Abs_wf_jvmprog (EP, Phi_EP)"
case (Target e)
then obtain C M pc nt ek C' M' pc' nt'
where [simp]: "e = ((C, M, pc, nt), ek, (C', M', pc', nt'))"
and [simp]: "n = (C', M', pc', nt')"
and edge: "(?prog, ''C'', ''M'') ⊢ (C, M, pc, nt) -ek→ (C', M', pc', nt')"
by (cases e) (fastforce simp: valid_edge_def)
from edge have trg_reachable: "(?prog, ''C'', ''M'') ⊢ ⇒(C', M', pc', nt')"
by -(drule targetnode_reachable)
show ?thesis
proof (cases "C' = ClassMain ?prog")
case True
with trg_reachable have "M' = MethodMain ?prog"
by (fastforce dest: ClassMain_imp_MethodMain)
with True edge show ?thesis
by -(clarsimp, (erule JVMCFG.cases, simp_all))+
next
case False
with trg_reachable obtain T Ts mb where "EP ⊢ C' sees M':Ts→T = mb in C'"
by (fastforce dest: method_of_reachable_node_exists)
hence [simp]: "C' = ''C''"
and [simp]: "M' = ''M''"
and [simp]: "Ts = []"
and [simp]: "T = Void"
and [simp]: "mb = (1, 0, [Push Unit, instr.Return], [])"
by (cases mb, fastforce dest: method_in_EP_is_M)+
from trg_reachable False have "pc' ∈ {None, ⌊0⌋, ⌊1⌋}"
by (fastforce dest: instr_of_reachable_node_typable)
show ?thesis
proof (cases pc')
case None
with edge False show ?thesis
by clarsimp (erule JVMCFG.cases, simp_all)
next
case (Some pc'')
show ?thesis
proof (cases pc'')
case 0
with Some False edge show ?thesis
by -(clarsimp, (erule JVMCFG.cases, fastforce+))+
next
case (Suc n)
with ‹pc' ∈ {None, ⌊0⌋, ⌊1⌋}› Some have "pc' = ⌊1⌋"
by simp
with False edge show ?thesis
by -(clarsimp, (erule JVMCFG.cases, fastforce+))+
qed
qed
qed
qed
lemma Main_Entry_valid [simp]:
"JVMCFG_Interpret.valid_node (Abs_wf_jvmprog (EP, Phi_EP)) ''C'' ''M''
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None, Enter)"
proof -
have "valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'')
((ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None,
Enter),
(λs. False)⇩√,
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)), None,
Return))"
by (auto simp: valid_edge_def intro: JVMCFG_reachable.intros)
thus ?thesis by (fastforce simp: JVMCFG_Interpret.valid_node_def)
qed
lemma main_0_Enter_reachable [simp]: "(P, C0, Main) ⊢ ⇒(ClassMain P, MethodMain P, ⌊0⌋, Enter)"
by (rule reachable_step [where n="(ClassMain P, MethodMain P, None, Enter)"])
(fastforce intro: JVMCFG_reachable.intros)+
lemma main_0_Normal_reachable [simp]: "(P, C0, Main) ⊢ ⇒(ClassMain P, MethodMain P, ⌊0⌋, Normal)"
by (rule reachable_step [where n="(ClassMain P, MethodMain P, ⌊0⌋, Enter)"], simp)
(fastforce intro: JVMCFG_reachable.intros)
lemma main_0_Return_reachable [simp]: "(P, C0, Main) ⊢ ⇒(ClassMain P, MethodMain P, ⌊0⌋, Return)"
by (rule reachable_step [where n="(ClassMain P, MethodMain P, ⌊0⌋, Normal)"], simp)
(fastforce intro: JVMCFG_reachable.intros)
lemma Exit_reachable [simp]: "(P, C0, Main) ⊢ ⇒(ClassMain P, MethodMain P, None, Return)"
by (rule reachable_step [where n="(ClassMain P, MethodMain P, ⌊0⌋, Return)"], simp)
(fastforce intro: JVMCFG_reachable.intros)
definition
"cfg_wf_prog =
{(P, C0, Main). (∀n. JVMCFG_Interpret.valid_node P C0 Main n ⟶
(∃as. CFG.valid_path' sourcenode targetnode kind (valid_edge (P, C0, Main))
(get_return_edges P) n as (ClassMain P, MethodMain P, None, Return)))}"
typedef cfg_wf_prog = cfg_wf_prog
unfolding cfg_wf_prog_def
proof
let ?prog = "(Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'')"
let ?edge_main0 = "((ClassMain (fst ?prog), MethodMain (fst ?prog), None, Enter),
(λs. False)⇩√,
(ClassMain (fst ?prog), MethodMain (fst ?prog), None, Return))"
let ?edge_main1 = "((ClassMain (fst ?prog), MethodMain (fst ?prog), None, Enter),
(λs. True)⇩√,
(ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Enter))"
let ?edge_main2 = "((ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Enter),
⇑id,
(ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Normal))"
let ?edge_main3 = "((ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Normal),
(λs. False)⇩√,
(ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Return))"
let ?edge_main4 = "((ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Return),
⇑id,
(ClassMain (fst ?prog), MethodMain (fst ?prog), None, Return))"
let ?edge_call = "((ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Normal),
((λ(s, ret). True):(ClassMain (fst ?prog),
MethodMain (fst ?prog), 0)↪⇘(''C'', ''M'')⇙[(λs. s Heap),(λs. ⌊Value Null⌋)]),
(''C'', ''M'', None, Enter))"
let ?edge_C0 = "((''C'', ''M'', None, Enter),
(λs. False)⇩√,
(''C'', ''M'', None, Return))"
let ?edge_C1 = "((''C'', ''M'', None, Enter),
(λs. True)⇩√,
(''C'', ''M'', ⌊0⌋, Enter))"
let ?edge_C2 = "((''C'', ''M'', ⌊0⌋, Enter),
⇑(λs. s(Stack 0 ↦ Value Unit)),
(''C'', ''M'', ⌊1⌋, Enter))"
let ?edge_C3 = "((''C'', ''M'', ⌊1⌋, Enter),
⇑(λs. s(Stack 0 := s (Stack 0))),
(''C'', ''M'', None, Return))"
let ?edge_return = "((''C'', ''M'', None, Return),
(λ(s, ret). ret = (ClassMain (fst ?prog),
MethodMain (fst ?prog), 0))↩⇘(''C'',''M'')⇙(λs s'. s'(Heap := s Heap,
Exception := s Exception,
Stack 0 := s (Stack 0))),
(ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Return))"
have [simp]:
"(Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ⊢ ⇒(''C'', ''M'', None, Enter)"
by (rule reachable_step [where n="(ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Normal)"]
, simp)
(fastforce intro: Main_Call C_sees_M_in_EP)
hence [simp]:
"(Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ⊢ ⇒(''C'', ''M'', None, nodeType.Return)"
by (rule reachable_step [where n="(''C'', ''M'', None, Enter)"])
(fastforce intro: JVMCFG_reachable.intros)
have [simp]:
"(Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ⊢ ⇒(''C'', ''M'', ⌊0⌋, Enter)"
by (rule reachable_step [where n="(''C'', ''M'', None, Enter)"], simp)
(fastforce intro: JVMCFG_reachable.intros)
hence [simp]:
"(Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M'') ⊢ ⇒(''C'', ''M'', ⌊Suc 0⌋, Enter)"
by (fastforce intro: reachable_step [where n="(''C'', ''M'', ⌊0⌋, Enter)"] CFG_Push
simp: ClassMain_not_C [symmetric])
show "?prog ∈ {(P, C0, Main).
∀n. CFG.valid_node sourcenode targetnode (valid_edge (P, C0, Main)) n ⟶
(∃as. CFG.valid_path' sourcenode targetnode kind (valid_edge (P, C0, Main))
(get_return_edges P) n as
(ClassMain P, MethodMain P, None, nodeType.Return))}"
proof (auto dest!: valid_node_in_EP_D)
have "CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP)))
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, Enter)
[?edge_main0]
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by (fastforce intro: JVMCFG_Interpret.intra_path_vp JVMCFG_reachable.intros
simp: JVMCFG_Interpret.intra_path_def intra_kind_def valid_edge_def)
thus " ∃as. CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP)))
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, Enter)
as (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by blast
next
have "CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP)))
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)
[] (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by (fastforce intro: JVMCFG_Interpret.intra_path_vp simp: JVMCFG_Interpret.intra_path_def)
thus "∃as. CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP)))
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)
as (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by blast
next
have "CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP)))
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
⌊0⌋, Enter)
[?edge_main2, ?edge_main3, ?edge_main4]
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by (fastforce intro: JVMCFG_Interpret.intra_path_vp JVMCFG_reachable.intros
simp: JVMCFG_Interpret.intra_path_def intra_kind_def valid_edge_def)
thus "∃as. CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP)))
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
⌊0⌋, Enter)
as (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by blast
next
have "CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP)))
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
⌊0⌋, Normal)
[?edge_main3, ?edge_main4]
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by (fastforce intro: JVMCFG_Interpret.intra_path_vp JVMCFG_reachable.intros
simp: JVMCFG_Interpret.intra_path_def intra_kind_def valid_edge_def)
thus "∃as. CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP)))
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
⌊0⌋, Normal)
as (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by blast
next
have "CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP)))
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
⌊0⌋, nodeType.Return)
[?edge_main4]
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by (fastforce intro: JVMCFG_Interpret.intra_path_vp JVMCFG_reachable.intros
simp: JVMCFG_Interpret.intra_path_def intra_kind_def valid_edge_def)
thus "∃as. CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP)))
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
⌊0⌋, nodeType.Return)
as (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by blast
next
have "CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP))) (''C'', ''M'', None, Enter)
[?edge_C0, ?edge_return, ?edge_main4]
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by (fastforce intro: JVMCFG_reachable.intros C_sees_M_in_EP
simp: JVMCFG_Interpret.vp_def valid_edge_def stkLength_def JVMCFG_Interpret.valid_path_def)
thus "∃as. CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP))) (''C'', ''M'', None, Enter) as
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by blast
next
have "CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP))) (''C'', ''M'', ⌊0⌋, Enter)
[?edge_C2, ?edge_C3, ?edge_return, ?edge_main4]
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by (fastforce intro: Main_Return_to_Exit CFG_Return_from_Method Main_Call
C_sees_M_in_EP CFG_Return CFG_Push
simp: JVMCFG_Interpret.vp_def valid_edge_def stkLength_def Phi_EP_def
ClassMain_not_C [symmetric] JVMCFG_Interpret.valid_path_def)
thus "∃as. CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP))) (''C'', ''M'', ⌊0⌋, Enter) as
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by blast
next
have "CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP))) (''C'', ''M'', ⌊Suc 0⌋, Enter)
[?edge_C3, ?edge_return, ?edge_main4]
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by (fastforce intro: JVMCFG_reachable.intros C_sees_M_in_EP
simp: JVMCFG_Interpret.vp_def valid_edge_def stkLength_def Phi_EP_def
ClassMain_not_C [symmetric] JVMCFG_Interpret.valid_path_def)
thus "∃as. CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP))) (''C'', ''M'', ⌊Suc 0⌋, Enter) as
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by blast
next
have "CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP))) (''C'', ''M'', None, nodeType.Return)
[?edge_return, ?edge_main4]
(ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by (fastforce intro: JVMCFG_reachable.intros C_sees_M_in_EP
simp: JVMCFG_Interpret.vp_def valid_edge_def JVMCFG_Interpret.valid_path_def stkLength_def)
thus "∃as. CFG.valid_path' sourcenode targetnode kind
(valid_edge (Abs_wf_jvmprog (EP, Phi_EP), ''C'', ''M''))
(get_return_edges (Abs_wf_jvmprog (EP, Phi_EP))) (''C'', ''M'', None, nodeType.Return)
as (ClassMain (Abs_wf_jvmprog (EP, Phi_EP)), MethodMain (Abs_wf_jvmprog (EP, Phi_EP)),
None, nodeType.Return)"
by blast
qed
qed
abbreviation lift_to_cfg_wf_prog :: "(jvm_method ⇒ 'a) ⇒ (cfg_wf_prog ⇒ 'a)"
(‹_⇘CFG⇙›)
where "f⇘CFG⇙ ≡ (λP. f (Rep_cfg_wf_prog P))"
lemma valid_edge_CFG_def: "valid_edge⇘CFG⇙ P = valid_edge (fst⇘CFG⇙ P, fst (snd⇘CFG⇙ P), snd (snd⇘CFG⇙ P))"
by (cases P) (clarsimp simp: Abs_cfg_wf_prog_inverse)