(* Title: JinjaThreads/BV/BVNoTypeError.thy Author: Gerwin Klein, Andreas Lochbihler *) section ‹Welltyped Programs produce no Type Errors› theory BVNoTypeError imports "../JVM/JVMDefensive" BVSpecTypeSafe begin lemma wt_jvm_prog_states: "⟦ wf_jvm_prog⇘Φ⇙ P; P ⊢ C sees M: Ts→T = ⌊(mxs, mxl, ins, et)⌋ in C; Φ C M ! pc = τ; pc < size ins ⟧ ⟹ OK τ ∈ states P mxs (1+size Ts+mxl)" (*<*) apply (unfold wf_jvm_prog_phi_def) apply (drule (1) sees_wf_mdecl) apply (simp add: wf_mdecl_def wt_method_def check_types_def) apply (blast intro: nth_in) done (*>*) context JVM_heap_conf_base' begin declare is_IntgI [simp, intro] declare is_BoolI [simp, intro] declare is_RefI [simp] text ‹ The main theorem: welltyped programs do not produce type errors if they are started in a conformant state. › theorem no_type_error: assumes welltyped: "wf_jvm_prog⇘Φ⇙ P" and conforms: "Φ ⊢ t:σ √" shows "exec_d P t σ ≠ TypeError" (*<*) proof - from welltyped obtain mb where wf: "wf_prog mb P" by (fast dest: wt_jvm_progD) obtain xcp h frs where s [simp]: "σ = (xcp, h, frs)" by (cases σ) have "check P σ" proof(cases frs) case Nil with conforms show ?thesis by (unfold correct_state_def check_def) auto next case (Cons f frs') then obtain stk reg C M pc where frs [simp]: "frs = (stk,reg,C,M,pc)#frs'" and f: "f = (stk,reg,C,M,pc)" by(cases f) fastforce from conforms obtain ST LT Ts T mxs mxl ins xt where hconf: "hconf h" and tconf: "P,h ⊢ t √t" and meth: "P ⊢ C sees M:Ts→T = ⌊(mxs, mxl, ins, xt)⌋ in C" and Φ: "Φ C M ! pc = Some (ST,LT)" and frame: "conf_f P h (ST,LT) ins (stk,reg,C,M,pc)" and frames: "conf_fs P h Φ M (size Ts) T frs'" and confxcp: "conf_xcp P h xcp (ins ! pc)" by (fastforce simp add: correct_state_def dest: sees_method_fun) from frame obtain stk: "P,h ⊢ stk [:≤] ST" and reg: "P,h ⊢ reg [:≤⇩_{⊤}] LT" and pc: "pc < size ins" by (simp add: conf_f_def) from welltyped meth Φ pc have "OK (Some (ST, LT)) ∈ states P mxs (1+size Ts+mxl)" by (rule wt_jvm_prog_states) hence "size ST ≤ mxs" by (auto simp add: JVM_states_unfold listE_length) with stk have mxs: "size stk ≤ mxs" by (auto dest: list_all2_lengthD) from welltyped meth pc have "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" by (rule wt_jvm_prog_impl_wt_instr) hence app⇩_{0}: "app (ins!pc) P mxs T pc (size ins) xt (Φ C M!pc) " by (simp add: wt_instr_def) with Φ have eff: "∀(pc',s')∈set (eff (ins ! pc) P pc xt (Φ C M ! pc)). pc' < size ins" by (unfold app_def) simp from app⇩_{0}Φ have app: "xcpt_app (ins!pc) P pc mxs xt (ST,LT) ∧ app⇩_{i}(ins!pc, P, pc, mxs, T, (ST,LT))" by (clarsimp simp add: app_def) show ?thesis proof(cases xcp) case None note xcp[simp] = this from app eff stk reg have "check_instr (ins!pc) P h stk reg C M pc frs'" proof (cases "ins!pc") case ALoad with app stk reg Φ obtain T ST' where ST: "ST = Integer # T # ST'" and TNT: "T ≠ NT ⟶ (∃T'. T = T'⌊⌉)" by auto from stk ST obtain i stk' ref where stk': "stk = Intg i # ref # stk'" and ref: "P,h ⊢ ref :≤ T" by(auto simp add: conf_def list_all2_Cons2) from ref TNT have is_Ref: "is_Ref ref" by(cases ref)(auto simp add: is_Ref_def conf_def) moreover { assume refN: "ref ≠ Null" with ref have "T ≠ NT" by auto with TNT obtain T' where T': "T = T'⌊⌉" by auto with ref refN is_Ref wf have "∃T n. typeof_addr h (the_Addr ref) = ⌊Array_type T n⌋" by(cases ref)(auto simp add:conf_def widen_Array) } ultimately show ?thesis using ALoad stk' by(auto) next case AStore with app stk reg Φ obtain T U ST' where ST: "ST = T # Integer # U # ST'" and TNT: "U ≠ NT ⟶ (∃T'. U = T'⌊⌉)" by auto from stk ST obtain e i stk' ref where stk': "stk = e # Intg i # ref # stk'" and ref: "P,h ⊢ ref :≤ U" and e: "P,h ⊢ e :≤ T" by(fastforce simp add: conf_def list_all2_Cons2) from ref TNT have is_Ref: "is_Ref ref" by(cases ref)(auto simp add: is_Ref_def conf_def) moreover { assume refN: "ref ≠ Null" with ref have "U ≠ NT" by auto with TNT obtain T' where T': "U = T'⌊⌉" by auto with ref refN is_Ref wf have "∃T n. typeof_addr h (the_Addr ref) = ⌊Array_type T n⌋" by(cases ref)(auto simp add:conf_def widen_Array) } ultimately show ?thesis using AStore stk' e by(auto simp add: conf_def) next case ALength with app stk reg Φ obtain T ST' where ST: "ST = T # ST'" and TNT: "T ≠ NT ⟶ (∃T'. T = T'⌊⌉)" by auto from stk ST obtain stk' ref where stk': "stk = ref # stk'" and ref: "P,h ⊢ ref :≤ T" by(auto simp add: conf_def list_all2_Cons2) from ref TNT have is_Ref: "is_Ref ref" by(cases ref)(auto simp add: is_Ref_def conf_def) moreover { assume refN: "ref ≠ Null" with ref have "T ≠ NT" by auto with TNT obtain T' where T': "T = T'⌊⌉" by auto with ref refN is_Ref wf have "∃T n. typeof_addr h (the_Addr ref) = ⌊Array_type T n⌋" by(cases ref)(auto simp add:conf_def widen_Array) } ultimately show ?thesis using ALength stk' by(auto) next case (Getfield F C) with app stk reg Φ obtain v vT stk' fm where field: "P ⊢ C sees F:vT (fm) in C" and stk: "stk = v # stk'" and conf: "P,h ⊢ v :≤ Class C" by(fastforce simp add: list_all2_Cons2) from conf have is_Ref: "is_Ref v" by(cases v)(auto simp add: is_Ref_def conf_def) moreover { assume "v ≠ Null" with conf field is_Ref wf have "∃U. typeof_addr h (the_Addr v) = Some U ∧ P ⊢ class_type_of U ≼⇧^{*}C" by (auto dest!: non_npD2) } ultimately show ?thesis using Getfield field stk by auto next case (Putfield F C) with app stk reg Φ obtain v ref vT stk' fm where field: "P ⊢ C sees F:vT (fm) in C" and stk: "stk = v # ref # stk'" and confv: "P,h ⊢ v :≤ vT" and confr: "P,h ⊢ ref :≤ Class C" by(fastforce simp add: list_all2_Cons2) from confr have is_Ref: "is_Ref ref" by(cases ref)(auto simp add: is_Ref_def conf_def) moreover { assume "ref ≠ Null" with confr field is_Ref wf have "∃U. typeof_addr h (the_Addr ref) = Some U ∧ P ⊢ class_type_of U ≼⇧^{*}C" by (auto dest: non_npD2) } ultimately show ?thesis using Putfield field stk confv by auto next case (CAS F C) with app stk reg Φ obtain v v' v'' T' stk' fm where field: "P ⊢ C sees F:T' (fm) in C" and stk: "stk = v'' # v' # v # stk'" and confv: "P,h ⊢ v' :≤ T'" "P,h ⊢ v'' :≤ T'" and confr: "P,h ⊢ v :≤ Class C" and vol: "volatile fm" by(fastforce simp add: list_all2_Cons2) from confr have is_Ref: "is_Ref v" by(cases v)(auto simp add: is_Ref_def conf_def) moreover { assume "v ≠ Null" with confr field is_Ref wf have "∃U. typeof_addr h (the_Addr v) = Some U ∧ P ⊢ class_type_of U ≼⇧^{*}C" by (auto dest: non_npD2) } ultimately show ?thesis using CAS field stk confv vol by auto next case (Invoke M' n) with app have n: "n < size ST" by simp from stk have [simp]: "size stk = size ST" by (rule list_all2_lengthD) { assume "stk!n = Null" with n Invoke have ?thesis by simp } moreover { assume "ST!n = NT" with n stk have "stk!n = Null" by (auto simp: list_all2_conv_all_nth) with n Invoke have ?thesis by simp } moreover { assume Null: "stk!n ≠ Null" and NT: "ST!n ≠ NT" from NT app Invoke obtain D D' Ts T m where D: "class_type_of' (ST!n) = ⌊D⌋" and M': "P ⊢ D sees M': Ts→T = m in D'" and Ts: "P ⊢ rev (take n ST) [≤] Ts" by auto from stk n have "P,h ⊢ stk!n :≤ ST!n" by (auto simp: list_all2_conv_all_nth) with Null D obtain a U where [simp]: "stk!n = Addr a" "typeof_addr h a = Some U" and UsubSTn: "P ⊢ ty_of_htype U ≤ ST!n" by(cases "stk ! n")(auto simp add: conf_def widen_Class) from D UsubSTn obtain C' where U: "class_type_of' (ty_of_htype U) = ⌊C'⌋" and "P ⊢ C' ≼⇧^{*}D" by(rule widen_is_class_type_of) simp from ‹P ⊢ C' ≼⇧^{*}D› wf M' obtain m' Ts' T' D'' where C': "P ⊢ C' sees M': Ts'→T' = m' in D''" and Ts': "P ⊢ Ts [≤] Ts'" by (auto dest!: sees_method_mono) from stk have "P,h ⊢ take n stk [:≤] take n ST" .. hence "P,h ⊢ rev (take n stk) [:≤] rev (take n ST)" .. also note Ts also note Ts' finally have "P,h ⊢ rev (take n stk) [:≤] Ts'" . hence ?thesis using Invoke Null n C' U by (auto simp add: is_Ref_def2 has_methodI intro: sees_wf_native[OF wf]) } ultimately show ?thesis by blast next case Return with stk app Φ meth frames show ?thesis by (fastforce simp add: has_methodI list_all2_Cons2) next case ThrowExc with stk app Φ meth frames show ?thesis by(auto 4 3 simp add: xcpt_app_def conf_def list_all2_Cons2 intro!: is_RefI intro: widen_trans[OF _ widen_subcls]) next case (BinOpInstr bop) with stk app Φ meth frames show ?thesis by(auto simp add: conf_def list_all2_Cons2)(force dest: WTrt_binop_widen_mono) qed (auto simp add: list_all2_lengthD list_all2_Cons2) thus "check P σ" using meth pc mxs by (simp add: check_def has_methodI) next case (Some a) with confxcp obtain D where "typeof_addr h a = ⌊Class_type D⌋" by(auto simp add: check_xcpt_def) moreover from stk have "length stk = length ST" by(rule list_all2_lengthD) ultimately show ?thesis using meth pc mxs Some confxcp app using match_is_relevant[of P D ins pc pc xt] by(auto simp add: check_def has_methodI check_xcpt_def xcpt_app_def dest: bspec) qed qed thus "exec_d P t σ ≠ TypeError" .. qed lemma welltyped_commute: "⟦wf_jvm_prog⇘Φ⇙ P; Φ ⊢ t:σ √⟧ ⟹ P,t ⊢ Normal σ -ta-jvmd→ Normal σ' = P,t ⊢ σ -ta-jvm→ σ'" apply(rule iffI) apply(erule exec_1_d.cases, simp, fastforce simp add: exec_d_def exec_1_iff split: if_split_asm) by(auto dest!: no_type_error intro!: exec_1_d.intros simp add: exec_d_def exec_1_iff split: if_split_asm) end lemma (in JVM_conf_read) BV_correct_d_1: "⟦ wf_jvm_prog⇘Φ⇙ P; P,t ⊢ Normal σ -ta-jvmd→ Normal σ'; Φ ⊢ t:σ √ ⟧ ⟹ Φ ⊢ t:σ' √" unfolding welltyped_commute by(rule BV_correct_1) lemma not_TypeError_eq [iff]: "x ≠ TypeError = (∃t. x = Normal t)" by (cases x) auto end