1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 *) 10 11theory CTranslation 12imports 13 "PackedTypes" 14 "PrettyProgs" 15 "StaticFun" 16 "IndirectCalls" 17 "ModifiesProofs" 18keywords 19 "cond_sorry_modifies_proofs" 20 "install_C_file" 21 "install_C_types" 22 "new_C_include_dir":: thy_decl 23and 24 "memsafe" 25 "c_types" 26 "c_defs" 27begin 28 29lemma TWO: "Suc (Suc 0) = 2" 30by arith 31 32definition 33 fun_addr_of :: "int \<Rightarrow> unit ptr" where 34 "fun_addr_of i \<equiv> Ptr (word_of_int i)" 35 36definition 37 ptr_range :: "'a::c_type ptr \<Rightarrow> addr set" where 38 "ptr_range p \<equiv> {ptr_val (p::'a ptr) ..< 39 ptr_val p + word_of_int(int(size_of (TYPE('a)))) }" 40 41lemma guarded_spec_body_wp [vcg_hoare]: 42"P \<subseteq> 43{s. (\<forall>t. (s,t) \<in> R \<longrightarrow> t \<in> Q) \<and> (Ft \<notin> F \<longrightarrow> (\<exists>t. (s,t) \<in> R))} 44\<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub> P (guarded_spec_body Ft R) Q, A" 45apply (simp add: guarded_spec_body_def) 46apply (cases "Ft \<in> F") 47apply (erule HoarePartialDef.Guarantee) 48apply (rule HoarePartialDef.conseqPre, rule HoarePartialDef.Spec) 49apply auto[1] 50apply (rule HoarePartialDef.conseqPre, rule HoarePartialDef.Guard[where P=P]) 51apply (rule HoarePartialDef.conseqPre, rule HoarePartialDef.Spec) 52apply auto[1] 53apply simp 54apply (erule order_trans) 55apply (auto simp: image_def Bex_def) 56done 57 58 59ML_file "tools/mlyacc/mlyacclib/MLY_base-sig.ML" 60ML_file "tools/mlyacc/mlyacclib/MLY_join.ML" 61ML_file "tools/mlyacc/mlyacclib/MLY_lrtable.ML" 62ML_file "tools/mlyacc/mlyacclib/MLY_stream.ML" 63ML_file "tools/mlyacc/mlyacclib/MLY_parser2.ML" 64ML_file "FunctionalRecordUpdate.ML" 65ML_file "topo_sort.ML" 66ML_file "isa_termstypes.ML" 67ML_file "StrictC.grm.sig" 68ML_file "StrictC.grm.sml" 69ML_file "StrictC.lex.sml" 70ML_file "StrictCParser.ML" 71ML_file "complit.ML" 72ML_file "hp_termstypes.ML" 73ML_file "termstypes-sig.ML" 74ML_file "termstypes.ML" 75ML_file "UMM_termstypes.ML" 76ML_file "recursive_records/recursive_record_pp.ML" 77ML_file "recursive_records/recursive_record_package.ML" 78ML_file "expression_typing.ML" 79ML_file "UMM_Proofs.ML" 80ML_file "program_analysis.ML" 81ML_file "heapstatetype.ML" 82ML_file "MemoryModelExtras-sig.ML" 83ML_file "MemoryModelExtras.ML" 84ML_file "calculate_state.ML" 85ML_file "syntax_transforms.ML" 86ML_file "expression_translation.ML" 87ML_file "modifies_proofs.ML" 88ML_file "HPInter.ML" 89ML_file "stmt_translation.ML" 90ML_file "isar_install.ML" 91 92declare typ_info_word [simp del] 93declare typ_info_ptr [simp del] 94 95lemma valid_call_Spec_eq_subset: 96 "\<Gamma>' procname = Some (Spec R) \<Longrightarrow> 97 HoarePartialDef.valid \<Gamma>' NF P (Call procname) Q A = (P \<subseteq> fst ` R \<and> (R \<subseteq> (- P) \<times> UNIV \<union> UNIV \<times> Q))" 98 apply (safe, simp_all) 99 apply (clarsimp simp: HoarePartialDef.valid_def) 100 apply (rule ccontr) 101 apply (drule_tac x="Normal x" in spec, elim allE, 102 drule mp, erule exec.Call, rule exec.SpecStuck) 103 apply (auto simp: image_def)[2] 104 apply (clarsimp simp: HoarePartialDef.valid_def) 105 apply (elim allE, drule mp, erule exec.Call, erule exec.Spec) 106 apply auto[1] 107 apply (clarsimp simp: HoarePartialDef.valid_def) 108 apply (erule exec_Normal_elim_cases, simp_all) 109 apply (erule exec_Normal_elim_cases, auto) 110 done 111 112lemma creturn_wp [vcg_hoare]: 113 assumes "P \<subseteq> {s. (exnupd (\<lambda>_. Return)) (rvupd (\<lambda>_. v s) s) \<in> A}" 114 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P creturn exnupd rvupd v Q, A" 115 unfolding creturn_def 116 by vcg 117 118lemma creturn_void_wp [vcg_hoare]: 119 assumes "P \<subseteq> {s. (exnupd (\<lambda>_. Return)) s \<in> A}" 120 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P creturn_void exnupd Q, A" 121 unfolding creturn_void_def 122 by vcg 123 124lemma cbreak_wp [vcg_hoare]: 125 assumes "P \<subseteq> {s. (exnupd (\<lambda>_. Break)) s \<in> A}" 126 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P cbreak exnupd Q, A" 127 unfolding cbreak_def 128 by vcg 129 130lemma ccatchbrk_wp [vcg_hoare]: 131 assumes "P \<subseteq> {s. (exnupd s = Break \<longrightarrow> s \<in> Q) \<and> 132 (exnupd s \<noteq> Break \<longrightarrow> s \<in> A)}" 133 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P ccatchbrk exnupd Q, A" 134 unfolding ccatchbrk_def 135 by vcg 136 137lemma cchaos_wp [vcg_hoare]: 138 assumes "P \<subseteq> {s. \<forall>x. (v x s) \<in> Q }" 139 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P cchaos v Q, A" 140 unfolding cchaos_def 141 apply (rule HoarePartial.Spec) 142 using assms 143 apply blast 144 done 145 146lemma lvar_nondet_init_wp [vcg_hoare]: 147 "P \<subseteq> {s. \<forall>v. (upd (\<lambda>_. v)) s \<in> Q} \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub> P lvar_nondet_init accessor upd Q, A" 148 unfolding lvar_nondet_init_def 149 by (rule HoarePartialDef.conseqPre, vcg, auto) 150 151lemma mem_safe_lvar_init [simp,intro]: 152 assumes upd: "\<And>g v s. globals_update g (upd (\<lambda>_. v) s) = upd (\<lambda>_. v) (globals_update g s)" 153 assumes acc: "\<And>v s. globals (upd (\<lambda>_. v) s) = globals s" 154 assumes upd_acc: "\<And>s. upd (\<lambda>_. accessor s) s = s" 155 shows "mem_safe (lvar_nondet_init accessor upd) x" 156 apply (clarsimp simp: mem_safe_def lvar_nondet_init_def) 157 apply (erule exec.cases, simp_all) 158 apply clarsimp 159 apply (clarsimp simp: restrict_safe_def restrict_safe_OK_def acc) 160 apply (rule exec.Spec) 161 apply clarsimp 162 apply (rule exI) 163 apply (simp add: restrict_htd_def upd acc) 164 apply (clarsimp simp: restrict_safe_def) 165 apply (simp add: exec_fatal_def) 166 apply (rule disjI2) 167 apply (rule exec.SpecStuck) 168 apply (clarsimp simp: restrict_htd_def upd acc) 169 apply (erule allE)+ 170 apply (erule notE) 171 apply (rule sym) 172 apply (rule upd_acc) 173 done 174 175lemma intra_safe_lvar_nondet_init [simp]: 176 "intra_safe (lvar_nondet_init accessor upd :: (('a::heap_state_type','d) state_scheme,'b,'c) com) = 177 (\<forall>\<Gamma>. mem_safe (lvar_nondet_init accessor upd :: (('a::heap_state_type','d) state_scheme,'b,'c) com) (\<Gamma> :: (('a,'d) state_scheme,'b,'c) body))" 178 by (simp add: lvar_nondet_init_def) 179 180lemma proc_deps_lvar_nondet_init [simp]: 181 "proc_deps (lvar_nondet_init accessor upd) \<Gamma> = {}" 182 by (simp add: lvar_nondet_init_def) 183 184end 185