source: C-semantics/Csem.ma @ 226

Last change on this file since 226 was 226, checked in by campbell, 8 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.