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