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