Quelle  JVMExec.thy

(*  Title:      JinjaDCI/JVM/JVMExec.thy
    Author: Cornelia Pusch, Gerwin Klein, Susannah Mansky
    Copyright   1999 Technische Universitaet Muenchen, 2019-20

    Based on the Jinja theory JVM/JVMExec.thy by Cornelia Pusch and Gerwin Klein
*)

section ‹ Program Execution in the JVM in full small step style ›

theory JVMExec
imports JVMExecInstr
begin

abbreviation
  instrs_of :: "jvm_prog ==> cname ==> mname ==> instr list" where
  "instrs_of P C M == fst(snd(snd(snd(snd(snd(snd(method P C M)))))))"

fun curr_instr :: "jvm_prog ==> frame ==> instr" where
"curr_instr P (stk,loc,C,M,pc,ics) = instrs_of P C M ! pc"

― ‹ execution of single step of the initialization procedure ›
fun exec_Calling :: "[cname, cname list, jvm_prog, heap, val list, val list,
                  cname, mname, pc, frame list, sheap] ==> jvm_state"
where
"exec_Calling C Cs P h stk loc C₀ M₀ pc frs sh =
  (case sh C of
        None ==> (None, h, (stk, loc, C₀, M₀, pc, Calling C Cs)#frs, sh(C := Some (sblank P C, Prepared)))
      | Some (obj, iflag) ==>
          (case iflag of
              Done ==> (None, h, (stk, loc, C₀, M₀, pc, Called Cs)#frs, sh)
            | Processing ==> (None, h, (stk, loc, C₀, M₀, pc, Called Cs)#frs, sh)
            | Error ==> (None, h, (stk, loc, C₀, M₀, pc,
                                   Throwing Cs (addr_of_sys_xcpt NoClassDefFoundError))#frs, sh)
            | Prepared ==>
                let sh' = sh(C:=Some(fst(the(sh C)), Processing));
                    D = fst(the(class P C))
                 in if C = Object
                    then (None, h, (stk, loc, C₀, M₀, pc, Called (C#Cs))#frs, sh')
                    else (None, h, (stk, loc, C₀, M₀, pc, Calling D (C#Cs))#frs, sh')
          )
  )"

― ‹ single step of execution without error handling ›
fun exec_step :: "[jvm_prog, heap, val list, val list,
                  cname, mname, pc, init_call_status, frame list, sheap] ==> jvm_state"
where
"exec_step P h stk loc C M pc (Calling C' Cs) frs sh
   = exec_Calling C' Cs P h stk loc C M pc frs sh" |
"exec_step P h stk loc C M pc (Called (C'#Cs)) frs sh
   = (None, h, create_init_frame P C'#(stk, loc, C, M, pc, Called Cs)#frs, sh)" |
"exec_step P h stk loc C M pc (Throwing (C'#Cs) a) frs sh
   = (None, h, (stk,loc,C,M,pc,Throwing Cs a)#frs, sh(C':=Some(fst(the(sh C')), Error)))" |
"exec_step P h stk loc C M pc (Throwing [] a) frs sh
   = (⌊a⌋, h, (stk,loc,C,M,pc,No_ics)#frs, sh)" |
"exec_step P h stk loc C M pc ics frs sh
   = exec_instr (instrs_of P C M ! pc) P h stk loc C M pc ics frs sh"

― ‹ execution including error handling ›
fun exec :: "jvm_prog × jvm_state ==> jvm_state option" ― ‹single step execution› where
"exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh) =
   (let (xp', h', frs', sh') = exec_step P h stk loc C M pc ics frs sh
     in case xp' of
            None ==> Some (None,h',frs',sh')
          | Some x ==> Some (find_handler P x h ((stk,loc,C,M,pc,ics)#frs) sh)
   )"
| "exec _ = None"

― ‹relational view›
inductive_set
  exec_1 :: "jvm_prog ==> (jvm_state × jvm_state) set"
  and exec_1' :: "jvm_prog ==> jvm_state ==> jvm_state ==> bool" 
    (‹_ ⊨/ _ -jvm→₁/ _› [61,61,61] 60)
  for P :: jvm_prog
where
  "P ⊨ σ -jvm→₁ σ' ≡ (σ,σ') ∈ exec_1 P"
| exec_1I: "exec (P,σ) = Some σ' ==> P ⊨ σ -jvm→₁ σ'"

― ‹reflexive transitive closure:›
definition exec_all :: "jvm_prog ==> jvm_state ==> jvm_state ==> bool"
    (‹(_ ⊨/ _ -jvm→/ _)› [61,61,61]60) where
  exec_all_def1: "P ⊨ σ -jvm→ σ' ⟷ (σ,σ') ∈ (exec_1 P)^*"

notation (ASCII)
  exec_all  (‹_ |-/ _ -jvm->/ _› [61,61,61]60)


lemma exec_1_eq:
  "exec_1 P = {(σ,σ'). exec (P,σ) = Some σ'}"
(*<*)by (auto intro: exec_1I elim: exec_1.cases)(*>*)

lemma exec_1_iff:
  "P ⊨ σ -jvm→₁ σ' = (exec (P,σ) = Some σ')"
(*<*)by (simp add: exec_1_eq)(*>*)

lemma exec_all_def:
  "P ⊨ σ -jvm→ σ' = ((σ,σ') ∈ {(σ,σ'). exec (P,σ) = Some σ'}^*)"
(*<*)by (simp add: exec_all_def1 exec_1_eq)(*>*)

lemma jvm_refl[iff]: "P ⊨ σ -jvm→ σ"
(*<*)by(simp add: exec_all_def)(*>*)

lemma jvm_trans[trans]:
 "[ P ⊨ σ -jvm→ σ'; P ⊨ σ' -jvm→ σ'' ] ==> P ⊨ σ -jvm→ σ''"
(*<*)by(simp add: exec_all_def)(*>*)

lemma jvm_one_step1[trans]:
 "[ P ⊨ σ -jvm→₁ σ'; P ⊨ σ' -jvm→ σ'' ] ==> P ⊨ σ -jvm→ σ''"
(*<*) by (simp add: exec_all_def1) (*>*)

lemma jvm_one_step2[trans]:
 "[ P ⊨ σ -jvm→ σ'; P ⊨ σ' -jvm→₁ σ'' ] ==> P ⊨ σ -jvm→ σ''"
(*<*) by (simp add: exec_all_def1) (*>*)

lemma exec_all_conf:
  "[ P ⊨ σ -jvm→ σ'; P ⊨ σ -jvm→ σ'' ]
  ==> P ⊨ σ' -jvm→ σ'' ∨ P ⊨ σ'' -jvm→ σ'"
(*<*)by(simp add: exec_all_def single_valued_def single_valued_confluent)(*>*)

lemma exec_1_exec_all_conf:
 "[ exec (P, σ) = Some σ'; P ⊨ σ -jvm→ σ''; σ ≠ σ'' ]
 ==> P ⊨ σ' -jvm→ σ''"
 by(auto elim: converse_rtranclE simp: exec_1_eq exec_all_def)

lemma exec_all_finalD: "P ⊨ (x, h, [], sh) -jvm→ σ ==> σ = (x, h, [], sh)"
(*<*)
proof -
  assume "P ⊨ (x, h, [], sh) -jvm→ σ"
  then have "((x, h, [], sh), σ) ∈ {(σ, σ'). exec (P, σ) = ⌊σ'⌋}^*"
    by(simp only: exec_all_def)
  then show ?thesis proof(rule converse_rtranclE) qed simp+
qed
(*>*)

lemma exec_all_deterministic:
  "[ P ⊨ σ -jvm→ (x,h,[],sh); P ⊨ σ -jvm→ σ' ] ==> P ⊨ σ' -jvm→ (x,h,[],sh)"
(*<*)
proof -
  assume assms: "P ⊨ σ -jvm→ (x,h,[],sh)" "P ⊨ σ -jvm→ σ'"
  show ?thesis using exec_all_conf[OF assms]
    by(blast dest!: exec_all_finalD)
qed
(*>*)

subsection "Preservation of preallocated"

lemma exec_Calling_prealloc_pres:
assumes "preallocated h"
  and "exec_Calling C Cs P h stk loc C₀ M₀ pc frs sh = (xp',h',frs',sh')"
shows "preallocated h'"
using assms
proof(cases "sh C")
  case (Some a)
  then obtain sfs i where sfsi:"a = (sfs, i)" by(cases a)
  then show ?thesis using Some assms
  proof(cases i)
    case Prepared
    then show ?thesis using sfsi Some assms by(cases "method P C clinit", auto split: if_split_asm)
  next
    case Error
    then show ?thesis using sfsi Some assms by(cases "method P C clinit", auto)
  qed(auto)
qed(auto)

lemma exec_step_prealloc_pres:
assumes pre: "preallocated h"
  and "exec_step P h stk loc C M pc ics frs sh = (xp',h',frs',sh')"
shows "preallocated h'"
proof(cases ics)
  case No_ics
  then show ?thesis using exec_instr_prealloc_pres assms by auto
next
  case Calling
  then show ?thesis using exec_Calling_prealloc_pres assms by auto
next
  case (Called Cs)
  then show ?thesis using exec_instr_prealloc_pres assms by(cases Cs, auto)
next
  case (Throwing Cs a)
  then show ?thesis using assms by(cases Cs, auto)
qed

lemma exec_prealloc_pres:
assumes pre: "preallocated h"
  and "exec (P, xp, h, frs, sh) = Some(xp',h',frs',sh')"
shows "preallocated h'"
using assms
proof(cases "∃x. xp = ⌊x⌋ ∨ frs = []")
  case False
  then obtain f1 frs1 where frs: "frs = f1#frs1" by(cases frs, simp+)
  then obtain stk1 loc1 C1 M1 pc1 ics1 where f1: "f1 = (stk1,loc1,C1,M1,pc1,ics1)" by(cases f1)
  let ?i = "instrs_of P C1 M1 ! pc1"
  obtain xp2 h2 frs2 sh2
     where exec_step: "exec_step P h stk1 loc1 C1 M1 pc1 ics1 frs1 sh = (xp2,h2,frs2,sh2)"
    by(cases "exec_step P h stk1 loc1 C1 M1 pc1 ics1 frs1 sh")
  then show ?thesis using exec_step_prealloc_pres[OF pre exec_step] f1 frs False assms
  proof(cases xp2)
    case (Some a)
    show ?thesis
      using find_handler_prealloc_pres[OF pre, where a=a]
            exec_step_prealloc_pres[OF pre]
            exec_step f1 frs Some False assms
       by(auto split: bool.splits init_call_status.splits list.splits)
  qed(auto split: init_call_status.splits)
qed(auto)

subsection "Start state"

text ‹ The @{term Start} class is defined based on a given initial class
 and method. It has two methods: one that calls the initial method in the
 initial class, which is called by the starting program, and @{term clinit},
 as required for the class to be well-formed. ›
definition start_method :: "cname ==> mname ==> jvm_method mdecl" where
"start_method C M = (start_m, Static, [], Void, (1,0,[Invokestatic C M 0,Return],[]))"
abbreviation start_clinit :: "jvm_method mdecl" where
"start_clinit ≡ (clinit, Static, [], Void, (1,0,[Push Unit,Return],[]))"
definition start_class :: "cname ==> mname ==> jvm_method cdecl" where
"start_class C M = (Start, Object, [], [start_method C M, start_clinit])"

text ‹
 The start configuration of the JVM in program @{text P}:
 in the start heap, we call the ``start'' method of the
 ``Start''; this method performs @{text Invokestatic} on the
 class and method given to create the start program's @{term Start} class.
 This allows the initialization procedure to be called on the
 initial class in a natural way before the initial method is performed.
 There is no @{text this} pointer of the frame as @{term start} is @{term Static}.
 The start sheap has every class pre-prepared; this decision is not
 necessary.
 The starting program includes the added @{term Start} class, given a
 method @{text M} of class @{text C}, added to program @{text P}.
 ›
definition start_state :: "jvm_prog ==> jvm_state" where
  "start_state P = (None, start_heap P, [([], [], Start, start_m, 0, No_ics)], start_sheap)"
abbreviation start_prog :: "jvm_prog ==> cname ==> mname ==> jvm_prog" where
"start_prog P C M ≡ start_class C M # P"

end