source: Deliverables/D3.1/C-semantics/Csem.ma @ 478

Last change on this file since 478 was 478, checked in by campbell, 10 years ago

Prevent clashes between names in AST and other parts of the development.
(Noticed when trying a large example file.)

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