source: src/Clight/Csem.ma @ 961

Last change on this file since 961 was 961, checked in by campbell, 8 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 80.4 KB
Line 
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".*)
25include "common/Globalenvs.ma".
26include "Clight/Csyntax.ma".
27include "common/Maps.ma".
28(*include "Events.ma".*)
29include "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
38inductive 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
46inductive 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
56inductive 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
72let 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
89let 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
95let 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
118let 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
152let 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
193let 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
212let 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
238let 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
258let 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
267let 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
276let 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
285let 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
295let 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
319let rec sem_cmp_mismatch (c: comparison): option val ≝
320  match c with
321  [ Ceq =>  Some ? Vfalse
322  | Cne =>  Some ? Vtrue
323  | _   => None ?
324  ].
325
326let rec sem_cmp_match (c: comparison): option val ≝
327  match c with
328  [ Ceq =>  Some ? Vtrue
329  | Cne =>  Some ? Vfalse
330  | _   => None ?
331  ].
332 
333let 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
383definition 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
392let 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
419let rec cast_int_int (srcsz: intsize) (sz: intsize) (sg: signedness) (i: BitVector (bitsize_of_intsize srcsz)) : BitVector (bitsize_of_intsize sz) ≝
420  match sg with [ Signed ⇒ sign_ext ?? i | Unsigned ⇒ zero_ext ?? i ].
421
422let 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
428let 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
434let rec cast_float_float (sz: floatsize) (f: float) : float ≝
435  match sz with
436  [ F32 ⇒ singleoffloat f
437  | F64 ⇒ f
438  ].
439
440inductive 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
446inductive 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 ? sz2 si2 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
478definition 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
484definition env ≝ (tree_t ? PTree) block. (* map variable -> location *)
485
486definition 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
494let 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  ].
504cases b //
505qed.
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
512let 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  ].
518cases loc //
519qed.
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
528inductive 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
545inductive 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
560definition 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. *)
567let 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
577let 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(*
584Section SEMANTICS.
585
586Variable ge: genv.
587
588(** ** Evaluation of expressions *)
589
590Section EXPR.
591
592Variable e: env.
593Variable 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
599inductive 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
666with 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
690let 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
726inverter eval_expr_inv_ind for eval_expr : Prop.
727
728let 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(*
745ninverter eval_lvalue_inv_ind for eval_lvalue : Prop.
746*)
747
748definition 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
797let 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  ]
839and 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
871definition 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. 
873conj ??
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(*
882Scheme 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
889inductive 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
903inductive 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
924let 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
935definition is_call_cont : cont → Prop ≝ λk.
936  match k with
937  [ Kstop => True
938  | Kcall _ _ _ _ => True
939  | _ => False
940  ].
941
942(* * States *)
943
944inductive 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
964let 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
1000and 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. *)
1014definition 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
1029inductive 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
1209inductive 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
1215inductive 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
1219inductive 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
1224Definition outcome_switch (out: outcome) : outcome :=
1225  match out with
1226  | Out_break => Out_normal
1227  | o => o
1228  end.
1229
1230Definition 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
1244inductive 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
1384with 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
1395Scheme 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
1405Coinductive 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
1496with 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
1503End 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
1512inductive 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
1522inductive 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
1531definition 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
1537inductive 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
1546inductive 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
1557Section BIGSTEP_TO_TRANSITIONS.
1558
1559Variable prog: program.
1560Let ge : genv := Genv.globalenv prog.
1561
1562Definition 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
1569inductive 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
1587Lemma is_call_cont_call_cont:
1588  ∀k. is_call_cont k -> call_cont k = k.
1589Proof.
1590  destruct k; simpl; intros; contradiction || auto.
1591Qed.
1592
1593Lemma 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')).
1605Proof.
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.
1842Qed.
1843
1844Lemma 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.
1850Proof (proj1 exec_stmt_eval_funcall_steps).
1851
1852Lemma 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').
1858Proof (proj2 exec_stmt_eval_funcall_steps).
1859
1860Definition order (x y: unit) := False.
1861
1862Lemma 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.
1866Proof.
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.
1994Qed.
1995
1996Theorem bigstep_program_terminates_exec:
1997  ∀t,r. bigstep_program_terminates prog t r -> exec_program prog (Terminates t r).
1998Proof.
1999  intros. inv H. unfold ge0, m0 in *.
2000  econstructor.
2001  econstructor. eauto. eauto.
2002  apply eval_funcall_steps. eauto. red; auto.
2003  econstructor.
2004Qed.
2005
2006Theorem 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.
2010Proof.
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.
2023Qed.
2024
2025End BIGSTEP_TO_TRANSITIONS.
2026
2027
2028
2029*)
2030
2031 
Note: See TracBrowser for help on using the repository browser.