source: C-semantics/Csem.ma @ 175

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

Add cost labels, with the semantics that the label is added to the
event trace.

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