(* Title: HOL/MicroJava/BV/BVNoTypeErrors.thy Author: Gerwin Klein Copyright GPL *) section ‹Welltyped Programs produce no Type Errors› theory BVNoTypeError imports "../JVM/JVMDefensive" BVSpecTypeSafe begin lemma has_methodI: "P ⊢ C sees M:Ts→T = m in D ⟹ P ⊢ C has M" by (unfold has_method_def) blast text ‹ Some simple lemmas about the type testing functions of the defensive JVM: › lemma typeof_NoneD [simp,dest]: "typeof v = Some x ⟹ ¬is_Addr v" by (cases v) auto lemma is_Ref_def2: "is_Ref v = (v = Null ∨ (∃a. v = Addr a))" by (cases v) (auto simp add: is_Ref_def) lemma [iff]: "is_Ref Null" by (simp add: is_Ref_def2) lemma is_RefI [intro, simp]: "P,h ⊢ v :≤ T ⟹ is_refT T ⟹ is_Ref v" (*<*) apply (cases T) apply (auto simp add: is_refT_def is_Ref_def dest: conf_ClassD) done (*>*) lemma is_IntgI [intro, simp]: "P,h ⊢ v :≤ Integer ⟹ is_Intg v" (*<*) apply (unfold conf_def) apply auto done (*>*) lemma is_BoolI [intro, simp]: "P,h ⊢ v :≤ Boolean ⟹ is_Bool v" (*<*) apply (unfold conf_def) apply auto done (*>*) declare defs1 [simp del] 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 (*>*) text ‹ The main theorem: welltyped programs do not produce type errors if they are started in a conformant state. › theorem no_type_error: fixes σ :: jvm_state assumes welltyped: "wf_jvm_prog⇘Φ⇙ P" and conforms: "P,Φ ⊢ σ √" shows "exec_d P σ ≠ 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 σ) from conforms have "xcp ≠ None ∨ frs = [] ⟹ check P σ" by (unfold correct_state_def check_def) auto moreover { assume "¬(xcp ≠ None ∨ frs = [])" then obtain stk reg C M pc frs' where xcp [simp]: "xcp = None" and frs [simp]: "frs = (stk,reg,C,M,pc)#frs'" by (clarsimp simp add: neq_Nil_conv) from conforms obtain ST LT Ts T mxs mxl ins xt where hconf: "P ⊢ h √" 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'" 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) 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) with eff stk reg have "check_instr (ins!pc) P h stk reg C M pc frs'" proof (cases "ins!pc") case (Getfield F C) with app stk reg Φ obtain v vT stk' where field: "P ⊢ C sees F:vT in C" and stk: "stk = v # stk'" and conf: "P,h ⊢ v :≤ Class C" by auto from conf have is_Ref: "is_Ref v" by auto moreover { assume "v ≠ Null" with conf field is_Ref wf have "∃D vs. h (the_Addr v) = Some (D,vs) ∧ P ⊢ D ≼⇧^{*}C" by (auto dest!: non_npD) } ultimately show ?thesis using Getfield field stk hconf apply clarsimp apply (rule conjI, fastforce) apply clarsimp apply (drule has_visible_field) apply (drule (1) has_field_mono) apply (drule (1) hconfD) apply (unfold oconf_def has_field_def) apply clarsimp apply (fastforce dest: has_fields_fun) done next case (Putfield F C) with app stk reg Φ obtain v ref vT stk' where field: "P ⊢ C sees F:vT in C" and stk: "stk = v # ref # stk'" and confv: "P,h ⊢ v :≤ vT" and confr: "P,h ⊢ ref :≤ Class C" by fastforce from confr have is_Ref: "is_Ref ref" by simp moreover { assume "ref ≠ Null" with confr field is_Ref wf have "∃D vs. h (the_Addr ref) = Some (D,vs) ∧ P ⊢ D ≼⇧^{*}C" by (auto dest: non_npD) } ultimately show ?thesis using Putfield field stk confv by fastforce 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: "ST!n = Class D" and M': "P ⊢ D sees M': Ts→T = m in D'" and Ts: "P ⊢ rev (take n ST) [≤] Ts" by auto from D stk n have "P,h ⊢ stk!n :≤ Class D" by (auto simp: list_all2_conv_all_nth) with Null obtain a C' fs where [simp]: "stk!n = Addr a" "h a = Some (C',fs)" and "P ⊢ C' ≼⇧^{*}D" by (fastforce dest!: conf_ClassD) with M' wf 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'" . with Invoke Null n C' have ?thesis by (auto simp add: is_Ref_def2 has_methodI) } ultimately show ?thesis by blast next case Return with stk app Φ meth frames show ?thesis by (auto simp add: has_methodI) qed (auto simp add: list_all2_lengthD) hence "check P σ" using meth pc mxs by (simp add: check_def has_methodI) } ultimately have "check P σ" by blast thus "exec_d P σ ≠ TypeError" .. qed (*>*) text ‹ The theorem above tells us that, in welltyped programs, the defensive machine reaches the same result as the aggressive one (after arbitrarily many steps). › theorem welltyped_aggressive_imp_defensive: "wf_jvm_prog⇘Φ⇙ P ⟹ P,Φ ⊢ σ √ ⟹ P ⊢ σ -jvm→ σ' ⟹ P ⊢ (Normal σ) -jvmd→ (Normal σ')" (*<*) apply (simp only: exec_all_def) apply (erule rtrancl_induct) apply (simp add: exec_all_d_def1) apply simp apply (simp only: exec_all_def [symmetric]) apply (frule BV_correct, assumption+) apply (drule no_type_error, assumption, drule no_type_error_commutes, simp) apply (simp add: exec_all_d_def1) apply (rule rtrancl_trans, assumption) apply (drule exec_1_d_NormalI) apply auto done (*>*) text ‹ As corollary we get that the aggressive and the defensive machine are equivalent for welltyped programs (if started in a conformant state or in the canonical start state) › corollary welltyped_commutes: fixes σ :: jvm_state assumes wf: "wf_jvm_prog⇘Φ⇙ P" and conforms: "P,Φ ⊢ σ √" shows "P ⊢ (Normal σ) -jvmd→ (Normal σ') = P ⊢ σ -jvm→ σ'" apply rule apply (erule defensive_imp_aggressive) apply (erule welltyped_aggressive_imp_defensive [OF wf conforms]) done corollary welltyped_initial_commutes: assumes wf: "wf_jvm_prog P" assumes meth: "P ⊢ C sees M:[]→T = b in C" defines start: "σ ≡ start_state P C M" shows "P ⊢ (Normal σ) -jvmd→ (Normal σ') = P ⊢ σ -jvm→ σ'" proof - from wf obtain Φ where wf': "wf_jvm_prog⇘Φ⇙ P" by (auto simp: wf_jvm_prog_def) from this meth have "P,Φ ⊢ σ √" unfolding start by (rule BV_correct_initial) with wf' show ?thesis by (rule welltyped_commutes) qed lemma not_TypeError_eq [iff]: "x ≠ TypeError = (∃t. x = Normal t)" by (cases x) auto locale cnf = fixes P and Φ and σ assumes wf: "wf_jvm_prog⇘Φ⇙ P" assumes cnf: "correct_state P Φ σ" theorem (in cnf) no_type_errors: "P ⊢ (Normal σ) -jvmd→ σ' ⟹ σ' ≠ TypeError" apply (unfold exec_all_d_def1) apply (erule rtrancl_induct) apply simp apply (fold exec_all_d_def1) apply (insert cnf wf) apply clarsimp apply (drule defensive_imp_aggressive) apply (frule (2) BV_correct) apply (drule (1) no_type_error) back apply (auto simp add: exec_1_d_eq) done locale start = fixes P and C and M and σ and T and b assumes wf: "wf_jvm_prog P" assumes sees: "P ⊢ C sees M:[]→T = b in C" defines "σ ≡ Normal (start_state P C M)" corollary (in start) bv_no_type_error: shows "P ⊢ σ -jvmd→ σ' ⟹ σ' ≠ TypeError" proof - from wf obtain Φ where "wf_jvm_prog⇘Φ⇙ P" by (auto simp: wf_jvm_prog_def) moreover with sees have "correct_state P Φ (start_state P C M)" by - (rule BV_correct_initial) ultimately have "cnf P Φ (start_state P C M)" by (rule cnf.intro) moreover assume "P ⊢ σ -jvmd→ σ'" ultimately show ?thesis by (unfold σ_def) (rule cnf.no_type_errors) qed end