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

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

Abstract pointer offsets a little, similar to the changes for the prototype
proposed in Bologna.

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