Commit d9e142c4 authored by nipkow's avatar nipkow
Browse files

New entry JinjaDCI

parent dd8e0cdca49e
......@@ -10020,3 +10020,16 @@ abstract =
CopyBuffer for arbitrary data and the Dijkstra's Dining
Philosopher Problem of arbitrary size.
 
[JinjaDCI]
title = JinjaDCI: a Java semantics with dynamic class initialization
author = Susannah Mansky <mailto:sjohnsn2@illinois.edu>
topic = Computer science/Programming languages/Language definitions
date = 2021-01-11
notify = sjohnsn2@illinois.edu, susannahej@gmail.com
abstract =
We extend Jinja to include static fields, methods, and instructions,
and dynamic class initialization, based on the Java SE 8
specification. This includes extension of definitions and proofs. This
work is partially described in Mansky and Gunter's paper at CPP
2019 and Mansky's doctoral thesis (UIUC, 2020).
(* Title: JinjaDCI/BV/BVConform.thy
Author: Cornelia Pusch, Gerwin Klein, Susannah Mansky
Copyright 1999 Technische Universitaet Muenchen, 2019-20 UIUC
Based on the Jinja theory BV/BVConform.thy by Cornelia Pusch and Gerwin Klein
The invariant for the type safety proof.
*)
section \<open> BV Type Safety Invariant \<close>
theory BVConform
imports BVSpec "../JVM/JVMExec" "../Common/Conform"
begin
subsection \<open> @{text "correct_state"} definitions \<close>
definition confT :: "'c prog \<Rightarrow> heap \<Rightarrow> val \<Rightarrow> ty err \<Rightarrow> bool"
("_,_ \<turnstile> _ :\<le>\<^sub>\<top> _" [51,51,51,51] 50)
where
"P,h \<turnstile> v :\<le>\<^sub>\<top> E \<equiv> case E of Err \<Rightarrow> True | OK T \<Rightarrow> P,h \<turnstile> v :\<le> T"
notation (ASCII)
confT ("_,_ |- _ :<=T _" [51,51,51,51] 50)
abbreviation
confTs :: "'c prog \<Rightarrow> heap \<Rightarrow> val list \<Rightarrow> ty\<^sub>l \<Rightarrow> bool"
("_,_ \<turnstile> _ [:\<le>\<^sub>\<top>] _" [51,51,51,51] 50) where
"P,h \<turnstile> vs [:\<le>\<^sub>\<top>] Ts \<equiv> list_all2 (confT P h) vs Ts"
notation (ASCII)
confTs ("_,_ |- _ [:<=T] _" [51,51,51,51] 50)
fun Called_context :: "jvm_prog \<Rightarrow> cname \<Rightarrow> instr \<Rightarrow> bool" where
"Called_context P C\<^sub>0 (New C') = (C\<^sub>0=C')" |
"Called_context P C\<^sub>0 (Getstatic C F D) = ((C\<^sub>0=D) \<and> (\<exists>t. P \<turnstile> C has F,Static:t in D))" |
"Called_context P C\<^sub>0 (Putstatic C F D) = ((C\<^sub>0=D) \<and> (\<exists>t. P \<turnstile> C has F,Static:t in D))" |
"Called_context P C\<^sub>0 (Invokestatic C M n)
= (\<exists>Ts T m D. (C\<^sub>0=D) \<and> P \<turnstile> C sees M,Static:Ts \<rightarrow> T = m in D)" |
"Called_context P _ _ = False"
abbreviation Called_set :: "instr set" where
"Called_set \<equiv> {i. \<exists>C. i = New C} \<union> {i. \<exists>C M n. i = Invokestatic C M n}
\<union> {i. \<exists>C F D. i = Getstatic C F D} \<union> {i. \<exists>C F D. i = Putstatic C F D}"
lemma Called_context_Called_set:
"Called_context P D i \<Longrightarrow> i \<in> Called_set" by(cases i, auto)
fun valid_ics :: "jvm_prog \<Rightarrow> heap \<Rightarrow> sheap \<Rightarrow> cname \<times> mname \<times> pc \<times> init_call_status \<Rightarrow> bool"
("_,_,_ \<turnstile>\<^sub>i _" [51,51,51,51] 50) where
"valid_ics P h sh (C,M,pc,Calling C' Cs)
= (let ins = instrs_of P C M in Called_context P (last (C'#Cs)) (ins!pc)
\<and> is_class P C')" |
"valid_ics P h sh (C,M,pc,Throwing Cs a)
=(let ins = instrs_of P C M in \<exists>C1. Called_context P C1 (ins!pc)
\<and> (\<exists>obj. h a = Some obj))" |
"valid_ics P h sh (C,M,pc,Called Cs)
= (let ins = instrs_of P C M
in \<exists>C1 sobj. Called_context P C1 (ins!pc) \<and> sh C1 = Some sobj)" |
"valid_ics P _ _ _ = True"
definition conf_f :: "jvm_prog \<Rightarrow> heap \<Rightarrow> sheap \<Rightarrow> ty\<^sub>i \<Rightarrow> bytecode \<Rightarrow> frame \<Rightarrow> bool"
where
"conf_f P h sh \<equiv> \<lambda>(ST,LT) is (stk,loc,C,M,pc,ics).
P,h \<turnstile> stk [:\<le>] ST \<and> P,h \<turnstile> loc [:\<le>\<^sub>\<top>] LT \<and> pc < size is \<and> P,h,sh \<turnstile>\<^sub>i (C,M,pc,ics)"
lemma conf_f_def2:
"conf_f P h sh (ST,LT) is (stk,loc,C,M,pc,ics) \<equiv>
P,h \<turnstile> stk [:\<le>] ST \<and> P,h \<turnstile> loc [:\<le>\<^sub>\<top>] LT \<and> pc < size is \<and> P,h,sh \<turnstile>\<^sub>i (C,M,pc,ics)"
by (simp add: conf_f_def)
primrec conf_fs :: "[jvm_prog,heap,sheap,ty\<^sub>P,cname,mname,nat,ty,frame list] \<Rightarrow> bool"
where
"conf_fs P h sh \<Phi> C\<^sub>0 M\<^sub>0 n\<^sub>0 T\<^sub>0 [] = True"
| "conf_fs P h sh \<Phi> C\<^sub>0 M\<^sub>0 n\<^sub>0 T\<^sub>0 (f#frs) =
(let (stk,loc,C,M,pc,ics) = f in
(\<exists>ST LT b Ts T mxs mxl\<^sub>0 is xt.
\<Phi> C M ! pc = Some (ST,LT) \<and>
(P \<turnstile> C sees M,b:Ts \<rightarrow> T = (mxs,mxl\<^sub>0,is,xt) in C) \<and>
((\<exists>D Ts' T' m D'. M\<^sub>0 \<noteq> clinit \<and> ics = No_ics \<and>
is!pc = Invoke M\<^sub>0 n\<^sub>0 \<and> ST!n\<^sub>0 = Class D \<and>
P \<turnstile> D sees M\<^sub>0,NonStatic:Ts' \<rightarrow> T' = m in D' \<and> P \<turnstile> C\<^sub>0 \<preceq>\<^sup>* D' \<and> P \<turnstile> T\<^sub>0 \<le> T') \<or>
(\<exists>D Ts' T' m. M\<^sub>0 \<noteq> clinit \<and> ics = No_ics \<and>
is!pc = Invokestatic D M\<^sub>0 n\<^sub>0 \<and>
P \<turnstile> D sees M\<^sub>0,Static:Ts' \<rightarrow> T' = m in C\<^sub>0 \<and> P \<turnstile> T\<^sub>0 \<le> T') \<or>
(M\<^sub>0 = clinit \<and> (\<exists>Cs. ics = Called Cs))) \<and>
conf_f P h sh (ST, LT) is f \<and> conf_fs P h sh \<Phi> C M (size Ts) T frs))"
fun ics_classes :: "init_call_status \<Rightarrow> cname list" where
"ics_classes (Calling C Cs) = Cs" |
"ics_classes (Throwing Cs a) = Cs" |
"ics_classes (Called Cs) = Cs" |
"ics_classes _ = []"
fun frame_clinit_classes :: "frame \<Rightarrow> cname list" where
"frame_clinit_classes (stk,loc,C,M,pc,ics) = (if M=clinit then [C] else []) @ ics_classes ics"
abbreviation clinit_classes :: "frame list \<Rightarrow> cname list" where
"clinit_classes frs \<equiv> concat (map frame_clinit_classes frs)"
definition distinct_clinit :: "frame list \<Rightarrow> bool" where
"distinct_clinit frs \<equiv> distinct (clinit_classes frs)"
definition conf_clinit :: "jvm_prog \<Rightarrow> sheap \<Rightarrow> frame list \<Rightarrow> bool" where
"conf_clinit P sh frs
\<equiv> distinct_clinit frs \<and>
(\<forall>C \<in> set(clinit_classes frs). is_class P C \<and> (\<exists>sfs. sh C = Some(sfs, Processing)))"
(*************************)
definition correct_state :: "[jvm_prog,ty\<^sub>P,jvm_state] \<Rightarrow> bool" ("_,_ \<turnstile> _ \<surd>" [61,0,0] 61)
where
"correct_state P \<Phi> \<equiv> \<lambda>(xp,h,frs,sh).
case xp of
None \<Rightarrow> (case frs of
[] \<Rightarrow> True
| (f#fs) \<Rightarrow> P\<turnstile> h\<surd> \<and> P,h\<turnstile>\<^sub>s sh\<surd> \<and> conf_clinit P sh frs \<and>
(let (stk,loc,C,M,pc,ics) = f
in \<exists>b Ts T mxs mxl\<^sub>0 is xt \<tau>.
(P \<turnstile> C sees M,b:Ts\<rightarrow>T = (mxs,mxl\<^sub>0,is,xt) in C) \<and>
\<Phi> C M ! pc = Some \<tau> \<and>
conf_f P h sh \<tau> is f \<and> conf_fs P h sh \<Phi> C M (size Ts) T fs))
| Some x \<Rightarrow> frs = []"
notation
correct_state ("_,_ |- _ [ok]" [61,0,0] 61)
subsection \<open> Values and @{text "\<top>"} \<close>
lemma confT_Err [iff]: "P,h \<turnstile> x :\<le>\<^sub>\<top> Err"
by (simp add: confT_def)
lemma confT_OK [iff]: "P,h \<turnstile> x :\<le>\<^sub>\<top> OK T = (P,h \<turnstile> x :\<le> T)"
by (simp add: confT_def)
lemma confT_cases:
"P,h \<turnstile> x :\<le>\<^sub>\<top> X = (X = Err \<or> (\<exists>T. X = OK T \<and> P,h \<turnstile> x :\<le> T))"
by (cases X) auto
lemma confT_hext [intro?, trans]:
"\<lbrakk> P,h \<turnstile> x :\<le>\<^sub>\<top> T; h \<unlhd> h' \<rbrakk> \<Longrightarrow> P,h' \<turnstile> x :\<le>\<^sub>\<top> T"
by (cases T) (blast intro: conf_hext)+
lemma confT_widen [intro?, trans]:
"\<lbrakk> P,h \<turnstile> x :\<le>\<^sub>\<top> T; P \<turnstile> T \<le>\<^sub>\<top> T' \<rbrakk> \<Longrightarrow> P,h \<turnstile> x :\<le>\<^sub>\<top> T'"
by (cases T', auto intro: conf_widen)
subsection \<open> Stack and Registers \<close>
lemmas confTs_Cons1 [iff] = list_all2_Cons1 [of "confT P h"] for P h
lemma confTs_confT_sup:
"\<lbrakk> P,h \<turnstile> loc [:\<le>\<^sub>\<top>] LT; n < size LT; LT!n = OK T; P \<turnstile> T \<le> T' \<rbrakk>
\<Longrightarrow> P,h \<turnstile> (loc!n) :\<le> T'"
(*<*)
apply (frule list_all2_lengthD)
apply (drule list_all2_nthD, simp)
apply simp
apply (erule conf_widen, assumption+)
done
(*>*)
lemma confTs_hext [intro?]:
"P,h \<turnstile> loc [:\<le>\<^sub>\<top>] LT \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> P,h' \<turnstile> loc [:\<le>\<^sub>\<top>] LT"
by (fast elim: list_all2_mono confT_hext)
lemma confTs_widen [intro?, trans]:
"P,h \<turnstile> loc [:\<le>\<^sub>\<top>] LT \<Longrightarrow> P \<turnstile> LT [\<le>\<^sub>\<top>] LT' \<Longrightarrow> P,h \<turnstile> loc [:\<le>\<^sub>\<top>] LT'"
by (rule list_all2_trans, rule confT_widen)
lemma confTs_map [iff]:
"\<And>vs. (P,h \<turnstile> vs [:\<le>\<^sub>\<top>] map OK Ts) = (P,h \<turnstile> vs [:\<le>] Ts)"
by (induct Ts) (auto simp: list_all2_Cons2)
lemma reg_widen_Err [iff]:
"\<And>LT. (P \<turnstile> replicate n Err [\<le>\<^sub>\<top>] LT) = (LT = replicate n Err)"
by (induct n) (auto simp: list_all2_Cons1)
lemma confTs_Err [iff]:
"P,h \<turnstile> replicate n v [:\<le>\<^sub>\<top>] replicate n Err"
by (induct n) auto
subsection \<open> valid @{text "init_call_status"} \<close>
lemma valid_ics_shupd:
assumes "P,h,sh \<turnstile>\<^sub>i (C, M, pc, ics)" and "distinct (C'#ics_classes ics)"
shows "P,h,sh(C' \<mapsto> (sfs, i')) \<turnstile>\<^sub>i (C, M, pc, ics)"
using assms by(cases ics; clarsimp simp: fun_upd_apply) fastforce
subsection \<open> correct-frame \<close>
lemma conf_f_Throwing:
assumes "conf_f P h sh (ST, LT) is (stk, loc, C, M, pc, Called Cs)"
and "is_class P C'" and "h xcp = Some obj" and "sh C' = Some(sfs,Processing)"
shows "conf_f P h sh (ST, LT) is (stk, loc, C, M, pc, Throwing (C' # Cs) xcp)"
using assms by(auto simp: conf_f_def2)
lemma conf_f_shupd:
assumes "conf_f P h sh (ST,LT) ins f"
and "i = Processing
\<or> (distinct (C#ics_classes (ics_of f)) \<and> (curr_method f = clinit \<longrightarrow> C \<noteq> curr_class f))"
shows "conf_f P h (sh(C \<mapsto> (sfs, i))) (ST,LT) ins f"
using assms
by(cases f, cases "ics_of f"; clarsimp simp: conf_f_def2 fun_upd_apply) fastforce+
lemma conf_f_shupd':
assumes "conf_f P h sh (ST,LT) ins f"
and "sh C = Some(sfs,i)"
shows "conf_f P h (sh(C \<mapsto> (sfs', i))) (ST,LT) ins f"
using assms
by(cases f, cases "ics_of f"; clarsimp simp: conf_f_def2 fun_upd_apply) fastforce+
subsection \<open> correct-frames \<close>
lemmas [simp del] = fun_upd_apply
lemma conf_fs_hext:
"\<And>C M n T\<^sub>r.
\<lbrakk> conf_fs P h sh \<Phi> C M n T\<^sub>r frs; h \<unlhd> h' \<rbrakk> \<Longrightarrow> conf_fs P h' sh \<Phi> C M n T\<^sub>r frs"
(*<*)
apply (induct frs)
apply simp
apply clarify
apply (simp (no_asm_use))
apply clarify
apply (unfold conf_f_def)
apply (simp (no_asm_use))
apply clarify
apply (fastforce elim!: confs_hext confTs_hext)
done
(*>*)
lemma conf_fs_shupd:
assumes "conf_fs P h sh \<Phi> C\<^sub>0 M n T frs"
and dist: "distinct (C#clinit_classes frs)"
shows "conf_fs P h (sh(C \<mapsto> (sfs, i))) \<Phi> C\<^sub>0 M n T frs"
using assms proof(induct frs arbitrary: C\<^sub>0 C M n T)
case (Cons f' frs')
then obtain stk' loc' C' M' pc' ics' where f': "f' = (stk',loc',C',M',pc',ics')" by(cases f')
with assms Cons obtain ST LT b Ts T1 mxs mxl\<^sub>0 ins xt where
ty: "\<Phi> C' M' ! pc' = Some (ST,LT)" and
meth: "P \<turnstile> C' sees M',b:Ts \<rightarrow> T1 = (mxs,mxl\<^sub>0,ins,xt) in C'" and
conf: "conf_f P h sh (ST, LT) ins f'" and
confs: "conf_fs P h sh \<Phi> C' M' (size Ts) T1 frs'" by clarsimp
from f' Cons.prems(2) have
"distinct (C#ics_classes (ics_of f')) \<and> (curr_method f' = clinit \<longrightarrow> C \<noteq> curr_class f')"
by fastforce
with conf_f_shupd[where C=C, OF conf] have
conf': "conf_f P h (sh(C \<mapsto> (sfs, i))) (ST, LT) ins f'" by simp
from Cons.prems(2) have dist': "distinct (C # clinit_classes frs')"
by(auto simp: distinct_length_2_or_more)
from Cons.hyps[OF confs dist'] have
confs': "conf_fs P h (sh(C \<mapsto> (sfs, i))) \<Phi> C' M' (length Ts) T1 frs'" by simp
from conf' confs' ty meth f' Cons.prems show ?case by(fastforce dest: sees_method_fun)
qed(simp)
lemma conf_fs_shupd':
assumes "conf_fs P h sh \<Phi> C\<^sub>0 M n T frs"
and shC: "sh C = Some(sfs,i)"
shows "conf_fs P h (sh(C \<mapsto> (sfs', i))) \<Phi> C\<^sub>0 M n T frs"
using assms proof(induct frs arbitrary: C\<^sub>0 C M n T sfs i sfs')
case (Cons f' frs')
then obtain stk' loc' C' M' pc' ics' where f': "f' = (stk',loc',C',M',pc',ics')" by(cases f')
with assms Cons obtain ST LT b Ts T1 mxs mxl\<^sub>0 ins xt where
ty: "\<Phi> C' M' ! pc' = Some (ST,LT)" and
meth: "P \<turnstile> C' sees M',b:Ts \<rightarrow> T1 = (mxs,mxl\<^sub>0,ins,xt) in C'" and
conf: "conf_f P h sh (ST, LT) ins f'" and
confs: "conf_fs P h sh \<Phi> C' M' (size Ts) T1 frs'" and
shC': "sh C = Some(sfs,i)" by clarsimp
have conf': "conf_f P h (sh(C \<mapsto> (sfs', i))) (ST, LT) ins f'" by(rule conf_f_shupd'[OF conf shC'])
from Cons.hyps[OF confs shC'] have
confs': "conf_fs P h (sh(C \<mapsto> (sfs', i))) \<Phi> C' M' (length Ts) T1 frs'" by simp
from conf' confs' ty meth f' Cons.prems show ?case by(fastforce dest: sees_method_fun)
qed(simp)
subsection \<open> correctness wrt @{term clinit} use \<close>
lemma conf_clinit_Cons:
assumes "conf_clinit P sh (f#frs)"
shows "conf_clinit P sh frs"
proof -
from assms have dist: "distinct_clinit (f#frs)"
by(cases "curr_method f = clinit", auto simp: conf_clinit_def)
then have dist': "distinct_clinit frs" by(simp add: distinct_clinit_def)
with assms show ?thesis by(cases frs; fastforce simp: conf_clinit_def)
qed
lemma conf_clinit_Cons_Cons:
"conf_clinit P sh (f'#f#frs) \<Longrightarrow> conf_clinit P sh (f'#frs)"
by(auto simp: conf_clinit_def distinct_clinit_def)
lemma conf_clinit_diff:
assumes "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)"
shows "conf_clinit P sh ((stk',loc',C,M,pc',ics)#frs)"
using assms by(cases "M = clinit", simp_all add: conf_clinit_def distinct_clinit_def)
lemma conf_clinit_diff':
assumes "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)"
shows "conf_clinit P sh ((stk',loc',C,M,pc',No_ics)#frs)"
using assms by(cases "M = clinit", simp_all add: conf_clinit_def distinct_clinit_def)
lemma conf_clinit_Called_Throwing:
"conf_clinit P sh ((stk', loc', C', clinit, pc', ics') # (stk, loc, C, M, pc, Called Cs) # fs)
\<Longrightarrow> conf_clinit P sh ((stk, loc, C, M, pc, Throwing (C' # Cs) xcp) # fs)"
by(simp add: conf_clinit_def distinct_clinit_def)
lemma conf_clinit_Throwing:
"conf_clinit P sh ((stk, loc, C, M, pc, Throwing (C'#Cs) xcp) # fs)
\<Longrightarrow> conf_clinit P sh ((stk, loc, C, M, pc, Throwing Cs xcp) # fs)"
by(simp add: conf_clinit_def distinct_clinit_def)
lemma conf_clinit_Called:
"\<lbrakk> conf_clinit P sh ((stk, loc, C, M, pc, Called (C'#Cs)) # frs);
P \<turnstile> C' sees clinit,Static: [] \<rightarrow> Void=(mxs',mxl',ins',xt') in C' \<rbrakk>
\<Longrightarrow> conf_clinit P sh (create_init_frame P C' # (stk, loc, C, M, pc, Called Cs) # frs)"
by(simp add: conf_clinit_def distinct_clinit_def)
lemma conf_clinit_Cons_nclinit:
assumes "conf_clinit P sh frs" and nclinit: "M \<noteq> clinit"
shows "conf_clinit P sh ((stk, loc, C, M, pc, No_ics) # frs)"
proof -
from nclinit
have "clinit_classes ((stk, loc, C, M, pc, No_ics) # frs) = clinit_classes frs" by simp
with assms show ?thesis by(simp add: conf_clinit_def distinct_clinit_def)
qed
lemma conf_clinit_Invoke:
assumes "conf_clinit P sh ((stk, loc, C, M, pc, ics) # frs)" and "M' \<noteq> clinit"
shows "conf_clinit P sh ((stk', loc', C', M', pc', No_ics) # (stk, loc, C, M, pc, No_ics) # frs)"
using assms conf_clinit_Cons_nclinit conf_clinit_diff' by auto
lemma conf_clinit_nProc_dist:
assumes "conf_clinit P sh frs"
and "\<forall>sfs. sh C \<noteq> Some(sfs,Processing)"
shows "distinct (C # clinit_classes frs)"
using assms by(auto simp: conf_clinit_def distinct_clinit_def)
lemma conf_clinit_shupd:
assumes "conf_clinit P sh frs"
and dist: "distinct (C#clinit_classes frs)"
shows "conf_clinit P (sh(C \<mapsto> (sfs, i))) frs"
using assms by(simp add: conf_clinit_def fun_upd_apply)
lemma conf_clinit_shupd':
assumes "conf_clinit P sh frs"
and "sh C = Some(sfs,i)"
shows "conf_clinit P (sh(C \<mapsto> (sfs', i))) frs"
using assms by(fastforce simp: conf_clinit_def fun_upd_apply)
lemma conf_clinit_shupd_Called:
assumes "conf_clinit P sh ((stk,loc,C,M,pc,Calling C' Cs)#frs)"
and dist: "distinct (C'#clinit_classes ((stk,loc,C,M,pc,Calling C' Cs)#frs))"
and cls: "is_class P C'"
shows "conf_clinit P (sh(C' \<mapsto> (sfs, Processing))) ((stk,loc,C,M,pc,Called (C'#Cs))#frs)"
using assms by(clarsimp simp: conf_clinit_def fun_upd_apply distinct_clinit_def)
lemma conf_clinit_shupd_Calling:
assumes "conf_clinit P sh ((stk,loc,C,M,pc,Calling C' Cs)#frs)"
and dist: "distinct (C'#clinit_classes ((stk,loc,C,M,pc,Calling C' Cs)#frs))"
and cls: "is_class P C'"
shows "conf_clinit P (sh(C' \<mapsto> (sfs, Processing)))
((stk,loc,C,M,pc,Calling (fst(the(class P C'))) (C'#Cs))#frs)"
using assms by(clarsimp simp: conf_clinit_def fun_upd_apply distinct_clinit_def)
subsection \<open> correct state \<close>
lemma correct_state_Cons:
assumes cr: "P,\<Phi> |- (xp,h,f#frs,sh) [ok]"
shows "P,\<Phi> |- (xp,h,frs,sh) [ok]"
proof -
from cr have dist: "conf_clinit P sh (f#frs)"
by(simp add: correct_state_def)
then have "conf_clinit P sh frs" by(rule conf_clinit_Cons)
with cr show ?thesis by(cases frs; fastforce simp: correct_state_def)
qed
lemma correct_state_shupd:
assumes cs: "P,\<Phi> |- (xp,h,frs,sh) [ok]" and shC: "sh C = Some(sfs,i)"
and dist: "distinct (C#clinit_classes frs)"
shows "P,\<Phi> |- (xp,h,frs,sh(C \<mapsto> (sfs, i'))) [ok]"
using assms
proof(cases xp)
case None with assms show ?thesis
proof(cases frs)
case (Cons f' frs')
let ?sh = "sh(C \<mapsto> (sfs, i'))"
obtain stk' loc' C' M' pc' ics' where f': "f' = (stk',loc',C',M',pc',ics')" by(cases f')
with cs Cons None obtain b Ts T mxs mxl\<^sub>0 ins xt ST LT where
meth: "P \<turnstile> C' sees M',b:Ts\<rightarrow>T = (mxs,mxl\<^sub>0,ins,xt) in C'"
and ty: "\<Phi> C' M' ! pc' = Some (ST,LT)" and conf: "conf_f P h sh (ST,LT) ins f'"
and confs: "conf_fs P h sh \<Phi> C' M' (size Ts) T frs'"
and confc: "conf_clinit P sh frs"
and h_ok: "P\<turnstile> h\<surd>" and sh_ok: "P,h \<turnstile>\<^sub>s sh \<surd>"
by(auto simp: correct_state_def)
from Cons dist have dist': "distinct (C#clinit_classes frs')"
by(auto simp: distinct_length_2_or_more)
from shconf_upd_obj[OF sh_ok shconfD[OF sh_ok shC]] have sh_ok': "P,h \<turnstile>\<^sub>s ?sh \<surd>"
by simp
from conf f' valid_ics_shupd Cons dist have conf': "conf_f P h ?sh (ST,LT) ins f'"
by(auto simp: conf_f_def2 fun_upd_apply)
have confs': "conf_fs P h ?sh \<Phi> C' M' (size Ts) T frs'" by(rule conf_fs_shupd[OF confs dist'])
have confc': "conf_clinit P ?sh frs" by(rule conf_clinit_shupd[OF confc dist])
with h_ok sh_ok' meth ty conf' confs' f' Cons None show ?thesis
by(fastforce simp: correct_state_def)
qed(simp add: correct_state_def)
qed(simp add: correct_state_def)
lemma correct_state_Throwing_ex:
assumes correct: "P,\<Phi> \<turnstile> (xp,h,(stk,loc,C,M,pc,ics)#frs,sh)\<surd>"
shows "\<And>Cs a. ics = Throwing Cs a \<Longrightarrow> \<exists>obj. h a = Some obj"
using correct by(clarsimp simp: correct_state_def conf_f_def)
end
This diff is collapsed.
(* Title: JinjaDCI/BV/BVExec.thy
Author: Tobias Nipkow, Gerwin Klein, Susannah Mansky
Copyright 2000 TUM, 2020 UIUC
Based on the Jinja theory BV/BVExec.thy by Tobias Nipkow and Gerwin Klein
*)
section \<open> Kildall for the JVM \label{sec:JVM} \<close>
theory BVExec
imports Jinja.Abstract_BV TF_JVM
begin
definition kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow>
instr list \<Rightarrow> ex_table \<Rightarrow> ty\<^sub>i' err list \<Rightarrow> ty\<^sub>i' err list"
where
"kiljvm P mxs mxl T\<^sub>r is xt \<equiv>
kildall (JVM_SemiType.le P mxs mxl) (JVM_SemiType.sup P mxs mxl)
(exec P mxs T\<^sub>r xt is)"
definition wt_kildall :: "jvm_prog \<Rightarrow> cname \<Rightarrow> staticb \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
instr list \<Rightarrow> ex_table \<Rightarrow> bool"
where
"wt_kildall P C' b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<equiv>
0 < size is \<and>
(let first = Some ([],(case b of Static \<Rightarrow> [] | NonStatic \<Rightarrow> [OK (Class C')])
@(map OK Ts)@(replicate mxl\<^sub>0 Err));
start = (OK first)#(replicate (size is - 1) (OK None));
result = kiljvm P mxs
((case b of Static \<Rightarrow> 0 | NonStatic \<Rightarrow> 1)+size Ts+mxl\<^sub>0)
T\<^sub>r is xt start
in \<forall>n < size is. result!n \<noteq> Err)"
definition wf_jvm_prog\<^sub>k :: "jvm_prog \<Rightarrow> bool"
where
"wf_jvm_prog\<^sub>k P \<equiv>
wf_prog (\<lambda>P C' (M,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). wt_kildall P C' b Ts T\<^sub>r mxs mxl\<^sub>0 is xt) P"
theorem (in start_context) is_bcv_kiljvm:
"is_bcv r Err step (size is) A (kiljvm P mxs mxl T\<^sub>r is xt)"
(*<*)
apply (insert wf)
apply (unfold kiljvm_def)
apply (fold r_def f_def step_def_exec)
apply (rule is_bcv_kildall)
apply simp apply (rule Semilat.intro)
apply (fold sl_def2)
apply (erule semilat_JVM)
apply simp
apply blast
apply (simp add: JVM_le_unfold)
apply (rule exec_pres_type)
apply (rule bounded_step)
apply (erule step_mono)
done
(*>*)
(* FIXME: move? *)
lemma subset_replicate [intro?]: "set (replicate n x) \<subseteq> {x}"
by (induct n) auto
lemma in_set_replicate:
assumes "x \<in> set (replicate n y)"
shows "x = y"
(*<*)
proof -
note assms
also have "set (replicate n y) \<subseteq> {y}" ..
finally show ?thesis by simp
qed
(*>*)
lemma (in start_context) start_in_A [intro?]:
"0 < size is \<Longrightarrow> start \<in> list (size is) A"
using Ts C
(*<*)
apply (simp add: JVM_states_unfold)
apply (cases b; force intro!: listI list_appendI dest!: in_set_replicate)
done
(*>*)
theorem (in start_context) wt_kil_correct:
assumes wtk: "wt_kildall P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt"
shows "\<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
(*<*)
proof -
from wtk obtain res where
result: "res = kiljvm P mxs mxl T\<^sub>r is xt start" and
success: "\<forall>n < size is. res!n \<noteq> Err" and
instrs: "0 < size is"
by (unfold wt_kildall_def) simp
have bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl T\<^sub>r is xt)"
by (rule is_bcv_kiljvm)
from instrs have "start \<in> list (size is) A" ..
with bcv success result have
"\<exists>ts\<in>list (size is) A. start [\<sqsubseteq>\<^sub>r] ts \<and> wt_step r Err step ts"
by (unfold is_bcv_def) blast
then obtain \<tau>s' where
in_A: "\<tau>s' \<in> list (size is) A" and
s: "start [\<sqsubseteq>\<^sub>r] \<tau>s'" and
w: "wt_step r Err step \<tau>s'"
by blast
hence wt_err_step: "wt_err_step (sup_state_opt P) step \<tau>s'"
by (simp add: wt_err_step_def JVM_le_Err_conv)
from in_A have l: "size \<tau>s' = size is" by simp
moreover {
from in_A have "check_types P mxs mxl \<tau>s'" by (simp add: check_types_def)
also from w have "\<forall>x \<in> set \<tau>s'. x \<noteq> Err"
by (auto simp add: wt_step_def all_set_conv_all_nth)
hence [symmetric]: "map OK (map ok_val \<tau>s') = \<tau>s'"
by (auto intro!: map_idI simp add: wt_step_def)
finally have "check_types P mxs mxl (map OK (map ok_val \<tau>s'))" .
}
moreover {
from s have "start!0 \<sqsubseteq>\<^sub>r \<tau>s'!0" by (rule le_listD) simp
moreover
from instrs w l
have "\<tau>s'!0 \<noteq> Err" by (unfold wt_step_def) simp
then obtain \<tau>s0 where "\<tau>s'!0 = OK \<tau>s0" by auto
ultimately
have "wt_start P C b Ts mxl\<^sub>0 (map ok_val \<tau>s')" using l instrs
by (unfold wt_start_def)
(cases b; simp add: lesub_def JVM_le_Err_conv Err.le_def)
}
moreover
from in_A have "set \<tau>s' \<subseteq> A" by simp
with wt_err_step bounded_step
have "wt_app_eff (sup_state_opt P) app eff (map ok_val \<tau>s')"
by (auto intro: wt_err_imp_wt_app_eff simp add: l)
ultimately
have "wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (map ok_val \<tau>s')"
using instrs by (simp add: wt_method_def2 check_types_def del: map_map)
thus ?thesis by blast
qed
(*>*)
theorem (in start_context) wt_kil_complete:
assumes wtm: "wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
shows "wt_kildall P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt"
(*<*)
proof -
from wtm obtain
instrs: "0 < size is" and
length: "length \<tau>s = length is" and
ck_type: "check_types P mxs mxl (map OK \<tau>s)" and
wt_start: "wt_start P C b Ts mxl\<^sub>0 \<tau>s" and
app_eff: "wt_app_eff (sup_state_opt P) app eff \<tau>s"
by (simp add: wt_method_def2 check_types_def)
from ck_type
have in_A: "set (map OK \<tau>s) \<subseteq> A"
by (simp add: check_types_def)
with app_eff in_A bounded_step
have "wt_err_step (sup_state_opt P) (err_step (size \<tau>s) app eff) (map OK \<tau>s)"
by - (erule wt_app_eff_imp_wt_err,
auto simp add: exec_def length states_def)
hence wt_err: "wt_err_step (sup_state_opt P) step (map OK \<tau>s)"
by (simp add: length)
have is_bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl T\<^sub>r is xt)"
by (rule is_bcv_kiljvm)
moreover from instrs have "start \<in> list (size is) A" ..
moreover
let ?\<tau>s = "map OK \<tau>s"
have less_\<tau>s: "start [\<sqsubseteq>\<^sub>r] ?\<tau>s"
proof (rule le_listI)
from length instrs
show "length start = length (map OK \<tau>s)" by simp
next
fix n
from wt_start have "P \<turnstile> ok_val (start!0) \<le>' \<tau>s!0"
by (cases b; simp add: wt_start_def)
moreover from instrs length have "0 < length \<tau>s" by simp
ultimately have "start!0 \<sqsubseteq>\<^sub>r ?\<tau>s!0"
by (simp add: JVM_le_Err_conv lesub_def)
moreover {
fix n'
have "OK None \<sqsubseteq>\<^sub>r ?\<tau>s!n"
by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def
split: err.splits)
hence "\<lbrakk>n = Suc n'; n < size start\<rbrakk> \<Longrightarrow> start!n \<sqsubseteq>\<^sub>r ?\<tau>s!n" by simp