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