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 (