Theory JVMInterpretation

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

text {*
\isaheader{Instatiation of the @{text 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, @{text "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⇙) \<turnstile> 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⇙) \<turnstile> 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 \<turnstile> (_ cs,None _) -(Q)⇣\<surd>-> (_ cs,⌊(cs', xf)⌋ _)) ∧
    (∃f. prog \<turnstile> (_ cs,⌊(cs', xf)⌋ _) -\<Up>f-> (_ cs',None _))"

fun valid_edge :: "jvmprog => j_edge => bool"
where
  "valid_edge prog a <->
    (prog \<turnstile> (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 \<turnstile> 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 \<turnstile> (_Exit_) -et-> n'" by simp
  thus False by fastforce
next
  have "prog \<turnstile> (_Entry_) -(λs. False)⇣\<surd>-> (_Exit_)" 
    by (rule JCFG_EntryExit)
  thus "∃a. valid_edge prog a ∧ sourcenode a = (_Entry_) ∧
            targetnode a = (_Exit_) ∧ kind a = (λs. False)⇣\<surd>"
    by fastforce
qed

end