Up to index of Isabelle/HOL/Jinja/HRB-Slicing
theory JVMPostdominationtheory JVMPostdomination imports JVMInterpretation "../StaticInter/Postdomination" begin
context CFG begin
lemma vp_snocI:
"[|n -as->⇣\<surd>* n'; n' -[a]->* n''; ∀Q p ret fs. kind a ≠ Q\<hookleftarrow>⇘p⇙ret |] ==> n -as @ [a]->⇣\<surd>* 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) \<turnstile> (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) \<turnstile> =>(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) \<turnstile> =>(ClassMain P, MethodMain P, ⌊0⌋, Enter)`
have "vp_snoc P C0 Main as (ClassMain P, MethodMain P, ⌊0⌋, Enter) \<Up>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) \<turnstile> =>(ClassMain P, MethodMain P, ⌊0⌋, Normal)`
have "vp_snoc P C0 Main as (ClassMain P, MethodMain P, ⌊0⌋, Normal) (λs. False)⇣\<surd>
(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) \<turnstile> =>(ClassMain P, MethodMain P, ⌊0⌋, Normal)`
`PROG P \<turnstile> C0 sees Main: []->T = (mxs, mxl⇣0, is, xt) in D`
`initParams = [λs. s Heap, λs. ⌊Value Null⌋]`
`ek = λ(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>⇘(D, Main)⇙initParams`
have "vp_snoc P C0 Main as (ClassMain P, MethodMain P, ⌊0⌋, Normal)
((λ(s, ret). True):(ClassMain P, MethodMain P, 0)\<hookrightarrow>⇘(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) \<turnstile> =>(ClassMain P, MethodMain P, ⌊0⌋, nodeType.Return)`
have "vp_snoc P C0 Main as (ClassMain P, MethodMain P, ⌊0⌋, nodeType.Return) \<Up>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) \<turnstile> =>(C, M, None, Enter)`
have "vp_snoc P C0 Main as (C, M, None, Enter) (λs. False)⇣\<surd> (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) \<turnstile> =>(C, M, None, Enter)`
have "vp_snoc P C0 Main as (C, M, None, Enter) (λs. True)⇣\<surd> (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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = Load n`
`ek = \<Up>λs. s(Stack (stkLength (P, C, M) pc) := s (Local n))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = Store n`
`ek = \<Up>λs. s(Local n := s (Stack (stkLength (P, C, M) pc - 1)))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = Push v`
`ek = \<Up>λs. s(Stack (stkLength (P, C, M) pc) \<mapsto> Value v)`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = Pop` `ek = \<Up>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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = IAdd`
`ek = \<Up>λs. let i1 = the_Intg (stkAt s (stkLength (P, C, M) pc - 1));
i2 = the_Intg (stkAt s (stkLength (P, C, M) pc - 2))
in s(Stack (stkLength (P, C, M) pc - 2) \<mapsto> Value (Intg (i1 + i2)))`
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) \<turnstile> =>(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)⇣\<surd> (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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = CmpEq`
`ek = \<Up>λs. let e1 = stkAt s (stkLength (P, C, M) pc - 1);
e2 = stkAt s (stkLength (P, C, M) pc - 2)
in s(Stack (stkLength (P, C, M) pc - 2) \<mapsto> Value (Bool (e1 = e2)))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = IfFalse i` `i ≠ 1`
`ek = (λs. stkAt s (stkLength (P, C, M) pc - 1) = Bool False)⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = IfFalse i`
`ek = (λs. stkAt s (stkLength (P, C, M) pc - 1) ≠ Bool False ∨ i = 1)⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = New Cl` `ek = (λs. new_Addr (heap_of s) ≠ None)⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
` instrs_of (PROG P) C M ! pc = New Cl`
`pc' = (case match_ex_table (PROG P) OutOfMemory pc (ex_table_of (PROG P) C M) of None => None
| ⌊(pc'', d)⌋ => ⌊pc''⌋)` `ek = (λs. new_Addr (heap_of s) = None)⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Normal)`
` instrs_of (PROG P) C M ! pc = New Cl`
` ek = \<Up>λs. let a = the (new_Addr (heap_of s)) in
s(Heap \<mapsto> Hp (heap_of s(a \<mapsto> blank (PROG P) Cl)),
Stack (stkLength (P, C, M) pc) \<mapsto> Value (Addr a))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional None Enter)`
`instrs_of (PROG P) C M ! pc = New Cl`
`ek = \<Up>λs. s(Exception \<mapsto> Value (Addr (addr_of_sys_xcpt OutOfMemory)))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)`
`instrs_of (PROG P) C M ! pc = New Cl`
`ek = \<Up>λs. s(Exception := None)(Stack (stkLength (P, C, M) pc' - 1) \<mapsto>
Value (Addr (addr_of_sys_xcpt OutOfMemory)))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = Getfield F Cl`
`ek = (λs. stkAt s (stkLength (P, C, M) pc - 1) ≠ Null)⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = Getfield F Cl`
`pc' = (case match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M) of None => None
| ⌊(pc'', d)⌋ => ⌊pc''⌋)` `ek = (λs. stkAt s (stkLength (P, C, M) pc - 1) = Null)⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Normal)`
`instrs_of (PROG P) C M ! pc = Getfield F Cl`
`ek = \<Up>λs. let (D, fs) = the (heap_of s (the_Addr (stkAt s (stkLength (P, C, M) pc - 1))))
in s(Stack (stkLength (P, C, M) pc - 1) \<mapsto> Value (the (fs (F, Cl))))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional None Enter)`
`instrs_of (PROG P) C M ! pc = Getfield F Cl`
`ek = \<Up>λs. s(Exception \<mapsto> Value (Addr (addr_of_sys_xcpt NullPointer)))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)`
`instrs_of (PROG P) C M ! pc = Getfield F Cl`
`ek = \<Up>λs. s(Exception := None)(Stack (stkLength (P, C, M) pc' - 1) \<mapsto>
Value (Addr (addr_of_sys_xcpt NullPointer)))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = Putfield F Cl`
`ek = (λs. stkAt s (stkLength (P, C, M) pc - 2) ≠ Null)⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = Putfield F Cl`
`pc' = (case match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M) of None => None
| ⌊(pc'', d)⌋ => ⌊pc''⌋)` `ek = (λs. stkAt s (stkLength (P, C, M) pc - 2) = Null)⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Normal)`
`instrs_of (PROG P) C M ! pc = Putfield F Cl`
`ek = \<Up>λs. let v = stkAt s (stkLength (P, C, M) pc - 1);
r = stkAt s (stkLength (P, C, M) pc - 2);
a = the_Addr r; (D, fs) = the (heap_of s a); h' = heap_of s(a \<mapsto> (D, fs((F, Cl) \<mapsto> v)))
in s(Heap \<mapsto> Hp h')`
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) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional None Enter)`
`instrs_of (PROG P) C M ! pc = Putfield F Cl`
`ek = \<Up>λs. s(Exception \<mapsto> Value (Addr (addr_of_sys_xcpt NullPointer)))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)`
`instrs_of (PROG P) C M ! pc = Putfield F Cl`
`ek = \<Up>λs. s(Exception := None)(Stack (stkLength (P, C, M) pc' - 1) \<mapsto>
Value (Addr (addr_of_sys_xcpt NullPointer)))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = Checkcast Cl`
`ek = (λs. cast_ok (PROG P) Cl (heap_of s) (stkAt s (stkLength (P, C, M) pc - 1)))⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = Checkcast Cl`
`pc' = (case match_ex_table (PROG P) ClassCast pc (ex_table_of (PROG P) C M) of None => None
| ⌊(pc'', d)⌋ => ⌊pc''⌋)`
`ek = (λs. ¬ cast_ok (PROG P) Cl (heap_of s) (stkAt s (stkLength (P, C, M) pc - 1)))⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional None Enter)`
`instrs_of (PROG P) C M ! pc = Checkcast Cl`
`ek = \<Up>λs. s(Exception \<mapsto> Value (Addr (addr_of_sys_xcpt ClassCast)))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)`
`instrs_of (PROG P) C M ! pc = Checkcast Cl`
`ek = \<Up>λs. s(Exception := None)(Stack (stkLength (P, C, M) pc' - 1) \<mapsto>
Value (Addr (addr_of_sys_xcpt ClassCast)))`
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) \<turnstile> =>(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)⌋)⇣\<surd>`
have "(P, C0, Main) \<turnstile> (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))⇣\<surd>-> (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)⌋)⇣\<surd>`
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) \<turnstile> =>(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)⌋)⇣\<surd>`
have "(P, C0, Main) \<turnstile> (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)⌋)))⇣\<surd>->
(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)⌋)⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional None Enter)`
`instrs_of (PROG P) C M ! pc = Throw`
`ek = \<Up>λs. s(Exception \<mapsto> Value (stkAt s (stkLength (P, C, M) pc - 1)))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)`
`pc' ≠ length (instrs_of (PROG P) C M)` `instrs_of (PROG P) C M ! pc = Throw`
`ek = \<Up>λs. s(Exception := None)(Stack (stkLength (P, C, M) pc' - 1) \<mapsto>
Value (stkAt s (stkLength (P, C, M) pc - 1)))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = Invoke M' n`
`ek = (λs. stkAt s (stkLength (P, C, M) pc - Suc n) ≠ Null)⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = Invoke M' n`
`pc' = (case match_ex_table (PROG P) NullPointer pc (ex_table_of (PROG P) C M) of None => None
| ⌊(pc'', d)⌋ => ⌊pc''⌋)`
`ek = (λs. stkAt s (stkLength (P, C, M) pc - Suc n) = Null)⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional None Enter)`
`instrs_of (PROG P) C M ! pc = Invoke M' n`
`ek = \<Up>λs. s(Exception \<mapsto> Value (Addr (addr_of_sys_xcpt NullPointer)))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ Enter)`
`instrs_of (PROG P) C M ! pc = Invoke M' n`
`ek = \<Up>λs. s(Exception := None)(Stack (stkLength (P, C, M) pc' - 1) \<mapsto>
Value (Addr (addr_of_sys_xcpt NullPointer)))`
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) \<turnstile> =>(C, M, ⌊pc⌋, Normal)`
`instrs_of (PROG P) C M ! pc = Invoke M' n` `TYPING P C M ! pc = ⌊(ST, LT)⌋`
`ST ! n = Class D'` `PROG P \<turnstile> D' sees M': Ts->T = (mxs, mxl⇣0, is, xt) in D`
`Q = (λ(s, ret). let r = stkAt s (stkLength (P, C, M) pc - Suc n);
C' = 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)\<hookrightarrow>⇘(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) \<turnstile> =>(C, M, ⌊pc⌋, Normal)`
`instrs_of (PROG P) C M ! pc = Invoke M' n` `ek = (λs. False)⇣\<surd>`
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) \<turnstile> =>(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)⇣\<surd>`
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) \<turnstile> =>(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)⌋)⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Exceptional ⌊pc'⌋ nodeType.Return)`
`instrs_of (PROG P) C M ! pc = Invoke M' n`
`ek = \<Up>λs. s(Exception := None, Stack (stkLength (P, C, M) pc' - 1) := s Exception)`
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) \<turnstile> =>(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)⇣\<surd>`
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) \<turnstile> =>(C, M, ⌊pc⌋, Enter)`
`instrs_of (PROG P) C M ! pc = instr.Return`
`ek = \<Up>λs. s(Stack 0 := s (Stack (stkLength (P, C, M) pc - 1)))`
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) \<turnstile> (C', M', ⌊pc'⌋, Normal) -Q':(C', M', pc')\<hookrightarrow>⇘(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)⇣\<surd> (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)⇣\<surd> (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 \<turnstile> 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
split_if_eq1 EP_def Method_def)
lemma [simp]:
"∃T Ts mxs mxl is. (∃xt. EP \<turnstile> ''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 \<turnstile> ''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 \<turnstile> ''C'' sees ''M'': []->Void = (Suc 0, 0, [Push Unit, instr.Return], []) in ''C''"
proof -
have "EP \<turnstile> ''C'' sees_methods [''M'' \<mapsto> (([], 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 \<turnstile> ''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'') \<turnstile> =>(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'') \<turnstile> (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'') \<turnstile> =>(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 \<turnstile> 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'') \<turnstile> (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'') \<turnstile> =>(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 \<turnstile> 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)⇣\<surd>,
(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) \<turnstile> =>(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) \<turnstile> =>(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) \<turnstile> =>(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) \<turnstile> =>(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)⇣\<surd>,
(ClassMain (fst ?prog), MethodMain (fst ?prog), None, Return))"
let ?edge_main1 = "((ClassMain (fst ?prog), MethodMain (fst ?prog), None, Enter),
(λs. True)⇣\<surd>,
(ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Enter))"
let ?edge_main2 = "((ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Enter),
\<Up>id,
(ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Normal))"
let ?edge_main3 = "((ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Normal),
(λs. False)⇣\<surd>,
(ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Return))"
let ?edge_main4 = "((ClassMain (fst ?prog), MethodMain (fst ?prog), ⌊0⌋, Return),
\<Up>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)\<hookrightarrow>⇘(''C'', ''M'')⇙[(λs. s Heap),(λs. ⌊Value Null⌋)]),
(''C'', ''M'', None, Enter))"
let ?edge_C0 = "((''C'', ''M'', None, Enter),
(λs. False)⇣\<surd>,
(''C'', ''M'', None, Return))"
let ?edge_C1 = "((''C'', ''M'', None, Enter),
(λs. True)⇣\<surd>,
(''C'', ''M'', ⌊0⌋, Enter))"
let ?edge_C2 = "((''C'', ''M'', ⌊0⌋, Enter),
\<Up>(λs. s(Stack 0 \<mapsto> Value Unit)),
(''C'', ''M'', ⌊1⌋, Enter))"
let ?edge_C3 = "((''C'', ''M'', ⌊1⌋, Enter),
\<Up>(λ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))\<hookleftarrow>⇘(''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'') \<turnstile> =>(''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'') \<turnstile> =>(''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'') \<turnstile> =>(''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'') \<turnstile> =>(''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)
interpretation JVMCFG_Postdomination!:
Postdomination "sourcenode" "targetnode" "kind" "valid_edge⇘CFG⇙ P"
"(ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P), None, Enter)"
"(λ(C, M, pc, type). (C, M))" "get_return_edges (fst⇘CFG⇙ P)"
"((ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P)),[],[]) # procs (PROG (fst⇘CFG⇙ P))"
"(ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P))"
"(ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P), None, Return)"
for P
unfolding valid_edge_CFG_def
proof
fix n
obtain P' C0 Main where [simp]: "fst⇘CFG⇙ P = P'" and [simp]: "fst (snd⇘CFG⇙ P) = C0"
and [simp]: "snd (snd⇘CFG⇙ P) = Main"
by (cases P) clarsimp
assume "CFG.valid_node sourcenode targetnode
(valid_edge (fst⇘CFG⇙ P, fst (snd⇘CFG⇙ P), snd (snd⇘CFG⇙ P))) n"
thus "∃as. CFG.valid_path' sourcenode targetnode kind
(valid_edge (fst⇘CFG⇙ P, fst (snd⇘CFG⇙ P), snd (snd⇘CFG⇙ P)))
(get_return_edges (fst⇘CFG⇙ P))
(ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P), None, Enter) as n"
by (auto dest: sourcenode_reachable targetnode_reachable valid_Entry_path
simp: JVMCFG_Interpret.valid_node_def valid_edge_def)
next
fix n
obtain P' C0 Main where [simp]: "fst⇘CFG⇙ P = P'" and [simp]: "fst (snd⇘CFG⇙ P) = C0"
and [simp]: "snd (snd⇘CFG⇙ P) = Main"
and "(P', C0, Main) ∈ cfg_wf_prog"
by (cases P) (clarsimp simp: Abs_cfg_wf_prog_inverse)
assume "CFG.valid_node sourcenode targetnode
(valid_edge (fst⇘CFG⇙ P, fst (snd⇘CFG⇙ P), snd (snd⇘CFG⇙ P))) n"
with `(P', C0, Main) ∈ cfg_wf_prog`
show "∃as. CFG.valid_path' sourcenode targetnode kind
(valid_edge (fst⇘CFG⇙ P, fst (snd⇘CFG⇙ P), snd (snd⇘CFG⇙ P)))
(get_return_edges (fst⇘CFG⇙ P)) n as
(ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P), None, nodeType.Return)"
by (cases n) (fastforce simp: cfg_wf_prog_def)
next
fix n n'
obtain P' C0 Main where [simp]: "fst⇘CFG⇙ P = P'" and [simp]: "fst (snd⇘CFG⇙ P) = C0"
and [simp]: "snd (snd⇘CFG⇙ P) = Main"
by (cases P) clarsimp
assume "CFGExit.method_exit sourcenode kind
(valid_edge (fst⇘CFG⇙ P, fst (snd⇘CFG⇙ P), snd (snd⇘CFG⇙ P)))
(ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P), None, nodeType.Return) n"
and "CFGExit.method_exit sourcenode kind
(valid_edge (fst⇘CFG⇙ P, fst (snd⇘CFG⇙ P), snd (snd⇘CFG⇙ P)))
(ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P), None, nodeType.Return) n'"
and "(λ(C, M, pc, type). (C, M)) n = (λ(C, M, pc, type). (C, M)) n'"
thus "n = n'"
by (auto simp: JVMCFG_Exit_Interpret.method_exit_def valid_edge_def)
(fastforce elim: JVMCFG.cases)+
qed
end