1 | (* *********************************************************************) |
---|
2 | (* *) |
---|
3 | (* The Compcert verified compiler *) |
---|
4 | (* *) |
---|
5 | (* Xavier Leroy, INRIA Paris-Rocquencourt *) |
---|
6 | (* *) |
---|
7 | (* Copyright Institut National de Recherche en Informatique et en *) |
---|
8 | (* Automatique. All rights reserved. This file is distributed *) |
---|
9 | (* under the terms of the GNU General Public License as published by *) |
---|
10 | (* the Free Software Foundation, either version 2 of the License, or *) |
---|
11 | (* (at your option) any later version. This file is also distributed *) |
---|
12 | (* under the terms of the INRIA Non-Commercial License Agreement. *) |
---|
13 | (* *) |
---|
14 | (* *********************************************************************) |
---|
15 | |
---|
16 | (* * Dynamic semantics for the Clight language *) |
---|
17 | |
---|
18 | (*include "Coqlib.ma".*) |
---|
19 | (*include "Errors.ma".*) |
---|
20 | (*include "Integers.ma".*) |
---|
21 | (*include "Floats.ma".*) |
---|
22 | (*include "Values.ma".*) |
---|
23 | (*include "AST.ma".*) |
---|
24 | (*include "Mem.ma".*) |
---|
25 | include "common/Globalenvs.ma". |
---|
26 | include "Clight/Csyntax.ma". |
---|
27 | include "common/Maps.ma". |
---|
28 | (*include "Events.ma".*) |
---|
29 | include "common/Smallstep.ma". |
---|
30 | |
---|
31 | (* * * Semantics of type-dependent operations *) |
---|
32 | |
---|
33 | (* * Interpretation of values as truth values. |
---|
34 | Non-zero integers, non-zero floats and non-null pointers are |
---|
35 | considered as true. The integer zero (which also represents |
---|
36 | the null pointer) and the float 0.0 are false. *) |
---|
37 | |
---|
38 | inductive is_false: val → type → Prop ≝ |
---|
39 | | is_false_int: ∀sz,sg. |
---|
40 | is_false (Vint sz (zero ?)) (Tint sz sg) |
---|
41 | | is_false_pointer: ∀r,r',t. |
---|
42 | is_false (Vnull r) (Tpointer r' t) |
---|
43 | | is_false_float: ∀sz. |
---|
44 | is_false (Vfloat Fzero) (Tfloat sz). |
---|
45 | |
---|
46 | inductive is_true: val → type → Prop ≝ |
---|
47 | | is_true_int_int: ∀sz,sg,n. |
---|
48 | n ≠ (zero ?) → |
---|
49 | is_true (Vint sz n) (Tint sz sg) |
---|
50 | | is_true_pointer_pointer: ∀r,b,pc,ofs,s,t. |
---|
51 | is_true (Vptr r b pc ofs) (Tpointer s t) |
---|
52 | | is_true_float: ∀f,sz. |
---|
53 | f ≠ Fzero → |
---|
54 | is_true (Vfloat f) (Tfloat sz). |
---|
55 | |
---|
56 | inductive bool_of_val : val → type → val → Prop ≝ |
---|
57 | | bool_of_val_true: ∀v,ty. |
---|
58 | is_true v ty → |
---|
59 | bool_of_val v ty Vtrue |
---|
60 | | bool_of_val_false: ∀v,ty. |
---|
61 | is_false v ty → |
---|
62 | bool_of_val v ty Vfalse. |
---|
63 | |
---|
64 | (* * The following [sem_] functions compute the result of an operator |
---|
65 | application. Since operators are overloaded, the result depends |
---|
66 | both on the static types of the arguments and on their run-time values. |
---|
67 | Unlike in C, automatic conversions between integers and floats |
---|
68 | are not performed. For instance, [e1 + e2] is undefined if [e1] |
---|
69 | is a float and [e2] an integer. The Clight producer must have explicitly |
---|
70 | promoted [e2] to a float. *) |
---|
71 | |
---|
72 | let rec sem_neg (v: val) (ty: type) : option val ≝ |
---|
73 | match ty with |
---|
74 | [ Tint sz _ ⇒ |
---|
75 | match v with |
---|
76 | [ Vint sz' n ⇒ if eq_intsize sz sz' |
---|
77 | then Some ? (Vint ? (two_complement_negation ? n)) |
---|
78 | else None ? |
---|
79 | | _ ⇒ None ? |
---|
80 | ] |
---|
81 | | Tfloat _ ⇒ |
---|
82 | match v with |
---|
83 | [ Vfloat f ⇒ Some ? (Vfloat (Fneg f)) |
---|
84 | | _ ⇒ None ? |
---|
85 | ] |
---|
86 | | _ ⇒ None ? |
---|
87 | ]. |
---|
88 | |
---|
89 | let rec sem_notint (v: val) : option val ≝ |
---|
90 | match v with |
---|
91 | [ Vint sz n ⇒ Some ? (Vint ? (exclusive_disjunction_bv ? n (mone ?))) (* XXX *) |
---|
92 | | _ ⇒ None ? |
---|
93 | ]. |
---|
94 | |
---|
95 | let rec sem_notbool (v: val) (ty: type) : option val ≝ |
---|
96 | match ty with |
---|
97 | [ Tint sz _ ⇒ |
---|
98 | match v with |
---|
99 | [ Vint sz' n ⇒ if eq_intsize sz sz' |
---|
100 | then Some ? (of_bool (eq_bv ? n (zero ?))) |
---|
101 | else None ? |
---|
102 | | _ ⇒ None ? |
---|
103 | ] |
---|
104 | | Tpointer _ _ ⇒ |
---|
105 | match v with |
---|
106 | [ Vptr _ _ _ _ ⇒ Some ? Vfalse |
---|
107 | | Vnull _ ⇒ Some ? Vtrue |
---|
108 | | _ ⇒ None ? |
---|
109 | ] |
---|
110 | | Tfloat _ ⇒ |
---|
111 | match v with |
---|
112 | [ Vfloat f ⇒ Some ? (of_bool (Fcmp Ceq f Fzero)) |
---|
113 | | _ ⇒ None ? |
---|
114 | ] |
---|
115 | | _ ⇒ None ? |
---|
116 | ]. |
---|
117 | |
---|
118 | let rec sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
119 | match classify_add t1 t2 with |
---|
120 | [ add_case_ii ⇒ (**r integer addition *) |
---|
121 | match v1 with |
---|
122 | [ Vint sz1 n1 ⇒ match v2 with |
---|
123 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
124 | (λn1. Some ? (Vint ? (addition_n ? n1 n2))) (None ?) |
---|
125 | | _ ⇒ None ? ] |
---|
126 | | _ ⇒ None ? ] |
---|
127 | | add_case_ff ⇒ (**r float addition *) |
---|
128 | match v1 with |
---|
129 | [ Vfloat n1 ⇒ match v2 with |
---|
130 | [ Vfloat n2 ⇒ Some ? (Vfloat (Fadd n1 n2)) |
---|
131 | | _ ⇒ None ? ] |
---|
132 | | _ ⇒ None ? ] |
---|
133 | | add_case_pi ty ⇒ (**r pointer plus integer *) |
---|
134 | match v1 with |
---|
135 | [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with |
---|
136 | [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (shift_offset_n ? ofs1 (sizeof ty) n2)) |
---|
137 | | _ ⇒ None ? ] |
---|
138 | | Vnull r ⇒ match v2 with |
---|
139 | [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? |
---|
140 | | _ ⇒ None ? ] |
---|
141 | | _ ⇒ None ? ] |
---|
142 | | add_case_ip ty ⇒ (**r integer plus pointer *) |
---|
143 | match v1 with |
---|
144 | [ Vint sz1 n1 ⇒ match v2 with |
---|
145 | [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset_n ? ofs2 (sizeof ty) n1)) |
---|
146 | | Vnull r ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ? |
---|
147 | | _ ⇒ None ? ] |
---|
148 | | _ ⇒ None ? ] |
---|
149 | | add_default ⇒ None ? |
---|
150 | ]. |
---|
151 | |
---|
152 | let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
153 | match classify_sub t1 t2 with |
---|
154 | [ sub_case_ii ⇒ (**r integer subtraction *) |
---|
155 | match v1 with |
---|
156 | [ Vint sz1 n1 ⇒ match v2 with |
---|
157 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
158 | (λn1.Some ? (Vint sz2 (subtraction ? n1 n2))) (None ?) |
---|
159 | | _ ⇒ None ? ] |
---|
160 | | _ ⇒ None ? ] |
---|
161 | | sub_case_ff ⇒ (**r float subtraction *) |
---|
162 | match v1 with |
---|
163 | [ Vfloat f1 ⇒ match v2 with |
---|
164 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2)) |
---|
165 | | _ ⇒ None ? ] |
---|
166 | | _ ⇒ None ? ] |
---|
167 | | sub_case_pi ty ⇒ (**r pointer minus integer *) |
---|
168 | match v1 with |
---|
169 | [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with |
---|
170 | [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset_n ? ofs1 (sizeof ty) n2)) |
---|
171 | | _ ⇒ None ? ] |
---|
172 | | Vnull r ⇒ match v2 with |
---|
173 | [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? |
---|
174 | | _ ⇒ None ? ] |
---|
175 | | _ ⇒ None ? ] |
---|
176 | | sub_case_pp ty ⇒ (**r pointer minus pointer *) |
---|
177 | match v1 with |
---|
178 | [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with |
---|
179 | [ Vptr r2 b2 p2 ofs2 ⇒ |
---|
180 | if eq_block b1 b2 then |
---|
181 | if eqb (sizeof ty) 0 then None ? |
---|
182 | else match division_u ? (sub_offset ? ofs1 ofs2) (repr (sizeof ty)) with |
---|
183 | [ None ⇒ None ? |
---|
184 | | Some v ⇒ Some ? (Vint I32 v) (* XXX choose size from result type? *) |
---|
185 | ] |
---|
186 | else None ? |
---|
187 | | _ ⇒ None ? ] |
---|
188 | | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ] |
---|
189 | | _ ⇒ None ? ] |
---|
190 | | sub_default ⇒ None ? |
---|
191 | ]. |
---|
192 | |
---|
193 | let rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
194 | match classify_mul t1 t2 with |
---|
195 | [ mul_case_ii ⇒ |
---|
196 | match v1 with |
---|
197 | [ Vint sz1 n1 ⇒ match v2 with |
---|
198 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
199 | (λn1. Some ? (Vint sz2 (\snd (split ??? (multiplication ? n1 n2))))) (None ?) |
---|
200 | | _ ⇒ None ? ] |
---|
201 | | _ ⇒ None ? ] |
---|
202 | | mul_case_ff ⇒ |
---|
203 | match v1 with |
---|
204 | [ Vfloat f1 ⇒ match v2 with |
---|
205 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2)) |
---|
206 | | _ ⇒ None ? ] |
---|
207 | | _ ⇒ None ? ] |
---|
208 | | mul_default ⇒ |
---|
209 | None ? |
---|
210 | ]. |
---|
211 | |
---|
212 | let rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
213 | match classify_div t1 t2 with |
---|
214 | [ div_case_I32unsi ⇒ |
---|
215 | match v1 with |
---|
216 | [ Vint sz1 n1 ⇒ match v2 with |
---|
217 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
218 | (λn1. option_map … (Vint ?) (division_u ? n1 n2)) (None ?) |
---|
219 | | _ ⇒ None ? ] |
---|
220 | | _ ⇒ None ? ] |
---|
221 | | div_case_ii ⇒ |
---|
222 | match v1 with |
---|
223 | [ Vint sz1 n1 ⇒ match v2 with |
---|
224 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
225 | (λn1. option_map … (Vint ?) (division_s ? n1 n2)) (None ?) |
---|
226 | | _ ⇒ None ? ] |
---|
227 | | _ ⇒ None ? ] |
---|
228 | | div_case_ff ⇒ |
---|
229 | match v1 with |
---|
230 | [ Vfloat f1 ⇒ match v2 with |
---|
231 | [ Vfloat f2 ⇒ Some ? (Vfloat(Fdiv f1 f2)) |
---|
232 | | _ ⇒ None ? ] |
---|
233 | | _ ⇒ None ? ] |
---|
234 | | div_default ⇒ |
---|
235 | None ? |
---|
236 | ]. |
---|
237 | |
---|
238 | let rec sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
239 | match classify_mod t1 t2 with |
---|
240 | [ mod_case_I32unsi ⇒ |
---|
241 | match v1 with |
---|
242 | [ Vint sz1 n1 ⇒ match v2 with |
---|
243 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
244 | (λn1. option_map … (Vint ?) (modulus_u ? n1 n2)) (None ?) |
---|
245 | | _ ⇒ None ? ] |
---|
246 | | _ ⇒ None ? ] |
---|
247 | | mod_case_ii ⇒ |
---|
248 | match v1 with |
---|
249 | [ Vint sz1 n1 ⇒ match v2 with |
---|
250 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
251 | (λn1. option_map … (Vint ?) (modulus_s ? n1 n2)) (None ?) |
---|
252 | | _ ⇒ None ? ] |
---|
253 | | _ ⇒ None ? ] |
---|
254 | | mod_default ⇒ |
---|
255 | None ? |
---|
256 | ]. |
---|
257 | |
---|
258 | let rec sem_and (v1,v2: val) : option val ≝ |
---|
259 | match v1 with |
---|
260 | [ Vint sz1 n1 ⇒ match v2 with |
---|
261 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
262 | (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2))) (None ?) |
---|
263 | | _ ⇒ None ? ] |
---|
264 | | _ ⇒ None ? |
---|
265 | ]. |
---|
266 | |
---|
267 | let rec sem_or (v1,v2: val) : option val ≝ |
---|
268 | match v1 with |
---|
269 | [ Vint sz1 n1 ⇒ match v2 with |
---|
270 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
271 | (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2))) (None ?) |
---|
272 | | _ ⇒ None ? ] |
---|
273 | | _ ⇒ None ? |
---|
274 | ]. |
---|
275 | |
---|
276 | let rec sem_xor (v1,v2: val) : option val ≝ |
---|
277 | match v1 with |
---|
278 | [ Vint sz1 n1 ⇒ match v2 with |
---|
279 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
280 | (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2))) (None ?) |
---|
281 | | _ ⇒ None ? ] |
---|
282 | | _ ⇒ None ? |
---|
283 | ]. |
---|
284 | |
---|
285 | let rec sem_shl (v1,v2: val): option val ≝ |
---|
286 | match v1 with |
---|
287 | [ Vint sz1 n1 ⇒ match v2 with |
---|
288 | [ Vint sz2 n2 ⇒ |
---|
289 | if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1)) |
---|
290 | then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false)) |
---|
291 | else None ? |
---|
292 | | _ ⇒ None ? ] |
---|
293 | | _ ⇒ None ? ]. |
---|
294 | |
---|
295 | let rec sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val ≝ |
---|
296 | match classify_shr t1 t2 with |
---|
297 | [ shr_case_I32unsi ⇒ |
---|
298 | match v1 with |
---|
299 | [ Vint sz1 n1 ⇒ match v2 with |
---|
300 | [ Vint sz2 n2 ⇒ |
---|
301 | if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1)) |
---|
302 | then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 false)) |
---|
303 | else None ? |
---|
304 | | _ ⇒ None ? ] |
---|
305 | | _ ⇒ None ? ] |
---|
306 | | shr_case_ii => |
---|
307 | match v1 with |
---|
308 | [ Vint sz1 n1 ⇒ match v2 with |
---|
309 | [ Vint sz2 n2 ⇒ |
---|
310 | if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1)) |
---|
311 | then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1))) |
---|
312 | else None ? |
---|
313 | | _ ⇒ None ? ] |
---|
314 | | _ ⇒ None ? ] |
---|
315 | | shr_default ⇒ |
---|
316 | None ? |
---|
317 | ]. |
---|
318 | |
---|
319 | let rec sem_cmp_mismatch (c: comparison): option val ≝ |
---|
320 | match c with |
---|
321 | [ Ceq => Some ? Vfalse |
---|
322 | | Cne => Some ? Vtrue |
---|
323 | | _ => None ? |
---|
324 | ]. |
---|
325 | |
---|
326 | let rec sem_cmp_match (c: comparison): option val ≝ |
---|
327 | match c with |
---|
328 | [ Ceq => Some ? Vtrue |
---|
329 | | Cne => Some ? Vfalse |
---|
330 | | _ => None ? |
---|
331 | ]. |
---|
332 | |
---|
333 | let rec sem_cmp (c:comparison) |
---|
334 | (v1: val) (t1: type) (v2: val) (t2: type) |
---|
335 | (m: mem): option val ≝ |
---|
336 | match classify_cmp t1 t2 with |
---|
337 | [ cmp_case_I32unsi ⇒ |
---|
338 | match v1 with |
---|
339 | [ Vint sz1 n1 ⇒ match v2 with |
---|
340 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
341 | (λn1. Some ? (of_bool (cmpu_int ? c n1 n2))) (None ?) |
---|
342 | | _ ⇒ None ? ] |
---|
343 | | _ ⇒ None ? ] |
---|
344 | | cmp_case_ii ⇒ |
---|
345 | match v1 with |
---|
346 | [ Vint sz1 n1 ⇒ match v2 with |
---|
347 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
348 | (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) (None ?) |
---|
349 | | _ ⇒ None ? |
---|
350 | ] |
---|
351 | | _ ⇒ None ? |
---|
352 | ] |
---|
353 | | cmp_case_pp ⇒ |
---|
354 | match v1 with |
---|
355 | [ Vptr r1 b1 p1 ofs1 ⇒ |
---|
356 | match v2 with |
---|
357 | [ Vptr r2 b2 p2 ofs2 ⇒ |
---|
358 | if valid_pointer m r1 b1 ofs1 |
---|
359 | ∧ valid_pointer m r2 b2 ofs2 then |
---|
360 | if eq_block b1 b2 |
---|
361 | then Some ? (of_bool (cmp_offset c ofs1 ofs2)) |
---|
362 | else sem_cmp_mismatch c |
---|
363 | else None ? |
---|
364 | | Vnull r2 ⇒ sem_cmp_mismatch c |
---|
365 | | _ ⇒ None ? ] |
---|
366 | | Vnull r1 ⇒ |
---|
367 | match v2 with |
---|
368 | [ Vptr r2 b2 p2 ofs2 ⇒ sem_cmp_mismatch c |
---|
369 | | Vnull r2 ⇒ sem_cmp_match c |
---|
370 | | _ ⇒ None ? |
---|
371 | ] |
---|
372 | | _ ⇒ None ? ] |
---|
373 | | cmp_case_ff ⇒ |
---|
374 | match v1 with |
---|
375 | [ Vfloat f1 ⇒ |
---|
376 | match v2 with |
---|
377 | [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2)) |
---|
378 | | _ ⇒ None ? ] |
---|
379 | | _ ⇒ None ? ] |
---|
380 | | cmp_default ⇒ None ? |
---|
381 | ]. |
---|
382 | |
---|
383 | definition sem_unary_operation |
---|
384 | : unary_operation → val → type → option val ≝ |
---|
385 | λop,v,ty. |
---|
386 | match op with |
---|
387 | [ Onotbool => sem_notbool v ty |
---|
388 | | Onotint => sem_notint v |
---|
389 | | Oneg => sem_neg v ty |
---|
390 | ]. |
---|
391 | |
---|
392 | let rec sem_binary_operation |
---|
393 | (op: binary_operation) |
---|
394 | (v1: val) (t1: type) (v2: val) (t2:type) |
---|
395 | (m: mem): option val ≝ |
---|
396 | match op with |
---|
397 | [ Oadd ⇒ sem_add v1 t1 v2 t2 |
---|
398 | | Osub ⇒ sem_sub v1 t1 v2 t2 |
---|
399 | | Omul ⇒ sem_mul v1 t1 v2 t2 |
---|
400 | | Omod ⇒ sem_mod v1 t1 v2 t2 |
---|
401 | | Odiv ⇒ sem_div v1 t1 v2 t2 |
---|
402 | | Oand ⇒ sem_and v1 v2 |
---|
403 | | Oor ⇒ sem_or v1 v2 |
---|
404 | | Oxor ⇒ sem_xor v1 v2 |
---|
405 | | Oshl ⇒ sem_shl v1 v2 |
---|
406 | | Oshr ⇒ sem_shr v1 t1 v2 t2 |
---|
407 | | Oeq ⇒ sem_cmp Ceq v1 t1 v2 t2 m |
---|
408 | | One ⇒ sem_cmp Cne v1 t1 v2 t2 m |
---|
409 | | Olt ⇒ sem_cmp Clt v1 t1 v2 t2 m |
---|
410 | | Ogt ⇒ sem_cmp Cgt v1 t1 v2 t2 m |
---|
411 | | Ole ⇒ sem_cmp Cle v1 t1 v2 t2 m |
---|
412 | | Oge ⇒ sem_cmp Cge v1 t1 v2 t2 m |
---|
413 | ]. |
---|
414 | |
---|
415 | (* * Semantic of casts. [cast v1 t1 t2 v2] holds if value [v1], |
---|
416 | viewed with static type [t1], can be cast to type [t2], |
---|
417 | resulting in value [v2]. *) |
---|
418 | |
---|
419 | let rec cast_int_int (sz: intsize) (sg: signedness) (dstsz: intsize) (i: BitVector (bitsize_of_intsize sz)) : BitVector (bitsize_of_intsize dstsz) ≝ |
---|
420 | match sg with [ Signed ⇒ sign_ext ?? i | Unsigned ⇒ zero_ext ?? i ]. |
---|
421 | |
---|
422 | let rec cast_int_float (si : signedness) (n:nat) (i: BitVector n) : float ≝ |
---|
423 | match si with |
---|
424 | [ Signed ⇒ floatofint ? i |
---|
425 | | Unsigned ⇒ floatofintu ? i |
---|
426 | ]. |
---|
427 | |
---|
428 | let rec cast_float_int (sz : intsize) (si : signedness) (f: float) : BitVector (bitsize_of_intsize sz) ≝ |
---|
429 | match si with |
---|
430 | [ Signed ⇒ intoffloat ? f |
---|
431 | | Unsigned ⇒ intuoffloat ? f |
---|
432 | ]. |
---|
433 | |
---|
434 | let rec cast_float_float (sz: floatsize) (f: float) : float ≝ |
---|
435 | match sz with |
---|
436 | [ F32 ⇒ singleoffloat f |
---|
437 | | F64 ⇒ f |
---|
438 | ]. |
---|
439 | |
---|
440 | inductive type_region : type → region → Prop ≝ |
---|
441 | | type_rgn_pointer : ∀s,t. type_region (Tpointer s t) s |
---|
442 | | type_rgn_array : ∀s,t,n. type_region (Tarray s t n) s |
---|
443 | (* XXX Is the following necessary? *) |
---|
444 | | type_rgn_code : ∀tys,ty. type_region (Tfunction tys ty) Code. |
---|
445 | |
---|
446 | inductive cast : mem → val → type → type → val → Prop ≝ |
---|
447 | | cast_ii: ∀m,sz2,sz1,si1,si2,i. (**r int to int *) |
---|
448 | cast m (Vint sz1 i) (Tint sz1 si1) (Tint sz2 si2) |
---|
449 | (Vint sz2 (cast_int_int sz1 si1 sz2 i)) |
---|
450 | | cast_fi: ∀m,f,sz1,sz2,si2. (**r float to int *) |
---|
451 | cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2) |
---|
452 | (Vint sz2 (cast_float_int sz2 si2 f)) |
---|
453 | | cast_if: ∀m,sz1,sz2,si1,i. (**r int to float *) |
---|
454 | cast m (Vint sz1 i) (Tint sz1 si1) (Tfloat sz2) |
---|
455 | (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i))) |
---|
456 | | cast_ff: ∀m,f,sz1,sz2. (**r float to float *) |
---|
457 | cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2) |
---|
458 | (Vfloat (cast_float_float sz2 f)) |
---|
459 | | cast_pp: ∀m,r,r',ty,ty',b,pc,ofs. |
---|
460 | type_region ty r → |
---|
461 | type_region ty' r' → |
---|
462 | ∀pc':pointer_compat b r'. |
---|
463 | cast m (Vptr r b pc ofs) ty ty' (Vptr r' b pc' ofs) |
---|
464 | | cast_ip_z: ∀m,sz,sg,ty',r. |
---|
465 | type_region ty' r → |
---|
466 | cast m (Vint sz (zero ?)) (Tint sz sg) ty' (Vnull r) |
---|
467 | | cast_pp_z: ∀m,ty,ty',r,r'. |
---|
468 | type_region ty r → |
---|
469 | type_region ty' r' → |
---|
470 | cast m (Vnull r) ty ty' (Vnull r'). |
---|
471 | |
---|
472 | (* * * Operational semantics *) |
---|
473 | |
---|
474 | (* * The semantics uses two environments. The global environment |
---|
475 | maps names of functions and global variables to memory block references, |
---|
476 | and function pointers to their definitions. (See module [Globalenvs].) *) |
---|
477 | |
---|
478 | definition genv ≝ (genv_t Genv) clight_fundef. |
---|
479 | |
---|
480 | (* * The local environment maps local variables to block references. |
---|
481 | The current value of the variable is stored in the associated memory |
---|
482 | block. *) |
---|
483 | |
---|
484 | definition env ≝ (tree_t ? PTree) block. (* map variable -> location *) |
---|
485 | |
---|
486 | definition empty_env: env ≝ (empty …). |
---|
487 | |
---|
488 | (* * [load_value_of_type ty m b ofs] computes the value of a datum |
---|
489 | of type [ty] residing in memory [m] at block [b], offset [ofs]. |
---|
490 | If the type [ty] indicates an access by value, the corresponding |
---|
491 | memory load is performed. If the type [ty] indicates an access by |
---|
492 | reference, the pointer [Vptr b ofs] is returned. *) |
---|
493 | |
---|
494 | let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: offset) : option val ≝ |
---|
495 | match access_mode ty with |
---|
496 | [ By_value chunk ⇒ loadv chunk m (Vptr Any b ? ofs) |
---|
497 | | By_reference r ⇒ |
---|
498 | match pointer_compat_dec b r with |
---|
499 | [ inl p ⇒ Some ? (Vptr r b p ofs) |
---|
500 | | inr _ ⇒ None ? |
---|
501 | ] |
---|
502 | | By_nothing ⇒ None ? |
---|
503 | ]. |
---|
504 | cases b // |
---|
505 | qed. |
---|
506 | |
---|
507 | (* * Symmetrically, [store_value_of_type ty m b ofs v] returns the |
---|
508 | memory state after storing the value [v] in the datum |
---|
509 | of type [ty] residing in memory [m] at block [b], offset [ofs]. |
---|
510 | This is allowed only if [ty] indicates an access by value. *) |
---|
511 | |
---|
512 | let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: offset) (v: val) : option mem ≝ |
---|
513 | match access_mode ty_dest with |
---|
514 | [ By_value chunk ⇒ storev chunk m (Vptr Any loc ? ofs) v |
---|
515 | | By_reference _ ⇒ None ? |
---|
516 | | By_nothing ⇒ None ? |
---|
517 | ]. |
---|
518 | cases loc // |
---|
519 | qed. |
---|
520 | |
---|
521 | (* * Allocation of function-local variables. |
---|
522 | [alloc_variables e1 m1 vars e2 m2] allocates one memory block |
---|
523 | for each variable declared in [vars], and associates the variable |
---|
524 | name with this block. [e1] and [m1] are the initial local environment |
---|
525 | and memory state. [e2] and [m2] are the final local environment |
---|
526 | and memory state. *) |
---|
527 | |
---|
528 | inductive alloc_variables: env → mem → |
---|
529 | list (ident × type) → |
---|
530 | env → mem → Prop ≝ |
---|
531 | | alloc_variables_nil: |
---|
532 | ∀e,m. |
---|
533 | alloc_variables e m (nil ?) e m |
---|
534 | | alloc_variables_cons: |
---|
535 | ∀e,m,id,ty,vars,m1,b1,m2,e2. |
---|
536 | alloc m 0 (sizeof ty) Any = 〈m1, b1〉 → |
---|
537 | alloc_variables (set … id b1 e) m1 vars e2 m2 → |
---|
538 | alloc_variables e m (〈id, ty〉 :: vars) e2 m2. |
---|
539 | |
---|
540 | (* * Initialization of local variables that are parameters to a function. |
---|
541 | [bind_parameters e m1 params args m2] stores the values [args] |
---|
542 | in the memory blocks corresponding to the variables [params]. |
---|
543 | [m1] is the initial memory state and [m2] the final memory state. *) |
---|
544 | |
---|
545 | inductive bind_parameters: env → |
---|
546 | mem → list (ident × type) → list val → |
---|
547 | mem → Prop ≝ |
---|
548 | | bind_parameters_nil: |
---|
549 | ∀e,m. |
---|
550 | bind_parameters e m (nil ?) (nil ?) m |
---|
551 | | bind_parameters_cons: |
---|
552 | ∀e,m,id,ty,params,v1,vl,b,m1,m2. |
---|
553 | get ??? id e = Some ? b → |
---|
554 | store_value_of_type ty m b zero_offset v1 = Some ? m1 → |
---|
555 | bind_parameters e m1 params vl m2 → |
---|
556 | bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2. |
---|
557 | |
---|
558 | (* * Return the list of blocks in the codomain of [e]. *) |
---|
559 | |
---|
560 | definition blocks_of_env : env → list block ≝ λe. |
---|
561 | map ?? (λx. snd ?? x) (elements ??? e). |
---|
562 | |
---|
563 | (* * Selection of the appropriate case of a [switch], given the value [n] |
---|
564 | of the selector expression. *) |
---|
565 | (* FIXME: now that we have several sizes of integer, it isn't clear whether we |
---|
566 | should allow case labels to be of a different size to the switch expression. *) |
---|
567 | let rec select_switch (sz:intsize) (n: BitVector (bitsize_of_intsize sz)) (sl: labeled_statements) |
---|
568 | on sl : labeled_statements ≝ |
---|
569 | match sl with |
---|
570 | [ LSdefault _ ⇒ sl |
---|
571 | | LScase sz' c s sl' ⇒ intsize_eq_elim ? sz sz' ? n |
---|
572 | (λn. if eq_bv ? c n then sl else select_switch sz' n sl') (select_switch sz n sl') |
---|
573 | ]. |
---|
574 | |
---|
575 | (* * Turn a labeled statement into a sequence *) |
---|
576 | |
---|
577 | let rec seq_of_labeled_statement (sl: labeled_statements) : statement ≝ |
---|
578 | match sl with |
---|
579 | [ LSdefault s ⇒ s |
---|
580 | | LScase _ c s sl' ⇒ Ssequence s (seq_of_labeled_statement sl') |
---|
581 | ]. |
---|
582 | |
---|
583 | (* |
---|
584 | Section SEMANTICS. |
---|
585 | |
---|
586 | Variable ge: genv. |
---|
587 | |
---|
588 | (** ** Evaluation of expressions *) |
---|
589 | |
---|
590 | Section EXPR. |
---|
591 | |
---|
592 | Variable e: env. |
---|
593 | Variable m: mem. |
---|
594 | *) |
---|
595 | (* * [eval_expr ge e m a v] defines the evaluation of expression [a] |
---|
596 | in r-value position. [v] is the value of the expression. |
---|
597 | [e] is the current environment and [m] is the current memory state. *) |
---|
598 | |
---|
599 | inductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝ |
---|
600 | | eval_Econst_int: ∀sz,sg,i. |
---|
601 | eval_expr ge e m (Expr (Econst_int sz i) (Tint sz sg)) (Vint sz i) E0 |
---|
602 | | eval_Econst_float: ∀f,ty. |
---|
603 | eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0 |
---|
604 | | eval_Elvalue: ∀a,ty,loc,ofs,v,tr. |
---|
605 | eval_lvalue ge e m (Expr a ty) loc ofs tr → |
---|
606 | load_value_of_type ty m loc ofs = Some ? v → |
---|
607 | eval_expr ge e m (Expr a ty) v tr |
---|
608 | | eval_Eaddrof: ∀a,ty,r,loc,ofs,tr. |
---|
609 | eval_lvalue ge e m a loc ofs tr → |
---|
610 | ∀pc:pointer_compat loc r. |
---|
611 | eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc pc ofs) tr |
---|
612 | | eval_Esizeof: ∀ty',sz,sg. |
---|
613 | eval_expr ge e m (Expr (Esizeof ty') (Tint sz sg)) (Vint sz (repr ? (sizeof ty'))) E0 |
---|
614 | | eval_Eunop: ∀op,a,ty,v1,v,tr. |
---|
615 | eval_expr ge e m a v1 tr → |
---|
616 | sem_unary_operation op v1 (typeof a) = Some ? v → |
---|
617 | eval_expr ge e m (Expr (Eunop op a) ty) v tr |
---|
618 | | eval_Ebinop: ∀op,a1,a2,ty,v1,v2,v,tr1,tr2. |
---|
619 | eval_expr ge e m a1 v1 tr1 → |
---|
620 | eval_expr ge e m a2 v2 tr2 → |
---|
621 | sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v → |
---|
622 | eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v (tr1⧺tr2) |
---|
623 | | eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2,tr1,tr2. |
---|
624 | eval_expr ge e m a1 v1 tr1 → |
---|
625 | is_true v1 (typeof a1) → |
---|
626 | eval_expr ge e m a2 v2 tr2 → |
---|
627 | eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v2 (tr1⧺tr2) |
---|
628 | | eval_Econdition_false: ∀a1,a2,a3,ty,v1,v3,tr1,tr2. |
---|
629 | eval_expr ge e m a1 v1 tr1 → |
---|
630 | is_false v1 (typeof a1) → |
---|
631 | eval_expr ge e m a3 v3 tr2 → |
---|
632 | eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3 (tr1⧺tr2) |
---|
633 | | eval_Eorbool_1: ∀a1,a2,ty,v1,tr. |
---|
634 | eval_expr ge e m a1 v1 tr → |
---|
635 | is_true v1 (typeof a1) → |
---|
636 | eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue tr |
---|
637 | | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2. |
---|
638 | eval_expr ge e m a1 v1 tr1 → |
---|
639 | is_false v1 (typeof a1) → |
---|
640 | eval_expr ge e m a2 v2 tr2 → |
---|
641 | bool_of_val v2 (typeof a2) v → |
---|
642 | eval_expr ge e m (Expr (Eorbool a1 a2) ty) v (tr1⧺tr2) |
---|
643 | | eval_Eandbool_1: ∀a1,a2,ty,v1,tr. |
---|
644 | eval_expr ge e m a1 v1 tr → |
---|
645 | is_false v1 (typeof a1) → |
---|
646 | eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse tr |
---|
647 | | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2. |
---|
648 | eval_expr ge e m a1 v1 tr1 → |
---|
649 | is_true v1 (typeof a1) → |
---|
650 | eval_expr ge e m a2 v2 tr2 → |
---|
651 | bool_of_val v2 (typeof a2) v → |
---|
652 | eval_expr ge e m (Expr (Eandbool a1 a2) ty) v (tr1⧺tr2) |
---|
653 | | eval_Ecast: ∀a,ty,ty',v1,v,tr. |
---|
654 | eval_expr ge e m a v1 tr → |
---|
655 | cast m v1 (typeof a) ty v → |
---|
656 | eval_expr ge e m (Expr (Ecast ty a) ty') v tr |
---|
657 | | eval_Ecost: ∀a,ty,v,l,tr. |
---|
658 | eval_expr ge e m a v tr → |
---|
659 | eval_expr ge e m (Expr (Ecost l a) ty) v (tr⧺Echarge l) |
---|
660 | |
---|
661 | (* * [eval_lvalue ge e m a r b ofs] defines the evaluation of expression [a] |
---|
662 | in l-value position. The result is the memory location [b, ofs] |
---|
663 | that contains the value of the expression [a]. The memory location should |
---|
664 | be representable in a pointer of region r. *) |
---|
665 | |
---|
666 | with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → offset → trace → Prop ≝ |
---|
667 | | eval_Evar_local: ∀id,l,ty. |
---|
668 | (* XXX notation? e!id*) get ??? id e = Some ? l → |
---|
669 | eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0 |
---|
670 | | eval_Evar_global: ∀id,l,ty. |
---|
671 | (* XXX e!id *) get ??? id e = None ? → |
---|
672 | find_symbol ?? ge id = Some ? l → |
---|
673 | eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0 |
---|
674 | | eval_Ederef: ∀a,ty,r,l,p,ofs,tr. |
---|
675 | eval_expr ge e m a (Vptr r l p ofs) tr → |
---|
676 | eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr |
---|
677 | (* Aside: note that each block of memory is entirely contained within one |
---|
678 | memory region; hence adding a field offset will not produce a location |
---|
679 | outside of the original location's region. *) |
---|
680 | | eval_Efield_struct: ∀a,i,ty,l,ofs,id,fList,delta,tr. |
---|
681 | eval_lvalue ge e m a l ofs tr → |
---|
682 | typeof a = Tstruct id fList → |
---|
683 | field_offset i fList = OK ? delta → |
---|
684 | eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ? ofs (repr I32 delta)) tr |
---|
685 | | eval_Efield_union: ∀a,i,ty,l,ofs,id,fList,tr. |
---|
686 | eval_lvalue ge e m a l ofs tr → |
---|
687 | typeof a = Tunion id fList → |
---|
688 | eval_lvalue ge e m (Expr (Efield a i) ty) l ofs tr. |
---|
689 | |
---|
690 | let rec eval_expr_ind (ge:genv) (e:env) (m:mem) |
---|
691 | (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) |
---|
692 | (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i)) |
---|
693 | (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) |
---|
694 | (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) |
---|
695 | (ead:∀a,ty,r,loc,pc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty r loc pc ofs tr H)) |
---|
696 | (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg)) |
---|
697 | (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2)) |
---|
698 | (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3)) |
---|
699 | (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3)) |
---|
700 | (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3)) |
---|
701 | (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2)) |
---|
702 | (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) |
---|
703 | (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2)) |
---|
704 | (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) |
---|
705 | (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2)) |
---|
706 | (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H)) |
---|
707 | (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝ |
---|
708 | match ev with |
---|
709 | [ eval_Econst_int sz sg i ⇒ eci sz sg i |
---|
710 | | eval_Econst_float f ty ⇒ ecF f ty |
---|
711 | | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 |
---|
712 | | eval_Eaddrof a ty r loc pc ofs tr H ⇒ ead a ty r loc pc ofs tr H |
---|
713 | | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg |
---|
714 | | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1) |
---|
715 | | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H2) |
---|
716 | | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3) |
---|
717 | | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a3 v3 tr2 H3) |
---|
718 | | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1) |
---|
719 | | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3) |
---|
720 | | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1) |
---|
721 | | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3) |
---|
722 | | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1) |
---|
723 | | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v tr H) |
---|
724 | ]. |
---|
725 | |
---|
726 | inverter eval_expr_inv_ind for eval_expr : Prop. |
---|
727 | |
---|
728 | let rec eval_lvalue_ind (ge:genv) (e:env) (m:mem) |
---|
729 | (P:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop) |
---|
730 | (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H)) |
---|
731 | (lvg:∀id,l,ty,H1,H2. P ???? (eval_Evar_global ge e m id l ty H1 H2)) |
---|
732 | (lde:∀a,ty,r,l,pc,ofs,tr,H. P ???? (eval_Ederef ge e m a ty r l pc ofs tr H)) |
---|
733 | (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. P a l ofs tr H1 → P ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3)) |
---|
734 | (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. P a l ofs tr H1 → P ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2)) |
---|
735 | (a:expr) (loc:block) (ofs:offset) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : P a loc ofs tr ev ≝ |
---|
736 | match ev with |
---|
737 | [ eval_Evar_local id l ty H ⇒ lvl id l ty H |
---|
738 | | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2 |
---|
739 | | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H |
---|
740 | | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1) |
---|
741 | | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1) |
---|
742 | ]. |
---|
743 | |
---|
744 | (* |
---|
745 | ninverter eval_lvalue_inv_ind for eval_lvalue : Prop. |
---|
746 | *) |
---|
747 | |
---|
748 | definition eval_lvalue_inv_ind : |
---|
749 | ∀x1: genv. |
---|
750 | ∀x2: env. |
---|
751 | ∀x3: mem. |
---|
752 | ∀x4: expr. |
---|
753 | ∀x6: block. |
---|
754 | ∀x7: offset. |
---|
755 | ∀x8: trace. |
---|
756 | ∀P: |
---|
757 | ∀_z1430: expr. |
---|
758 | ∀_z1428: block. ∀_z1427: offset. ∀_z1426: trace. Prop. |
---|
759 | ∀_H1: ?. |
---|
760 | ∀_H2: ?. |
---|
761 | ∀_H3: ?. |
---|
762 | ∀_H4: ?. |
---|
763 | ∀_H5: ?. |
---|
764 | ∀_Hterm: eval_lvalue x1 x2 x3 x4 x6 x7 x8. |
---|
765 | P x4 x6 x7 x8 |
---|
766 | := |
---|
767 | (λx1:genv. |
---|
768 | (λx2:env. |
---|
769 | (λx3:mem. |
---|
770 | (λx4:expr. |
---|
771 | (λx6:block. |
---|
772 | (λx7:offset. |
---|
773 | (λx8:trace. |
---|
774 | (λP:∀_z1430: expr. |
---|
775 | ∀_z1428: block. |
---|
776 | ∀_z1427: offset. ∀_z1426: trace. Prop. |
---|
777 | (λH1:?. |
---|
778 | (λH2:?. |
---|
779 | (λH3:?. |
---|
780 | (λH4:?. |
---|
781 | (λH5:?. |
---|
782 | (λHterm:eval_lvalue x1 x2 x3 x4 x6 x7 x8. |
---|
783 | ((λHcut:∀z1435: eq expr x4 x4. |
---|
784 | ∀z1433: eq block x6 x6. |
---|
785 | ∀z1432: eq offset x7 x7. |
---|
786 | ∀z1431: eq trace x8 x8. |
---|
787 | P x4 x6 x7 x8. |
---|
788 | (Hcut (refl expr x4) |
---|
789 | (refl block x6) |
---|
790 | (refl offset x7) (refl trace x8))) |
---|
791 | ?))))))))))))))). |
---|
792 | [ @(eval_lvalue_ind x1 x2 x3 (λa,loc,ofs,tr,e. ∀e1:eq ? x4 a. ∀e3:eq ? x6 loc. ∀e4:eq ? x7 ofs. ∀e5:eq ? x8 tr. P a loc ofs tr) … Hterm) |
---|
793 | [ @H1 | @H2 | @H3 | @H4 | @H5 ] |
---|
794 | | *: skip |
---|
795 | ] qed. |
---|
796 | |
---|
797 | let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem) |
---|
798 | (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) |
---|
799 | (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop) |
---|
800 | (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i)) |
---|
801 | (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) |
---|
802 | (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) |
---|
803 | (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc)) |
---|
804 | (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg)) |
---|
805 | (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2)) |
---|
806 | (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3)) |
---|
807 | (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3)) |
---|
808 | (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3)) |
---|
809 | (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2)) |
---|
810 | (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) |
---|
811 | (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2)) |
---|
812 | (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) |
---|
813 | (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2)) |
---|
814 | (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H)) |
---|
815 | (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) |
---|
816 | (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) |
---|
817 | (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr r l pc ofs) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H)) |
---|
818 | (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3)) |
---|
819 | (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2)) |
---|
820 | |
---|
821 | (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝ |
---|
822 | match ev with |
---|
823 | [ eval_Econst_int sz sg i ⇒ eci sz sg i |
---|
824 | | eval_Econst_float f ty ⇒ ecF f ty |
---|
825 | | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) loc ofs tr H1) |
---|
826 | | eval_Eaddrof a ty r loc ofs tr H pc ⇒ ead a ty r loc pc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H) |
---|
827 | | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg |
---|
828 | | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1) |
---|
829 | | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H2) |
---|
830 | | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3) |
---|
831 | | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a3 v3 tr2 H3) |
---|
832 | | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1) |
---|
833 | | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3) |
---|
834 | | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1) |
---|
835 | | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3) |
---|
836 | | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1) |
---|
837 | | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v tr H) |
---|
838 | ] |
---|
839 | and eval_lvalue_ind2 (ge:genv) (e:env) (m:mem) |
---|
840 | (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) |
---|
841 | (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop) |
---|
842 | (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i)) |
---|
843 | (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) |
---|
844 | (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) |
---|
845 | (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc)) |
---|
846 | (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg)) |
---|
847 | (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2)) |
---|
848 | (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3)) |
---|
849 | (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3)) |
---|
850 | (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3)) |
---|
851 | (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2)) |
---|
852 | (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) |
---|
853 | (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2)) |
---|
854 | (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) |
---|
855 | (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2)) |
---|
856 | (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H)) |
---|
857 | (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) |
---|
858 | (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) |
---|
859 | (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr r l pc ofs) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H)) |
---|
860 | (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3)) |
---|
861 | (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2)) |
---|
862 | (a:expr) (loc:block) (ofs:offset) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : Q a loc ofs tr ev ≝ |
---|
863 | match ev with |
---|
864 | [ eval_Evar_local id l ty H ⇒ lvl id l ty H |
---|
865 | | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2 |
---|
866 | | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr r l pc ofs) tr H) |
---|
867 | | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1) |
---|
868 | | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1) |
---|
869 | ]. |
---|
870 | |
---|
871 | definition combined_expr_lvalue_ind ≝ |
---|
872 | λge,e,m,P,Q,eci,ecF,elv,ead,esz,eun,ebi,ect,ecf,eo1,eo2,ea1,ea2,ecs,eco,lvl,lvg,lde,lfs,lfu. |
---|
873 | conj ?? |
---|
874 | (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu) |
---|
875 | (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu). |
---|
876 | |
---|
877 | (* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a] |
---|
878 | in l-value position. The result is the memory location [b, ofs] |
---|
879 | that contains the value of the expression [a]. *) |
---|
880 | |
---|
881 | (* |
---|
882 | Scheme eval_expr_ind22 := Minimality for eval_expr Sort Prop |
---|
883 | with eval_lvalue_ind2 := Minimality for eval_lvalue Sort Prop. |
---|
884 | *) |
---|
885 | |
---|
886 | (* * [eval_exprlist ge e m al vl] evaluates a list of r-value |
---|
887 | expressions [al] to their values [vl]. *) |
---|
888 | |
---|
889 | inductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝ |
---|
890 | | eval_Enil: |
---|
891 | eval_exprlist ge e m (nil ?) (nil ?) E0 |
---|
892 | | eval_Econs: ∀a,bl,v,vl,tr1,tr2. |
---|
893 | eval_expr ge e m a v tr1 → |
---|
894 | eval_exprlist ge e m bl vl tr2 → |
---|
895 | eval_exprlist ge e m (a :: bl) (v :: vl) (tr1⧺tr2). |
---|
896 | |
---|
897 | (*End EXPR.*) |
---|
898 | |
---|
899 | (* * ** Transition semantics for statements and functions *) |
---|
900 | |
---|
901 | (* * Continuations *) |
---|
902 | |
---|
903 | inductive cont: Type[0] := |
---|
904 | | Kstop: cont |
---|
905 | | Kseq: statement -> cont -> cont |
---|
906 | (**r [Kseq s2 k] = after [s1] in [s1;s2] *) |
---|
907 | | Kwhile: expr -> statement -> cont -> cont |
---|
908 | (**r [Kwhile e s k] = after [s] in [while (e) s] *) |
---|
909 | | Kdowhile: expr -> statement -> cont -> cont |
---|
910 | (**r [Kdowhile e s k] = after [s] in [do s while (e)] *) |
---|
911 | | Kfor2: expr -> statement -> statement -> cont -> cont |
---|
912 | (**r [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *) |
---|
913 | | Kfor3: expr -> statement -> statement -> cont -> cont |
---|
914 | (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *) |
---|
915 | | Kswitch: cont -> cont |
---|
916 | (**r catches [break] statements arising out of [switch] *) |
---|
917 | | Kcall: option (block × offset × type) -> (**r where to store result *) |
---|
918 | function -> (**r calling function *) |
---|
919 | env -> (**r local env of calling function *) |
---|
920 | cont -> cont. |
---|
921 | |
---|
922 | (* * Pop continuation until a call or stop *) |
---|
923 | |
---|
924 | let rec call_cont (k: cont) : cont := |
---|
925 | match k with |
---|
926 | [ Kseq s k => call_cont k |
---|
927 | | Kwhile e s k => call_cont k |
---|
928 | | Kdowhile e s k => call_cont k |
---|
929 | | Kfor2 e2 e3 s k => call_cont k |
---|
930 | | Kfor3 e2 e3 s k => call_cont k |
---|
931 | | Kswitch k => call_cont k |
---|
932 | | _ => k |
---|
933 | ]. |
---|
934 | |
---|
935 | definition is_call_cont : cont → Prop ≝ λk. |
---|
936 | match k with |
---|
937 | [ Kstop => True |
---|
938 | | Kcall _ _ _ _ => True |
---|
939 | | _ => False |
---|
940 | ]. |
---|
941 | |
---|
942 | (* * States *) |
---|
943 | |
---|
944 | inductive state: Type[0] := |
---|
945 | | State: |
---|
946 | ∀f: function. |
---|
947 | ∀s: statement. |
---|
948 | ∀k: cont. |
---|
949 | ∀e: env. |
---|
950 | ∀m: mem. state |
---|
951 | | Callstate: |
---|
952 | ∀fd: clight_fundef. |
---|
953 | ∀args: list val. |
---|
954 | ∀k: cont. |
---|
955 | ∀m: mem. state |
---|
956 | | Returnstate: |
---|
957 | ∀res: val. |
---|
958 | ∀k: cont. |
---|
959 | ∀m: mem. state. |
---|
960 | |
---|
961 | (* * Find the statement and manufacture the continuation |
---|
962 | corresponding to a label *) |
---|
963 | |
---|
964 | let rec find_label (lbl: label) (s: statement) (k: cont) |
---|
965 | on s: option (statement × cont) := |
---|
966 | match s with |
---|
967 | [ Ssequence s1 s2 => |
---|
968 | match find_label lbl s1 (Kseq s2 k) with |
---|
969 | [ Some sk => Some ? sk |
---|
970 | | None => find_label lbl s2 k |
---|
971 | ] |
---|
972 | | Sifthenelse a s1 s2 => |
---|
973 | match find_label lbl s1 k with |
---|
974 | [ Some sk => Some ? sk |
---|
975 | | None => find_label lbl s2 k |
---|
976 | ] |
---|
977 | | Swhile a s1 => |
---|
978 | find_label lbl s1 (Kwhile a s1 k) |
---|
979 | | Sdowhile a s1 => |
---|
980 | find_label lbl s1 (Kdowhile a s1 k) |
---|
981 | | Sfor a1 a2 a3 s1 => |
---|
982 | match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 s1) k) with |
---|
983 | [ Some sk => Some ? sk |
---|
984 | | None => |
---|
985 | match find_label lbl s1 (Kfor2 a2 a3 s1 k) with |
---|
986 | [ Some sk => Some ? sk |
---|
987 | | None => find_label lbl a3 (Kfor3 a2 a3 s1 k) |
---|
988 | ] |
---|
989 | ] |
---|
990 | | Sswitch e sl => |
---|
991 | find_label_ls lbl sl (Kswitch k) |
---|
992 | | Slabel lbl' s' => |
---|
993 | match ident_eq lbl lbl' with |
---|
994 | [ inl _ ⇒ Some ? 〈s', k〉 |
---|
995 | | inr _ ⇒ find_label lbl s' k |
---|
996 | ] |
---|
997 | | _ => None ? |
---|
998 | ] |
---|
999 | |
---|
1000 | and find_label_ls (lbl: label) (sl: labeled_statements) (k: cont) |
---|
1001 | on sl: option (statement × cont) := |
---|
1002 | match sl with |
---|
1003 | [ LSdefault s => find_label lbl s k |
---|
1004 | | LScase _ _ s sl' => |
---|
1005 | match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with |
---|
1006 | [ Some sk => Some ? sk |
---|
1007 | | None => find_label_ls lbl sl' k |
---|
1008 | ] |
---|
1009 | ]. |
---|
1010 | |
---|
1011 | (* * Transition relation *) |
---|
1012 | |
---|
1013 | (* Strip off outer pointer for use when comparing function types. *) |
---|
1014 | definition fun_typeof ≝ |
---|
1015 | λe. match typeof e with |
---|
1016 | [ Tvoid ⇒ Tvoid |
---|
1017 | | Tint a b ⇒ Tint a b |
---|
1018 | | Tfloat a ⇒ Tfloat a |
---|
1019 | | Tpointer _ ty ⇒ ty |
---|
1020 | | Tarray a b c ⇒ Tarray a b c |
---|
1021 | | Tfunction a b ⇒ Tfunction a b |
---|
1022 | | Tstruct a b ⇒ Tstruct a b |
---|
1023 | | Tunion a b ⇒ Tunion a b |
---|
1024 | | Tcomp_ptr a b ⇒ Tcomp_ptr a b |
---|
1025 | ]. |
---|
1026 | |
---|
1027 | (* XXX: note that cost labels in exprs expose a particular eval order. *) |
---|
1028 | |
---|
1029 | inductive step (ge:genv) : state → trace → state → Prop ≝ |
---|
1030 | |
---|
1031 | | step_assign: ∀f,a1,a2,k,e,m,loc,ofs,v2,m',tr1,tr2. |
---|
1032 | eval_lvalue ge e m a1 loc ofs tr1 → |
---|
1033 | eval_expr ge e m a2 v2 tr2 → |
---|
1034 | store_value_of_type (typeof a1) m loc ofs v2 = Some ? m' → |
---|
1035 | step ge (State f (Sassign a1 a2) k e m) |
---|
1036 | (tr1⧺tr2) (State f Sskip k e m') |
---|
1037 | |
---|
1038 | | step_call_none: ∀f,a,al,k,e,m,vf,vargs,fd,tr1,tr2. |
---|
1039 | eval_expr ge e m a vf tr1 → |
---|
1040 | eval_exprlist ge e m al vargs tr2 → |
---|
1041 | find_funct ?? ge vf = Some ? fd → |
---|
1042 | type_of_fundef fd = fun_typeof a → |
---|
1043 | step ge (State f (Scall (None ?) a al) k e m) |
---|
1044 | (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m) |
---|
1045 | |
---|
1046 | | step_call_some: ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,tr1,tr2,tr3. |
---|
1047 | eval_lvalue ge e m lhs loc ofs tr1 → |
---|
1048 | eval_expr ge e m a vf tr2 → |
---|
1049 | eval_exprlist ge e m al vargs tr3 → |
---|
1050 | find_funct ?? ge vf = Some ? fd → |
---|
1051 | type_of_fundef fd = fun_typeof a → |
---|
1052 | step ge (State f (Scall (Some ? lhs) a al) k e m) |
---|
1053 | (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m) |
---|
1054 | |
---|
1055 | | step_seq: ∀f,s1,s2,k,e,m. |
---|
1056 | step ge (State f (Ssequence s1 s2) k e m) |
---|
1057 | E0 (State f s1 (Kseq s2 k) e m) |
---|
1058 | | step_skip_seq: ∀f,s,k,e,m. |
---|
1059 | step ge (State f Sskip (Kseq s k) e m) |
---|
1060 | E0 (State f s k e m) |
---|
1061 | | step_continue_seq: ∀f,s,k,e,m. |
---|
1062 | step ge (State f Scontinue (Kseq s k) e m) |
---|
1063 | E0 (State f Scontinue k e m) |
---|
1064 | | step_break_seq: ∀f,s,k,e,m. |
---|
1065 | step ge (State f Sbreak (Kseq s k) e m) |
---|
1066 | E0 (State f Sbreak k e m) |
---|
1067 | |
---|
1068 | | step_ifthenelse_true: ∀f,a,s1,s2,k,e,m,v1,tr. |
---|
1069 | eval_expr ge e m a v1 tr → |
---|
1070 | is_true v1 (typeof a) → |
---|
1071 | step ge (State f (Sifthenelse a s1 s2) k e m) |
---|
1072 | tr (State f s1 k e m) |
---|
1073 | | step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1,tr. |
---|
1074 | eval_expr ge e m a v1 tr → |
---|
1075 | is_false v1 (typeof a) → |
---|
1076 | step ge (State f (Sifthenelse a s1 s2) k e m) |
---|
1077 | tr (State f s2 k e m) |
---|
1078 | |
---|
1079 | | step_while_false: ∀f,a,s,k,e,m,v,tr. |
---|
1080 | eval_expr ge e m a v tr → |
---|
1081 | is_false v (typeof a) → |
---|
1082 | step ge (State f (Swhile a s) k e m) |
---|
1083 | tr (State f Sskip k e m) |
---|
1084 | | step_while_true: ∀f,a,s,k,e,m,v,tr. |
---|
1085 | eval_expr ge e m a v tr → |
---|
1086 | is_true v (typeof a) → |
---|
1087 | step ge (State f (Swhile a s) k e m) |
---|
1088 | tr (State f s (Kwhile a s k) e m) |
---|
1089 | | step_skip_or_continue_while: ∀f,x,a,s,k,e,m. |
---|
1090 | x = Sskip ∨ x = Scontinue → |
---|
1091 | step ge (State f x (Kwhile a s k) e m) |
---|
1092 | E0 (State f (Swhile a s) k e m) |
---|
1093 | | step_break_while: ∀f,a,s,k,e,m. |
---|
1094 | step ge (State f Sbreak (Kwhile a s k) e m) |
---|
1095 | E0 (State f Sskip k e m) |
---|
1096 | |
---|
1097 | | step_dowhile: ∀f,a,s,k,e,m. |
---|
1098 | step ge (State f (Sdowhile a s) k e m) |
---|
1099 | E0 (State f s (Kdowhile a s k) e m) |
---|
1100 | | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v,tr. |
---|
1101 | x = Sskip ∨ x = Scontinue → |
---|
1102 | eval_expr ge e m a v tr → |
---|
1103 | is_false v (typeof a) → |
---|
1104 | step ge (State f x (Kdowhile a s k) e m) |
---|
1105 | tr (State f Sskip k e m) |
---|
1106 | | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v,tr. |
---|
1107 | x = Sskip ∨ x = Scontinue → |
---|
1108 | eval_expr ge e m a v tr → |
---|
1109 | is_true v (typeof a) → |
---|
1110 | step ge (State f x (Kdowhile a s k) e m) |
---|
1111 | tr (State f (Sdowhile a s) k e m) |
---|
1112 | | step_break_dowhile: ∀f,a,s,k,e,m. |
---|
1113 | step ge (State f Sbreak (Kdowhile a s k) e m) |
---|
1114 | E0 (State f Sskip k e m) |
---|
1115 | |
---|
1116 | | step_for_start: ∀f,a1,a2,a3,s,k,e,m. |
---|
1117 | a1 ≠ Sskip → |
---|
1118 | step ge (State f (Sfor a1 a2 a3 s) k e m) |
---|
1119 | E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) |
---|
1120 | | step_for_false: ∀f,a2,a3,s,k,e,m,v,tr. |
---|
1121 | eval_expr ge e m a2 v tr → |
---|
1122 | is_false v (typeof a2) → |
---|
1123 | step ge (State f (Sfor Sskip a2 a3 s) k e m) |
---|
1124 | tr (State f Sskip k e m) |
---|
1125 | | step_for_true: ∀f,a2,a3,s,k,e,m,v,tr. |
---|
1126 | eval_expr ge e m a2 v tr → |
---|
1127 | is_true v (typeof a2) → |
---|
1128 | step ge (State f (Sfor Sskip a2 a3 s) k e m) |
---|
1129 | tr (State f s (Kfor2 a2 a3 s k) e m) |
---|
1130 | | step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m. |
---|
1131 | x = Sskip ∨ x = Scontinue → |
---|
1132 | step ge (State f x (Kfor2 a2 a3 s k) e m) |
---|
1133 | E0 (State f a3 (Kfor3 a2 a3 s k) e m) |
---|
1134 | | step_break_for2: ∀f,a2,a3,s,k,e,m. |
---|
1135 | step ge (State f Sbreak (Kfor2 a2 a3 s k) e m) |
---|
1136 | E0 (State f Sskip k e m) |
---|
1137 | | step_skip_for3: ∀f,a2,a3,s,k,e,m. |
---|
1138 | step ge (State f Sskip (Kfor3 a2 a3 s k) e m) |
---|
1139 | E0 (State f (Sfor Sskip a2 a3 s) k e m) |
---|
1140 | |
---|
1141 | | step_return_0: ∀f,k,e,m. |
---|
1142 | fn_return f = Tvoid → |
---|
1143 | step ge (State f (Sreturn (None ?)) k e m) |
---|
1144 | E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))) |
---|
1145 | | step_return_1: ∀f,a,k,e,m,v,tr. |
---|
1146 | fn_return f ≠ Tvoid → |
---|
1147 | eval_expr ge e m a v tr → |
---|
1148 | step ge (State f (Sreturn (Some ? a)) k e m) |
---|
1149 | tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e))) |
---|
1150 | | step_skip_call: ∀f,k,e,m. |
---|
1151 | is_call_cont k → |
---|
1152 | fn_return f = Tvoid → |
---|
1153 | step ge (State f Sskip k e m) |
---|
1154 | E0 (Returnstate Vundef k (free_list m (blocks_of_env e))) |
---|
1155 | |
---|
1156 | | step_switch: ∀f,a,sl,k,e,m,sz,n,tr. |
---|
1157 | eval_expr ge e m a (Vint sz n) tr → |
---|
1158 | step ge (State f (Sswitch a sl) k e m) |
---|
1159 | tr (State f (seq_of_labeled_statement (select_switch ? n sl)) (Kswitch k) e m) |
---|
1160 | | step_skip_break_switch: ∀f,x,k,e,m. |
---|
1161 | x = Sskip ∨ x = Sbreak → |
---|
1162 | step ge (State f x (Kswitch k) e m) |
---|
1163 | E0 (State f Sskip k e m) |
---|
1164 | | step_continue_switch: ∀f,k,e,m. |
---|
1165 | step ge (State f Scontinue (Kswitch k) e m) |
---|
1166 | E0 (State f Scontinue k e m) |
---|
1167 | |
---|
1168 | | step_label: ∀f,lbl,s,k,e,m. |
---|
1169 | step ge (State f (Slabel lbl s) k e m) |
---|
1170 | E0 (State f s k e m) |
---|
1171 | |
---|
1172 | | step_goto: ∀f,lbl,k,e,m,s',k'. |
---|
1173 | find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉 → |
---|
1174 | step ge (State f (Sgoto lbl) k e m) |
---|
1175 | E0 (State f s' k' e m) |
---|
1176 | |
---|
1177 | | step_internal_function: ∀f,vargs,k,m,e,m1,m2. |
---|
1178 | alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 → |
---|
1179 | bind_parameters e m1 (fn_params f) vargs m2 → |
---|
1180 | step ge (Callstate (CL_Internal f) vargs k m) |
---|
1181 | E0 (State f (fn_body f) k e m2) |
---|
1182 | |
---|
1183 | | step_external_function: ∀id,targs,tres,vargs,k,m,vres,t. |
---|
1184 | event_match (external_function id targs tres) vargs t vres → |
---|
1185 | step ge (Callstate (CL_External id targs tres) vargs k m) |
---|
1186 | t (Returnstate vres k m) |
---|
1187 | |
---|
1188 | | step_returnstate_0: ∀v,f,e,k,m. |
---|
1189 | step ge (Returnstate v (Kcall (None ?) f e k) m) |
---|
1190 | E0 (State f Sskip k e m) |
---|
1191 | |
---|
1192 | | step_returnstate_1: ∀v,f,e,k,m,m',loc,ofs,ty. |
---|
1193 | store_value_of_type ty m loc ofs v = Some ? m' → |
---|
1194 | step ge (Returnstate v (Kcall (Some ? 〈〈loc, ofs〉, ty〉) f e k) m) |
---|
1195 | E0 (State f Sskip k e m') |
---|
1196 | |
---|
1197 | | step_cost: ∀f,lbl,s,k,e,m. |
---|
1198 | step ge (State f (Scost lbl s) k e m) |
---|
1199 | (Echarge lbl) (State f s k e m). |
---|
1200 | (* |
---|
1201 | (** * Alternate big-step semantics *) |
---|
1202 | |
---|
1203 | (** ** Big-step semantics for terminating statements and functions *) |
---|
1204 | |
---|
1205 | (** The execution of a statement produces an ``outcome'', indicating |
---|
1206 | how the execution terminated: either normally or prematurely |
---|
1207 | through the execution of a [break], [continue] or [return] statement. *) |
---|
1208 | |
---|
1209 | inductive outcome: Type[0] := |
---|
1210 | | Out_break: outcome (**r terminated by [break] *) |
---|
1211 | | Out_continue: outcome (**r terminated by [continue] *) |
---|
1212 | | Out_normal: outcome (**r terminated normally *) |
---|
1213 | | Out_return: option val -> outcome. (**r terminated by [return] *) |
---|
1214 | |
---|
1215 | inductive out_normal_or_continue : outcome -> Prop := |
---|
1216 | | Out_normal_or_continue_N: out_normal_or_continue Out_normal |
---|
1217 | | Out_normal_or_continue_C: out_normal_or_continue Out_continue. |
---|
1218 | |
---|
1219 | inductive out_break_or_return : outcome -> outcome -> Prop := |
---|
1220 | | Out_break_or_return_B: out_break_or_return Out_break Out_normal |
---|
1221 | | Out_break_or_return_R: ∀ov. |
---|
1222 | out_break_or_return (Out_return ov) (Out_return ov). |
---|
1223 | |
---|
1224 | Definition outcome_switch (out: outcome) : outcome := |
---|
1225 | match out with |
---|
1226 | | Out_break => Out_normal |
---|
1227 | | o => o |
---|
1228 | end. |
---|
1229 | |
---|
1230 | Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := |
---|
1231 | match out, t with |
---|
1232 | | Out_normal, Tvoid => v = Vundef |
---|
1233 | | Out_return None, Tvoid => v = Vundef |
---|
1234 | | Out_return (Some v'), ty => ty <> Tvoid /\ v'=v |
---|
1235 | | _, _ => False |
---|
1236 | end. |
---|
1237 | |
---|
1238 | (** [exec_stmt ge e m1 s t m2 out] describes the execution of |
---|
1239 | the statement [s]. [out] is the outcome for this execution. |
---|
1240 | [m1] is the initial memory state, [m2] the final memory state. |
---|
1241 | [t] is the trace of input/output events performed during this |
---|
1242 | evaluation. *) |
---|
1243 | |
---|
1244 | inductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := |
---|
1245 | | exec_Sskip: ∀e,m. |
---|
1246 | exec_stmt e m Sskip |
---|
1247 | E0 m Out_normal |
---|
1248 | | exec_Sassign: ∀e,m,a1,a2,loc,ofs,v2,m'. |
---|
1249 | eval_lvalue e m a1 loc ofs -> |
---|
1250 | eval_expr e m a2 v2 -> |
---|
1251 | store_value_of_type (typeof a1) m loc ofs v2 = Some m' -> |
---|
1252 | exec_stmt e m (Sassign a1 a2) |
---|
1253 | E0 m' Out_normal |
---|
1254 | | exec_Scall_none: ∀e,m,a,al,vf,vargs,f,t,m',vres. |
---|
1255 | eval_expr e m a vf -> |
---|
1256 | eval_exprlist e m al vargs -> |
---|
1257 | Genv.find_funct ge vf = Some f -> |
---|
1258 | type_of_fundef f = typeof a -> |
---|
1259 | eval_funcall m f vargs t m' vres -> |
---|
1260 | exec_stmt e m (Scall None a al) |
---|
1261 | t m' Out_normal |
---|
1262 | | exec_Scall_some: ∀e,m,lhs,a,al,loc,ofs,vf,vargs,f,t,m',vres,m''. |
---|
1263 | eval_lvalue e m lhs loc ofs -> |
---|
1264 | eval_expr e m a vf -> |
---|
1265 | eval_exprlist e m al vargs -> |
---|
1266 | Genv.find_funct ge vf = Some f -> |
---|
1267 | type_of_fundef f = typeof a -> |
---|
1268 | eval_funcall m f vargs t m' vres -> |
---|
1269 | store_value_of_type (typeof lhs) m' loc ofs vres = Some m'' -> |
---|
1270 | exec_stmt e m (Scall (Some lhs) a al) |
---|
1271 | t m'' Out_normal |
---|
1272 | | exec_Sseq_1: ∀e,m,s1,s2,t1,m1,t2,m2,out. |
---|
1273 | exec_stmt e m s1 t1 m1 Out_normal -> |
---|
1274 | exec_stmt e m1 s2 t2 m2 out -> |
---|
1275 | exec_stmt e m (Ssequence s1 s2) |
---|
1276 | (t1 ** t2) m2 out |
---|
1277 | | exec_Sseq_2: ∀e,m,s1,s2,t1,m1,out. |
---|
1278 | exec_stmt e m s1 t1 m1 out -> |
---|
1279 | out <> Out_normal -> |
---|
1280 | exec_stmt e m (Ssequence s1 s2) |
---|
1281 | t1 m1 out |
---|
1282 | | exec_Sifthenelse_true: ∀e,m,a,s1,s2,v1,t,m',out. |
---|
1283 | eval_expr e m a v1 -> |
---|
1284 | is_true v1 (typeof a) -> |
---|
1285 | exec_stmt e m s1 t m' out -> |
---|
1286 | exec_stmt e m (Sifthenelse a s1 s2) |
---|
1287 | t m' out |
---|
1288 | | exec_Sifthenelse_false: ∀e,m,a,s1,s2,v1,t,m',out. |
---|
1289 | eval_expr e m a v1 -> |
---|
1290 | is_false v1 (typeof a) -> |
---|
1291 | exec_stmt e m s2 t m' out -> |
---|
1292 | exec_stmt e m (Sifthenelse a s1 s2) |
---|
1293 | t m' out |
---|
1294 | | exec_Sreturn_none: ∀e,m. |
---|
1295 | exec_stmt e m (Sreturn None) |
---|
1296 | E0 m (Out_return None) |
---|
1297 | | exec_Sreturn_some: ∀e,m,a,v. |
---|
1298 | eval_expr e m a v -> |
---|
1299 | exec_stmt e m (Sreturn (Some a)) |
---|
1300 | E0 m (Out_return (Some v)) |
---|
1301 | | exec_Sbreak: ∀e,m. |
---|
1302 | exec_stmt e m Sbreak |
---|
1303 | E0 m Out_break |
---|
1304 | | exec_Scontinue: ∀e,m. |
---|
1305 | exec_stmt e m Scontinue |
---|
1306 | E0 m Out_continue |
---|
1307 | | exec_Swhile_false: ∀e,m,a,s,v. |
---|
1308 | eval_expr e m a v -> |
---|
1309 | is_false v (typeof a) -> |
---|
1310 | exec_stmt e m (Swhile a s) |
---|
1311 | E0 m Out_normal |
---|
1312 | | exec_Swhile_stop: ∀e,m,a,v,s,t,m',out',out. |
---|
1313 | eval_expr e m a v -> |
---|
1314 | is_true v (typeof a) -> |
---|
1315 | exec_stmt e m s t m' out' -> |
---|
1316 | out_break_or_return out' out -> |
---|
1317 | exec_stmt e m (Swhile a s) |
---|
1318 | t m' out |
---|
1319 | | exec_Swhile_loop: ∀e,m,a,s,v,t1,m1,out1,t2,m2,out. |
---|
1320 | eval_expr e m a v -> |
---|
1321 | is_true v (typeof a) -> |
---|
1322 | exec_stmt e m s t1 m1 out1 -> |
---|
1323 | out_normal_or_continue out1 -> |
---|
1324 | exec_stmt e m1 (Swhile a s) t2 m2 out -> |
---|
1325 | exec_stmt e m (Swhile a s) |
---|
1326 | (t1 ** t2) m2 out |
---|
1327 | | exec_Sdowhile_false: ∀e,m,s,a,t,m1,out1,v. |
---|
1328 | exec_stmt e m s t m1 out1 -> |
---|
1329 | out_normal_or_continue out1 -> |
---|
1330 | eval_expr e m1 a v -> |
---|
1331 | is_false v (typeof a) -> |
---|
1332 | exec_stmt e m (Sdowhile a s) |
---|
1333 | t m1 Out_normal |
---|
1334 | | exec_Sdowhile_stop: ∀e,m,s,a,t,m1,out1,out. |
---|
1335 | exec_stmt e m s t m1 out1 -> |
---|
1336 | out_break_or_return out1 out -> |
---|
1337 | exec_stmt e m (Sdowhile a s) |
---|
1338 | t m1 out |
---|
1339 | | exec_Sdowhile_loop: ∀e,m,s,a,m1,m2,t1,t2,out,out1,v. |
---|
1340 | exec_stmt e m s t1 m1 out1 -> |
---|
1341 | out_normal_or_continue out1 -> |
---|
1342 | eval_expr e m1 a v -> |
---|
1343 | is_true v (typeof a) -> |
---|
1344 | exec_stmt e m1 (Sdowhile a s) t2 m2 out -> |
---|
1345 | exec_stmt e m (Sdowhile a s) |
---|
1346 | (t1 ** t2) m2 out |
---|
1347 | | exec_Sfor_start: ∀e,m,s,a1,a2,a3,out,m1,m2,t1,t2. |
---|
1348 | a1 <> Sskip -> |
---|
1349 | exec_stmt e m a1 t1 m1 Out_normal -> |
---|
1350 | exec_stmt e m1 (Sfor Sskip a2 a3 s) t2 m2 out -> |
---|
1351 | exec_stmt e m (Sfor a1 a2 a3 s) |
---|
1352 | (t1 ** t2) m2 out |
---|
1353 | | exec_Sfor_false: ∀e,m,s,a2,a3,v. |
---|
1354 | eval_expr e m a2 v -> |
---|
1355 | is_false v (typeof a2) -> |
---|
1356 | exec_stmt e m (Sfor Sskip a2 a3 s) |
---|
1357 | E0 m Out_normal |
---|
1358 | | exec_Sfor_stop: ∀e,m,s,a2,a3,v,m1,t,out1,out. |
---|
1359 | eval_expr e m a2 v -> |
---|
1360 | is_true v (typeof a2) -> |
---|
1361 | exec_stmt e m s t m1 out1 -> |
---|
1362 | out_break_or_return out1 out -> |
---|
1363 | exec_stmt e m (Sfor Sskip a2 a3 s) |
---|
1364 | t m1 out |
---|
1365 | | exec_Sfor_loop: ∀e,m,s,a2,a3,v,m1,m2,m3,t1,t2,t3,out1,out. |
---|
1366 | eval_expr e m a2 v -> |
---|
1367 | is_true v (typeof a2) -> |
---|
1368 | exec_stmt e m s t1 m1 out1 -> |
---|
1369 | out_normal_or_continue out1 -> |
---|
1370 | exec_stmt e m1 a3 t2 m2 Out_normal -> |
---|
1371 | exec_stmt e m2 (Sfor Sskip a2 a3 s) t3 m3 out -> |
---|
1372 | exec_stmt e m (Sfor Sskip a2 a3 s) |
---|
1373 | (t1 ** t2 ** t3) m3 out |
---|
1374 | | exec_Sswitch: ∀e,m,a,t,n,sl,m1,out. |
---|
1375 | eval_expr e m a (Vint n) -> |
---|
1376 | exec_stmt e m (seq_of_labeled_statement (select_switch n sl)) t m1 out -> |
---|
1377 | exec_stmt e m (Sswitch a sl) |
---|
1378 | t m1 (outcome_switch out) |
---|
1379 | |
---|
1380 | (** [eval_funcall m1 fd args t m2 res] describes the invocation of |
---|
1381 | function [fd] with arguments [args]. [res] is the value returned |
---|
1382 | by the call. *) |
---|
1383 | |
---|
1384 | with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := |
---|
1385 | | eval_funcall_internal: ∀m,f,vargs,t,e,m1,m2,m3,out,vres. |
---|
1386 | alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> |
---|
1387 | bind_parameters e m1 f.(fn_params) vargs m2 -> |
---|
1388 | exec_stmt e m2 f.(fn_body) t m3 out -> |
---|
1389 | outcome_result_value out f.(fn_return) vres -> |
---|
1390 | eval_funcall m (Internal f) vargs t (Mem.free_list m3 (blocks_of_env e)) vres |
---|
1391 | | eval_funcall_external: ∀m,id,targs,tres,vargs,t,vres. |
---|
1392 | event_match (external_function id targs tres) vargs t vres -> |
---|
1393 | eval_funcall m (External id targs tres) vargs t m vres. |
---|
1394 | |
---|
1395 | Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop |
---|
1396 | with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop. |
---|
1397 | |
---|
1398 | (** ** Big-step semantics for diverging statements and functions *) |
---|
1399 | |
---|
1400 | (** Coinductive semantics for divergence. |
---|
1401 | [execinf_stmt ge e m s t] holds if the execution of statement [s] |
---|
1402 | diverges, i.e. loops infinitely. [t] is the possibly infinite |
---|
1403 | trace of observable events performed during the execution. *) |
---|
1404 | |
---|
1405 | Coinductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop := |
---|
1406 | | execinf_Scall_none: ∀e,m,a,al,vf,vargs,f,t. |
---|
1407 | eval_expr e m a vf -> |
---|
1408 | eval_exprlist e m al vargs -> |
---|
1409 | Genv.find_funct ge vf = Some f -> |
---|
1410 | type_of_fundef f = typeof a -> |
---|
1411 | evalinf_funcall m f vargs t -> |
---|
1412 | execinf_stmt e m (Scall None a al) t |
---|
1413 | | execinf_Scall_some: ∀e,m,lhs,a,al,loc,ofs,vf,vargs,f,t. |
---|
1414 | eval_lvalue e m lhs loc ofs -> |
---|
1415 | eval_expr e m a vf -> |
---|
1416 | eval_exprlist e m al vargs -> |
---|
1417 | Genv.find_funct ge vf = Some f -> |
---|
1418 | type_of_fundef f = typeof a -> |
---|
1419 | evalinf_funcall m f vargs t -> |
---|
1420 | execinf_stmt e m (Scall (Some lhs) a al) t |
---|
1421 | | execinf_Sseq_1: ∀e,m,s1,s2,t. |
---|
1422 | execinf_stmt e m s1 t -> |
---|
1423 | execinf_stmt e m (Ssequence s1 s2) t |
---|
1424 | | execinf_Sseq_2: ∀e,m,s1,s2,t1,m1,t2. |
---|
1425 | exec_stmt e m s1 t1 m1 Out_normal -> |
---|
1426 | execinf_stmt e m1 s2 t2 -> |
---|
1427 | execinf_stmt e m (Ssequence s1 s2) (t1 *** t2) |
---|
1428 | | execinf_Sifthenelse_true: ∀e,m,a,s1,s2,v1,t. |
---|
1429 | eval_expr e m a v1 -> |
---|
1430 | is_true v1 (typeof a) -> |
---|
1431 | execinf_stmt e m s1 t -> |
---|
1432 | execinf_stmt e m (Sifthenelse a s1 s2) t |
---|
1433 | | execinf_Sifthenelse_false: ∀e,m,a,s1,s2,v1,t. |
---|
1434 | eval_expr e m a v1 -> |
---|
1435 | is_false v1 (typeof a) -> |
---|
1436 | execinf_stmt e m s2 t -> |
---|
1437 | execinf_stmt e m (Sifthenelse a s1 s2) t |
---|
1438 | | execinf_Swhile_body: ∀e,m,a,v,s,t. |
---|
1439 | eval_expr e m a v -> |
---|
1440 | is_true v (typeof a) -> |
---|
1441 | execinf_stmt e m s t -> |
---|
1442 | execinf_stmt e m (Swhile a s) t |
---|
1443 | | execinf_Swhile_loop: ∀e,m,a,s,v,t1,m1,out1,t2. |
---|
1444 | eval_expr e m a v -> |
---|
1445 | is_true v (typeof a) -> |
---|
1446 | exec_stmt e m s t1 m1 out1 -> |
---|
1447 | out_normal_or_continue out1 -> |
---|
1448 | execinf_stmt e m1 (Swhile a s) t2 -> |
---|
1449 | execinf_stmt e m (Swhile a s) (t1 *** t2) |
---|
1450 | | execinf_Sdowhile_body: ∀e,m,s,a,t. |
---|
1451 | execinf_stmt e m s t -> |
---|
1452 | execinf_stmt e m (Sdowhile a s) t |
---|
1453 | | execinf_Sdowhile_loop: ∀e,m,s,a,m1,t1,t2,out1,v. |
---|
1454 | exec_stmt e m s t1 m1 out1 -> |
---|
1455 | out_normal_or_continue out1 -> |
---|
1456 | eval_expr e m1 a v -> |
---|
1457 | is_true v (typeof a) -> |
---|
1458 | execinf_stmt e m1 (Sdowhile a s) t2 -> |
---|
1459 | execinf_stmt e m (Sdowhile a s) (t1 *** t2) |
---|
1460 | | execinf_Sfor_start_1: ∀e,m,s,a1,a2,a3,t. |
---|
1461 | execinf_stmt e m a1 t -> |
---|
1462 | execinf_stmt e m (Sfor a1 a2 a3 s) t |
---|
1463 | | execinf_Sfor_start_2: ∀e,m,s,a1,a2,a3,m1,t1,t2. |
---|
1464 | a1 <> Sskip -> |
---|
1465 | exec_stmt e m a1 t1 m1 Out_normal -> |
---|
1466 | execinf_stmt e m1 (Sfor Sskip a2 a3 s) t2 -> |
---|
1467 | execinf_stmt e m (Sfor a1 a2 a3 s) (t1 *** t2) |
---|
1468 | | execinf_Sfor_body: ∀e,m,s,a2,a3,v,t. |
---|
1469 | eval_expr e m a2 v -> |
---|
1470 | is_true v (typeof a2) -> |
---|
1471 | execinf_stmt e m s t -> |
---|
1472 | execinf_stmt e m (Sfor Sskip a2 a3 s) t |
---|
1473 | | execinf_Sfor_next: ∀e,m,s,a2,a3,v,m1,t1,t2,out1. |
---|
1474 | eval_expr e m a2 v -> |
---|
1475 | is_true v (typeof a2) -> |
---|
1476 | exec_stmt e m s t1 m1 out1 -> |
---|
1477 | out_normal_or_continue out1 -> |
---|
1478 | execinf_stmt e m1 a3 t2 -> |
---|
1479 | execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2) |
---|
1480 | | execinf_Sfor_loop: ∀e,m,s,a2,a3,v,m1,m2,t1,t2,t3,out1. |
---|
1481 | eval_expr e m a2 v -> |
---|
1482 | is_true v (typeof a2) -> |
---|
1483 | exec_stmt e m s t1 m1 out1 -> |
---|
1484 | out_normal_or_continue out1 -> |
---|
1485 | exec_stmt e m1 a3 t2 m2 Out_normal -> |
---|
1486 | execinf_stmt e m2 (Sfor Sskip a2 a3 s) t3 -> |
---|
1487 | execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2 *** t3) |
---|
1488 | | execinf_Sswitch: ∀e,m,a,t,n,sl. |
---|
1489 | eval_expr e m a (Vint n) -> |
---|
1490 | execinf_stmt e m (seq_of_labeled_statement (select_switch n sl)) t -> |
---|
1491 | execinf_stmt e m (Sswitch a sl) t |
---|
1492 | |
---|
1493 | (** [evalinf_funcall ge m fd args t] holds if the invocation of function |
---|
1494 | [fd] on arguments [args] diverges, with observable trace [t]. *) |
---|
1495 | |
---|
1496 | with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop := |
---|
1497 | | evalinf_funcall_internal: ∀m,f,vargs,t,e,m1,m2. |
---|
1498 | alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> |
---|
1499 | bind_parameters e m1 f.(fn_params) vargs m2 -> |
---|
1500 | execinf_stmt e m2 f.(fn_body) t -> |
---|
1501 | evalinf_funcall m (Internal f) vargs t. |
---|
1502 | |
---|
1503 | End SEMANTICS. |
---|
1504 | *) |
---|
1505 | (* * * Whole-program semantics *) |
---|
1506 | |
---|
1507 | (* * Execution of whole programs are described as sequences of transitions |
---|
1508 | from an initial state to a final state. An initial state is a [Callstate] |
---|
1509 | corresponding to the invocation of the ``main'' function of the program |
---|
1510 | without arguments and with an empty continuation. *) |
---|
1511 | |
---|
1512 | inductive initial_state (p: clight_program): state -> Prop := |
---|
1513 | | initial_state_intro: ∀b,f,ge,m0. |
---|
1514 | globalenv Genv ?? p = OK ? ge → |
---|
1515 | init_mem Genv ?? p = OK ? m0 → |
---|
1516 | find_symbol ?? ge (prog_main ?? p) = Some ? b → |
---|
1517 | find_funct_ptr ?? ge b = Some ? f → |
---|
1518 | initial_state p (Callstate f (nil ?) Kstop m0). |
---|
1519 | |
---|
1520 | (* * A final state is a [Returnstate] with an empty continuation. *) |
---|
1521 | |
---|
1522 | inductive final_state: state -> int -> Prop := |
---|
1523 | | final_state_intro: ∀r,m. |
---|
1524 | final_state (Returnstate (Vint I32 r) Kstop m) r. |
---|
1525 | |
---|
1526 | (* * Execution of a whole program: [exec_program p beh] |
---|
1527 | holds if the application of [p]'s main function to no arguments |
---|
1528 | in the initial memory state for [p] has [beh] as observable |
---|
1529 | behavior. *) |
---|
1530 | |
---|
1531 | definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh. |
---|
1532 | ∀ge. globalenv ??? p = OK ? ge → |
---|
1533 | program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh. |
---|
1534 | (* |
---|
1535 | (** Big-step execution of a whole program. *) |
---|
1536 | |
---|
1537 | inductive bigstep_program_terminates (p: program): trace -> int -> Prop := |
---|
1538 | | bigstep_program_terminates_intro: ∀b,f,m1,t,r. |
---|
1539 | let ge := Genv.globalenv p in |
---|
1540 | let m0 := Genv.init_mem p in |
---|
1541 | Genv.find_symbol ge p.(prog_main) = Some b -> |
---|
1542 | Genv.find_funct_ptr ge b = Some f -> |
---|
1543 | eval_funcall ge m0 f nil t m1 (Vint r) -> |
---|
1544 | bigstep_program_terminates p t r. |
---|
1545 | |
---|
1546 | inductive bigstep_program_diverges (p: program): traceinf -> Prop := |
---|
1547 | | bigstep_program_diverges_intro: ∀b,f,t. |
---|
1548 | let ge := Genv.globalenv p in |
---|
1549 | let m0 := Genv.init_mem p in |
---|
1550 | Genv.find_symbol ge p.(prog_main) = Some b -> |
---|
1551 | Genv.find_funct_ptr ge b = Some f -> |
---|
1552 | evalinf_funcall ge m0 f nil t -> |
---|
1553 | bigstep_program_diverges p t. |
---|
1554 | |
---|
1555 | (** * Implication from big-step semantics to transition semantics *) |
---|
1556 | |
---|
1557 | Section BIGSTEP_TO_TRANSITIONS. |
---|
1558 | |
---|
1559 | Variable prog: program. |
---|
1560 | Let ge : genv := Genv.globalenv prog. |
---|
1561 | |
---|
1562 | Definition exec_stmt_eval_funcall_ind |
---|
1563 | (PS: env -> mem -> statement -> trace -> mem -> outcome -> Prop) |
---|
1564 | (PF: mem -> fundef -> list val -> trace -> mem -> val -> Prop) := |
---|
1565 | fun a b c d e f g h i j k l m n o p q r s t u v w x y => |
---|
1566 | conj (exec_stmt_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y) |
---|
1567 | (eval_funcall_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y). |
---|
1568 | |
---|
1569 | inductive outcome_state_match |
---|
1570 | (e: env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop := |
---|
1571 | | osm_normal: |
---|
1572 | outcome_state_match e m f k Out_normal (State f Sskip k e m) |
---|
1573 | | osm_break: |
---|
1574 | outcome_state_match e m f k Out_break (State f Sbreak k e m) |
---|
1575 | | osm_continue: |
---|
1576 | outcome_state_match e m f k Out_continue (State f Scontinue k e m) |
---|
1577 | | osm_return_none: ∀k'. |
---|
1578 | call_cont k' = call_cont k -> |
---|
1579 | outcome_state_match e m f k |
---|
1580 | (Out_return None) (State f (Sreturn None) k' e m) |
---|
1581 | | osm_return_some: ∀a,v,k'. |
---|
1582 | call_cont k' = call_cont k -> |
---|
1583 | eval_expr ge e m a v -> |
---|
1584 | outcome_state_match e m f k |
---|
1585 | (Out_return (Some v)) (State f (Sreturn (Some a)) k' e m). |
---|
1586 | |
---|
1587 | Lemma is_call_cont_call_cont: |
---|
1588 | ∀k. is_call_cont k -> call_cont k = k. |
---|
1589 | Proof. |
---|
1590 | destruct k; simpl; intros; contradiction || auto. |
---|
1591 | Qed. |
---|
1592 | |
---|
1593 | Lemma exec_stmt_eval_funcall_steps: |
---|
1594 | (∀e,m,s,t,m',out. |
---|
1595 | exec_stmt ge e m s t m' out -> |
---|
1596 | ∀f,k. exists S, |
---|
1597 | star step ge (State f s k e m) t S |
---|
1598 | /\ outcome_state_match e m' f k out S) |
---|
1599 | /\ |
---|
1600 | (∀m,fd,args,t,m',res. |
---|
1601 | eval_funcall ge m fd args t m' res -> |
---|
1602 | ∀k. |
---|
1603 | is_call_cont k -> |
---|
1604 | star step ge (Callstate fd args k m) t (Returnstate res k m')). |
---|
1605 | Proof. |
---|
1606 | apply exec_stmt_eval_funcall_ind; intros. |
---|
1607 | |
---|
1608 | (* skip *) |
---|
1609 | econstructor; split. apply star_refl. constructor. |
---|
1610 | |
---|
1611 | (* assign *) |
---|
1612 | econstructor; split. apply star_one. econstructor; eauto. constructor. |
---|
1613 | |
---|
1614 | (* call none *) |
---|
1615 | econstructor; split. |
---|
1616 | eapply star_left. econstructor; eauto. |
---|
1617 | eapply star_right. apply H4. simpl; auto. econstructor. reflexivity. traceEq. |
---|
1618 | constructor. |
---|
1619 | |
---|
1620 | (* call some *) |
---|
1621 | econstructor; split. |
---|
1622 | eapply star_left. econstructor; eauto. |
---|
1623 | eapply star_right. apply H5. simpl; auto. econstructor; eauto. reflexivity. traceEq. |
---|
1624 | constructor. |
---|
1625 | |
---|
1626 | (* sequence 2 *) |
---|
1627 | destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. inv B1. |
---|
1628 | destruct (H2 f k) as [S2 [A2 B2]]. |
---|
1629 | econstructor; split. |
---|
1630 | eapply star_left. econstructor. |
---|
1631 | eapply star_trans. eexact A1. |
---|
1632 | eapply star_left. constructor. eexact A2. |
---|
1633 | reflexivity. reflexivity. traceEq. |
---|
1634 | auto. |
---|
1635 | |
---|
1636 | (* sequence 1 *) |
---|
1637 | destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. |
---|
1638 | set (S2 := |
---|
1639 | match out with |
---|
1640 | | Out_break => State f Sbreak k e m1 |
---|
1641 | | Out_continue => State f Scontinue k e m1 |
---|
1642 | | _ => S1 |
---|
1643 | end). |
---|
1644 | exists S2; split. |
---|
1645 | eapply star_left. econstructor. |
---|
1646 | eapply star_trans. eexact A1. |
---|
1647 | unfold S2; inv B1. |
---|
1648 | congruence. |
---|
1649 | apply star_one. apply step_break_seq. |
---|
1650 | apply star_one. apply step_continue_seq. |
---|
1651 | apply star_refl. |
---|
1652 | apply star_refl. |
---|
1653 | reflexivity. traceEq. |
---|
1654 | unfold S2; inv B1; congruence || econstructor; eauto. |
---|
1655 | |
---|
1656 | (* ifthenelse true *) |
---|
1657 | destruct (H2 f k) as [S1 [A1 B1]]. |
---|
1658 | exists S1; split. |
---|
1659 | eapply star_left. eapply step_ifthenelse_true; eauto. eexact A1. traceEq. |
---|
1660 | auto. |
---|
1661 | |
---|
1662 | (* ifthenelse false *) |
---|
1663 | destruct (H2 f k) as [S1 [A1 B1]]. |
---|
1664 | exists S1; split. |
---|
1665 | eapply star_left. eapply step_ifthenelse_false; eauto. eexact A1. traceEq. |
---|
1666 | auto. |
---|
1667 | |
---|
1668 | (* return none *) |
---|
1669 | econstructor; split. apply star_refl. constructor. auto. |
---|
1670 | |
---|
1671 | (* return some *) |
---|
1672 | econstructor; split. apply star_refl. econstructor; eauto. |
---|
1673 | |
---|
1674 | (* break *) |
---|
1675 | econstructor; split. apply star_refl. constructor. |
---|
1676 | |
---|
1677 | (* continue *) |
---|
1678 | econstructor; split. apply star_refl. constructor. |
---|
1679 | |
---|
1680 | (* while false *) |
---|
1681 | econstructor; split. |
---|
1682 | apply star_one. eapply step_while_false; eauto. |
---|
1683 | constructor. |
---|
1684 | |
---|
1685 | (* while stop *) |
---|
1686 | destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]]. |
---|
1687 | set (S2 := |
---|
1688 | match out' with |
---|
1689 | | Out_break => State f Sskip k e m' |
---|
1690 | | _ => S1 |
---|
1691 | end). |
---|
1692 | exists S2; split. |
---|
1693 | eapply star_left. eapply step_while_true; eauto. |
---|
1694 | eapply star_trans. eexact A1. |
---|
1695 | unfold S2. inversion H3; subst. |
---|
1696 | inv B1. apply star_one. constructor. |
---|
1697 | apply star_refl. |
---|
1698 | reflexivity. traceEq. |
---|
1699 | unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto. |
---|
1700 | |
---|
1701 | (* while loop *) |
---|
1702 | destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]]. |
---|
1703 | destruct (H5 f k) as [S2 [A2 B2]]. |
---|
1704 | exists S2; split. |
---|
1705 | eapply star_left. eapply step_while_true; eauto. |
---|
1706 | eapply star_trans. eexact A1. |
---|
1707 | eapply star_left. |
---|
1708 | inv H3; inv B1; apply step_skip_or_continue_while; auto. |
---|
1709 | eexact A2. |
---|
1710 | reflexivity. reflexivity. traceEq. |
---|
1711 | auto. |
---|
1712 | |
---|
1713 | (* dowhile false *) |
---|
1714 | destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. |
---|
1715 | exists (State f Sskip k e m1); split. |
---|
1716 | eapply star_left. constructor. |
---|
1717 | eapply star_right. eexact A1. |
---|
1718 | inv H1; inv B1; eapply step_skip_or_continue_dowhile_false; eauto. |
---|
1719 | reflexivity. traceEq. |
---|
1720 | constructor. |
---|
1721 | |
---|
1722 | (* dowhile stop *) |
---|
1723 | destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. |
---|
1724 | set (S2 := |
---|
1725 | match out1 with |
---|
1726 | | Out_break => State f Sskip k e m1 |
---|
1727 | | _ => S1 |
---|
1728 | end). |
---|
1729 | exists S2; split. |
---|
1730 | eapply star_left. apply step_dowhile. |
---|
1731 | eapply star_trans. eexact A1. |
---|
1732 | unfold S2. inversion H1; subst. |
---|
1733 | inv B1. apply star_one. constructor. |
---|
1734 | apply star_refl. |
---|
1735 | reflexivity. traceEq. |
---|
1736 | unfold S2. inversion H1; subst. constructor. inv B1; econstructor; eauto. |
---|
1737 | |
---|
1738 | (* dowhile loop *) |
---|
1739 | destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. |
---|
1740 | destruct (H5 f k) as [S2 [A2 B2]]. |
---|
1741 | exists S2; split. |
---|
1742 | eapply star_left. apply step_dowhile. |
---|
1743 | eapply star_trans. eexact A1. |
---|
1744 | eapply star_left. |
---|
1745 | inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto. |
---|
1746 | eexact A2. |
---|
1747 | reflexivity. reflexivity. traceEq. |
---|
1748 | auto. |
---|
1749 | |
---|
1750 | (* for start *) |
---|
1751 | destruct (H1 f (Kseq (Sfor Sskip a2 a3 s) k)) as [S1 [A1 B1]]. inv B1. |
---|
1752 | destruct (H3 f k) as [S2 [A2 B2]]. |
---|
1753 | exists S2; split. |
---|
1754 | eapply star_left. apply step_for_start; auto. |
---|
1755 | eapply star_trans. eexact A1. |
---|
1756 | eapply star_left. constructor. eexact A2. |
---|
1757 | reflexivity. reflexivity. traceEq. |
---|
1758 | auto. |
---|
1759 | |
---|
1760 | (* for false *) |
---|
1761 | econstructor; split. |
---|
1762 | eapply star_one. eapply step_for_false; eauto. |
---|
1763 | constructor. |
---|
1764 | |
---|
1765 | (* for stop *) |
---|
1766 | destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]]. |
---|
1767 | set (S2 := |
---|
1768 | match out1 with |
---|
1769 | | Out_break => State f Sskip k e m1 |
---|
1770 | | _ => S1 |
---|
1771 | end). |
---|
1772 | exists S2; split. |
---|
1773 | eapply star_left. eapply step_for_true; eauto. |
---|
1774 | eapply star_trans. eexact A1. |
---|
1775 | unfold S2. inversion H3; subst. |
---|
1776 | inv B1. apply star_one. constructor. |
---|
1777 | apply star_refl. |
---|
1778 | reflexivity. traceEq. |
---|
1779 | unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto. |
---|
1780 | |
---|
1781 | (* for loop *) |
---|
1782 | destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]]. |
---|
1783 | destruct (H5 f (Kfor3 a2 a3 s k)) as [S2 [A2 B2]]. inv B2. |
---|
1784 | destruct (H7 f k) as [S3 [A3 B3]]. |
---|
1785 | exists S3; split. |
---|
1786 | eapply star_left. eapply step_for_true; eauto. |
---|
1787 | eapply star_trans. eexact A1. |
---|
1788 | eapply star_trans with (s2 := State f a3 (Kfor3 a2 a3 s k) e m1). |
---|
1789 | inv H3; inv B1. |
---|
1790 | apply star_one. constructor. auto. |
---|
1791 | apply star_one. constructor. auto. |
---|
1792 | eapply star_trans. eexact A2. |
---|
1793 | eapply star_left. constructor. |
---|
1794 | eexact A3. |
---|
1795 | reflexivity. reflexivity. reflexivity. reflexivity. traceEq. |
---|
1796 | auto. |
---|
1797 | |
---|
1798 | (* switch *) |
---|
1799 | destruct (H1 f (Kswitch k)) as [S1 [A1 B1]]. |
---|
1800 | set (S2 := |
---|
1801 | match out with |
---|
1802 | | Out_normal => State f Sskip k e m1 |
---|
1803 | | Out_break => State f Sskip k e m1 |
---|
1804 | | Out_continue => State f Scontinue k e m1 |
---|
1805 | | _ => S1 |
---|
1806 | end). |
---|
1807 | exists S2; split. |
---|
1808 | eapply star_left. eapply step_switch; eauto. |
---|
1809 | eapply star_trans. eexact A1. |
---|
1810 | unfold S2; inv B1. |
---|
1811 | apply star_one. constructor. auto. |
---|
1812 | apply star_one. constructor. auto. |
---|
1813 | apply star_one. constructor. |
---|
1814 | apply star_refl. |
---|
1815 | apply star_refl. |
---|
1816 | reflexivity. traceEq. |
---|
1817 | unfold S2. inv B1; simpl; econstructor; eauto. |
---|
1818 | |
---|
1819 | (* call internal *) |
---|
1820 | destruct (H2 f k) as [S1 [A1 B1]]. |
---|
1821 | eapply star_left. eapply step_internal_function; eauto. |
---|
1822 | eapply star_right. eexact A1. |
---|
1823 | inv B1; simpl in H3; try contradiction. |
---|
1824 | (* Out_normal *) |
---|
1825 | assert (fn_return f = Tvoid /\ vres = Vundef). |
---|
1826 | destruct (fn_return f); auto || contradiction. |
---|
1827 | destruct H5. subst vres. apply step_skip_call; auto. |
---|
1828 | (* Out_return None *) |
---|
1829 | assert (fn_return f = Tvoid /\ vres = Vundef). |
---|
1830 | destruct (fn_return f); auto || contradiction. |
---|
1831 | destruct H6. subst vres. |
---|
1832 | rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. |
---|
1833 | apply step_return_0; auto. |
---|
1834 | (* Out_return Some *) |
---|
1835 | destruct H3. subst vres. |
---|
1836 | rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. |
---|
1837 | eapply step_return_1; eauto. |
---|
1838 | reflexivity. traceEq. |
---|
1839 | |
---|
1840 | (* call external *) |
---|
1841 | apply star_one. apply step_external_function; auto. |
---|
1842 | Qed. |
---|
1843 | |
---|
1844 | Lemma exec_stmt_steps: |
---|
1845 | ∀e,m,s,t,m',out. |
---|
1846 | exec_stmt ge e m s t m' out -> |
---|
1847 | ∀f,k. exists S, |
---|
1848 | star step ge (State f s k e m) t S |
---|
1849 | /\ outcome_state_match e m' f k out S. |
---|
1850 | Proof (proj1 exec_stmt_eval_funcall_steps). |
---|
1851 | |
---|
1852 | Lemma eval_funcall_steps: |
---|
1853 | ∀m,fd,args,t,m',res. |
---|
1854 | eval_funcall ge m fd args t m' res -> |
---|
1855 | ∀k. |
---|
1856 | is_call_cont k -> |
---|
1857 | star step ge (Callstate fd args k m) t (Returnstate res k m'). |
---|
1858 | Proof (proj2 exec_stmt_eval_funcall_steps). |
---|
1859 | |
---|
1860 | Definition order (x y: unit) := False. |
---|
1861 | |
---|
1862 | Lemma evalinf_funcall_forever: |
---|
1863 | ∀m,fd,args,T,k. |
---|
1864 | evalinf_funcall ge m fd args T -> |
---|
1865 | forever_N step order ge tt (Callstate fd args k m) T. |
---|
1866 | Proof. |
---|
1867 | cofix CIH_FUN. |
---|
1868 | assert (∀e,m,s,T,f,k. |
---|
1869 | execinf_stmt ge e m s T -> |
---|
1870 | forever_N step order ge tt (State f s k e m) T). |
---|
1871 | cofix CIH_STMT. |
---|
1872 | intros. inv H. |
---|
1873 | |
---|
1874 | (* call none *) |
---|
1875 | eapply forever_N_plus. |
---|
1876 | apply plus_one. eapply step_call_none; eauto. |
---|
1877 | apply CIH_FUN. eauto. traceEq. |
---|
1878 | (* call some *) |
---|
1879 | eapply forever_N_plus. |
---|
1880 | apply plus_one. eapply step_call_some; eauto. |
---|
1881 | apply CIH_FUN. eauto. traceEq. |
---|
1882 | |
---|
1883 | (* seq 1 *) |
---|
1884 | eapply forever_N_plus. |
---|
1885 | apply plus_one. econstructor. |
---|
1886 | apply CIH_STMT; eauto. traceEq. |
---|
1887 | (* seq 2 *) |
---|
1888 | destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kseq s2 k)) as [S1 [A1 B1]]. |
---|
1889 | inv B1. |
---|
1890 | eapply forever_N_plus. |
---|
1891 | eapply plus_left. constructor. eapply star_trans. eexact A1. |
---|
1892 | apply star_one. constructor. reflexivity. reflexivity. |
---|
1893 | apply CIH_STMT; eauto. traceEq. |
---|
1894 | |
---|
1895 | (* ifthenelse true *) |
---|
1896 | eapply forever_N_plus. |
---|
1897 | apply plus_one. eapply step_ifthenelse_true; eauto. |
---|
1898 | apply CIH_STMT; eauto. traceEq. |
---|
1899 | (* ifthenelse false *) |
---|
1900 | eapply forever_N_plus. |
---|
1901 | apply plus_one. eapply step_ifthenelse_false; eauto. |
---|
1902 | apply CIH_STMT; eauto. traceEq. |
---|
1903 | |
---|
1904 | (* while body *) |
---|
1905 | eapply forever_N_plus. |
---|
1906 | eapply plus_one. eapply step_while_true; eauto. |
---|
1907 | apply CIH_STMT; eauto. traceEq. |
---|
1908 | (* while loop *) |
---|
1909 | destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kwhile a s0 k)) as [S1 [A1 B1]]. |
---|
1910 | eapply forever_N_plus with (s2 := State f (Swhile a s0) k e m1). |
---|
1911 | eapply plus_left. eapply step_while_true; eauto. |
---|
1912 | eapply star_right. eexact A1. |
---|
1913 | inv H3; inv B1; apply step_skip_or_continue_while; auto. |
---|
1914 | reflexivity. reflexivity. |
---|
1915 | apply CIH_STMT; eauto. traceEq. |
---|
1916 | |
---|
1917 | (* dowhile body *) |
---|
1918 | eapply forever_N_plus. |
---|
1919 | eapply plus_one. eapply step_dowhile. |
---|
1920 | apply CIH_STMT; eauto. |
---|
1921 | traceEq. |
---|
1922 | |
---|
1923 | (* dowhile loop *) |
---|
1924 | destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kdowhile a s0 k)) as [S1 [A1 B1]]. |
---|
1925 | eapply forever_N_plus with (s2 := State f (Sdowhile a s0) k e m1). |
---|
1926 | eapply plus_left. eapply step_dowhile. |
---|
1927 | eapply star_right. eexact A1. |
---|
1928 | inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto. |
---|
1929 | reflexivity. reflexivity. |
---|
1930 | apply CIH_STMT. eauto. |
---|
1931 | traceEq. |
---|
1932 | |
---|
1933 | (* for start 1 *) |
---|
1934 | assert (a1 <> Sskip). red; intros; subst. inv H0. |
---|
1935 | eapply forever_N_plus. |
---|
1936 | eapply plus_one. apply step_for_start; auto. |
---|
1937 | apply CIH_STMT; eauto. |
---|
1938 | traceEq. |
---|
1939 | |
---|
1940 | (* for start 2 *) |
---|
1941 | destruct (exec_stmt_steps _ _ _ _ _ _ H1 f (Kseq (Sfor Sskip a2 a3 s0) k)) as [S1 [A1 B1]]. |
---|
1942 | inv B1. |
---|
1943 | eapply forever_N_plus. |
---|
1944 | eapply plus_left. eapply step_for_start; eauto. |
---|
1945 | eapply star_right. eexact A1. |
---|
1946 | apply step_skip_seq. |
---|
1947 | reflexivity. reflexivity. |
---|
1948 | apply CIH_STMT; eauto. |
---|
1949 | traceEq. |
---|
1950 | |
---|
1951 | (* for body *) |
---|
1952 | eapply forever_N_plus. |
---|
1953 | apply plus_one. eapply step_for_true; eauto. |
---|
1954 | apply CIH_STMT; eauto. |
---|
1955 | traceEq. |
---|
1956 | |
---|
1957 | (* for next *) |
---|
1958 | destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]]. |
---|
1959 | eapply forever_N_plus. |
---|
1960 | eapply plus_left. eapply step_for_true; eauto. |
---|
1961 | eapply star_trans. eexact A1. |
---|
1962 | apply star_one. |
---|
1963 | inv H3; inv B1; apply step_skip_or_continue_for2; auto. |
---|
1964 | reflexivity. reflexivity. |
---|
1965 | apply CIH_STMT; eauto. |
---|
1966 | traceEq. |
---|
1967 | |
---|
1968 | (* for body *) |
---|
1969 | destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]]. |
---|
1970 | destruct (exec_stmt_steps _ _ _ _ _ _ H4 f (Kfor3 a2 a3 s0 k)) as [S2 [A2 B2]]. |
---|
1971 | inv B2. |
---|
1972 | eapply forever_N_plus. |
---|
1973 | eapply plus_left. eapply step_for_true; eauto. |
---|
1974 | eapply star_trans. eexact A1. |
---|
1975 | eapply star_left. inv H3; inv B1; apply step_skip_or_continue_for2; auto. |
---|
1976 | eapply star_right. eexact A2. |
---|
1977 | constructor. |
---|
1978 | reflexivity. reflexivity. reflexivity. reflexivity. |
---|
1979 | apply CIH_STMT; eauto. |
---|
1980 | traceEq. |
---|
1981 | |
---|
1982 | (* switch *) |
---|
1983 | eapply forever_N_plus. |
---|
1984 | eapply plus_one. eapply step_switch; eauto. |
---|
1985 | apply CIH_STMT; eauto. |
---|
1986 | traceEq. |
---|
1987 | |
---|
1988 | (* call internal *) |
---|
1989 | intros. inv H0. |
---|
1990 | eapply forever_N_plus. |
---|
1991 | eapply plus_one. econstructor; eauto. |
---|
1992 | apply H; eauto. |
---|
1993 | traceEq. |
---|
1994 | Qed. |
---|
1995 | |
---|
1996 | Theorem bigstep_program_terminates_exec: |
---|
1997 | ∀t,r. bigstep_program_terminates prog t r -> exec_program prog (Terminates t r). |
---|
1998 | Proof. |
---|
1999 | intros. inv H. unfold ge0, m0 in *. |
---|
2000 | econstructor. |
---|
2001 | econstructor. eauto. eauto. |
---|
2002 | apply eval_funcall_steps. eauto. red; auto. |
---|
2003 | econstructor. |
---|
2004 | Qed. |
---|
2005 | |
---|
2006 | Theorem bigstep_program_diverges_exec: |
---|
2007 | ∀T. bigstep_program_diverges prog T -> |
---|
2008 | exec_program prog (Reacts T) \/ |
---|
2009 | exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T. |
---|
2010 | Proof. |
---|
2011 | intros. inv H. |
---|
2012 | set (st := Callstate f nil Kstop m0). |
---|
2013 | assert (forever step ge0 st T). |
---|
2014 | eapply forever_N_forever with (order := order). |
---|
2015 | red; intros. constructor; intros. red in H. elim H. |
---|
2016 | eapply evalinf_funcall_forever; eauto. |
---|
2017 | destruct (forever_silent_or_reactive _ _ _ _ _ _ H) |
---|
2018 | as [A | [t [s' [T' [B [C D]]]]]]. |
---|
2019 | left. econstructor. econstructor. eauto. eauto. auto. |
---|
2020 | right. exists t. split. |
---|
2021 | econstructor. econstructor; eauto. eauto. auto. |
---|
2022 | subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor. |
---|
2023 | Qed. |
---|
2024 | |
---|
2025 | End BIGSTEP_TO_TRANSITIONS. |
---|
2026 | |
---|
2027 | |
---|
2028 | |
---|
2029 | *) |
---|
2030 | |
---|
2031 | |
---|