source: src/Clight/Csem.ma @ 816

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

Clight to Cminor compilation, modulo switch statements, temporary
generation, 32 to 8 bit translation and miscellaneous bugs.

Also, remove (unused) signatures from function call statements in Cminor
and RTLabs; and separate comparison of integers and pointers in Clight
semantics.

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