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

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

Oops, wrong bitvector negation.

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