source: src/Clight/Csem.ma @ 779

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

Fix up some minor null pointer issues in Clight.
Add corresponding Cminor example and fix up pretty printer a little.

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