Theory Effect
section ‹Effect of Instructions on the State Type›
theory Effect
imports JVM_SemiType "../JVM/JVMExceptions"
begin
locale prog =
fixes P :: "'a prog"
locale jvm_method = prog +
fixes mxs :: nat
fixes mxl⇩0 :: nat
fixes Ts :: "ty list"
fixes T⇩r :: ty
fixes "is" :: "instr list"
fixes xt :: ex_table
fixes mxl :: nat
defines mxl_def: "mxl ≡ 1+size Ts+mxl⇩0"
text ‹ Program counter of successor instructions: ›
primrec succs :: "instr ⇒ ty⇩i ⇒ pc ⇒ pc list" where
"succs (Load idx) τ pc = [pc+1]"
| "succs (Store idx) τ pc = [pc+1]"
| "succs (Push v) τ pc = [pc+1]"
| "succs (Getfield F C) τ pc = [pc+1]"
| "succs (Getstatic C F D) τ pc = [pc+1]"
| "succs (Putfield F C) τ pc = [pc+1]"
| "succs (Putstatic C F D) τ pc = [pc+1]"
| "succs (New C) τ pc = [pc+1]"
| "succs (Checkcast C) τ pc = [pc+1]"
| "succs Pop τ pc = [pc+1]"
| "succs IAdd τ pc = [pc+1]"
| "succs CmpEq τ pc = [pc+1]"
| succs_IfFalse:
"succs (IfFalse b) τ pc = [pc+1, nat (int pc + b)]"
| succs_Goto:
"succs (Goto b) τ pc = [nat (int pc + b)]"
| succs_Return:
"succs Return τ pc = []"
| succs_Invoke:
"succs (Invoke M n) τ pc = (if (fst τ)!n = NT then [] else [pc+1])"
| succs_Invokestatic:
"succs (Invokestatic C M n) τ pc = [pc+1]"
| succs_Throw:
"succs Throw τ pc = []"
text "Effect of instruction on the state type:"
fun the_class:: "ty ⇒ cname" where
"the_class (Class C) = C"
fun eff⇩i :: "instr × 'm prog × ty⇩i ⇒ ty⇩i" where
eff⇩i_Load:
"eff⇩i (Load n, P, (ST, LT)) = (ok_val (LT ! n) # ST, LT)"
| eff⇩i_Store:
"eff⇩i (Store n, P, (T#ST, LT)) = (ST, LT[n:= OK T])"
| eff⇩i_Push:
"eff⇩i (Push v, P, (ST, LT)) = (the (typeof v) # ST, LT)"
| eff⇩i_Getfield:
"eff⇩i (Getfield F C, P, (T#ST, LT)) = (snd (snd (field P C F)) # ST, LT)"
| eff⇩i_Getstatic:
"eff⇩i (Getstatic C F D, P, (ST, LT)) = (snd (snd (field P C F)) # ST, LT)"
| eff⇩i_Putfield:
"eff⇩i (Putfield F C, P, (T⇩1#T⇩2#ST, LT)) = (ST,LT)"
| eff⇩i_Putstatic:
"eff⇩i (Putstatic C F D, P, (T#ST, LT)) = (ST,LT)"
| eff⇩i_New:
"eff⇩i (New C, P, (ST,LT)) = (Class C # ST, LT)"
| eff⇩i_Checkcast:
"eff⇩i (Checkcast C, P, (T#ST,LT)) = (Class C # ST,LT)"
| eff⇩i_Pop:
"eff⇩i (Pop, P, (T#ST,LT)) = (ST,LT)"
| eff⇩i_IAdd:
"eff⇩i (IAdd, P,(T⇩1#T⇩2#ST,LT)) = (Integer#ST,LT)"
| eff⇩i_CmpEq:
"eff⇩i (CmpEq, P, (T⇩1#T⇩2#ST,LT)) = (Boolean#ST,LT)"
| eff⇩i_IfFalse:
"eff⇩i (IfFalse b, P, (T⇩1#ST,LT)) = (ST,LT)"
| eff⇩i_Invoke:
"eff⇩i (Invoke M n, P, (ST,LT)) =
(let C = the_class (ST!n); (D,b,Ts,T⇩r,m) = method P C M
in (T⇩r # drop (n+1) ST, LT))"
| eff⇩i_Invokestatic:
"eff⇩i (Invokestatic C M n, P, (ST,LT)) =
(let (D,b,Ts,T⇩r,m) = method P C M
in (T⇩r # drop n ST, LT))"
| eff⇩i_Goto:
"eff⇩i (Goto n, P, s) = s"
fun is_relevant_class :: "instr ⇒ 'm prog ⇒ cname ⇒ bool" where
rel_Getfield:
"is_relevant_class (Getfield F D)
= (λP C. P ⊢ NullPointer ≼⇧* C ∨ P ⊢ NoSuchFieldError ≼⇧* C
∨ P ⊢ IncompatibleClassChangeError ≼⇧* C)"
| rel_Getstatic:
"is_relevant_class (Getstatic C F D)
= (λP C. True)"
| rel_Putfield:
"is_relevant_class (Putfield F D)
= (λP C. P ⊢ NullPointer ≼⇧* C ∨ P ⊢ NoSuchFieldError ≼⇧* C
∨ P ⊢ IncompatibleClassChangeError ≼⇧* C)"
| rel_Putstatic:
"is_relevant_class (Putstatic C F D)
= (λP C. True)"
| rel_Checkcast:
"is_relevant_class (Checkcast D) = (λP C. P ⊢ ClassCast ≼⇧* C)"
| rel_New:
"is_relevant_class (New D) = (λP C. True)"
| rel_Throw:
"is_relevant_class Throw = (λP C. True)"
| rel_Invoke:
"is_relevant_class (Invoke M n) = (λP C. True)"
| rel_Invokestatic:
"is_relevant_class (Invokestatic C M n) = (λP C. True)"
| rel_default:
"is_relevant_class i = (λP C. False)"
definition is_relevant_entry :: "'m prog ⇒ instr ⇒ pc ⇒ ex_entry ⇒ bool" where
"is_relevant_entry P i pc e ⟷ (let (f,t,C,h,d) = e in is_relevant_class i P C ∧ pc ∈ {f..<t})"
definition relevant_entries :: "'m prog ⇒ instr ⇒ pc ⇒ ex_table ⇒ ex_table" where
"relevant_entries P i pc = filter (is_relevant_entry P i pc)"
definition xcpt_eff :: "instr ⇒ 'm prog ⇒ pc ⇒ ty⇩i
⇒ ex_table ⇒ (pc × ty⇩i') list" where
"xcpt_eff i P pc τ et = (let (ST,LT) = τ in
map (λ(f,t,C,h,d). (h, Some (Class C#drop (size ST - d) ST, LT))) (relevant_entries P i pc et))"
definition norm_eff :: "instr ⇒ 'm prog ⇒ nat ⇒ ty⇩i ⇒ (pc × ty⇩i') list" where
"norm_eff i P pc τ = map (λpc'. (pc',Some (eff⇩i (i,P,τ)))) (succs i τ pc)"
definition eff :: "instr ⇒ 'm prog ⇒ pc ⇒ ex_table ⇒ ty⇩i' ⇒ (pc × ty⇩i') list" where
"eff i P pc et t = (case t of
None ⇒ []
| Some τ ⇒ (norm_eff i P pc τ) @ (xcpt_eff i P pc τ et))"
lemma eff_None:
"eff i P pc xt None = []"
by (simp add: eff_def)
lemma eff_Some:
"eff i P pc xt (Some τ) = norm_eff i P pc τ @ xcpt_eff i P pc τ xt"
by (simp add: eff_def)
text "Conditions under which eff is applicable:"
fun app⇩i :: "instr × 'm prog × pc × nat × ty × ty⇩i ⇒ bool" where
app⇩i_Load:
"app⇩i (Load n, P, pc, mxs, T⇩r, (ST,LT)) =
(n < length LT ∧ LT ! n ≠ Err ∧ length ST < mxs)"
| app⇩i_Store:
"app⇩i (Store n, P, pc, mxs, T⇩r, (T#ST, LT)) =
(n < length LT)"
| app⇩i_Push:
"app⇩i (Push v, P, pc, mxs, T⇩r, (ST,LT)) =
(length ST < mxs ∧ typeof v ≠ None)"
| app⇩i_Getfield:
"app⇩i (Getfield F C, P, pc, mxs, T⇩r, (T#ST, LT)) =
(∃T⇩f. P ⊢ C sees F,NonStatic:T⇩f in C ∧ P ⊢ T ≤ Class C)"
| app⇩i_Getstatic:
"app⇩i (Getstatic C F D, P, pc, mxs, T⇩r, (ST, LT)) =
(length ST < mxs ∧ (∃T⇩f. P ⊢ C sees F,Static:T⇩f in D))"
| app⇩i_Putfield:
"app⇩i (Putfield F C, P, pc, mxs, T⇩r, (T⇩1#T⇩2#ST, LT)) =
(∃T⇩f. P ⊢ C sees F,NonStatic:T⇩f in C ∧ P ⊢ T⇩2 ≤ (Class C) ∧ P ⊢ T⇩1 ≤ T⇩f)"
| app⇩i_Putstatic:
"app⇩i (Putstatic C F D, P, pc, mxs, T⇩r, (T#ST, LT)) =
(∃T⇩f. P ⊢ C sees F,Static:T⇩f in D ∧ P ⊢ T ≤ T⇩f)"
| app⇩i_New:
"app⇩i (New C, P, pc, mxs, T⇩r, (ST,LT)) =
(is_class P C ∧ length ST < mxs)"
| app⇩i_Checkcast:
"app⇩i (Checkcast C, P, pc, mxs, T⇩r, (T#ST,LT)) =
(is_class P C ∧ is_refT T)"
| app⇩i_Pop:
"app⇩i (Pop, P, pc, mxs, T⇩r, (T#ST,LT)) =
True"
| app⇩i_IAdd:
"app⇩i (IAdd, P, pc, mxs, T⇩r, (T⇩1#T⇩2#ST,LT)) = (T⇩1 = T⇩2 ∧ T⇩1 = Integer)"
| app⇩i_CmpEq:
"app⇩i (CmpEq, P, pc, mxs, T⇩r, (T⇩1#T⇩2#ST,LT)) =
(T⇩1 = T⇩2 ∨ is_refT T⇩1 ∧ is_refT T⇩2)"
| app⇩i_IfFalse:
"app⇩i (IfFalse b, P, pc, mxs, T⇩r, (Boolean#ST,LT)) =
(0 ≤ int pc + b)"
| app⇩i_Goto:
"app⇩i (Goto b, P, pc, mxs, T⇩r, s) =
(0 ≤ int pc + b)"
| app⇩i_Return:
"app⇩i (Return, P, pc, mxs, T⇩r, (T#ST,LT)) =
(P ⊢ T ≤ T⇩r)"
| app⇩i_Throw:
"app⇩i (Throw, P, pc, mxs, T⇩r, (T#ST,LT)) =
is_refT T"
| app⇩i_Invoke:
"app⇩i (Invoke M n, P, pc, mxs, T⇩r, (ST,LT)) =
(n < length ST ∧
(ST!n ≠ NT ⟶
(∃C D Ts T m. ST!n = Class C ∧ P ⊢ C sees M,NonStatic:Ts → T = m in D ∧
P ⊢ rev (take n ST) [≤] Ts)))"
| app⇩i_Invokestatic:
"app⇩i (Invokestatic C M n, P, pc, mxs, T⇩r, (ST,LT)) =
(length ST - n < mxs ∧ n ≤ length ST ∧ M ≠ clinit ∧
(∃D Ts T m. P ⊢ C sees M,Static:Ts → T = m in D ∧
P ⊢ rev (take n ST) [≤] Ts))"
| app⇩i_default:
"app⇩i (i,P, pc,mxs,T⇩r,s) = False"
definition xcpt_app :: "instr ⇒ 'm prog ⇒ pc ⇒ nat ⇒ ex_table ⇒ ty⇩i ⇒ bool" where
"xcpt_app i P pc mxs xt τ ⟷ (∀(f,t,C,h,d) ∈ set (relevant_entries P i pc xt). is_class P C ∧ d ≤ size (fst τ) ∧ d < mxs)"
definition app :: "instr ⇒ 'm prog ⇒ nat ⇒ ty ⇒ nat ⇒ nat ⇒ ex_table ⇒ ty⇩i' ⇒ bool" where
"app i P mxs T⇩r pc mpc xt t = (case t of None ⇒ True | Some τ ⇒
app⇩i (i,P,pc,mxs,T⇩r,τ) ∧ xcpt_app i P pc mxs xt τ ∧
(∀(pc',τ') ∈ set (eff i P pc xt t). pc' < mpc))"
lemma app_Some:
"app i P mxs T⇩r pc mpc xt (Some τ) =
(app⇩i (i,P,pc,mxs,T⇩r,τ) ∧ xcpt_app i P pc mxs xt τ ∧
(∀(pc',s') ∈ set (eff i P pc xt (Some τ)). pc' < mpc))"
by (simp add: app_def)
locale eff = jvm_method +
fixes eff⇩i and app⇩i and eff and app
fixes norm_eff and xcpt_app and xcpt_eff
fixes mpc
defines "mpc ≡ size is"
defines "eff⇩i i τ ≡ Effect.eff⇩i (i,P,τ)"
notes eff⇩i_simps [simp] = Effect.eff⇩i.simps [where P = P, folded eff⇩i_def]
defines "app⇩i i pc τ ≡ Effect.app⇩i (i, P, pc, mxs, T⇩r, τ)"
notes app⇩i_simps [simp] = Effect.app⇩i.simps [where P=P and mxs=mxs and T⇩r=T⇩r, folded app⇩i_def]
defines "xcpt_eff i pc τ ≡ Effect.xcpt_eff i P pc τ xt"
notes xcpt_eff = Effect.xcpt_eff_def [of _ P _ _ xt, folded xcpt_eff_def]
defines "norm_eff i pc τ ≡ Effect.norm_eff i P pc τ"
notes norm_eff = Effect.norm_eff_def [of _ P, folded norm_eff_def eff⇩i_def]
defines "eff i pc ≡ Effect.eff i P pc xt"
notes eff = Effect.eff_def [of _ P _ xt, folded eff_def norm_eff_def xcpt_eff_def]
defines "xcpt_app i pc τ ≡ Effect.xcpt_app i P pc mxs xt τ"
notes xcpt_app = Effect.xcpt_app_def [of _ P _ mxs xt, folded xcpt_app_def]
defines "app i pc ≡ Effect.app i P mxs T⇩r pc mpc xt"
notes app = Effect.app_def [of _ P mxs T⇩r _ mpc xt, folded app_def xcpt_app_def app⇩i_def eff_def]
lemma length_cases2:
assumes "⋀LT. P ([],LT)"
assumes "⋀l ST LT. P (l#ST,LT)"
shows "P s"
by (cases s, cases "fst s") (auto intro!: assms)
lemma length_cases3:
assumes "⋀LT. P ([],LT)"
assumes "⋀l LT. P ([l],LT)"
assumes "⋀l ST LT. P (l#ST,LT)"
shows "P s"
proof -
obtain xs LT where s: "s = (xs,LT)" by (cases s)
show ?thesis
proof (cases xs)
case Nil with assms s show ?thesis by simp
next
fix l xs' assume "xs = l#xs'"
with assms s show ?thesis by simp
qed
qed
lemma length_cases4:
assumes "⋀LT. P ([],LT)"
assumes "⋀l LT. P ([l],LT)"
assumes "⋀l l' LT. P ([l,l'],LT)"
assumes "⋀l l' ST LT. P (l#l'#ST,LT)"
shows "P s"
proof -
obtain xs LT where s: "s = (xs,LT)" by (cases s)
show ?thesis
proof (cases xs)
case Nil with assms s show ?thesis by simp
next
fix l xs' assume xs: "xs = l#xs'"
thus ?thesis
proof (cases xs')
case Nil with assms s xs show ?thesis by simp
next
fix l' ST assume "xs' = l'#ST"
with assms s xs show ?thesis by simp
qed
qed
qed
text ‹
\medskip
simp rules for @{term app}
›
lemma appNone[simp]: "app i P mxs T⇩r pc mpc et None = True"
by (simp add: app_def)
lemma appLoad[simp]:
"app⇩i (Load idx, P, T⇩r, mxs, pc, s) = (∃ST LT. s = (ST,LT) ∧ idx < length LT ∧ LT!idx ≠ Err ∧ length ST < mxs)"
by (cases s, simp)
lemma appStore[simp]:
"app⇩i (Store idx,P,pc,mxs,T⇩r,s) = (∃ts ST LT. s = (ts#ST,LT) ∧ idx < length LT)"
by (rule length_cases2, auto)
lemma appPush[simp]:
"app⇩i (Push v,P,pc,mxs,T⇩r,s) =
(∃ST LT. s = (ST,LT) ∧ length ST < mxs ∧ typeof v ≠ None)"
by (cases s, simp)
lemma appGetField[simp]:
"app⇩i (Getfield F C,P,pc,mxs,T⇩r,s) =
(∃ oT vT ST LT. s = (oT#ST, LT) ∧
P ⊢ C sees F,NonStatic:vT in C ∧ P ⊢ oT ≤ (Class C))"
by (rule length_cases2 [of _ s]) auto
lemma appGetStatic[simp]:
"app⇩i (Getstatic C F D,P,pc,mxs,T⇩r,s) =
(∃ vT ST LT. s = (ST, LT) ∧ length ST < mxs ∧ P ⊢ C sees F,Static:vT in D)"
by (rule length_cases2 [of _ s]) auto
lemma appPutField[simp]:
"app⇩i (Putfield F C,P,pc,mxs,T⇩r,s) =
(∃ vT vT' oT ST LT. s = (vT#oT#ST, LT) ∧
P ⊢ C sees F,NonStatic:vT' in C ∧ P ⊢ oT ≤ (Class C) ∧ P ⊢ vT ≤ vT')"
by (rule length_cases4 [of _ s], auto)
lemma appPutstatic[simp]:
"app⇩i (Putstatic C F D,P,pc,mxs,T⇩r,s) =
(∃ vT vT' ST LT. s = (vT#ST, LT) ∧
P ⊢ C sees F,Static:vT' in D ∧ P ⊢ vT ≤ vT')"
by (rule length_cases4 [of _ s], auto)
lemma appNew[simp]:
"app⇩i (New C,P,pc,mxs,T⇩r,s) =
(∃ST LT. s=(ST,LT) ∧ is_class P C ∧ length ST < mxs)"
by (cases s, simp)
lemma appCheckcast[simp]:
"app⇩i (Checkcast C,P,pc,mxs,T⇩r,s) =
(∃T ST LT. s = (T#ST,LT) ∧ is_class P C ∧ is_refT T)"
by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto)
lemma app⇩iPop[simp]:
"app⇩i (Pop,P,pc,mxs,T⇩r,s) = (∃ts ST LT. s = (ts#ST,LT))"
by (rule length_cases2, auto)
lemma appIAdd[simp]:
"app⇩i (IAdd,P,pc,mxs,T⇩r,s) = (∃ST LT. s = (Integer#Integer#ST,LT))"
proof -
obtain ST LT where [simp]: "s = (ST,LT)" by (cases s)
have "ST = [] ∨ (∃T. ST = [T]) ∨ (∃T⇩1 T⇩2 ST'. ST = T⇩1#T⇩2#ST')"
by (cases ST, auto, case_tac list, auto)
moreover
{ assume "ST = []" hence ?thesis by simp }
moreover
{ fix T assume "ST = [T]" hence ?thesis by (cases T, auto) }
moreover
{ fix T⇩1 T⇩2 ST' assume "ST = T⇩1#T⇩2#ST'"
hence ?thesis by (cases T⇩1, auto)
}
ultimately show ?thesis by blast
qed
lemma appIfFalse [simp]:
"app⇩i (IfFalse b,P,pc,mxs,T⇩r,s) =
(∃ST LT. s = (Boolean#ST,LT) ∧ 0 ≤ int pc + b)"
(is "?P s")
proof(rule length_cases2)
fix LT show "?P ([],LT)" by simp
next
fix l ST LT show "?P (l#ST,LT)"
by (case_tac l) auto
qed
lemma appCmpEq[simp]:
"app⇩i (CmpEq,P,pc,mxs,T⇩r,s) =
(∃T⇩1 T⇩2 ST LT. s = (T⇩1#T⇩2#ST,LT) ∧ (¬is_refT T⇩1 ∧ T⇩2 = T⇩1 ∨ is_refT T⇩1 ∧ is_refT T⇩2))"
by (rule length_cases4, auto)
lemma appReturn[simp]:
"app⇩i (Return,P,pc,mxs,T⇩r,s) = (∃T ST LT. s = (T#ST,LT) ∧ P ⊢ T ≤ T⇩r)"
by (rule length_cases2, auto)
lemma appThrow[simp]:
"app⇩i (Throw,P,pc,mxs,T⇩r,s) = (∃T ST LT. s=(T#ST,LT) ∧ is_refT T)"
by (rule length_cases2, auto)
lemma effNone:
"(pc', s') ∈ set (eff i P pc et None) ⟹ s' = None"
by (auto simp add: eff_def xcpt_eff_def norm_eff_def)
text ‹ some helpers to make the specification directly executable: ›
lemma relevant_entries_append [simp]:
"relevant_entries P i pc (xt @ xt') = relevant_entries P i pc xt @ relevant_entries P i pc xt'"
by (unfold relevant_entries_def) simp
lemma xcpt_app_append [iff]:
"xcpt_app i P pc mxs (xt@xt') τ = (xcpt_app i P pc mxs xt τ ∧ xcpt_app i P pc mxs xt' τ)"
by (unfold xcpt_app_def) fastforce
lemma xcpt_eff_append [simp]:
"xcpt_eff i P pc τ (xt@xt') = xcpt_eff i P pc τ xt @ xcpt_eff i P pc τ xt'"
by (unfold xcpt_eff_def, cases τ) simp
lemma app_append [simp]:
"app i P pc T mxs mpc (xt@xt') τ = (app i P pc T mxs mpc xt τ ∧ app i P pc T mxs mpc xt' τ)"
by (unfold app_def eff_def) auto
end