# Theory JVMInterpretation

```theory JVMInterpretation imports JVMCFG "../Basic/CFGExit" begin

section ‹Instatiation of the ‹CFG› locale›

abbreviation sourcenode :: "j_edge ⇒ j_node"
where "sourcenode e ≡ fst e"

abbreviation targetnode :: "j_edge ⇒ j_node"
where "targetnode e ≡ snd(snd e)"

abbreviation kind :: "j_edge ⇒ state edge_kind"
where "kind e ≡ fst(snd e)"

text ‹
The following predicates define the aforementioned well-formedness requirements
for nodes. Later, ‹valid_callstack› will be implied by Jinja's state conformance.
›

fun valid_callstack :: "jvmprog ⇒ callstack ⇒ bool"
where
"valid_callstack prog [] = True"
| "valid_callstack (P, C0, Main) [(C, M, pc)] ⟷
C = C0 ∧ M = Main ∧
(P⇘Φ⇙) C M ! pc ≠ None ∧
(∃T Ts mxs mxl is xt. (P⇘wf⇙) ⊢ C sees M:Ts→T=(mxs, mxl, is, xt) in C ∧ pc < length is)"
| "valid_callstack (P, C0, Main) ((C, M, pc)#(C', M', pc')#cs) ⟷
instrs_of (P⇘wf⇙) C' M' ! pc' =
Invoke M (locLength P C M 0 - Suc (fst(snd(snd(snd(snd(method (P⇘wf⇙) C M)))))) ) ∧
(P⇘Φ⇙) C M ! pc ≠ None ∧
(∃T Ts mxs mxl is xt. (P⇘wf⇙) ⊢ C sees M:Ts→T=(mxs, mxl, is, xt) in C ∧ pc < length is) ∧
valid_callstack (P, C0, Main) ((C', M', pc')#cs)"

fun valid_node :: "jvmprog ⇒ j_node ⇒ bool"
where
"valid_node prog (_Entry_) = True"
(* | "valid_node prog (_Exit_) = True" *)
| "valid_node prog (_ cs,None _) ⟷ valid_callstack prog cs"
| "valid_node prog (_ cs,⌊(cs', xf)⌋ _) ⟷
valid_callstack prog cs ∧ valid_callstack prog cs' ∧
(∃Q. prog ⊢ (_ cs,None _) -(Q)⇩√→ (_ cs,⌊(cs', xf)⌋ _)) ∧
(∃f. prog ⊢ (_ cs,⌊(cs', xf)⌋ _) -⇑f→ (_ cs',None _))"

fun valid_edge :: "jvmprog ⇒ j_edge ⇒ bool"
where
"valid_edge prog a ⟷
(prog ⊢ (sourcenode a) -(kind a)→ (targetnode a))
∧ (valid_node prog (sourcenode a))
∧ (valid_node prog (targetnode a))"

interpretation JVM_CFG_Interpret:
CFG "sourcenode" "targetnode" "kind" "valid_edge prog" "Entry"
for prog
proof (unfold_locales)
fix a
assume ve: "valid_edge prog a"
and trg: "targetnode a = (_Entry_)"
obtain n et n'
where "a = (n,et,n')"
by (cases a) fastforce
with ve trg
have "prog ⊢ n -et→ (_Entry_)" by simp
thus False by fastforce
next
fix a a'
assume valid: "valid_edge prog a"
and valid': "valid_edge prog a'"
and sourceeq: "sourcenode a = sourcenode a'"
and targeteq: "targetnode a = targetnode a'"
obtain n1 et n2
where a:"a = (n1, et, n2)"
by (cases a) fastforce
obtain n1' et' n2'
where a':"a' = (n1', et', n2')"
by (cases a') fastforce
from a valid a' valid' sourceeq targeteq
have "et = et'"
by (fastforce elim: JVMCFG_edge_det)
with a a' sourceeq targeteq
show "a = a'"
by simp
qed

interpretation JVM_CFGExit_Interpret:
CFGExit "sourcenode" "targetnode" "kind" "valid_edge prog" "Entry" "(_Exit_)"
for prog
proof(unfold_locales)
fix a
assume ve: "valid_edge prog a"
and src: "sourcenode a = (_Exit_)"
obtain n et n'
where "a = (n,et,n')"
by (cases a) fastforce
with ve src
have "prog ⊢ (_Exit_) -et→ n'" by simp
thus False by fastforce
next
have "prog ⊢ (_Entry_) -(λs. False)⇩√→ (_Exit_)"
by (rule JCFG_EntryExit)
thus "∃a. valid_edge prog a ∧ sourcenode a = (_Entry_) ∧
targetnode a = (_Exit_) ∧ kind a = (λs. False)⇩√"
by fastforce
qed

end

```