diff --git a/thys/JinjaDCI/BV/BVConform.thy b/thys/JinjaDCI/BV/BVConform.thy --- a/thys/JinjaDCI/BV/BVConform.thy +++ b/thys/JinjaDCI/BV/BVConform.thy @@ -1,431 +1,433 @@ (* 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 \ BV Type Safety Invariant \ theory BVConform imports BVSpec "../JVM/JVMExec" "../Common/Conform" begin subsection \ @{text "correct_state"} definitions \ definition confT :: "'c prog \ heap \ val \ ty err \ bool" ("_,_ \ _ :\\<^sub>\ _" [51,51,51,51] 50) where "P,h \ v :\\<^sub>\ E \ case E of Err \ True | OK T \ P,h \ v :\ T" notation (ASCII) confT ("_,_ |- _ :<=T _" [51,51,51,51] 50) abbreviation confTs :: "'c prog \ heap \ val list \ ty\<^sub>l \ bool" ("_,_ \ _ [:\\<^sub>\] _" [51,51,51,51] 50) where "P,h \ vs [:\\<^sub>\] Ts \ list_all2 (confT P h) vs Ts" notation (ASCII) confTs ("_,_ |- _ [:<=T] _" [51,51,51,51] 50) fun Called_context :: "jvm_prog \ cname \ instr \ 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) \ (\t. P \ C has F,Static:t in D))" | "Called_context P C\<^sub>0 (Putstatic C F D) = ((C\<^sub>0=D) \ (\t. P \ C has F,Static:t in D))" | "Called_context P C\<^sub>0 (Invokestatic C M n) = (\Ts T m D. (C\<^sub>0=D) \ P \ C sees M,Static:Ts \ T = m in D)" | "Called_context P _ _ = False" abbreviation Called_set :: "instr set" where "Called_set \ {i. \C. i = New C} \ {i. \C M n. i = Invokestatic C M n} \ {i. \C F D. i = Getstatic C F D} \ {i. \C F D. i = Putstatic C F D}" lemma Called_context_Called_set: "Called_context P D i \ i \ Called_set" by(cases i, auto) fun valid_ics :: "jvm_prog \ heap \ sheap \ cname \ mname \ pc \ init_call_status \ bool" ("_,_,_ \\<^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) \ is_class P C')" | "valid_ics P h sh (C,M,pc,Throwing Cs a) =(let ins = instrs_of P C M in \C1. Called_context P C1 (ins!pc) \ (\obj. h a = Some obj))" | "valid_ics P h sh (C,M,pc,Called Cs) = (let ins = instrs_of P C M in \C1 sobj. Called_context P C1 (ins!pc) \ sh C1 = Some sobj)" | "valid_ics P _ _ _ = True" definition conf_f :: "jvm_prog \ heap \ sheap \ ty\<^sub>i \ bytecode \ frame \ bool" where "conf_f P h sh \ \(ST,LT) is (stk,loc,C,M,pc,ics). P,h \ stk [:\] ST \ P,h \ loc [:\\<^sub>\] LT \ pc < size is \ P,h,sh \\<^sub>i (C,M,pc,ics)" lemma conf_f_def2: "conf_f P h sh (ST,LT) is (stk,loc,C,M,pc,ics) \ P,h \ stk [:\] ST \ P,h \ loc [:\\<^sub>\] LT \ pc < size is \ P,h,sh \\<^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] \ bool" where "conf_fs P h sh \ C\<^sub>0 M\<^sub>0 n\<^sub>0 T\<^sub>0 [] = True" | "conf_fs P h sh \ C\<^sub>0 M\<^sub>0 n\<^sub>0 T\<^sub>0 (f#frs) = (let (stk,loc,C,M,pc,ics) = f in (\ST LT b Ts T mxs mxl\<^sub>0 is xt. \ C M ! pc = Some (ST,LT) \ (P \ C sees M,b:Ts \ T = (mxs,mxl\<^sub>0,is,xt) in C) \ ((\D Ts' T' m D'. M\<^sub>0 \ clinit \ ics = No_ics \ is!pc = Invoke M\<^sub>0 n\<^sub>0 \ ST!n\<^sub>0 = Class D \ P \ D sees M\<^sub>0,NonStatic:Ts' \ T' = m in D' \ P \ C\<^sub>0 \\<^sup>* D' \ P \ T\<^sub>0 \ T') \ (\D Ts' T' m. M\<^sub>0 \ clinit \ ics = No_ics \ is!pc = Invokestatic D M\<^sub>0 n\<^sub>0 \ P \ D sees M\<^sub>0,Static:Ts' \ T' = m in C\<^sub>0 \ P \ T\<^sub>0 \ T') \ (M\<^sub>0 = clinit \ (\Cs. ics = Called Cs))) \ conf_f P h sh (ST, LT) is f \ conf_fs P h sh \ C M (size Ts) T frs))" fun ics_classes :: "init_call_status \ 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 \ 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 \ cname list" where "clinit_classes frs \ concat (map frame_clinit_classes frs)" definition distinct_clinit :: "frame list \ bool" where "distinct_clinit frs \ distinct (clinit_classes frs)" definition conf_clinit :: "jvm_prog \ sheap \ frame list \ bool" where "conf_clinit P sh frs \ distinct_clinit frs \ (\C \ set(clinit_classes frs). is_class P C \ (\sfs. sh C = Some(sfs, Processing)))" (*************************) definition correct_state :: "[jvm_prog,ty\<^sub>P,jvm_state] \ bool" ("_,_ \ _ \" [61,0,0] 61) where "correct_state P \ \ \(xp,h,frs,sh). case xp of None \ (case frs of [] \ True | (f#fs) \ P\ h\ \ P,h\\<^sub>s sh\ \ conf_clinit P sh frs \ (let (stk,loc,C,M,pc,ics) = f in \b Ts T mxs mxl\<^sub>0 is xt \. (P \ C sees M,b:Ts\T = (mxs,mxl\<^sub>0,is,xt) in C) \ \ C M ! pc = Some \ \ conf_f P h sh \ is f \ conf_fs P h sh \ C M (size Ts) T fs)) | Some x \ frs = []" notation correct_state ("_,_ |- _ [ok]" [61,0,0] 61) subsection \ Values and @{text "\"} \ lemma confT_Err [iff]: "P,h \ x :\\<^sub>\ Err" by (simp add: confT_def) lemma confT_OK [iff]: "P,h \ x :\\<^sub>\ OK T = (P,h \ x :\ T)" by (simp add: confT_def) lemma confT_cases: "P,h \ x :\\<^sub>\ X = (X = Err \ (\T. X = OK T \ P,h \ x :\ T))" by (cases X) auto lemma confT_hext [intro?, trans]: "\ P,h \ x :\\<^sub>\ T; h \ h' \ \ P,h' \ x :\\<^sub>\ T" by (cases T) (blast intro: conf_hext)+ lemma confT_widen [intro?, trans]: "\ P,h \ x :\\<^sub>\ T; P \ T \\<^sub>\ T' \ \ P,h \ x :\\<^sub>\ T'" by (cases T', auto intro: conf_widen) subsection \ Stack and Registers \ lemmas confTs_Cons1 [iff] = list_all2_Cons1 [of "confT P h"] for P h lemma confTs_confT_sup: - "\ P,h \ loc [:\\<^sub>\] LT; n < size LT; LT!n = OK T; P \ T \ T' \ - \ P,h \ (loc!n) :\ T'" +assumes confTs: "P,h \ loc [:\\<^sub>\] LT" and n: "n < size LT" and + LTn: "LT!n = OK T" and subtype: "P \ T \ T'" +shows "P,h \ (loc!n) :\ T'" (*<*) - apply (frule list_all2_lengthD) - apply (drule list_all2_nthD, simp) - apply simp - apply (erule conf_widen, assumption+) - done +proof - + have len: "n < length loc" using list_all2_lengthD[OF confTs] n + by simp + show ?thesis + using list_all2_nthD[OF confTs len] conf_widen[OF _ subtype] LTn + by simp +qed (*>*) lemma confTs_hext [intro?]: "P,h \ loc [:\\<^sub>\] LT \ h \ h' \ P,h' \ loc [:\\<^sub>\] LT" by (fast elim: list_all2_mono confT_hext) lemma confTs_widen [intro?, trans]: "P,h \ loc [:\\<^sub>\] LT \ P \ LT [\\<^sub>\] LT' \ P,h \ loc [:\\<^sub>\] LT'" by (rule list_all2_trans, rule confT_widen) lemma confTs_map [iff]: "\vs. (P,h \ vs [:\\<^sub>\] map OK Ts) = (P,h \ vs [:\] Ts)" by (induct Ts) (auto simp: list_all2_Cons2) lemma reg_widen_Err [iff]: "\LT. (P \ replicate n Err [\\<^sub>\] LT) = (LT = replicate n Err)" by (induct n) (auto simp: list_all2_Cons1) lemma confTs_Err [iff]: "P,h \ replicate n v [:\\<^sub>\] replicate n Err" by (induct n) auto subsection \ valid @{text "init_call_status"} \ lemma valid_ics_shupd: assumes "P,h,sh \\<^sub>i (C, M, pc, ics)" and "distinct (C'#ics_classes ics)" shows "P,h,sh(C' \ (sfs, i')) \\<^sub>i (C, M, pc, ics)" using assms by(cases ics; clarsimp simp: fun_upd_apply) fastforce subsection \ correct-frame \ 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 \ (distinct (C#ics_classes (ics_of f)) \ (curr_method f = clinit \ C \ curr_class f))" shows "conf_f P h (sh(C \ (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 \ (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 \ correct-frames \ lemmas [simp del] = fun_upd_apply lemma conf_fs_hext: "\C M n T\<^sub>r. \ conf_fs P h sh \ C M n T\<^sub>r frs; h \ h' \ \ conf_fs P h' sh \ 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 +proof(induct frs) + case (Cons fr frs) + obtain stk ls C M pc ics where fr: "fr = (stk, ls, C, M, pc, ics)" by(cases fr) simp + moreover obtain ST LT where \: "\ C M ! pc = \(ST, LT)\" and + ST: "P,h \ stk [:\] ST" and LT: "P,h \ ls [:\\<^sub>\] LT" + using Cons.prems(1) fr by(auto simp: conf_f_def) + ultimately show ?case using Cons confs_hext[OF ST Cons(3)] confTs_hext[OF LT Cons(3)] + by (fastforce simp: conf_f_def) +qed simp (*>*) lemma conf_fs_shupd: assumes "conf_fs P h sh \ C\<^sub>0 M n T frs" and dist: "distinct (C#clinit_classes frs)" shows "conf_fs P h (sh(C \ (sfs, i))) \ 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: "\ C' M' ! pc' = Some (ST,LT)" and meth: "P \ C' sees M',b:Ts \ 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 \ C' M' (size Ts) T1 frs'" by clarsimp from f' Cons.prems(2) have "distinct (C#ics_classes (ics_of f')) \ (curr_method f' = clinit \ C \ curr_class f')" by fastforce with conf_f_shupd[where C=C, OF conf] have conf': "conf_f P h (sh(C \ (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 \ (sfs, i))) \ 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 \ C\<^sub>0 M n T frs" and shC: "sh C = Some(sfs,i)" shows "conf_fs P h (sh(C \ (sfs', i))) \ 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: "\ C' M' ! pc' = Some (ST,LT)" and meth: "P \ C' sees M',b:Ts \ 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 \ C' M' (size Ts) T1 frs'" and shC': "sh C = Some(sfs,i)" by clarsimp have conf': "conf_f P h (sh(C \ (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 \ (sfs', i))) \ 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 \ correctness wrt @{term clinit} use \ 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) \ 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) \ 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) \ 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: "\ conf_clinit P sh ((stk, loc, C, M, pc, Called (C'#Cs)) # frs); P \ C' sees clinit,Static: [] \ Void=(mxs',mxl',ins',xt') in C' \ \ 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 \ 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' \ 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 "\sfs. sh C \ 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 \ (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 \ (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' \ (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' \ (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 \ correct state \ lemma correct_state_Cons: assumes cr: "P,\ |- (xp,h,f#frs,sh) [ok]" shows "P,\ |- (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,\ |- (xp,h,frs,sh) [ok]" and shC: "sh C = Some(sfs,i)" and dist: "distinct (C#clinit_classes frs)" shows "P,\ |- (xp,h,frs,sh(C \ (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 \ (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 \ C' sees M',b:Ts\T = (mxs,mxl\<^sub>0,ins,xt) in C'" and ty: "\ C' M' ! pc' = Some (ST,LT)" and conf: "conf_f P h sh (ST,LT) ins f'" and confs: "conf_fs P h sh \ C' M' (size Ts) T frs'" and confc: "conf_clinit P sh frs" and h_ok: "P\ h\" and sh_ok: "P,h \\<^sub>s sh \" 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 \\<^sub>s ?sh \" 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 \ 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,\ \ (xp,h,(stk,loc,C,M,pc,ics)#frs,sh)\" shows "\Cs a. ics = Throwing Cs a \ \obj. h a = Some obj" using correct by(clarsimp simp: correct_state_def conf_f_def) end diff --git a/thys/JinjaDCI/BV/BVExec.thy b/thys/JinjaDCI/BV/BVExec.thy --- a/thys/JinjaDCI/BV/BVExec.thy +++ b/thys/JinjaDCI/BV/BVExec.thy @@ -1,238 +1,253 @@ (* 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 \ Kildall for the JVM \label{sec:JVM} \ theory BVExec imports Jinja.Abstract_BV TF_JVM begin definition kiljvm :: "jvm_prog \ nat \ nat \ ty \ instr list \ ex_table \ ty\<^sub>i' err list \ ty\<^sub>i' err list" where "kiljvm P mxs mxl T\<^sub>r is xt \ 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 \ cname \ staticb \ ty list \ ty \ nat \ nat \ instr list \ ex_table \ bool" where "wt_kildall P C' b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \ 0 < size is \ (let first = Some ([],(case b of Static \ [] | NonStatic \ [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 \ 0 | NonStatic \ 1)+size Ts+mxl\<^sub>0) T\<^sub>r is xt start in \n < size is. result!n \ Err)" definition wf_jvm_prog\<^sub>k :: "jvm_prog \ bool" where "wf_jvm_prog\<^sub>k P \ wf_prog (\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 +proof - + let ?n = "length is" + have "Semilat A r f" using semilat_JVM[OF wf] + by (simp add: Semilat.intro sl_def2) + moreover have "acc r" using wf by simp blast + moreover have "top r Err" by (simp add: JVM_le_unfold) + moreover have "pres_type step ?n A" by (rule exec_pres_type) + moreover have "bounded step ?n" by (rule bounded_step) + moreover have "mono r step ?n A" using step_mono[OF wf] by simp + ultimately have "is_bcv r Err step ?n A (kildall r f step)" + by(rule is_bcv_kildall) + moreover have kileq: "kiljvm P mxs mxl T\<^sub>r is xt = kildall r f step" + using f_def kiljvm_def r_def step_def_exec by blast + ultimately show ?thesis by simp +qed (*>*) (* FIXME: move? *) lemma subset_replicate [intro?]: "set (replicate n x) \ {x}" by (induct n) auto lemma in_set_replicate: assumes "x \ set (replicate n y)" shows "x = y" (*<*) proof - note assms also have "set (replicate n y) \ {y}" .. finally show ?thesis by simp qed (*>*) lemma (in start_context) start_in_A [intro?]: "0 < size is \ start \ 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 +proof(cases b) +qed (force simp: JVM_states_unfold intro!: listI list_appendI + dest!: in_set_replicate)+ (*>*) 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 "\\s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \s" (*<*) proof - from wtk obtain res where result: "res = kiljvm P mxs mxl T\<^sub>r is xt start" and success: "\n < size is. res!n \ 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 \ list (size is) A" .. with bcv success result have "\ts\list (size is) A. start [\\<^sub>r] ts \ wt_step r Err step ts" by (unfold is_bcv_def) blast then obtain \s' where in_A: "\s' \ list (size is) A" and s: "start [\\<^sub>r] \s'" and w: "wt_step r Err step \s'" by blast hence wt_err_step: "wt_err_step (sup_state_opt P) step \s'" by (simp add: wt_err_step_def JVM_le_Err_conv) from in_A have l: "size \s' = size is" by simp moreover { from in_A have "check_types P mxs mxl \s'" by (simp add: check_types_def) also from w have "\x \ set \s'. x \ Err" by (auto simp add: wt_step_def all_set_conv_all_nth) hence [symmetric]: "map OK (map ok_val \s') = \s'" by (auto intro!: map_idI simp add: wt_step_def) finally have "check_types P mxs mxl (map OK (map ok_val \s'))" . } moreover { from s have "start!0 \\<^sub>r \s'!0" by (rule le_listD) simp moreover from instrs w l have "\s'!0 \ Err" by (unfold wt_step_def) simp then obtain \s0 where "\s'!0 = OK \s0" by auto ultimately have "wt_start P C b Ts mxl\<^sub>0 (map ok_val \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 \s' \ A" by simp with wt_err_step bounded_step have "wt_app_eff (sup_state_opt P) app eff (map ok_val \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 \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 \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 \s = length is" and ck_type: "check_types P mxs mxl (map OK \s)" and wt_start: "wt_start P C b Ts mxl\<^sub>0 \s" and app_eff: "wt_app_eff (sup_state_opt P) app eff \s" by (simp add: wt_method_def2 check_types_def) from ck_type have in_A: "set (map OK \s) \ 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 \s) app eff) (map OK \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 \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 \ list (size is) A" .. moreover let ?\s = "map OK \s" have less_\s: "start [\\<^sub>r] ?\s" proof (rule le_listI) from length instrs show "length start = length (map OK \s)" by simp next fix n from wt_start have "P \ ok_val (start!0) \' \s!0" by (cases b; simp add: wt_start_def) moreover from instrs length have "0 < length \s" by simp ultimately have "start!0 \\<^sub>r ?\s!0" by (simp add: JVM_le_Err_conv lesub_def) moreover { fix n' have "OK None \\<^sub>r ?\s!n" by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def split: err.splits) hence "\n = Suc n'; n < size start\ \ start!n \\<^sub>r ?\s!n" by simp } ultimately show "n < size start \ start!n \\<^sub>r ?\s!n" by (cases n, blast+) qed moreover from ck_type length have "?\s \ list (size is) A" by (auto intro!: listI simp add: check_types_def) moreover from wt_err have "wt_step r Err step ?\s" by (simp add: wt_err_step_def JVM_le_Err_conv) ultimately have "\p. p < size is \ kiljvm P mxs mxl T\<^sub>r is xt start ! p \ Err" by (unfold is_bcv_def) blast with instrs show "wt_kildall P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt" by (unfold wt_kildall_def) simp qed (*>*) theorem jvm_kildall_correct: "wf_jvm_prog\<^sub>k P = wf_jvm_prog P" (*<*) -proof +proof - let ?\ = "\C M. let (C,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)) = method P C M in SOME \s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \s" + let ?A = "\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" + let ?B\<^sub>\ = "\\. (\P C (M,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). + wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\ C M))" - \ \soundness\ - assume wt: "wf_jvm_prog\<^sub>k P" - hence "wf_jvm_prog\<^bsub>?\\<^esub> P" - apply (unfold wf_jvm_prog_phi_def wf_jvm_prog\<^sub>k_def) - apply (erule wf_prog_lift) - apply (auto dest!: start_context.wt_kil_correct [OF start_context.intro] - intro: someI) - apply (erule sees_method_is_class) - done - thus "wf_jvm_prog P" by (unfold wf_jvm_prog_def) fast -next - \ \completeness\ - assume wt: "wf_jvm_prog P" - thus "wf_jvm_prog\<^sub>k P" - apply (unfold wf_jvm_prog_def wf_jvm_prog_phi_def wf_jvm_prog\<^sub>k_def) - apply (clarify) - apply (erule wf_prog_lift) - apply (auto intro!: start_context.wt_kil_complete start_context.intro) - apply (erule sees_method_is_class) - done + show ?thesis proof(rule iffI) + \ \soundness\ + assume wt: "wf_jvm_prog\<^sub>k P" + then have "wf_prog ?A P" by(simp add: wf_jvm_prog\<^sub>k_def) + moreover { + fix wf_md C M b Ts Ca T m bd + assume "wf_prog wf_md P" and sees: "P \ Ca sees M, b : Ts\T = m in Ca" and + "set Ts \ types P" and "bd = (M, b, Ts, T, m)" and + "?A P Ca bd" + then have "(?B\<^sub>\ ?\) P Ca bd" using sees_method_is_class[OF sees] + by (auto dest!: start_context.wt_kil_correct [OF start_context.intro] + intro: someI) + } + ultimately have "wf_prog (?B\<^sub>\ ?\) P" by(rule wf_prog_lift) + then have "wf_jvm_prog\<^bsub>?\\<^esub> P" by (simp add: wf_jvm_prog_phi_def) + thus "wf_jvm_prog P" by (unfold wf_jvm_prog_def) fast + next + \ \completeness\ + assume wt: "wf_jvm_prog P" + then obtain \ where "wf_prog (?B\<^sub>\ \) P" by(clarsimp simp: wf_jvm_prog_def wf_jvm_prog_phi_def) + moreover { + fix wf_md C M b Ts Ca T m bd + assume "wf_prog wf_md P" and sees: "P \ Ca sees M, b : Ts\T = m in Ca" and + "set Ts \ types P" and "bd = (M, b, Ts, T, m)" and + "(?B\<^sub>\ \) P Ca bd" + then have "?A P Ca bd" using sees_method_is_class[OF sees] + by (auto intro!: start_context.wt_kil_complete start_context.intro) + } + ultimately have "wf_prog ?A P" by(rule wf_prog_lift) + thus "wf_jvm_prog\<^sub>k P" by (simp add: wf_jvm_prog\<^sub>k_def) + qed qed (*>*) end diff --git a/thys/JinjaDCI/BV/BVSpec.thy b/thys/JinjaDCI/BV/BVSpec.thy --- a/thys/JinjaDCI/BV/BVSpec.thy +++ b/thys/JinjaDCI/BV/BVSpec.thy @@ -1,104 +1,113 @@ (* Title: JinjaDCI/BV/BVSpec.thy Author: Cornelia Pusch, Gerwin Klein, Susannah Mansky Copyright 1999 Technische Universitaet Muenchen, 2019-20 UIUC Based on the Jinja theory BV/BVSpec.thy by Tobias Nipkow *) section \ The Bytecode Verifier \label{sec:BVSpec} \ theory BVSpec imports Effect begin text \ This theory contains a specification of the BV. The specification describes correct typings of method bodies; it corresponds to type \emph{checking}. \ definition \ \The method type only contains declared classes:\ check_types :: "'m prog \ nat \ nat \ ty\<^sub>i' err list \ bool" where "check_types P mxs mxl \s \ set \s \ states P mxs mxl" \ \An instruction is welltyped if it is applicable and its effect\ \ \is compatible with the type at all successor instructions:\ definition wt_instr :: "['m prog,ty,nat,pc,ex_table,instr,pc,ty\<^sub>m] \ bool" ("_,_,_,_,_ \ _,_ :: _" [60,0,0,0,0,0,0,61] 60) where "P,T,mxs,mpc,xt \ i,pc :: \s \ app i P mxs T pc mpc xt (\s!pc) \ (\(pc',\') \ set (eff i P pc xt (\s!pc)). P \ \' \' \s!pc')" \ \The type at @{text "pc=0"} conforms to the method calling convention:\ definition wt_start :: "['m prog,cname,staticb,ty list,nat,ty\<^sub>m] \ bool" where "wt_start P C b Ts mxl\<^sub>0 \s \ case b of NonStatic \ P \ Some ([],OK (Class C)#map OK Ts@replicate mxl\<^sub>0 Err) \' \s!0 | Static \ P \ Some ([],map OK Ts@replicate mxl\<^sub>0 Err) \' \s!0" \ \A method is welltyped if the body is not empty,\ \ \if the method type covers all instructions and mentions\ \ \declared classes only, if the method calling convention is respected, and\ \ \if all instructions are welltyped.\ definition wt_method :: "['m prog,cname,staticb,ty list,ty,nat,nat,instr list, ex_table,ty\<^sub>m] \ bool" where "wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \s \ 0 < size is \ size \s = size is \ check_types P mxs ((case b of Static \ 0 | NonStatic \ 1)+size Ts+mxl\<^sub>0) (map OK \s) \ wt_start P C b Ts mxl\<^sub>0 \s \ (\pc < size is. P,T\<^sub>r,mxs,size is,xt \ is!pc,pc :: \s)" \ \A program is welltyped if it is wellformed and all methods are welltyped\ definition wf_jvm_prog_phi :: "ty\<^sub>P \ jvm_prog \ bool" ("wf'_jvm'_prog\<^bsub>_\<^esub>") where "wf_jvm_prog\<^bsub>\\<^esub> \ wf_prog (\P C (M,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\ C M))" definition wf_jvm_prog :: "jvm_prog \ bool" where "wf_jvm_prog P \ \\. wf_jvm_prog\<^bsub>\\<^esub> P" lemma wt_jvm_progD: "wf_jvm_prog\<^bsub>\\<^esub> P \ \wt. wf_prog wt P" (*<*) by (unfold wf_jvm_prog_phi_def, blast) (*>*) lemma wt_jvm_prog_impl_wt_instr: - "\ wf_jvm_prog\<^bsub>\\<^esub> P; - P \ C sees M,b:Ts \ T = (mxs,mxl\<^sub>0,ins,xt) in C; pc < size ins \ - \ P,T,mxs,size ins,xt \ ins!pc,pc :: \ C M" +assumes wf: "wf_jvm_prog\<^bsub>\\<^esub> P" and + sees: "P \ C sees M,b:Ts \ T = (mxs,mxl\<^sub>0,ins,xt) in C" and + pc: "pc < size ins" +shows "P,T,mxs,size ins,xt \ ins!pc,pc :: \ C M" (*<*) - apply (unfold wf_jvm_prog_phi_def) - apply (drule (1) sees_wf_mdecl) - apply (simp add: wf_mdecl_def wt_method_def) - done +proof - + have wfm: "wf_prog + (\P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). + wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\ C M)) P" using wf + by (unfold wf_jvm_prog_phi_def) + show ?thesis using sees_wf_mdecl[OF wfm sees] pc + by (simp add: wf_mdecl_def wt_method_def) +qed (*>*) lemma wt_jvm_prog_impl_wt_start: - "\ wf_jvm_prog\<^bsub>\\<^esub> P; - P \ C sees M,b:Ts \ T = (mxs,mxl\<^sub>0,ins,xt) in C \ \ - 0 < size ins \ wt_start P C b Ts mxl\<^sub>0 (\ C M)" +assumes wf: "wf_jvm_prog\<^bsub>\\<^esub> P" and + sees: "P \ C sees M,b:Ts \ T = (mxs,mxl\<^sub>0,ins,xt) in C" +shows "0 < size ins \ wt_start P C b Ts mxl\<^sub>0 (\ C M)" (*<*) - apply (unfold wf_jvm_prog_phi_def) - apply (drule (1) sees_wf_mdecl) - apply (simp add: wf_mdecl_def wt_method_def) - done +proof - + have wfm: "wf_prog + (\P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). + wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\ C M)) P" using wf + by (unfold wf_jvm_prog_phi_def) + show ?thesis using sees_wf_mdecl[OF wfm sees] + by (simp add: wf_mdecl_def wt_method_def) +qed (*>*) lemma wf_jvm_prog_nclinit: assumes wtp: "wf_jvm_prog\<^bsub>\\<^esub> P" and meth: "P \ C sees M, b : Ts\T = (mxs, mxl\<^sub>0, ins, xt) in D" and wt: "P,T,mxs,size ins,xt \ ins!pc,pc :: \ C M" and pc: "pc < length ins" and \: "\ C M ! pc = Some(ST,LT)" and ins: "ins ! pc = Invokestatic C\<^sub>0 M\<^sub>0 n" shows "M\<^sub>0 \ clinit" using assms by(simp add: wf_jvm_prog_phi_def wt_instr_def app_def) end diff --git a/thys/JinjaDCI/BV/Effect.thy b/thys/JinjaDCI/BV/Effect.thy --- a/thys/JinjaDCI/BV/Effect.thy +++ b/thys/JinjaDCI/BV/Effect.thy @@ -1,441 +1,443 @@ (* Title: JinjaDCI/BV/Effect.thy Author: Gerwin Klein, Susannah Mansky Copyright 2000 Technische Universitaet Muenchen, 2019-20 UIUC Based on the Jinja theory BV/Effect.thy by Gerwin Klein *) section \Effect of Instructions on the State Type\ theory Effect imports JVM_SemiType "../JVM/JVMExceptions" begin \ \FIXME\ locale prog = fixes P :: "'a prog" locale jvm_method = prog + fixes mxs :: nat fixes mxl\<^sub>0 :: nat fixes Ts :: "ty list" fixes T\<^sub>r :: ty fixes "is" :: "instr list" fixes xt :: ex_table fixes mxl :: nat defines mxl_def: "mxl \ 1+size Ts+mxl\<^sub>0" text \ Program counter of successor instructions: \ primrec succs :: "instr \ ty\<^sub>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\<^sub>i :: "instr \ 'm prog \ ty\<^sub>i \ ty\<^sub>i" where eff\<^sub>i_Load: "eff\<^sub>i (Load n, P, (ST, LT)) = (ok_val (LT ! n) # ST, LT)" | eff\<^sub>i_Store: "eff\<^sub>i (Store n, P, (T#ST, LT)) = (ST, LT[n:= OK T])" | eff\<^sub>i_Push: "eff\<^sub>i (Push v, P, (ST, LT)) = (the (typeof v) # ST, LT)" | eff\<^sub>i_Getfield: "eff\<^sub>i (Getfield F C, P, (T#ST, LT)) = (snd (snd (field P C F)) # ST, LT)" | eff\<^sub>i_Getstatic: "eff\<^sub>i (Getstatic C F D, P, (ST, LT)) = (snd (snd (field P C F)) # ST, LT)" | eff\<^sub>i_Putfield: "eff\<^sub>i (Putfield F C, P, (T\<^sub>1#T\<^sub>2#ST, LT)) = (ST,LT)" | eff\<^sub>i_Putstatic: "eff\<^sub>i (Putstatic C F D, P, (T#ST, LT)) = (ST,LT)" | eff\<^sub>i_New: "eff\<^sub>i (New C, P, (ST,LT)) = (Class C # ST, LT)" | eff\<^sub>i_Checkcast: "eff\<^sub>i (Checkcast C, P, (T#ST,LT)) = (Class C # ST,LT)" | eff\<^sub>i_Pop: "eff\<^sub>i (Pop, P, (T#ST,LT)) = (ST,LT)" | eff\<^sub>i_IAdd: "eff\<^sub>i (IAdd, P,(T\<^sub>1#T\<^sub>2#ST,LT)) = (Integer#ST,LT)" | eff\<^sub>i_CmpEq: "eff\<^sub>i (CmpEq, P, (T\<^sub>1#T\<^sub>2#ST,LT)) = (Boolean#ST,LT)" | eff\<^sub>i_IfFalse: "eff\<^sub>i (IfFalse b, P, (T\<^sub>1#ST,LT)) = (ST,LT)" | eff\<^sub>i_Invoke: "eff\<^sub>i (Invoke M n, P, (ST,LT)) = (let C = the_class (ST!n); (D,b,Ts,T\<^sub>r,m) = method P C M in (T\<^sub>r # drop (n+1) ST, LT))" | eff\<^sub>i_Invokestatic: "eff\<^sub>i (Invokestatic C M n, P, (ST,LT)) = (let (D,b,Ts,T\<^sub>r,m) = method P C M in (T\<^sub>r # drop n ST, LT))" | eff\<^sub>i_Goto: "eff\<^sub>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 \\<^sup>* C \ P \ NoSuchFieldError \\<^sup>* C \ P \ IncompatibleClassChangeError \\<^sup>* 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 \\<^sup>* C \ P \ NoSuchFieldError \\<^sup>* C \ P \ IncompatibleClassChangeError \\<^sup>* C)" | rel_Putstatic: "is_relevant_class (Putstatic C F D) = (\P C. True)" | rel_Checkcast: "is_relevant_class (Checkcast D) = (\P C. P \ ClassCast \\<^sup>* 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.. 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\<^sub>i \ ex_table \ (pc \ ty\<^sub>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\<^sub>i \ (pc \ ty\<^sub>i') list" where "norm_eff i P pc \ = map (\pc'. (pc',Some (eff\<^sub>i (i,P,\)))) (succs i \ pc)" definition eff :: "instr \ 'm prog \ pc \ ex_table \ ty\<^sub>i' \ (pc \ ty\<^sub>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) (* FIXME: getfield, \T D. P \ C sees F:T in D \ .. *) text "Conditions under which eff is applicable:" fun app\<^sub>i :: "instr \ 'm prog \ pc \ nat \ ty \ ty\<^sub>i \ bool" where app\<^sub>i_Load: "app\<^sub>i (Load n, P, pc, mxs, T\<^sub>r, (ST,LT)) = (n < length LT \ LT ! n \ Err \ length ST < mxs)" | app\<^sub>i_Store: "app\<^sub>i (Store n, P, pc, mxs, T\<^sub>r, (T#ST, LT)) = (n < length LT)" | app\<^sub>i_Push: "app\<^sub>i (Push v, P, pc, mxs, T\<^sub>r, (ST,LT)) = (length ST < mxs \ typeof v \ None)" | app\<^sub>i_Getfield: "app\<^sub>i (Getfield F C, P, pc, mxs, T\<^sub>r, (T#ST, LT)) = (\T\<^sub>f. P \ C sees F,NonStatic:T\<^sub>f in C \ P \ T \ Class C)" | app\<^sub>i_Getstatic: "app\<^sub>i (Getstatic C F D, P, pc, mxs, T\<^sub>r, (ST, LT)) = (length ST < mxs \ (\T\<^sub>f. P \ C sees F,Static:T\<^sub>f in D))" | app\<^sub>i_Putfield: "app\<^sub>i (Putfield F C, P, pc, mxs, T\<^sub>r, (T\<^sub>1#T\<^sub>2#ST, LT)) = (\T\<^sub>f. P \ C sees F,NonStatic:T\<^sub>f in C \ P \ T\<^sub>2 \ (Class C) \ P \ T\<^sub>1 \ T\<^sub>f)" | app\<^sub>i_Putstatic: "app\<^sub>i (Putstatic C F D, P, pc, mxs, T\<^sub>r, (T#ST, LT)) = (\T\<^sub>f. P \ C sees F,Static:T\<^sub>f in D \ P \ T \ T\<^sub>f)" | app\<^sub>i_New: "app\<^sub>i (New C, P, pc, mxs, T\<^sub>r, (ST,LT)) = (is_class P C \ length ST < mxs)" | app\<^sub>i_Checkcast: "app\<^sub>i (Checkcast C, P, pc, mxs, T\<^sub>r, (T#ST,LT)) = (is_class P C \ is_refT T)" | app\<^sub>i_Pop: "app\<^sub>i (Pop, P, pc, mxs, T\<^sub>r, (T#ST,LT)) = True" | app\<^sub>i_IAdd: "app\<^sub>i (IAdd, P, pc, mxs, T\<^sub>r, (T\<^sub>1#T\<^sub>2#ST,LT)) = (T\<^sub>1 = T\<^sub>2 \ T\<^sub>1 = Integer)" | app\<^sub>i_CmpEq: "app\<^sub>i (CmpEq, P, pc, mxs, T\<^sub>r, (T\<^sub>1#T\<^sub>2#ST,LT)) = (T\<^sub>1 = T\<^sub>2 \ is_refT T\<^sub>1 \ is_refT T\<^sub>2)" | app\<^sub>i_IfFalse: "app\<^sub>i (IfFalse b, P, pc, mxs, T\<^sub>r, (Boolean#ST,LT)) = (0 \ int pc + b)" | app\<^sub>i_Goto: "app\<^sub>i (Goto b, P, pc, mxs, T\<^sub>r, s) = (0 \ int pc + b)" | app\<^sub>i_Return: "app\<^sub>i (Return, P, pc, mxs, T\<^sub>r, (T#ST,LT)) = (P \ T \ T\<^sub>r)" | app\<^sub>i_Throw: "app\<^sub>i (Throw, P, pc, mxs, T\<^sub>r, (T#ST,LT)) = is_refT T" | app\<^sub>i_Invoke: "app\<^sub>i (Invoke M n, P, pc, mxs, T\<^sub>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\<^sub>i_Invokestatic: "app\<^sub>i (Invokestatic C M n, P, pc, mxs, T\<^sub>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\<^sub>i_default: "app\<^sub>i (i,P, pc,mxs,T\<^sub>r,s) = False" definition xcpt_app :: "instr \ 'm prog \ pc \ nat \ ex_table \ ty\<^sub>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\<^sub>i' \ bool" where "app i P mxs T\<^sub>r pc mpc xt t = (case t of None \ True | Some \ \ app\<^sub>i (i,P,pc,mxs,T\<^sub>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\<^sub>r pc mpc xt (Some \) = (app\<^sub>i (i,P,pc,mxs,T\<^sub>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\<^sub>i and app\<^sub>i and eff and app fixes norm_eff and xcpt_app and xcpt_eff fixes mpc defines "mpc \ size is" defines "eff\<^sub>i i \ \ Effect.eff\<^sub>i (i,P,\)" notes eff\<^sub>i_simps [simp] = Effect.eff\<^sub>i.simps [where P = P, folded eff\<^sub>i_def] defines "app\<^sub>i i pc \ \ Effect.app\<^sub>i (i, P, pc, mxs, T\<^sub>r, \)" notes app\<^sub>i_simps [simp] = Effect.app\<^sub>i.simps [where P=P and mxs=mxs and T\<^sub>r=T\<^sub>r, folded app\<^sub>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\<^sub>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\<^sub>r pc mpc xt" notes app = Effect.app_def [of _ P mxs T\<^sub>r _ mpc xt, folded app_def xcpt_app_def app\<^sub>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\<^sub>r pc mpc et None = True" by (simp add: app_def) lemma appLoad[simp]: "app\<^sub>i (Load idx, P, T\<^sub>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\<^sub>i (Store idx,P,pc,mxs,T\<^sub>r,s) = (\ts ST LT. s = (ts#ST,LT) \ idx < length LT)" by (rule length_cases2, auto) lemma appPush[simp]: "app\<^sub>i (Push v,P,pc,mxs,T\<^sub>r,s) = (\ST LT. s = (ST,LT) \ length ST < mxs \ typeof v \ None)" by (cases s, simp) lemma appGetField[simp]: "app\<^sub>i (Getfield F C,P,pc,mxs,T\<^sub>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\<^sub>i (Getstatic C F D,P,pc,mxs,T\<^sub>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\<^sub>i (Putfield F C,P,pc,mxs,T\<^sub>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\<^sub>i (Putstatic C F D,P,pc,mxs,T\<^sub>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\<^sub>i (New C,P,pc,mxs,T\<^sub>r,s) = (\ST LT. s=(ST,LT) \ is_class P C \ length ST < mxs)" by (cases s, simp) lemma appCheckcast[simp]: "app\<^sub>i (Checkcast C,P,pc,mxs,T\<^sub>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\<^sub>iPop[simp]: "app\<^sub>i (Pop,P,pc,mxs,T\<^sub>r,s) = (\ts ST LT. s = (ts#ST,LT))" by (rule length_cases2, auto) lemma appIAdd[simp]: "app\<^sub>i (IAdd,P,pc,mxs,T\<^sub>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\<^sub>1 T\<^sub>2 ST'. ST = T\<^sub>1#T\<^sub>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\<^sub>1 T\<^sub>2 ST' assume "ST = T\<^sub>1#T\<^sub>2#ST'" hence ?thesis by (cases T\<^sub>1, auto) } ultimately show ?thesis by blast qed (*>*) lemma appIfFalse [simp]: "app\<^sub>i (IfFalse b,P,pc,mxs,T\<^sub>r,s) = (\ST LT. s = (Boolean#ST,LT) \ 0 \ int pc + b)" (*<*) - apply (rule length_cases2) - apply simp - apply (case_tac l) - apply auto - done + (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\<^sub>i (CmpEq,P,pc,mxs,T\<^sub>r,s) = (\T\<^sub>1 T\<^sub>2 ST LT. s = (T\<^sub>1#T\<^sub>2#ST,LT) \ (\is_refT T\<^sub>1 \ T\<^sub>2 = T\<^sub>1 \ is_refT T\<^sub>1 \ is_refT T\<^sub>2))" by (rule length_cases4, auto) lemma appReturn[simp]: "app\<^sub>i (Return,P,pc,mxs,T\<^sub>r,s) = (\T ST LT. s = (T#ST,LT) \ P \ T \ T\<^sub>r)" by (rule length_cases2, auto) lemma appThrow[simp]: "app\<^sub>i (Throw,P,pc,mxs,T\<^sub>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 diff --git a/thys/JinjaDCI/BV/LBVJVM.thy b/thys/JinjaDCI/BV/LBVJVM.thy --- a/thys/JinjaDCI/BV/LBVJVM.thy +++ b/thys/JinjaDCI/BV/LBVJVM.thy @@ -1,226 +1,245 @@ (* Title: JinjaDCI/BV/LBVJVM.thy Author: Tobias Nipkow, Gerwin Klein, Susannah Mansky Copyright 2000 TUM, 2020 UIUC Based on the Jinja theory BV/LBVJVM.thy by Tobias Nipkow and Gerwin Klein *) section \ LBV for the JVM \label{sec:JVM} \ theory LBVJVM imports Jinja.Abstract_BV TF_JVM begin type_synonym prog_cert = "cname \ mname \ ty\<^sub>i' err list" definition check_cert :: "jvm_prog \ nat \ nat \ nat \ ty\<^sub>i' err list \ bool" where "check_cert P mxs mxl n cert \ check_types P mxs mxl cert \ size cert = n+1 \ (\i Err) \ cert!n = OK None" definition lbvjvm :: "jvm_prog \ nat \ nat \ ty \ ex_table \ ty\<^sub>i' err list \ instr list \ ty\<^sub>i' err \ ty\<^sub>i' err" where "lbvjvm P mxs maxr T\<^sub>r et cert bs \ wtl_inst_list bs cert (JVM_SemiType.sup P mxs maxr) (JVM_SemiType.le P mxs maxr) Err (OK None) (exec P mxs T\<^sub>r et bs) 0" definition wt_lbv :: "jvm_prog \ cname \ staticb \ ty list \ ty \ nat \ nat \ ex_table \ ty\<^sub>i' err list \ instr list \ bool" where "wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et cert ins \ check_cert P mxs ((case b of Static \ 0 | NonStatic \ 1)+size Ts+mxl\<^sub>0) (size ins) cert \ 0 < size ins \ (let start = Some ([],(case b of Static \ [] | NonStatic \ [OK (Class C)]) @((map OK Ts))@(replicate mxl\<^sub>0 Err)); result = lbvjvm P mxs ((case b of Static \ 0 | NonStatic \ 1)+size Ts+mxl\<^sub>0) T\<^sub>r et cert ins (OK start) in result \ Err)" definition wt_jvm_prog_lbv :: "jvm_prog \ prog_cert \ bool" where "wt_jvm_prog_lbv P cert \ wf_prog (\P C (mn,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,ins,et)). wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (cert C mn) ins) P" definition mk_cert :: "jvm_prog \ nat \ ty \ ex_table \ instr list \ ty\<^sub>m \ ty\<^sub>i' err list" where "mk_cert P mxs T\<^sub>r et bs phi \ make_cert (exec P mxs T\<^sub>r et bs) (map OK phi) (OK None)" definition prg_cert :: "jvm_prog \ ty\<^sub>P \ prog_cert" where "prg_cert P phi C mn \ let (C,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,ins,et)) = method P C mn in mk_cert P mxs T\<^sub>r et ins (phi C mn)" lemma check_certD [intro?]: "check_cert P mxs mxl n cert \ cert_ok cert n Err (OK None) (states P mxs mxl)" by (unfold cert_ok_def check_cert_def check_types_def) auto lemma (in start_context) wt_lbv_wt_step: assumes lbv: "wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is" shows "\\s \ list (size is) A. wt_step r Err step \s \ OK first \\<^sub>r \s!0" (*<*) proof - from wf have "semilat (JVM_SemiType.sl P mxs mxl)" .. hence "semilat (A, r, f)" by (simp add: sl_def2) moreover have "top r Err" by (simp add: JVM_le_Err_conv) moreover have "Err \ A" by (simp add: JVM_states_unfold) moreover have "bottom r (OK None)" by (simp add: JVM_le_Err_conv bottom_def lesub_def Err.le_def split: err.split) moreover have "OK None \ A" by (simp add: JVM_states_unfold) moreover note bounded_step moreover from lbv have "cert_ok cert (size is) Err (OK None) A" by (unfold wt_lbv_def) (auto dest: check_certD) moreover note exec_pres_type moreover from lbv have "wtl_inst_list is cert f r Err (OK None) step 0 (OK first) \ Err" by (cases b; simp add: wt_lbv_def lbvjvm_def step_def_exec [symmetric]) moreover note first_in_A moreover from lbv have "0 < size is" by (simp add: wt_lbv_def) ultimately show ?thesis by (rule lbvs.wtl_sound_strong [OF lbvs.intro, OF lbv.intro lbvs_axioms.intro, OF Semilat.intro lbv_axioms.intro]) qed (*>*) lemma (in start_context) wt_lbv_wt_method: assumes lbv: "wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is" shows "\\s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \s" (*<*) proof - from lbv have l: "is \ []" by (simp add: wt_lbv_def) moreover from wf lbv C Ts obtain \s where list: "\s \ list (size is) A" and step: "wt_step r Err step \s" and start: "OK first \\<^sub>r \s!0" by (blast dest: wt_lbv_wt_step) from list have [simp]: "size \s = size is" by simp have "size (map ok_val \s) = size is" by simp moreover from l have 0: "0 < size \s" by simp with step obtain \s0 where "\s!0 = OK \s0" by (unfold wt_step_def) blast with start 0 have "wt_start P C b Ts mxl\<^sub>0 (map ok_val \s)" by (cases b; simp add: wt_start_def JVM_le_Err_conv lesub_def Err.le_def) moreover { from list have "check_types P mxs mxl \s" by (simp add: check_types_def) also from step have "\x \ set \s. x \ Err" by (auto simp add: all_set_conv_all_nth wt_step_def) hence [symmetric]: "map OK (map ok_val \s) = \s" by (auto intro!: map_idI) finally have "check_types P mxs mxl (map OK (map ok_val \s))" . } moreover { note bounded_step moreover from list have "set \s \ A" by simp moreover from step have "wt_err_step (sup_state_opt P) step \s" by (simp add: wt_err_step_def JVM_le_Err_conv) ultimately have "wt_app_eff (sup_state_opt P) app eff (map ok_val \s)" by (auto intro: wt_err_imp_wt_app_eff simp add: exec_def states_def) } ultimately have "wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (map ok_val \s)" by (simp add: wt_method_def2 check_types_def del: map_map) thus ?thesis .. qed (*>*) lemma (in start_context) wt_method_wt_lbv: assumes wt: "wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \s" defines [simp]: "cert \ mk_cert P mxs T\<^sub>r xt is \s" shows "wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is" (*<*) proof - let ?\s = "map OK \s" let ?cert = "make_cert step ?\s (OK None)" from wt obtain 0: "0 < size is" and size: "size is = size ?\s" and ck_types: "check_types P mxs mxl ?\s" and wt_start: "wt_start P C b Ts mxl\<^sub>0 \s" and app_eff: "wt_app_eff (sup_state_opt P) app eff \s" by (force simp add: wt_method_def2 check_types_def) from wf have "semilat (JVM_SemiType.sl P mxs mxl)" .. hence "semilat (A, r, f)" by (simp add: sl_def2) moreover have "top r Err" by (simp add: JVM_le_Err_conv) moreover have "Err \ A" by (simp add: JVM_states_unfold) moreover have "bottom r (OK None)" by (simp add: JVM_le_Err_conv bottom_def lesub_def Err.le_def split: err.split) moreover have "OK None \ A" by (simp add: JVM_states_unfold) moreover from wf have "mono r step (size is) A" by (rule step_mono) hence "mono r step (size ?\s) A" by (simp add: size) moreover from exec_pres_type have "pres_type step (size ?\s) A" by (simp add: size) moreover from ck_types have \s_in_A: "set ?\s \ A" by (simp add: check_types_def) hence "\pc. pc < size ?\s \ ?\s!pc \ A \ ?\s!pc \ Err" by auto moreover from bounded_step have "bounded step (size ?\s)" by (simp add: size) moreover have "OK None \ Err" by simp moreover from bounded_step size \s_in_A app_eff have "wt_err_step (sup_state_opt P) step ?\s" by (auto intro: wt_app_eff_imp_wt_err simp add: exec_def states_def) hence "wt_step r Err step ?\s" by (simp add: wt_err_step_def JVM_le_Err_conv) moreover from 0 size have "0 < size \s" by auto hence "?\s!0 = OK (\s!0)" by simp with wt_start have "OK first \\<^sub>r ?\s!0" by (cases b; clarsimp simp add: wt_start_def lesub_def Err.le_def JVM_le_Err_conv) moreover note first_in_A moreover have "OK first \ Err" by simp moreover note size ultimately have "wtl_inst_list is ?cert f r Err (OK None) step 0 (OK first) \ Err" by (rule lbvc.wtl_complete [OF lbvc.intro, OF lbv.intro lbvc_axioms.intro, OF Semilat.intro lbv_axioms.intro]) moreover from 0 size have "\s \ []" by auto moreover from ck_types have "check_types P mxs mxl ?cert" - apply (auto simp add: make_cert_def check_types_def JVM_states_unfold) - apply (subst Ok_in_err [symmetric]) - apply (drule nth_mem) - apply auto - done + by (fastforce simp: make_cert_def check_types_def JVM_states_unfold + dest!: nth_mem) moreover note 0 size ultimately show ?thesis by (simp add: wt_lbv_def lbvjvm_def mk_cert_def step_def_exec [symmetric] check_cert_def make_cert_def nth_append) qed (*>*) theorem jvm_lbv_correct: "wt_jvm_prog_lbv P Cert \ wf_jvm_prog P" (*<*) proof - let ?\ = "\C mn. let (C,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)) = method P C mn in SOME \s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \s" - + + let ?A = "\P C (mn,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,ins,et)). wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert C mn) ins" + let ?B = "\P C (M,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). + wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (?\ C M)" + assume wt: "wt_jvm_prog_lbv P Cert" - hence "wf_jvm_prog\<^bsub>?\\<^esub> P" - apply (unfold wf_jvm_prog_phi_def wt_jvm_prog_lbv_def) - apply (erule wf_prog_lift) - apply (auto dest!: start_context.wt_lbv_wt_method [OF start_context.intro] - intro: someI) - apply (erule sees_method_is_class) - done + then have "wf_prog ?A P" by(simp add: wt_jvm_prog_lbv_def) + moreover { + fix wf_md C M b Ts Ca T m bd + assume "wf_prog wf_md P" and sees: "P \ Ca sees M, b : Ts\T = m in Ca" and + "set Ts \ types P" and "bd = (M, b, Ts, T, m)" and + "?A P Ca bd" + then have "?B P Ca bd" using sees_method_is_class[OF sees] + by (auto dest!: start_context.wt_lbv_wt_method [OF start_context.intro] + intro: someI) + } + ultimately have "wf_prog ?B P" by(rule wf_prog_lift) + hence "wf_jvm_prog\<^bsub>?\\<^esub> P" by (simp add: wf_jvm_prog_phi_def) thus ?thesis by (unfold wf_jvm_prog_def) blast qed (*>*) theorem jvm_lbv_complete: assumes wt: "wf_jvm_prog\<^bsub>\\<^esub> P" shows "wt_jvm_prog_lbv P (prg_cert P \)" (*<*) - using wt - apply (unfold wf_jvm_prog_phi_def wt_jvm_prog_lbv_def) - apply (erule wf_prog_lift) - apply (auto simp add: prg_cert_def - intro!: start_context.wt_method_wt_lbv start_context.intro) - apply (erule sees_method_is_class) - done +proof - + let ?cert = "prg_cert P \" + let ?A = "\P C (M,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). + wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\ C M)" + let ?B = "\P C (mn,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,ins,et)). + wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (?cert C mn) ins" + + from wt have "wf_prog ?A P" by(clarsimp simp: wf_jvm_prog_def wf_jvm_prog_phi_def) + moreover { + fix wf_md C M b Ts Ca T m bd + assume "wf_prog wf_md P" and sees: "P \ Ca sees M, b : Ts\T = m in Ca" and + "set Ts \ types P" and "bd = (M, b, Ts, T, m)" and + "?A P Ca bd" + then have "?B P Ca bd" using sees_method_is_class[OF sees] + by (auto simp add: prg_cert_def + intro!: start_context.wt_method_wt_lbv start_context.intro) + } + ultimately have "wf_prog ?B P" by(rule wf_prog_lift) + thus "wt_jvm_prog_lbv P (prg_cert P \)" by (simp add: wt_jvm_prog_lbv_def) +qed (*>*) -end +end diff --git a/thys/JinjaDCI/BV/TF_JVM.thy b/thys/JinjaDCI/BV/TF_JVM.thy --- a/thys/JinjaDCI/BV/TF_JVM.thy +++ b/thys/JinjaDCI/BV/TF_JVM.thy @@ -1,292 +1,319 @@ (* Title: JinjaDCI/BV/TF_JVM.thy Author: Tobias Nipkow, Gerwin Klein, Susannah Mansky Copyright 2000 TUM, 2019-20 UIUC Based on the Jinja theory BV/TF_JVM.thy by Tobias Nipkow and Gerwin Klein *) section \ The Typing Framework for the JVM \label{sec:JVM} \ theory TF_JVM imports Jinja.Typing_Framework_err EffectMono BVSpec begin definition exec :: "jvm_prog \ nat \ ty \ ex_table \ instr list \ ty\<^sub>i' err step_type" where "exec G maxs rT et bs \ err_step (size bs) (\pc. app (bs!pc) G maxs rT pc (size bs) et) (\pc. eff (bs!pc) G pc et)" locale JVM_sl = fixes P :: jvm_prog and mxs and mxl\<^sub>0 fixes b and Ts :: "ty list" and "is" and xt and T\<^sub>r fixes mxl and A and r and f and app and eff and step defines [simp]: "mxl \ (case b of Static \ 0 | NonStatic \ 1)+size Ts+mxl\<^sub>0" defines [simp]: "A \ states P mxs mxl" defines [simp]: "r \ JVM_SemiType.le P mxs mxl" defines [simp]: "f \ JVM_SemiType.sup P mxs mxl" defines [simp]: "app \ \pc. Effect.app (is!pc) P mxs T\<^sub>r pc (size is) xt" defines [simp]: "eff \ \pc. Effect.eff (is!pc) P pc xt" defines [simp]: "step \ err_step (size is) app eff" locale start_context = JVM_sl + fixes p and C assumes wf: "wf_prog p P" assumes C: "is_class P C" assumes Ts: "set Ts \ types P" fixes first :: ty\<^sub>i' and start defines [simp]: "first \ Some ([],(case b of Static \ [] | NonStatic \ [OK (Class C)]) @ map OK Ts @ replicate mxl\<^sub>0 Err)" defines [simp]: "start \ (OK first) # replicate (size is - 1) (OK None)" subsection \ Connecting JVM and Framework \ lemma (in JVM_sl) step_def_exec: "step \ exec P mxs T\<^sub>r xt is" by (simp add: exec_def) lemma special_ex_swap_lemma [iff]: "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)" by blast lemma ex_in_list [iff]: "(\n. ST \ list n A \ n \ mxs) = (set ST \ A \ size ST \ mxs)" by (unfold list_def) auto lemma singleton_list: "(\n. [Class C] \ list n (types P) \ n \ mxs) = (is_class P C \ 0 < mxs)" by auto lemma set_drop_subset: "set xs \ A \ set (drop n xs) \ A" by (auto dest: in_set_dropD) lemma Suc_minus_minus_le: "n < mxs \ Suc (n - (n - b)) \ mxs" by arith lemma in_listE: "\ xs \ list n A; \size xs = n; set xs \ A\ \ P \ \ P" by (unfold list_def) blast declare is_relevant_entry_def [simp] declare set_drop_subset [simp] theorem (in start_context) exec_pres_type: "pres_type step (size is) A" (*<*) - apply (insert wf) - apply simp - apply (unfold JVM_states_unfold) - apply (rule pres_type_lift) - apply clarify - apply (rename_tac s pc pc' s') - apply (case_tac s) - apply simp - apply (drule effNone) - apply simp - apply (simp add: Effect.app_def xcpt_app_def Effect.eff_def - xcpt_eff_def norm_eff_def relevant_entries_def) - apply (case_tac "is!pc") - - \ \Load\ - apply clarsimp - apply (frule listE_nth_in, assumption) - apply fastforce - - \ \Store\ - apply fastforce - - \ \Push\ - apply (fastforce simp add: typeof_lit_is_type) - - \ \New\ - apply fastforce - - \ \Getfield\ - apply (fastforce dest: sees_field_is_type) - - \ \Getstatic\ - apply (fastforce dest: sees_field_is_type) - - \ \Putfield\ - apply fastforce - - \ \Putstatic\ - apply fastforce - - \ \Checkcast\ - apply fastforce - - defer defer \ \Invoke and Invokestatic deferred\ - - \ \Return\ - apply fastforce - - \ \Pop\ - apply fastforce - - \ \IAdd\ - apply fastforce - - \ \Goto\ - apply fastforce - - \ \CmpEq\ - apply fastforce - - \ \IfFalse\ - apply fastforce - - \ \Throw\ - apply fastforce - - \ \Invoke\ - apply (clarsimp split!: if_splits) - apply fastforce - apply (erule disjE) - prefer 2 - apply fastforce - apply clarsimp - apply (rule conjI) - apply (drule (1) sees_wf_mdecl) - apply (clarsimp simp add: wf_mdecl_def) - apply arith - - \ \Invokestatic\ - apply (clarsimp split!: if_splits) - apply (erule disjE) - prefer 2 - apply fastforce - apply clarsimp - apply (drule (1) sees_wf_mdecl) - apply (clarsimp simp add: wf_mdecl_def) - done +proof - + let ?n = "size is" and ?app = app and ?step = eff + let ?mxl = "(case b of Static \ 0 | NonStatic \ 1) + length Ts + mxl\<^sub>0" + let ?A = "opt((Union {list n (types P) |n. n <= mxs}) \ + list ?mxl (err(types P)))" + have "pres_type (err_step ?n ?app ?step) ?n (err ?A)" + proof(rule pres_type_lift) + have "\s pc pc' s'. s\?A \ pc < ?n \ ?app pc s + \ (pc', s')\set (?step pc s) \ s' \ ?A" + proof - + fix s pc pc' s' + assume asms: "s\?A" "pc < ?n" "?app pc s" "(pc', s')\set (?step pc s)" + show "s' \ ?A" + proof(cases s) + case None + then show ?thesis using asms by (fastforce dest: effNone) + next + case (Some ab) + then show ?thesis using asms proof(cases "is!pc") + case Load + then show ?thesis using asms + by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def + xcpt_eff_def norm_eff_def + dest: listE_nth_in) + next + case Push + then show ?thesis using asms Some + by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def + xcpt_eff_def norm_eff_def typeof_lit_is_type) + next + case Getfield + then show ?thesis using asms wf + by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def + xcpt_eff_def norm_eff_def + dest: sees_field_is_type) + next + case Getstatic + then show ?thesis using asms wf + by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def + xcpt_eff_def norm_eff_def + dest: sees_field_is_type) + next + case (Invoke M n) + obtain a b where [simp]: "s = \(a,b)\" using Some asms(1) by blast + show ?thesis + proof(cases "a!n = NT") + case True + then show ?thesis using Invoke asms wf + by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def + xcpt_eff_def norm_eff_def) + next + case False + have "(pc', s') \ set (norm_eff (Invoke M n) P pc (a, b)) \ + (pc', s') \ set (xcpt_eff (Invoke M n) P pc (a, b) xt)" + using Invoke asms(4) by (simp add: Effect.eff_def) + then show ?thesis proof(rule disjE) + assume "(pc', s') \ set (xcpt_eff (Invoke M n) P pc (a, b) xt)" + then show ?thesis using Invoke asms(1-3) + by (fastforce simp: Effect.app_def xcpt_app_def xcpt_eff_def) + next + assume norm: "(pc', s') \ set (norm_eff (Invoke M n) P pc (a, b))" + also have "Suc (length a - Suc n) \ mxs" using Invoke asms(1,3) + by (simp add: Effect.app_def xcpt_app_def) arith + ultimately show ?thesis using False Invoke asms(1-3) wf + by (auto simp: Effect.app_def xcpt_app_def norm_eff_def wf_mdecl_def + dest!: sees_wf_mdecl) + qed + qed + next + case (Invokestatic C M n) + obtain a b where [simp]: "s = \(a,b)\" using Some asms(1) by blast + have "(pc', s') \ set (norm_eff (Invokestatic C M n) P pc (a, b)) \ + (pc', s') \ set (xcpt_eff (Invokestatic C M n) P pc (a, b) xt)" + using Invokestatic asms(4) by (simp add: Effect.eff_def) + then show ?thesis proof(rule disjE) + assume "(pc', s') \ set (xcpt_eff (Invokestatic C M n) P pc (a, b) xt)" + then show ?thesis using Invokestatic asms(1-3) + by (fastforce simp: Effect.app_def xcpt_app_def xcpt_eff_def) + next + assume norm: "(pc', s') \ set (norm_eff (Invokestatic C M n) P pc (a, b))" + also have "Suc (length a - Suc n) \ mxs" using Invokestatic asms(1,3) + by (simp add: Effect.app_def xcpt_app_def) arith + ultimately show ?thesis using Invokestatic asms(1-3) wf + by (auto simp: Effect.app_def xcpt_app_def norm_eff_def wf_mdecl_def + dest!: sees_wf_mdecl) + qed + qed (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def + xcpt_eff_def norm_eff_def)+ + qed + qed + then show "\s\?A. \p. p < ?n \ ?app p s \ (\(q, s')\set (?step p s). s' \ ?A)" + by clarsimp + qed + then show ?thesis by (simp add: JVM_states_unfold) +qed (*>*) declare is_relevant_entry_def [simp del] declare set_drop_subset [simp del] lemma lesubstep_type_simple: "xs [\\<^bsub>Product.le (=) r\<^esub>] ys \ set xs {\\<^bsub>r\<^esub>} set ys" (*<*) - apply (unfold lesubstep_type_def) - apply clarify - apply (simp add: set_conv_nth) - apply clarify - apply (drule le_listD, assumption) - apply (clarsimp simp add: lesub_def Product.le_def) - apply (rule exI) - apply (rule conjI) - apply (rule exI) - apply (rule conjI) - apply (rule sym) - apply assumption - apply assumption - apply assumption - done +proof - + assume assm: "xs [\\<^bsub>Product.le (=) r\<^esub>] ys" + have "\a b i y. (a, b) = xs ! i \ i < length xs + \ \\'. (\i. (a, \') = ys ! i \ i < length xs) \ b \\<^bsub>r\<^esub> \'" + proof - + fix a b i assume ith: "(a, b) = xs ! i" and len: "i < length xs" + obtain \ where "ys ! i = (a, \) \ r b \" + using le_listD[OF assm len] ith + by (clarsimp simp: lesub_def Product.le_def) + then have "(a, \) = ys ! i \ b \\<^bsub>r\<^esub> \" + by (clarsimp simp: lesub_def) + with len show "\\'. (\i. (a, \') = ys ! i \ i < length xs) \ b \\<^bsub>r\<^esub> \'" + by fastforce + qed + then show "set xs {\\<^bsub>r\<^esub>} set ys" using assm + by (clarsimp simp: lesubstep_type_def set_conv_nth) +qed (*>*) declare is_relevant_entry_def [simp del] lemma conjI2: "\ A; A \ B \ \ A \ B" by blast lemma (in JVM_sl) eff_mono: - "\wf_prog p P; pc < length is; s \\<^bsub>sup_state_opt P\<^esub> t; app pc t\ - \ set (eff pc s) {\\<^bsub>sup_state_opt P\<^esub>} set (eff pc t)" +assumes wf: "wf_prog p P" and "pc < length is" and + lesub: "s \\<^bsub>sup_state_opt P\<^esub> t" and app: "app pc t" +shows "set (eff pc s) {\\<^bsub>sup_state_opt P\<^esub>} set (eff pc t)" (*<*) - apply simp - apply (unfold Effect.eff_def) - apply (cases t) - apply (simp add: lesub_def) - apply (rename_tac a) - apply (cases s) - apply simp - apply (rename_tac b) - apply simp - apply (rule lesubstep_union) - prefer 2 - apply (rule lesubstep_type_simple) - apply (simp add: xcpt_eff_def) - apply (rule le_listI) - apply (simp add: split_beta) - apply (simp add: split_beta) - apply (simp add: lesub_def fun_of_def) - apply (case_tac a) - apply (case_tac b) - apply simp - apply (subgoal_tac "size ab = size aa") - prefer 2 - apply (clarsimp simp add: list_all2_lengthD) - apply simp - apply (clarsimp simp add: norm_eff_def lesubstep_type_def lesub_def iff del: sup_state_conv) - apply (rule exI) - apply (rule conjI2) - apply (rule imageI) - apply (clarsimp simp add: Effect.app_def iff del: sup_state_conv) - apply (drule (2) succs_mono) - apply blast - apply simp - apply (erule eff\<^sub>i_mono) - apply simp - apply assumption - apply clarsimp - apply clarsimp - done +proof(cases t) + case None then show ?thesis using lesub + by (simp add: Effect.eff_def lesub_def) +next + case tSome: (Some a) + show ?thesis proof(cases s) + case None then show ?thesis using lesub + by (simp add: Effect.eff_def lesub_def) + next + case (Some b) + let ?norm = "\x. norm_eff (is ! pc) P pc x" + let ?xcpt = "\x. xcpt_eff (is ! pc) P pc x xt" + let ?r = "Product.le (=) (sup_state_opt P)" + let ?\' = "\eff\<^sub>i (is ! pc, P, a)\" + { + fix x assume xb: "x \ set (succs (is ! pc) b pc)" + then have appi: "app\<^sub>i (is ! pc, P, pc, mxs, T\<^sub>r, a)" and + bia: "P \ b \\<^sub>i a" and appa: "app pc \a\" + using lesub app tSome Some by (auto simp add: lesub_def Effect.app_def) + have xa: "x \ set (succs (is ! pc) a pc)" + using xb succs_mono[OF wf appi bia] by auto + then have "(x, ?\') \ (\pc'. (pc', ?\')) ` set (succs (is ! pc) a pc)" + by (rule imageI) + moreover have "P \ \eff\<^sub>i (is ! pc, P, b)\ \' ?\'" + using xb xa eff\<^sub>i_mono[OF wf bia] appa by fastforce + ultimately have "\\'. (x, \') \ (\pc'. (pc', \eff\<^sub>i (is ! pc, P, a)\)) ` set (succs (is ! pc) a pc) \ + P \ \eff\<^sub>i (is ! pc, P, b)\ \' \'" by blast + } + then have norm: "set (?norm b) {\\<^bsub>sup_state_opt P\<^esub>} set (?norm a)" + using tSome Some by (clarsimp simp: norm_eff_def lesubstep_type_def lesub_def) + obtain a1 b1 a2 b2 where a: "a = (a1, b1)" and b: "b = (a2, b2)" + using tSome Some by fastforce + then have a12: "size a2 = size a1" using lesub tSome Some + by (clarsimp simp: lesub_def list_all2_lengthD) + have "length (?xcpt b) = length (?xcpt a)" + by (simp add: xcpt_eff_def split_beta) + moreover have "\n. n < length (?xcpt b) \ (?xcpt b) ! n \\<^bsub>?r\<^esub> (?xcpt a) ! n" + using lesub tSome Some a b a12 + by (simp add: xcpt_eff_def split_beta fun_of_def) (simp add: lesub_def) + ultimately have "?xcpt b [\\<^bsub>?r\<^esub>] ?xcpt a" + by(rule le_listI) + then have "set (?xcpt b) {\\<^bsub>sup_state_opt P\<^esub>} set (?xcpt a)" + by (rule lesubstep_type_simple) + moreover note norm + ultimately have + "set (?norm b) \ set (?xcpt b) {\\<^bsub>sup_state_opt P\<^esub>} set (?norm a) \ set (?xcpt a)" + by(intro lesubstep_union) + then show ?thesis using tSome Some by(simp add: Effect.eff_def) + qed +qed (*>*) lemma (in JVM_sl) bounded_step: "bounded step (size is)" (*<*) - apply simp - apply (unfold bounded_def err_step_def Effect.app_def Effect.eff_def) - apply (auto simp add: error_def map_snd_def split: err.splits option.splits) - done + by (auto simp: bounded_def err_step_def Effect.app_def Effect.eff_def + error_def map_snd_def + split: err.splits option.splits) (*>*) theorem (in JVM_sl) step_mono: "wf_prog wf_mb P \ mono r step (size is) A" (*<*) - apply (simp add: JVM_le_Err_conv) - apply (insert bounded_step) - apply (unfold JVM_states_unfold) - apply (rule mono_lift) - apply blast - apply (unfold app_mono_def lesub_def) - apply clarsimp - apply (erule (2) app_mono) - apply simp - apply clarify - apply (drule eff_mono) - apply (auto simp add: lesub_def) - done +proof - + assume wf: "wf_prog wf_mb P" + let ?r = "sup_state_opt P" and ?n = "length is" and ?app = app and ?step = eff + let ?A = "opt (\ {list n (types P) |n. n \ mxs} \ + list ((case b of Static \ 0 | NonStatic \ 1) + length Ts + mxl\<^sub>0) + (err (types P)))" + have "order ?r" using wf by simp + moreover have "app_mono ?r ?app ?n ?A" using app_mono[OF wf] + by (clarsimp simp: app_mono_def lesub_def) + moreover have "bounded (err_step ?n ?app ?step) ?n" using bounded_step + by simp + moreover have "\s p t. s \ ?A \ p < ?n \ s \\<^bsub>?r\<^esub> t \ + ?app p t \ set (?step p s) {\\<^bsub>?r\<^esub>} set (?step p t)" + using eff_mono[OF wf] by simp + ultimately have "mono (Err.le ?r) (err_step ?n ?app ?step) ?n (err ?A)" + by(rule mono_lift) + then show "mono r step (size is) A" using bounded_step + by (simp add: JVM_le_Err_conv JVM_states_unfold) +qed (*>*) lemma (in start_context) first_in_A [iff]: "OK first \ A" using Ts C by (cases b; force intro!: list_appendI simp add: JVM_states_unfold) lemma (in JVM_sl) wt_method_def2: "wt_method P C' b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \s = (is \ [] \ size \s = size is \ OK ` set \s \ states P mxs mxl \ wt_start P C' b Ts mxl\<^sub>0 \s \ wt_app_eff (sup_state_opt P) app eff \s)" (*<*) - apply (unfold wt_method_def wt_app_eff_def wt_instr_def lesub_def check_types_def) - apply auto - done + by (unfold wt_method_def wt_app_eff_def wt_instr_def lesub_def + check_types_def) auto (*>*) end