source: src/Clight/Csem.ma @ 1139

Last change on this file since 1139 was 1139, checked in by campbell, 9 years ago

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

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