Theory JinjaDCI.JVMExec
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"
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⇩0 M⇩0 pc frs sh =
(case sh C of
None ⇒ (None, h, (stk, loc, C⇩0, M⇩0, pc, Calling C Cs)#frs, sh(C := Some (sblank P C, Prepared)))
| Some (obj, iflag) ⇒
(case iflag of
Done ⇒ (None, h, (stk, loc, C⇩0, M⇩0, pc, Called Cs)#frs, sh)
| Processing ⇒ (None, h, (stk, loc, C⇩0, M⇩0, pc, Called Cs)#frs, sh)
| Error ⇒ (None, h, (stk, loc, C⇩0, M⇩0, 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⇩0, M⇩0, pc, Called (C#Cs))#frs, sh')
else (None, h, (stk, loc, C⇩0, M⇩0, pc, Calling D (C#Cs))#frs, sh')
)
)"
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"
fun exec :: "jvm_prog × jvm_state ⇒ jvm_state option" 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"
inductive_set
exec_1 :: "jvm_prog ⇒ (jvm_state × jvm_state) set"
and exec_1' :: "jvm_prog ⇒ jvm_state ⇒ jvm_state ⇒ bool"
("_ ⊢/ _ -jvm→⇩1/ _" [61,61,61] 60)
for P :: jvm_prog
where
"P ⊢ σ -jvm→⇩1 σ' ≡ (σ,σ') ∈ exec_1 P"
| exec_1I: "exec (P,σ) = Some σ' ⟹ P ⊢ σ -jvm→⇩1 σ'"
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→⇩1 σ' = (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→⇩1 σ'; P ⊢ σ' -jvm→ σ'' ⟧ ⟹ P ⊢ σ -jvm→ σ''"
by (simp add: exec_all_def1)
lemma jvm_one_step2[trans]:
"⟦ P ⊢ σ -jvm→ σ'; P ⊢ σ' -jvm→⇩1 σ'' ⟧ ⟹ 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⇩0 M⇩0 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