source: C-semantics/Csem.ma @ 251

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

Some incomplete work on completeness of CexecIO wrt Csem.
Features some rather nasty induction principles.

File size: 78.3 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
18include "Coqlib.ma".
19include "Errors.ma".
20include "Integers.ma".
21include "Floats.ma".
22include "Values.ma".
23include "AST.ma".
24include "Mem.ma".
25include "Globalenvs.ma".
26include "Csyntax.ma".
27include "Maps.ma".
28include "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(* XXX: note that cost labels in exprs expose a particular eval order. *)
985
986ninductive step (ge:genv) : state → trace → state → Prop ≝
987
988  | step_assign:   ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m',tr1,tr2.
989      eval_lvalue ge e m a1 psp loc ofs tr1 →
990      eval_expr ge e m a2 v2 tr2 →
991      store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' →
992      step ge (State f (Sassign a1 a2) k e m)
993           (tr1⧺tr2) (State f Sskip k e m')
994
995  | step_call_none:   ∀f,a,al,k,e,m,vf,vargs,fd,tr1,tr2.
996      eval_expr ge e m a vf tr1 →
997      eval_exprlist ge e m al vargs tr2 →
998      find_funct ?? ge vf = Some ? fd →
999      type_of_fundef fd = typeof a →
1000      step ge (State f (Scall (None ?) a al) k e m)
1001           (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m)
1002
1003  | step_call_some:   ∀f,lhs,a,al,k,e,m,psp,loc,ofs,vf,vargs,fd,tr1,tr2,tr3.
1004      eval_lvalue ge e m lhs psp loc ofs tr1 →
1005      eval_expr ge e m a vf tr2 →
1006      eval_exprlist ge e m al vargs tr3 →
1007      find_funct ?? ge vf = Some ? fd →
1008      type_of_fundef fd = typeof a →
1009      step ge (State f (Scall (Some ? lhs) a al) k e m)
1010           (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈〈psp, loc〉, ofs〉, typeof lhs〉) f e k) m)
1011
1012  | step_seq:  ∀f,s1,s2,k,e,m.
1013      step ge (State f (Ssequence s1 s2) k e m)
1014           E0 (State f s1 (Kseq s2 k) e m)
1015  | step_skip_seq: ∀f,s,k,e,m.
1016      step ge (State f Sskip (Kseq s k) e m)
1017           E0 (State f s k e m)
1018  | step_continue_seq: ∀f,s,k,e,m.
1019      step ge (State f Scontinue (Kseq s k) e m)
1020           E0 (State f Scontinue k e m)
1021  | step_break_seq: ∀f,s,k,e,m.
1022      step ge (State f Sbreak (Kseq s k) e m)
1023           E0 (State f Sbreak k e m)
1024
1025  | step_ifthenelse_true:  ∀f,a,s1,s2,k,e,m,v1,tr.
1026      eval_expr ge e m a v1 tr →
1027      is_true v1 (typeof a) →
1028      step ge (State f (Sifthenelse a s1 s2) k e m)
1029           tr (State f s1 k e m)
1030  | step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1,tr.
1031      eval_expr ge e m a v1 tr →
1032      is_false v1 (typeof a) →
1033      step ge (State f (Sifthenelse a s1 s2) k e m)
1034           tr (State f s2 k e m)
1035
1036  | step_while_false: ∀f,a,s,k,e,m,v,tr.
1037      eval_expr ge e m a v tr →
1038      is_false v (typeof a) →
1039      step ge (State f (Swhile a s) k e m)
1040           tr (State f Sskip k e m)
1041  | step_while_true: ∀f,a,s,k,e,m,v,tr.
1042      eval_expr ge e m a v tr →
1043      is_true v (typeof a) →
1044      step ge (State f (Swhile a s) k e m)
1045           tr (State f s (Kwhile a s k) e m)
1046  | step_skip_or_continue_while: ∀f,x,a,s,k,e,m.
1047      x = Sskip ∨ x = Scontinue →
1048      step ge (State f x (Kwhile a s k) e m)
1049           E0 (State f (Swhile a s) k e m)
1050  | step_break_while: ∀f,a,s,k,e,m.
1051      step ge (State f Sbreak (Kwhile a s k) e m)
1052           E0 (State f Sskip k e m)
1053
1054  | step_dowhile: ∀f,a,s,k,e,m.
1055      step ge (State f (Sdowhile a s) k e m)
1056        E0 (State f s (Kdowhile a s k) e m)
1057  | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v,tr.
1058      x = Sskip ∨ x = Scontinue →
1059      eval_expr ge e m a v tr →
1060      is_false v (typeof a) →
1061      step ge (State f x (Kdowhile a s k) e m)
1062           tr (State f Sskip k e m)
1063  | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v,tr.
1064      x = Sskip ∨ x = Scontinue →
1065      eval_expr ge e m a v tr →
1066      is_true v (typeof a) →
1067      step ge (State f x (Kdowhile a s k) e m)
1068           tr (State f (Sdowhile a s) k e m)
1069  | step_break_dowhile: ∀f,a,s,k,e,m.
1070      step ge (State f Sbreak (Kdowhile a s k) e m)
1071           E0 (State f Sskip k e m)
1072
1073  | step_for_start: ∀f,a1,a2,a3,s,k,e,m.
1074      a1 ≠ Sskip →
1075      step ge (State f (Sfor a1 a2 a3 s) k e m)
1076           E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
1077  | step_for_false: ∀f,a2,a3,s,k,e,m,v,tr.
1078      eval_expr ge e m a2 v tr →
1079      is_false v (typeof a2) →
1080      step ge (State f (Sfor Sskip a2 a3 s) k e m)
1081           tr (State f Sskip k e m)
1082  | step_for_true: ∀f,a2,a3,s,k,e,m,v,tr.
1083      eval_expr ge e m a2 v tr →
1084      is_true v (typeof a2) →
1085      step ge (State f (Sfor Sskip a2 a3 s) k e m)
1086           tr (State f s (Kfor2 a2 a3 s k) e m)
1087  | step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m.
1088      x = Sskip ∨ x = Scontinue →
1089      step ge (State f x (Kfor2 a2 a3 s k) e m)
1090           E0 (State f a3 (Kfor3 a2 a3 s k) e m)
1091  | step_break_for2: ∀f,a2,a3,s,k,e,m.
1092      step ge (State f Sbreak (Kfor2 a2 a3 s k) e m)
1093           E0 (State f Sskip k e m)
1094  | step_skip_for3: ∀f,a2,a3,s,k,e,m.
1095      step ge (State f Sskip (Kfor3 a2 a3 s k) e m)
1096           E0 (State f (Sfor Sskip a2 a3 s) k e m)
1097
1098  | step_return_0: ∀f,k,e,m.
1099      fn_return f = Tvoid →
1100      step ge (State f (Sreturn (None ?)) k e m)
1101           E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e)))
1102  | step_return_1: ∀f,a,k,e,m,v,tr.
1103      fn_return f ≠ Tvoid →
1104      eval_expr ge e m a v tr →
1105      step ge (State f (Sreturn (Some ? a)) k e m)
1106           tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e)))
1107  | step_skip_call: ∀f,k,e,m.
1108      is_call_cont k →
1109      fn_return f = Tvoid →
1110      step ge (State f Sskip k e m)
1111           E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
1112
1113  | step_switch: ∀f,a,sl,k,e,m,n,tr.
1114      eval_expr ge e m a (Vint n) tr →
1115      step ge (State f (Sswitch a sl) k e m)
1116           tr (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m)
1117  | step_skip_break_switch: ∀f,x,k,e,m.
1118      x = Sskip ∨ x = Sbreak →
1119      step ge (State f x (Kswitch k) e m)
1120           E0 (State f Sskip k e m)
1121  | step_continue_switch: ∀f,k,e,m.
1122      step ge (State f Scontinue (Kswitch k) e m)
1123           E0 (State f Scontinue k e m)
1124
1125  | step_label: ∀f,lbl,s,k,e,m.
1126      step ge (State f (Slabel lbl s) k e m)
1127           E0 (State f s k e m)
1128
1129  | step_goto: ∀f,lbl,k,e,m,s',k'.
1130      find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉 →
1131      step ge (State f (Sgoto lbl) k e m)
1132           E0 (State f s' k' e m)
1133
1134  | step_internal_function: ∀f,vargs,k,m,e,m1,m2.
1135      alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 →
1136      bind_parameters e m1 (fn_params f) vargs m2 →
1137      step ge (Callstate (Internal f) vargs k m)
1138           E0 (State f (fn_body f) k e m2)
1139
1140  | step_external_function: ∀id,targs,tres,vargs,k,m,vres,t.
1141      event_match (external_function id targs tres) vargs t vres →
1142      step ge (Callstate (External id targs tres) vargs k m)
1143            t (Returnstate vres k m)
1144
1145  | step_returnstate_0: ∀v,f,e,k,m.
1146      step ge (Returnstate v (Kcall (None ?) f e k) m)
1147           E0 (State f Sskip k e m)
1148
1149  | step_returnstate_1: ∀v,f,e,k,m,m',psp,loc,ofs,ty.
1150      store_value_of_type ty m psp loc ofs v = Some ? m' →
1151      step ge (Returnstate v (Kcall (Some ? 〈〈〈psp,loc〉, ofs〉, ty〉) f e k) m)
1152           E0 (State f Sskip k e m')
1153           
1154  | step_cost: ∀f,lbl,s,k,e,m.
1155      step ge (State f (Scost lbl s) k e m)
1156           (Echarge lbl) (State f s k e m).
1157(*
1158(** * Alternate big-step semantics *)
1159
1160(** ** Big-step semantics for terminating statements and functions *)
1161
1162(** The execution of a statement produces an ``outcome'', indicating
1163  how the execution terminated: either normally or prematurely
1164  through the execution of a [break], [continue] or [return] statement. *)
1165
1166ninductive outcome: Type :=
1167   | Out_break: outcome                 (**r terminated by [break] *)
1168   | Out_continue: outcome              (**r terminated by [continue] *)
1169   | Out_normal: outcome                (**r terminated normally *)
1170   | Out_return: option val -> outcome. (**r terminated by [return] *)
1171
1172ninductive out_normal_or_continue : outcome -> Prop :=
1173  | Out_normal_or_continue_N: out_normal_or_continue Out_normal
1174  | Out_normal_or_continue_C: out_normal_or_continue Out_continue.
1175
1176ninductive out_break_or_return : outcome -> outcome -> Prop :=
1177  | Out_break_or_return_B: out_break_or_return Out_break Out_normal
1178  | Out_break_or_return_R: ∀ov.
1179      out_break_or_return (Out_return ov) (Out_return ov).
1180
1181Definition outcome_switch (out: outcome) : outcome :=
1182  match out with
1183  | Out_break => Out_normal
1184  | o => o
1185  end.
1186
1187Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop :=
1188  match out, t with
1189  | Out_normal, Tvoid => v = Vundef
1190  | Out_return None, Tvoid => v = Vundef
1191  | Out_return (Some v'), ty => ty <> Tvoid /\ v'=v
1192  | _, _ => False
1193  end.
1194
1195(** [exec_stmt ge e m1 s t m2 out] describes the execution of
1196  the statement [s].  [out] is the outcome for this execution.
1197  [m1] is the initial memory state, [m2] the final memory state.
1198  [t] is the trace of input/output events performed during this
1199  evaluation. *)
1200
1201ninductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop :=
1202  | exec_Sskip:   ∀e,m.
1203      exec_stmt e m Sskip
1204               E0 m Out_normal
1205  | exec_Sassign:   ∀e,m,a1,a2,loc,ofs,v2,m'.
1206      eval_lvalue e m a1 loc ofs ->
1207      eval_expr e m a2 v2 ->
1208      store_value_of_type (typeof a1) m loc ofs v2 = Some m' ->
1209      exec_stmt e m (Sassign a1 a2)
1210               E0 m' Out_normal
1211  | exec_Scall_none:   ∀e,m,a,al,vf,vargs,f,t,m',vres.
1212      eval_expr e m a vf ->
1213      eval_exprlist e m al vargs ->
1214      Genv.find_funct ge vf = Some f ->
1215      type_of_fundef f = typeof a ->
1216      eval_funcall m f vargs t m' vres ->
1217      exec_stmt e m (Scall None a al)
1218                t m' Out_normal
1219  | exec_Scall_some:   ∀e,m,lhs,a,al,loc,ofs,vf,vargs,f,t,m',vres,m''.
1220      eval_lvalue e m lhs loc ofs ->
1221      eval_expr e m a vf ->
1222      eval_exprlist e m al vargs ->
1223      Genv.find_funct ge vf = Some f ->
1224      type_of_fundef f = typeof a ->
1225      eval_funcall m f vargs t m' vres ->
1226      store_value_of_type (typeof lhs) m' loc ofs vres = Some m'' ->
1227      exec_stmt e m (Scall (Some lhs) a al)
1228                t m'' Out_normal
1229  | exec_Sseq_1:   ∀e,m,s1,s2,t1,m1,t2,m2,out.
1230      exec_stmt e m s1 t1 m1 Out_normal ->
1231      exec_stmt e m1 s2 t2 m2 out ->
1232      exec_stmt e m (Ssequence s1 s2)
1233                (t1 ** t2) m2 out
1234  | exec_Sseq_2:   ∀e,m,s1,s2,t1,m1,out.
1235      exec_stmt e m s1 t1 m1 out ->
1236      out <> Out_normal ->
1237      exec_stmt e m (Ssequence s1 s2)
1238                t1 m1 out
1239  | exec_Sifthenelse_true: ∀e,m,a,s1,s2,v1,t,m',out.
1240      eval_expr e m a v1 ->
1241      is_true v1 (typeof a) ->
1242      exec_stmt e m s1 t m' out ->
1243      exec_stmt e m (Sifthenelse a s1 s2)
1244                t m' out
1245  | exec_Sifthenelse_false: ∀e,m,a,s1,s2,v1,t,m',out.
1246      eval_expr e m a v1 ->
1247      is_false v1 (typeof a) ->
1248      exec_stmt e m s2 t m' out ->
1249      exec_stmt e m (Sifthenelse a s1 s2)
1250                t m' out
1251  | exec_Sreturn_none:   ∀e,m.
1252      exec_stmt e m (Sreturn None)
1253               E0 m (Out_return None)
1254  | exec_Sreturn_some: ∀e,m,a,v.
1255      eval_expr e m a v ->
1256      exec_stmt e m (Sreturn (Some a))
1257               E0 m (Out_return (Some v))
1258  | exec_Sbreak:   ∀e,m.
1259      exec_stmt e m Sbreak
1260               E0 m Out_break
1261  | exec_Scontinue:   ∀e,m.
1262      exec_stmt e m Scontinue
1263               E0 m Out_continue
1264  | exec_Swhile_false: ∀e,m,a,s,v.
1265      eval_expr e m a v ->
1266      is_false v (typeof a) ->
1267      exec_stmt e m (Swhile a s)
1268               E0 m Out_normal
1269  | exec_Swhile_stop: ∀e,m,a,v,s,t,m',out',out.
1270      eval_expr e m a v ->
1271      is_true v (typeof a) ->
1272      exec_stmt e m s t m' out' ->
1273      out_break_or_return out' out ->
1274      exec_stmt e m (Swhile a s)
1275                t m' out
1276  | exec_Swhile_loop: ∀e,m,a,s,v,t1,m1,out1,t2,m2,out.
1277      eval_expr e m a v ->
1278      is_true v (typeof a) ->
1279      exec_stmt e m s t1 m1 out1 ->
1280      out_normal_or_continue out1 ->
1281      exec_stmt e m1 (Swhile a s) t2 m2 out ->
1282      exec_stmt e m (Swhile a s)
1283                (t1 ** t2) m2 out
1284  | exec_Sdowhile_false: ∀e,m,s,a,t,m1,out1,v.
1285      exec_stmt e m s t m1 out1 ->
1286      out_normal_or_continue out1 ->
1287      eval_expr e m1 a v ->
1288      is_false v (typeof a) ->
1289      exec_stmt e m (Sdowhile a s)
1290                t m1 Out_normal
1291  | exec_Sdowhile_stop: ∀e,m,s,a,t,m1,out1,out.
1292      exec_stmt e m s t m1 out1 ->
1293      out_break_or_return out1 out ->
1294      exec_stmt e m (Sdowhile a s)
1295                t m1 out
1296  | exec_Sdowhile_loop: ∀e,m,s,a,m1,m2,t1,t2,out,out1,v.
1297      exec_stmt e m s t1 m1 out1 ->
1298      out_normal_or_continue out1 ->
1299      eval_expr e m1 a v ->
1300      is_true v (typeof a) ->
1301      exec_stmt e m1 (Sdowhile a s) t2 m2 out ->
1302      exec_stmt e m (Sdowhile a s)
1303                (t1 ** t2) m2 out
1304  | exec_Sfor_start: ∀e,m,s,a1,a2,a3,out,m1,m2,t1,t2.
1305      a1 <> Sskip ->
1306      exec_stmt e m a1 t1 m1 Out_normal ->
1307      exec_stmt e m1 (Sfor Sskip a2 a3 s) t2 m2 out ->
1308      exec_stmt e m (Sfor a1 a2 a3 s)
1309                (t1 ** t2) m2 out
1310  | exec_Sfor_false: ∀e,m,s,a2,a3,v.
1311      eval_expr e m a2 v ->
1312      is_false v (typeof a2) ->
1313      exec_stmt e m (Sfor Sskip a2 a3 s)
1314               E0 m Out_normal
1315  | exec_Sfor_stop: ∀e,m,s,a2,a3,v,m1,t,out1,out.
1316      eval_expr e m a2 v ->
1317      is_true v (typeof a2) ->
1318      exec_stmt e m s t m1 out1 ->
1319      out_break_or_return out1 out ->
1320      exec_stmt e m (Sfor Sskip a2 a3 s)
1321                t m1 out
1322  | exec_Sfor_loop: ∀e,m,s,a2,a3,v,m1,m2,m3,t1,t2,t3,out1,out.
1323      eval_expr e m a2 v ->
1324      is_true v (typeof a2) ->
1325      exec_stmt e m s t1 m1 out1 ->
1326      out_normal_or_continue out1 ->
1327      exec_stmt e m1 a3 t2 m2 Out_normal ->
1328      exec_stmt e m2 (Sfor Sskip a2 a3 s) t3 m3 out ->
1329      exec_stmt e m (Sfor Sskip a2 a3 s)
1330                (t1 ** t2 ** t3) m3 out
1331  | exec_Sswitch:   ∀e,m,a,t,n,sl,m1,out.
1332      eval_expr e m a (Vint n) ->
1333      exec_stmt e m (seq_of_labeled_statement (select_switch n sl)) t m1 out ->
1334      exec_stmt e m (Sswitch a sl)
1335                t m1 (outcome_switch out)
1336
1337(** [eval_funcall m1 fd args t m2 res] describes the invocation of
1338  function [fd] with arguments [args].  [res] is the value returned
1339  by the call.  *)
1340
1341with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
1342  | eval_funcall_internal: ∀m,f,vargs,t,e,m1,m2,m3,out,vres.
1343      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
1344      bind_parameters e m1 f.(fn_params) vargs m2 ->
1345      exec_stmt e m2 f.(fn_body) t m3 out ->
1346      outcome_result_value out f.(fn_return) vres ->
1347      eval_funcall m (Internal f) vargs t (Mem.free_list m3 (blocks_of_env e)) vres
1348  | eval_funcall_external: ∀m,id,targs,tres,vargs,t,vres.
1349      event_match (external_function id targs tres) vargs t vres ->
1350      eval_funcall m (External id targs tres) vargs t m vres.
1351
1352Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
1353  with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop.
1354
1355(** ** Big-step semantics for diverging statements and functions *)
1356
1357(** Coinductive semantics for divergence.
1358  [execinf_stmt ge e m s t] holds if the execution of statement [s]
1359  diverges, i.e. loops infinitely.  [t] is the possibly infinite
1360  trace of observable events performed during the execution. *)
1361
1362Coninductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop :=
1363  | execinf_Scall_none:   ∀e,m,a,al,vf,vargs,f,t.
1364      eval_expr e m a vf ->
1365      eval_exprlist e m al vargs ->
1366      Genv.find_funct ge vf = Some f ->
1367      type_of_fundef f = typeof a ->
1368      evalinf_funcall m f vargs t ->
1369      execinf_stmt e m (Scall None a al) t
1370  | execinf_Scall_some:   ∀e,m,lhs,a,al,loc,ofs,vf,vargs,f,t.
1371      eval_lvalue e m lhs loc ofs ->
1372      eval_expr e m a vf ->
1373      eval_exprlist e m al vargs ->
1374      Genv.find_funct ge vf = Some f ->
1375      type_of_fundef f = typeof a ->
1376      evalinf_funcall m f vargs t ->
1377      execinf_stmt e m (Scall (Some lhs) a al) t
1378  | execinf_Sseq_1:   ∀e,m,s1,s2,t.
1379      execinf_stmt e m s1 t ->
1380      execinf_stmt e m (Ssequence s1 s2) t
1381  | execinf_Sseq_2:   ∀e,m,s1,s2,t1,m1,t2.
1382      exec_stmt e m s1 t1 m1 Out_normal ->
1383      execinf_stmt e m1 s2 t2 ->
1384      execinf_stmt e m (Ssequence s1 s2) (t1 *** t2)
1385  | execinf_Sifthenelse_true: ∀e,m,a,s1,s2,v1,t.
1386      eval_expr e m a v1 ->
1387      is_true v1 (typeof a) ->
1388      execinf_stmt e m s1 t ->
1389      execinf_stmt e m (Sifthenelse a s1 s2) t
1390  | execinf_Sifthenelse_false: ∀e,m,a,s1,s2,v1,t.
1391      eval_expr e m a v1 ->
1392      is_false v1 (typeof a) ->
1393      execinf_stmt e m s2 t ->
1394      execinf_stmt e m (Sifthenelse a s1 s2) t
1395  | execinf_Swhile_body: ∀e,m,a,v,s,t.
1396      eval_expr e m a v ->
1397      is_true v (typeof a) ->
1398      execinf_stmt e m s t ->
1399      execinf_stmt e m (Swhile a s) t
1400  | execinf_Swhile_loop: ∀e,m,a,s,v,t1,m1,out1,t2.
1401      eval_expr e m a v ->
1402      is_true v (typeof a) ->
1403      exec_stmt e m s t1 m1 out1 ->
1404      out_normal_or_continue out1 ->
1405      execinf_stmt e m1 (Swhile a s) t2 ->
1406      execinf_stmt e m (Swhile a s) (t1 *** t2)
1407  | execinf_Sdowhile_body: ∀e,m,s,a,t.
1408      execinf_stmt e m s t ->
1409      execinf_stmt e m (Sdowhile a s) t
1410  | execinf_Sdowhile_loop: ∀e,m,s,a,m1,t1,t2,out1,v.
1411      exec_stmt e m s t1 m1 out1 ->
1412      out_normal_or_continue out1 ->
1413      eval_expr e m1 a v ->
1414      is_true v (typeof a) ->
1415      execinf_stmt e m1 (Sdowhile a s) t2 ->
1416      execinf_stmt e m (Sdowhile a s) (t1 *** t2)
1417  | execinf_Sfor_start_1: ∀e,m,s,a1,a2,a3,t.
1418      execinf_stmt e m a1 t ->
1419      execinf_stmt e m (Sfor a1 a2 a3 s) t
1420  | execinf_Sfor_start_2: ∀e,m,s,a1,a2,a3,m1,t1,t2.
1421      a1 <> Sskip ->
1422      exec_stmt e m a1 t1 m1 Out_normal ->
1423      execinf_stmt e m1 (Sfor Sskip a2 a3 s) t2 ->
1424      execinf_stmt e m (Sfor a1 a2 a3 s) (t1 *** t2)
1425  | execinf_Sfor_body: ∀e,m,s,a2,a3,v,t.
1426      eval_expr e m a2 v ->
1427      is_true v (typeof a2) ->
1428      execinf_stmt e m s t ->
1429      execinf_stmt e m (Sfor Sskip a2 a3 s) t
1430  | execinf_Sfor_next: ∀e,m,s,a2,a3,v,m1,t1,t2,out1.
1431      eval_expr e m a2 v ->
1432      is_true v (typeof a2) ->
1433      exec_stmt e m s t1 m1 out1 ->
1434      out_normal_or_continue out1 ->
1435      execinf_stmt e m1 a3 t2 ->
1436      execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2)
1437  | execinf_Sfor_loop: ∀e,m,s,a2,a3,v,m1,m2,t1,t2,t3,out1.
1438      eval_expr e m a2 v ->
1439      is_true v (typeof a2) ->
1440      exec_stmt e m s t1 m1 out1 ->
1441      out_normal_or_continue out1 ->
1442      exec_stmt e m1 a3 t2 m2 Out_normal ->
1443      execinf_stmt e m2 (Sfor Sskip a2 a3 s) t3 ->
1444      execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2 *** t3)
1445  | execinf_Sswitch:   ∀e,m,a,t,n,sl.
1446      eval_expr e m a (Vint n) ->
1447      execinf_stmt e m (seq_of_labeled_statement (select_switch n sl)) t ->
1448      execinf_stmt e m (Sswitch a sl) t
1449
1450(** [evalinf_funcall ge m fd args t] holds if the invocation of function
1451    [fd] on arguments [args] diverges, with observable trace [t]. *)
1452
1453with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop :=
1454  | evalinf_funcall_internal: ∀m,f,vargs,t,e,m1,m2.
1455      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
1456      bind_parameters e m1 f.(fn_params) vargs m2 ->
1457      execinf_stmt e m2 f.(fn_body) t ->
1458      evalinf_funcall m (Internal f) vargs t.
1459
1460End SEMANTICS.
1461*)
1462(* * * Whole-program semantics *)
1463
1464(* * Execution of whole programs are described as sequences of transitions
1465  from an initial state to a final state.  An initial state is a [Callstate]
1466  corresponding to the invocation of the ``main'' function of the program
1467  without arguments and with an empty continuation. *)
1468
1469ninductive initial_state (p: program): state -> Prop :=
1470  | initial_state_intro: ∀b,f.
1471      let ge := globalenv Genv ?? p in
1472      let m0 := init_mem Genv ?? p in
1473      find_symbol ?? ge (prog_main ?? p) = Some ? 〈Code,b〉 ->
1474      find_funct_ptr ?? ge b = Some ? f ->
1475      initial_state p (Callstate f (nil ?) Kstop m0).
1476
1477(* * A final state is a [Returnstate] with an empty continuation. *)
1478
1479ninductive final_state: state -> int -> Prop :=
1480  | final_state_intro: ∀r,m.
1481      final_state (Returnstate (Vint r) Kstop m) r.
1482
1483(* * Execution of a whole program: [exec_program p beh]
1484  holds if the application of [p]'s main function to no arguments
1485  in the initial memory state for [p] has [beh] as observable
1486  behavior. *)
1487
1488ndefinition exec_program : program → program_behavior → Prop ≝ λp,beh.
1489  program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv ??? p) beh.
1490(*
1491(** Big-step execution of a whole program.  *)
1492
1493ninductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
1494  | bigstep_program_terminates_intro: ∀b,f,m1,t,r.
1495      let ge := Genv.globalenv p in
1496      let m0 := Genv.init_mem p in
1497      Genv.find_symbol ge p.(prog_main) = Some b ->
1498      Genv.find_funct_ptr ge b = Some f ->
1499      eval_funcall ge m0 f nil t m1 (Vint r) ->
1500      bigstep_program_terminates p t r.
1501
1502ninductive bigstep_program_diverges (p: program): traceinf -> Prop :=
1503  | bigstep_program_diverges_intro: ∀b,f,t.
1504      let ge := Genv.globalenv p in
1505      let m0 := Genv.init_mem p in
1506      Genv.find_symbol ge p.(prog_main) = Some b ->
1507      Genv.find_funct_ptr ge b = Some f ->
1508      evalinf_funcall ge m0 f nil t ->
1509      bigstep_program_diverges p t.
1510
1511(** * Implication from big-step semantics to transition semantics *)
1512
1513Section BIGSTEP_TO_TRANSITIONS.
1514
1515Variable prog: program.
1516Let ge : genv := Genv.globalenv prog.
1517
1518Definition exec_stmt_eval_funcall_ind
1519  (PS: env -> mem -> statement -> trace -> mem -> outcome -> Prop)
1520  (PF: mem -> fundef -> list val -> trace -> mem -> val -> Prop) :=
1521  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 =>
1522  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)
1523       (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).
1524
1525ninductive outcome_state_match
1526       (e: env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop :=
1527  | osm_normal:
1528      outcome_state_match e m f k Out_normal (State f Sskip k e m)
1529  | osm_break:
1530      outcome_state_match e m f k Out_break (State f Sbreak k e m)
1531  | osm_continue:
1532      outcome_state_match e m f k Out_continue (State f Scontinue k e m)
1533  | osm_return_none: ∀k'.
1534      call_cont k' = call_cont k ->
1535      outcome_state_match e m f k
1536        (Out_return None) (State f (Sreturn None) k' e m)
1537  | osm_return_some: ∀a,v,k'.
1538      call_cont k' = call_cont k ->
1539      eval_expr ge e m a v ->
1540      outcome_state_match e m f k
1541        (Out_return (Some v)) (State f (Sreturn (Some a)) k' e m).
1542
1543Lemma is_call_cont_call_cont:
1544  ∀k. is_call_cont k -> call_cont k = k.
1545Proof.
1546  destruct k; simpl; intros; contradiction || auto.
1547Qed.
1548
1549Lemma exec_stmt_eval_funcall_steps:
1550  (∀e,m,s,t,m',out.
1551   exec_stmt ge e m s t m' out ->
1552   ∀f,k. exists S,
1553   star step ge (State f s k e m) t S
1554   /\ outcome_state_match e m' f k out S)
1555/\
1556  (∀m,fd,args,t,m',res.
1557   eval_funcall ge m fd args t m' res ->
1558   ∀k.
1559   is_call_cont k ->
1560   star step ge (Callstate fd args k m) t (Returnstate res k m')).
1561Proof.
1562  apply exec_stmt_eval_funcall_ind; intros.
1563
1564(* skip *)
1565  econstructor; split. apply star_refl. constructor.
1566
1567(* assign *)
1568  econstructor; split. apply star_one. econstructor; eauto. constructor.
1569
1570(* call none *)
1571  econstructor; split.
1572  eapply star_left. econstructor; eauto.
1573  eapply star_right. apply H4. simpl; auto. econstructor. reflexivity. traceEq.
1574  constructor.
1575
1576(* call some *)
1577  econstructor; split.
1578  eapply star_left. econstructor; eauto.
1579  eapply star_right. apply H5. simpl; auto. econstructor; eauto. reflexivity. traceEq.
1580  constructor.
1581
1582(* sequence 2 *)
1583  destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. inv B1.
1584  destruct (H2 f k) as [S2 [A2 B2]].
1585  econstructor; split.
1586  eapply star_left. econstructor.
1587  eapply star_trans. eexact A1.
1588  eapply star_left. constructor. eexact A2.
1589  reflexivity. reflexivity. traceEq.
1590  auto.
1591
1592(* sequence 1 *)
1593  destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]].
1594  set (S2 :=
1595    match out with
1596    | Out_break => State f Sbreak k e m1
1597    | Out_continue => State f Scontinue k e m1
1598    | _ => S1
1599    end).
1600  exists S2; split.
1601  eapply star_left. econstructor.
1602  eapply star_trans. eexact A1.
1603  unfold S2; inv B1.
1604    congruence.
1605    apply star_one. apply step_break_seq.
1606    apply star_one. apply step_continue_seq.
1607    apply star_refl.
1608    apply star_refl.
1609  reflexivity. traceEq.
1610  unfold S2; inv B1; congruence || econstructor; eauto.
1611
1612(* ifthenelse true *)
1613  destruct (H2 f k) as [S1 [A1 B1]].
1614  exists S1; split.
1615  eapply star_left. eapply step_ifthenelse_true; eauto. eexact A1. traceEq.
1616  auto.
1617
1618(* ifthenelse false *)
1619  destruct (H2 f k) as [S1 [A1 B1]].
1620  exists S1; split.
1621  eapply star_left. eapply step_ifthenelse_false; eauto. eexact A1. traceEq.
1622  auto.
1623
1624(* return none *)
1625  econstructor; split. apply star_refl. constructor. auto.
1626
1627(* return some *)
1628  econstructor; split. apply star_refl. econstructor; eauto.
1629
1630(* break *)
1631  econstructor; split. apply star_refl. constructor.
1632
1633(* continue *)
1634  econstructor; split. apply star_refl. constructor.
1635
1636(* while false *)
1637  econstructor; split.
1638  apply star_one. eapply step_while_false; eauto.
1639  constructor.
1640
1641(* while stop *)
1642  destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]].
1643  set (S2 :=
1644    match out' with
1645    | Out_break => State f Sskip k e m'
1646    | _ => S1
1647    end).
1648  exists S2; split.
1649  eapply star_left. eapply step_while_true; eauto.
1650  eapply star_trans. eexact A1.
1651  unfold S2. inversion H3; subst.
1652  inv B1. apply star_one. constructor.   
1653  apply star_refl.
1654  reflexivity. traceEq.
1655  unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto.
1656
1657(* while loop *)
1658  destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]].
1659  destruct (H5 f k) as [S2 [A2 B2]].
1660  exists S2; split.
1661  eapply star_left. eapply step_while_true; eauto.
1662  eapply star_trans. eexact A1.
1663  eapply star_left.
1664  inv H3; inv B1; apply step_skip_or_continue_while; auto.
1665  eexact A2.
1666  reflexivity. reflexivity. traceEq.
1667  auto.
1668
1669(* dowhile false *)
1670  destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
1671  exists (State f Sskip k e m1); split.
1672  eapply star_left. constructor.
1673  eapply star_right. eexact A1.
1674  inv H1; inv B1; eapply step_skip_or_continue_dowhile_false; eauto.
1675  reflexivity. traceEq.
1676  constructor.
1677
1678(* dowhile stop *)
1679  destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
1680  set (S2 :=
1681    match out1 with
1682    | Out_break => State f Sskip k e m1
1683    | _ => S1
1684    end).
1685  exists S2; split.
1686  eapply star_left. apply step_dowhile.
1687  eapply star_trans. eexact A1.
1688  unfold S2. inversion H1; subst.
1689  inv B1. apply star_one. constructor.
1690  apply star_refl.
1691  reflexivity. traceEq.
1692  unfold S2. inversion H1; subst. constructor. inv B1; econstructor; eauto.
1693
1694(* dowhile loop *)
1695  destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
1696  destruct (H5 f k) as [S2 [A2 B2]].
1697  exists S2; split.
1698  eapply star_left. apply step_dowhile.
1699  eapply star_trans. eexact A1.
1700  eapply star_left.
1701  inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto.
1702  eexact A2.
1703  reflexivity. reflexivity. traceEq.
1704  auto.
1705
1706(* for start *)
1707  destruct (H1 f (Kseq (Sfor Sskip a2 a3 s) k)) as [S1 [A1 B1]]. inv B1.
1708  destruct (H3 f k) as [S2 [A2 B2]].
1709  exists S2; split.
1710  eapply star_left. apply step_for_start; auto.   
1711  eapply star_trans. eexact A1.
1712  eapply star_left. constructor. eexact A2.
1713  reflexivity. reflexivity. traceEq.
1714  auto.
1715
1716(* for false *)
1717  econstructor; split.
1718  eapply star_one. eapply step_for_false; eauto.
1719  constructor.
1720
1721(* for stop *)
1722  destruct (H2 f (Kfor2 a2 a3 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. eapply step_for_true; eauto.
1730  eapply star_trans. eexact A1.
1731  unfold S2. inversion H3; subst.
1732  inv B1. apply star_one. constructor.
1733  apply star_refl.
1734  reflexivity. traceEq.
1735  unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto.
1736
1737(* for loop *)
1738  destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]].
1739  destruct (H5 f (Kfor3 a2 a3 s k)) as [S2 [A2 B2]]. inv B2.
1740  destruct (H7 f k) as [S3 [A3 B3]].
1741  exists S3; split.
1742  eapply star_left. eapply step_for_true; eauto.
1743  eapply star_trans. eexact A1.
1744  eapply star_trans with (s2 := State f a3 (Kfor3 a2 a3 s k) e m1).
1745  inv H3; inv B1.
1746  apply star_one. constructor. auto.
1747  apply star_one. constructor. auto.
1748  eapply star_trans. eexact A2.
1749  eapply star_left. constructor.
1750  eexact A3.
1751  reflexivity. reflexivity. reflexivity. reflexivity. traceEq.
1752  auto.
1753
1754(* switch *)
1755  destruct (H1 f (Kswitch k)) as [S1 [A1 B1]].
1756  set (S2 :=
1757    match out with
1758    | Out_normal => State f Sskip k e m1
1759    | Out_break => State f Sskip k e m1
1760    | Out_continue => State f Scontinue k e m1
1761    | _ => S1
1762    end).
1763  exists S2; split.
1764  eapply star_left. eapply step_switch; eauto.
1765  eapply star_trans. eexact A1.
1766  unfold S2; inv B1.
1767    apply star_one. constructor. auto.
1768    apply star_one. constructor. auto.
1769    apply star_one. constructor.
1770    apply star_refl.
1771    apply star_refl.
1772  reflexivity. traceEq.
1773  unfold S2. inv B1; simpl; econstructor; eauto.
1774
1775(* call internal *)
1776  destruct (H2 f k) as [S1 [A1 B1]].
1777  eapply star_left. eapply step_internal_function; eauto.
1778  eapply star_right. eexact A1.
1779  inv B1; simpl in H3; try contradiction.
1780  (* Out_normal *)
1781  assert (fn_return f = Tvoid /\ vres = Vundef).
1782    destruct (fn_return f); auto || contradiction.
1783  destruct H5. subst vres. apply step_skip_call; auto.
1784  (* Out_return None *)
1785  assert (fn_return f = Tvoid /\ vres = Vundef).
1786    destruct (fn_return f); auto || contradiction.
1787  destruct H6. subst vres.
1788  rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5.
1789  apply step_return_0; auto.
1790  (* Out_return Some *)
1791  destruct H3. subst vres.
1792  rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5.
1793  eapply step_return_1; eauto.
1794  reflexivity. traceEq.
1795
1796(* call external *)
1797  apply star_one. apply step_external_function; auto.
1798Qed.
1799
1800Lemma exec_stmt_steps:
1801   ∀e,m,s,t,m',out.
1802   exec_stmt ge e m s t m' out ->
1803   ∀f,k. exists S,
1804   star step ge (State f s k e m) t S
1805   /\ outcome_state_match e m' f k out S.
1806Proof (proj1 exec_stmt_eval_funcall_steps).
1807
1808Lemma eval_funcall_steps:
1809   ∀m,fd,args,t,m',res.
1810   eval_funcall ge m fd args t m' res ->
1811   ∀k.
1812   is_call_cont k ->
1813   star step ge (Callstate fd args k m) t (Returnstate res k m').
1814Proof (proj2 exec_stmt_eval_funcall_steps).
1815
1816Definition order (x y: unit) := False.
1817
1818Lemma evalinf_funcall_forever:
1819  ∀m,fd,args,T,k.
1820  evalinf_funcall ge m fd args T ->
1821  forever_N step order ge tt (Callstate fd args k m) T.
1822Proof.
1823  cofix CIH_FUN.
1824  assert (∀e,m,s,T,f,k.
1825          execinf_stmt ge e m s T ->
1826          forever_N step order ge tt (State f s k e m) T).
1827  cofix CIH_STMT.
1828  intros. inv H.
1829
1830(* call none *)
1831  eapply forever_N_plus.
1832  apply plus_one. eapply step_call_none; eauto.
1833  apply CIH_FUN. eauto. traceEq.
1834(* call some *)
1835  eapply forever_N_plus.
1836  apply plus_one. eapply step_call_some; eauto.
1837  apply CIH_FUN. eauto. traceEq.
1838
1839(* seq 1 *)
1840  eapply forever_N_plus.
1841  apply plus_one. econstructor.
1842  apply CIH_STMT; eauto. traceEq.
1843(* seq 2 *)
1844  destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kseq s2 k)) as [S1 [A1 B1]].
1845  inv B1.
1846  eapply forever_N_plus.
1847  eapply plus_left. constructor. eapply star_trans. eexact A1.
1848  apply star_one. constructor. reflexivity. reflexivity.
1849  apply CIH_STMT; eauto. traceEq.
1850
1851(* ifthenelse true *)
1852  eapply forever_N_plus.
1853  apply plus_one. eapply step_ifthenelse_true; eauto.
1854  apply CIH_STMT; eauto. traceEq.
1855(* ifthenelse false *)
1856  eapply forever_N_plus.
1857  apply plus_one. eapply step_ifthenelse_false; eauto.
1858  apply CIH_STMT; eauto. traceEq.
1859
1860(* while body *)
1861  eapply forever_N_plus.
1862  eapply plus_one. eapply step_while_true; eauto.
1863  apply CIH_STMT; eauto. traceEq.
1864(* while loop *)
1865  destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kwhile a s0 k)) as [S1 [A1 B1]].
1866  eapply forever_N_plus with (s2 := State f (Swhile a s0) k e m1).
1867  eapply plus_left. eapply step_while_true; eauto.
1868  eapply star_right. eexact A1.
1869  inv H3; inv B1; apply step_skip_or_continue_while; auto.
1870  reflexivity. reflexivity.
1871  apply CIH_STMT; eauto. traceEq.
1872
1873(* dowhile body *)
1874  eapply forever_N_plus.
1875  eapply plus_one. eapply step_dowhile.
1876  apply CIH_STMT; eauto.
1877  traceEq.
1878
1879(* dowhile loop *)
1880  destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kdowhile a s0 k)) as [S1 [A1 B1]].
1881  eapply forever_N_plus with (s2 := State f (Sdowhile a s0) k e m1).
1882  eapply plus_left. eapply step_dowhile.
1883  eapply star_right. eexact A1.
1884  inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto.
1885  reflexivity. reflexivity.
1886  apply CIH_STMT. eauto.
1887  traceEq.
1888
1889(* for start 1 *)
1890  assert (a1 <> Sskip). red; intros; subst. inv H0.
1891  eapply forever_N_plus.
1892  eapply plus_one. apply step_for_start; auto.
1893  apply CIH_STMT; eauto.
1894  traceEq.
1895
1896(* for start 2 *)
1897  destruct (exec_stmt_steps _ _ _ _ _ _ H1 f (Kseq (Sfor Sskip a2 a3 s0) k)) as [S1 [A1 B1]].
1898  inv B1.
1899  eapply forever_N_plus.
1900  eapply plus_left. eapply step_for_start; eauto.
1901  eapply star_right. eexact A1.
1902  apply step_skip_seq.
1903  reflexivity. reflexivity.
1904  apply CIH_STMT; eauto.
1905  traceEq.
1906
1907(* for body *)
1908  eapply forever_N_plus.
1909  apply plus_one. eapply step_for_true; eauto.
1910  apply CIH_STMT; eauto.
1911  traceEq.
1912
1913(* for next *)
1914  destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]].
1915  eapply forever_N_plus.
1916  eapply plus_left. eapply step_for_true; eauto.
1917  eapply star_trans. eexact A1.
1918  apply star_one.
1919  inv H3; inv B1; apply step_skip_or_continue_for2; auto.
1920  reflexivity. reflexivity.
1921  apply CIH_STMT; eauto.
1922  traceEq.
1923
1924(* for body *)
1925  destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]].
1926  destruct (exec_stmt_steps _ _ _ _ _ _ H4 f (Kfor3 a2 a3 s0 k)) as [S2 [A2 B2]].
1927  inv B2.
1928  eapply forever_N_plus.
1929  eapply plus_left. eapply step_for_true; eauto.
1930  eapply star_trans. eexact A1.
1931  eapply star_left. inv H3; inv B1; apply step_skip_or_continue_for2; auto.
1932  eapply star_right. eexact A2.
1933  constructor.
1934  reflexivity. reflexivity. reflexivity. reflexivity. 
1935  apply CIH_STMT; eauto.
1936  traceEq.
1937
1938(* switch *)
1939  eapply forever_N_plus.
1940  eapply plus_one. eapply step_switch; eauto.
1941  apply CIH_STMT; eauto.
1942  traceEq.
1943
1944(* call internal *)
1945  intros. inv H0.
1946  eapply forever_N_plus.
1947  eapply plus_one. econstructor; eauto.
1948  apply H; eauto.
1949  traceEq.
1950Qed.
1951
1952Theorem bigstep_program_terminates_exec:
1953  ∀t,r. bigstep_program_terminates prog t r -> exec_program prog (Terminates t r).
1954Proof.
1955  intros. inv H. unfold ge0, m0 in *.
1956  econstructor.
1957  econstructor. eauto. eauto.
1958  apply eval_funcall_steps. eauto. red; auto.
1959  econstructor.
1960Qed.
1961
1962Theorem bigstep_program_diverges_exec:
1963  ∀T. bigstep_program_diverges prog T ->
1964  exec_program prog (Reacts T) \/
1965  exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T.
1966Proof.
1967  intros. inv H.
1968  set (st := Callstate f nil Kstop m0).
1969  assert (forever step ge0 st T).
1970    eapply forever_N_forever with (order := order).
1971    red; intros. constructor; intros. red in H. elim H.
1972    eapply evalinf_funcall_forever; eauto.
1973  destruct (forever_silent_or_reactive _ _ _ _ _ _ H)
1974  as [A | [t [s' [T' [B [C D]]]]]].
1975  left. econstructor. econstructor. eauto. eauto. auto.
1976  right. exists t. split.
1977  econstructor. econstructor; eauto. eauto. auto.
1978  subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor.
1979Qed.
1980
1981End BIGSTEP_TO_TRANSITIONS.
1982
1983
1984
1985*)
1986
1987 
Note: See TracBrowser for help on using the repository browser.