Theory JVMInterpretation
theory JVMInterpretation imports JVMCFG "../StaticInter/CFGExit" begin
section ‹Instatiation of the ‹CFG› locale›
abbreviation sourcenode :: "cfg_edge ⇒ cfg_node"
where "sourcenode e ≡ fst e"
abbreviation targetnode :: "cfg_edge ⇒ cfg_node"
where "targetnode e ≡ snd(snd e)"
abbreviation kind :: "cfg_edge ⇒ (var, val, cname × mname × pc, cname × mname) edge_kind"
where "kind e ≡ fst(snd e)"
definition valid_edge :: "jvm_method ⇒ cfg_edge ⇒ bool"
where "valid_edge P e ≡ P ⊢ (sourcenode e) -(kind e)→ (targetnode e)"
fun methods :: "cname ⇒ JVMInstructions.jvm_method mdecl list ⇒ ((cname × mname) × var list × var list) list"
where "methods C [] = []"
| "methods C ((M, Ts, T, mb) # ms)
= ((C, M), Heap # (map Local [0..<Suc (length Ts)]), [Heap, Stack 0, Exception]) # (methods C ms)"
fun procs :: "jvm_prog ⇒ ((cname × mname) × var list × var list) list"
where "procs [] = []"
|"procs ((C, D, fs, ms) # P) = (methods C ms) @ (procs P)"
lemma in_set_methodsI: "map_of ms M = ⌊(Ts, T, mxs, mxl⇩0, is, xt)⌋
⟹ ((C', M), Heap # map Local [0..<length Ts] @ [Local (length Ts)], [Heap, Stack 0, Exception])
∈ set (methods C' ms)"
by (induct rule: methods.induct) (auto split: if_split_asm)
lemma in_methods_in_msD: "((C, M), ins, outs) ∈ set (methods D ms)
⟹ M ∈ set (map fst ms) ∧ D = C"
by (induct ms) auto
lemma in_methods_in_msD': "((C, M), ins, outs) ∈ set (methods D ms)
⟹ ∃Ts T mb. (M, Ts, T, mb) ∈ set ms
∧ D = C
∧ ins = Heap # (map Local [0..<Suc (length Ts)])
∧ outs = [Heap, Stack 0, Exception]"
by (induct rule: methods.induct) fastforce+
lemma in_set_methodsE:
assumes "((C, M), ins, outs) ∈ set (methods D ms)"
obtains Ts T mb
where "(M, Ts, T, mb) ∈ set ms"
and "D = C"
and "ins = Heap # (map Local [0..<Suc (length Ts)])"
and "outs = [Heap, Stack 0, Exception]"
using assms
by (induct ms) fastforce+
lemma in_set_procsI:
assumes sees: "P ⊢ D sees M: Ts→T = mb in D"
and ins_def: "ins = Heap # map Local [0..<Suc (length Ts)]"
and outs_def: "outs = [Heap, Stack 0, Exception]"
shows "((D, M), ins, outs) ∈ set (procs P)"
proof -
from sees obtain D' fs ms where "map_of P D = ⌊(D', fs, ms)⌋" and "map_of ms M = ⌊(Ts, T, mb)⌋"
by (fastforce dest: visible_method_exists simp: class_def)
hence "(D, D', fs, ms) ∈ set P"
by -(drule map_of_SomeD)
thus ?thesis
proof (induct P)
case Nil thus ?case by simp
next
case (Cons Class P)
with ins_def outs_def ‹map_of ms M = ⌊(Ts, T, mb)⌋› show ?case
by (cases Class, cases mb) (auto intro: in_set_methodsI)
qed
qed
lemma distinct_methods: "distinct (map fst ms) ⟹ distinct (map fst (methods C ms))"
proof (induct ms)
case Nil thus ?case by simp
next
case (Cons M ms)
thus ?case
by (cases M) (auto dest: in_methods_in_msD)
qed
lemma in_set_procsD:
"((C, M), ins, out) ∈ set (procs P) ⟹ ∃D fs ms. (C, D, fs, ms) ∈ set P ∧ M ∈ set (map fst ms)"
proof (induct P)
case Nil thus ?case by simp
next
case (Cons Class P)
thus ?case
by (cases Class) (fastforce dest: in_methods_in_msD intro: rev_image_eqI)
qed
lemma in_set_procsE':
assumes "((C, M), ins, outs) ∈ set (procs P)"
obtains D fs ms Ts T mb
where "(C, D, fs, ms) ∈ set P"
and "(M, Ts, T, mb) ∈ set ms"
and "ins = Heap # (map (λn. Local n) [0..<Suc (length Ts)])"
and "outs = [Heap, Stack 0, Exception]"
using assms
by (induct P) (fastforce elim: in_set_methodsE)+
lemma distinct_Local_vars [simp]: "distinct (map Local [0..<n])"
by (induct n) auto
lemma distinct_Stack_vars [simp]: "distinct (map Stack [0..<n])"
by (induct n) auto
inductive_set get_return_edges :: "wf_jvmprog ⇒ cfg_edge ⇒ cfg_edge set"
for P :: "wf_jvmprog"
and a :: "cfg_edge"
where
"kind a = Q:(C, M, pc)↪⇘(D, M')⇙paramDefs
⟹ ((D, M', None, Return),
(λ(s, ret). ret = (C, M, pc))↩⇘(D, M')⇙(λs s'. s'(Heap := s Heap, Exception := s Exception,
Stack (stkLength (P, C, M) (Suc pc) - 1) := s (Stack 0))),
(C, M, ⌊pc⌋, Return)) ∈ (get_return_edges P a)"
lemma get_return_edgesE [elim!]:
assumes "a ∈ get_return_edges P a'"
obtains Q C M pc D M' paramDefs where
"kind a' = Q:(C, M, pc)↪⇘(D, M')⇙paramDefs"
and "a = ((D, M', None, Return),
(λ(s, ret). ret = (C, M, pc))↩⇘(D, M')⇙(λs s'. s'(Heap := s Heap, Exception := s Exception,
Stack (stkLength (P, C, M) (Suc pc) - 1) := s (Stack 0))),
(C, M, ⌊pc⌋, Return))"
using assms
by -(cases a, cases a', clarsimp, erule get_return_edges.cases, fastforce)
lemma distinct_class_names: "distinct_fst (PROG P)"
using wf_jvmprog_is_wf_typ [of P]
by (clarsimp simp: wf_jvm_prog_phi_def wf_prog_def)
lemma distinct_method_names:
"class (PROG P) C = ⌊(D, fs, ms)⌋ ⟹ distinct_fst ms"
using wf_jvmprog_is_wf_typ [of P]
unfolding wf_jvm_prog_phi_def
by (fastforce dest: class_wf simp: wf_cdecl_def)
lemma distinct_fst_is_distinct_fst: "distinct_fst = BasicDefs.distinct_fst"
by (simp add: distinct_fst_def BasicDefs.distinct_fst_def)
lemma ClassMain_not_in_set_PROG [dest!]: "(ClassMain P, D, fs, ms) ∈ set (PROG P) ⟹ False"
using distinct_class_names [of P] ClassMain_is_no_class [of P]
by (fastforce intro: map_of_SomeI simp: class_def)
lemma in_set_procsE:
assumes "((C, M), ins, outs) ∈ set (procs (PROG P))"
obtains D fs ms Ts T mb
where "class (PROG P) C = ⌊(D, fs, ms)⌋"
and "PROG P ⊢ C sees M:Ts→T = mb in C"
and "ins = Heap # (map (λn. Local n) [0..<Suc (length Ts)])"
and "outs = [Heap, Stack 0, Exception]"
proof -
from ‹((C, M), ins, outs) ∈ set (procs (PROG P))›
obtain D fs ms Ts T mxs mxl⇩0 "is" xt
where "(C, D, fs, ms) ∈ set (PROG P)"
and "(M, Ts, T, mxs, mxl⇩0, is, xt) ∈ set ms"
and "ins = Heap # (map (λn. Local n) [0..<Suc (length Ts)])"
and "outs = [Heap, Stack 0, Exception]"
by (fastforce elim: in_set_procsE')
moreover from ‹(C, D, fs, ms) ∈ set (PROG P)› distinct_class_names [of P]
have "class (PROG P) C = ⌊(D, fs, ms)⌋"
by (fastforce intro: map_of_SomeI simp: class_def)
moreover from wf_jvmprog_is_wf_typ [of P]
‹(M, Ts, T, mxs, mxl⇩0, is, xt) ∈ set ms› ‹(C, D, fs, ms) ∈ set (PROG P)›
have "PROG P ⊢ C sees M:Ts→T = (mxs, mxl⇩0, is, xt) in C"
by (fastforce intro: mdecl_visible simp: wf_jvm_prog_phi_def)
ultimately show ?thesis using that by blast
qed
declare has_method_def [simp]