source: C-semantics/Csem.ma @ 124

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

Initial work on Clight semantics with 8051 memory spaces.

File size: 60.7 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: ∀pcl,b,ofs,sz,sg.
51      is_true (Vptr pcl 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: ∀pcl,b,ofs,s,t.
56      is_true (Vptr pcl 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 pcl 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
402(* XXX should go somewhere else? *)
403ndefinition ptr_cls_spc : ptr_class → mem_space ≝
404λp.match p with
405[ Universal ⇒ Generic
406| Data ⇒ Data
407| IData ⇒ IData
408| XData ⇒ XData
409| Code ⇒ Code
410].
411ndefinition ptr_spc_cls : mem_space → ptr_class ≝
412λp.match p with
413[ Generic ⇒ Universal
414| Data ⇒ Data
415| IData ⇒ IData
416| XData ⇒ XData
417| Code ⇒ Code
418].
419
420ndefinition blk_ptr_cls : block_class → ptr_class ≝
421λb.match b with
422[ UnspecifiedB ⇒ Universal
423| DataB ⇒ Data
424| IDataB ⇒ IData
425| XDataB ⇒ XData
426| CodeB ⇒ Code
427].
428
429ninductive type_pointable : type → Prop ≝
430| type_ptr_int : type_pointable (Tint I32 Unsigned)
431| type_ptr_pointer : ∀s,t. type_pointable (Tpointer s t)
432| type_ptr_array : ∀s,t,n. type_pointable (Tarray s t n)
433| type_ptr_function : ∀tys,ty. type_pointable (Tfunction tys ty).
434
435ninductive type_space : type → mem_space → Prop ≝
436| type_spc_int : type_space (Tint I32 Unsigned) Generic
437| type_spc_pointer : ∀s,t. type_space (Tpointer s t) s
438| type_spc_array : ∀s,t,n. type_space (Tarray s t n) s
439| type_spc_code : ∀tys,ty. type_space (Tfunction tys ty) Code.
440
441ninductive cast : mem → val → type → type → val → Prop ≝
442  | cast_ii:   ∀m,i,sz2,sz1,si1,si2.            (**r int to int  *)
443      cast m (Vint i) (Tint sz1 si1) (Tint sz2 si2)
444           (Vint (cast_int_int sz2 si2 i))
445  | cast_fi:   ∀m,f,sz1,sz2,si2.                (**r float to int *)
446      cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
447           (Vint (cast_int_int sz2 si2 (cast_float_int si2 f)))
448  | cast_if:   ∀m,i,sz1,sz2,si1.                (**r int to float  *)
449      cast m (Vint i) (Tint sz1 si1) (Tfloat sz2)
450          (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
451  | cast_ff:   ∀m,f,sz1,sz2.                    (**r float to float *)
452      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
453           (Vfloat (cast_float_float sz2 f))
454  | cast_pp: ∀m,pcl,psp,ty,ty',b,ofs.
455      type_pointable ty →
456      type_space ty' psp →
457      class_compat (blockclass m b) (ptr_spc_cls psp) →
458      cast m (Vptr pcl b ofs) ty ty' (Vptr (ptr_spc_cls psp) b ofs)
459  | cast_pp_z: ∀m,ty,ty'.
460      type_pointable ty → (* Don't care which space it is for the source type *)
461      type_pointable ty' →
462      cast m (Vint zero) ty ty' (Vint zero).
463(* XXX: other integers?
464  | cast_nn_i: ∀m,n,t1,t2.     (**r no change in data representation *)
465      neutral_for_cast t1 → neutral_for_cast t2 →
466      cast m (Vint n) t1 t2 (Vint n).
467*)
468(* * * Operational semantics *)
469
470(* * The semantics uses two environments.  The global environment
471  maps names of functions and global variables to memory block references,
472  and function pointers to their definitions.  (See module [Globalenvs].) *)
473
474ndefinition genv ≝ (genv_t Genv) fundef.
475
476(* * The local environment maps local variables to block references.
477  The current value of the variable is stored in the associated memory
478  block. *)
479
480ndefinition env ≝ (tree_t ? PTree) (block_class × block). (* map variable -> location *)
481
482ndefinition empty_env: env ≝ (empty …).
483
484(* * [load_value_of_type ty m b ofs] computes the value of a datum
485  of type [ty] residing in memory [m] at block [b], offset [ofs].
486  If the type [ty] indicates an access by value, the corresponding
487  memory load is performed.  If the type [ty] indicates an access by
488  reference, the pointer [Vptr b ofs] is returned. *)
489
490nlet rec load_value_of_type (ty: type) (m: mem) (pcl:ptr_class) (b: block) (ofs: int) : option val ≝
491  match access_mode ty with
492  [ By_value chunk ⇒ loadv chunk m (Vptr pcl b ofs)
493  | By_reference ⇒ Some ? (Vptr pcl b ofs)
494  | By_nothing ⇒ None ?
495  ].
496
497(* * Symmetrically, [store_value_of_type ty m b ofs v] returns the
498  memory state after storing the value [v] in the datum
499  of type [ty] residing in memory [m] at block [b], offset [ofs].
500  This is allowed only if [ty] indicates an access by value. *)
501
502nlet rec store_value_of_type (ty_dest: type) (m: mem) (pcl:ptr_class) (loc: block) (ofs: int) (v: val) : option mem ≝
503  match access_mode ty_dest with
504  [ By_value chunk ⇒ storev chunk m (Vptr pcl loc ofs) v
505  | By_reference ⇒ None ?
506  | By_nothing ⇒ None ?
507  ].
508
509(* * Allocation of function-local variables.
510  [alloc_variables e1 m1 vars e2 m2] allocates one memory block
511  for each variable declared in [vars], and associates the variable
512  name with this block.  [e1] and [m1] are the initial local environment
513  and memory state.  [e2] and [m2] are the final local environment
514  and memory state. *)
515
516ninductive alloc_variables: env → mem →
517                            list (ident × type) →
518                            env → mem → Prop ≝
519  | alloc_variables_nil:
520      ∀e,m.
521      alloc_variables e m (nil ?) e m
522  | alloc_variables_cons:
523      ∀e,m,id,ty,vars,m1,b1,m2,e2.
524      alloc m 0 (sizeof ty) UnspecifiedB = 〈m1, b1〉 → (* XXX *)
525      alloc_variables (set … id 〈UnspecifiedB, b1〉 e) m1 vars e2 m2 →
526      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
527
528(* * Initialization of local variables that are parameters to a function.
529  [bind_parameters e m1 params args m2] stores the values [args]
530  in the memory blocks corresponding to the variables [params].
531  [m1] is the initial memory state and [m2] the final memory state. *)
532
533ninductive bind_parameters: env →
534                           mem → list (ident × type) → list val →
535                           mem → Prop ≝
536  | bind_parameters_nil:
537      ∀e,m.
538      bind_parameters e m (nil ?) (nil ?) m
539  | bind_parameters_cons:
540      ∀e,m,id,ty,params,v1,vl,bcls,b,m1,m2.
541      get ??? id e = Some ? 〈bcls,b〉 →
542      store_value_of_type ty m (blk_ptr_cls bcls) b zero v1 = Some ? m1 →
543      bind_parameters e m1 params vl m2 →
544      bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2.
545
546(* * Return the list of blocks in the codomain of [e]. *)
547
548ndefinition blocks_of_env : env → list block ≝ λe.
549  map ?? (λx. snd ?? (snd ?? x)) (elements ??? e).
550
551(* * Selection of the appropriate case of a [switch], given the value [n]
552  of the selector expression. *)
553
554nlet rec select_switch (n: int) (sl: labeled_statements)
555                       on sl : labeled_statements ≝
556  match sl with
557  [ LSdefault _ ⇒ sl
558  | LScase c s sl' ⇒ if eq c n then sl else select_switch n sl'
559  ].
560
561(* * Turn a labeled statement into a sequence *)
562
563nlet rec seq_of_labeled_statement (sl: labeled_statements) : statement ≝
564  match sl with
565  [ LSdefault s ⇒ s
566  | LScase c s sl' ⇒ Ssequence s (seq_of_labeled_statement sl')
567  ].
568
569(*
570Section SEMANTICS.
571
572Variable ge: genv.
573
574(** ** Evaluation of expressions *)
575
576Section EXPR.
577
578Variable e: env.
579Variable m: mem.
580*)
581(* * [eval_expr ge e m a v] defines the evaluation of expression [a]
582  in r-value position.  [v] is the value of the expression.
583  [e] is the current environment and [m] is the current memory state. *)
584
585ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → Prop ≝
586  | eval_Econst_int:   ∀i,ty.
587      eval_expr ge e m (Expr (Econst_int i) ty) (Vint i)
588  | eval_Econst_float:   ∀f,ty.
589      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f)
590  | eval_Elvalue: ∀a,ty,pcl,loc,ofs,v.
591      eval_lvalue ge e m (Expr a ty) pcl loc ofs ->
592      load_value_of_type ty m pcl loc ofs = Some ? v ->
593      eval_expr ge e m (Expr a ty) v
594  | eval_Eaddrof: ∀a,ty,pcl,loc,ofs.
595      eval_lvalue ge e m a pcl loc ofs ->
596      eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr pcl loc ofs)
597  | eval_Esizeof: ∀ty',ty.
598      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty')))
599  | eval_Eunop:  ∀op,a,ty,v1,v.
600      eval_expr ge e m a v1 ->
601      sem_unary_operation op v1 (typeof a) = Some ? v ->
602      eval_expr ge e m (Expr (Eunop op a) ty) v
603  | eval_Ebinop: ∀op,a1,a2,ty,v1,v2,v.
604      eval_expr ge e m a1 v1 ->
605      eval_expr ge e m a2 v2 ->
606      sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v ->
607      eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v
608  | eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2.
609      eval_expr ge e m a1 v1 ->
610      is_true v1 (typeof a1) ->
611      eval_expr ge e m a2 v2 ->
612      eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v2
613  | eval_Econdition_false: ∀a1,a2,a3,ty,v1,v3.
614      eval_expr ge e m a1 v1 ->
615      is_false v1 (typeof a1) ->
616      eval_expr ge e m a3 v3 ->
617      eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3
618  | eval_Eorbool_1: ∀a1,a2,ty,v1.
619      eval_expr ge e m a1 v1 ->
620      is_true v1 (typeof a1) ->
621      eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue
622  | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v.
623      eval_expr ge e m a1 v1 ->
624      is_false v1 (typeof a1) ->
625      eval_expr ge e m a2 v2 ->
626      bool_of_val v2 (typeof a2) v ->
627      eval_expr ge e m (Expr (Eorbool a1 a2) ty) v
628  | eval_Eandbool_1: ∀a1,a2,ty,v1.
629      eval_expr ge e m a1 v1 ->
630      is_false v1 (typeof a1) ->
631      eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse
632  | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v.
633      eval_expr ge e m a1 v1 ->
634      is_true v1 (typeof a1) ->
635      eval_expr ge e m a2 v2 ->
636      bool_of_val v2 (typeof a2) v ->
637      eval_expr ge e m (Expr (Eandbool a1 a2) ty) v
638  | eval_Ecast:   ∀a,ty,ty',v1,v.
639      eval_expr ge e m a v1 ->
640      cast m v1 (typeof a) ty v ->
641      eval_expr ge e m (Expr (Ecast ty a) ty') v
642
643(* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]
644  in l-value position.  The result is the memory location [b, ofs]
645  that contains the value of the expression [a]. *)
646
647with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → ptr_class → block -> int -> Prop ≝
648  | eval_Evar_local:   ∀id,bcl,l,ty.
649      (* XXX notation? e!id*) get ??? id e = Some ? 〈bcl,l〉 ->
650      eval_lvalue ge e m (Expr (Evar id) ty) (blk_ptr_cls bcl) l zero
651  | eval_Evar_global: ∀id,l,ty.
652      (* XXX e!id *) get ??? id e = None ? ->
653      find_symbol ?? ge id = Some ? l ->
654      eval_lvalue ge e m (Expr (Evar id) ty) Universal l zero (* XXX *)
655  | eval_Ederef: ∀a,ty,pcl,l,ofs.
656      eval_expr ge e m a (Vptr pcl l ofs) ->
657      eval_lvalue ge e m (Expr (Ederef a) ty) pcl l ofs
658 | eval_Efield_struct:   ∀a,i,ty,pcl,l,ofs,id,fList,delta.
659      eval_lvalue ge e m a pcl l ofs ->
660      typeof a = Tstruct id fList ->
661      field_offset i fList = OK ? delta ->
662      eval_lvalue ge e m (Expr (Efield a i) ty) pcl l (add ofs (repr delta))
663 | eval_Efield_union:   ∀a,i,ty,pcl,l,ofs,id,fList.
664      eval_lvalue ge e m a pcl l ofs ->
665      typeof a = Tunion id fList ->
666      eval_lvalue ge e m (Expr (Efield a i) ty) pcl l ofs.
667
668(*
669Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop
670  with eval_lvalue_ind2 := Minimality for eval_lvalue Sort Prop.
671*)
672
673(* * [eval_exprlist ge e m al vl] evaluates a list of r-value
674  expressions [al] to their values [vl]. *)
675
676ninductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr -> list val -> Prop :=
677  | eval_Enil:
678      eval_exprlist ge e m (nil ?) (nil ?)
679  | eval_Econs:   ∀a,bl,v,vl.
680      eval_expr ge e m a v ->
681      eval_exprlist ge e m bl vl ->
682      eval_exprlist ge e m (a :: bl) (v :: vl).
683
684(*End EXPR.*)
685
686(* * ** Transition semantics for statements and functions *)
687
688(* * Continuations *)
689
690ninductive cont: Type :=
691  | Kstop: cont
692  | Kseq: statement -> cont -> cont
693       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
694  | Kwhile: expr -> statement -> cont -> cont
695       (**r [Kwhile e s k] = after [s] in [while (e) s] *)
696  | Kdowhile: expr -> statement -> cont -> cont
697       (**r [Kdowhile e s k] = after [s] in [do s while (e)] *)
698  | Kfor2: expr -> statement -> statement -> cont -> cont
699       (**r [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *)
700  | Kfor3: expr -> statement -> statement -> cont -> cont
701       (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *)
702  | Kswitch: cont -> cont
703       (**r catches [break] statements arising out of [switch] *)
704  | Kcall: option (ptr_class × block × int × type) ->   (**r where to store result *)
705           function ->                      (**r calling function *)
706           env ->                           (**r local env of calling function *)
707           cont -> cont.
708
709(* * Pop continuation until a call or stop *)
710
711nlet rec call_cont (k: cont) : cont :=
712  match k with
713  [ Kseq s k => call_cont k
714  | Kwhile e s k => call_cont k
715  | Kdowhile e s k => call_cont k
716  | Kfor2 e2 e3 s k => call_cont k
717  | Kfor3 e2 e3 s k => call_cont k
718  | Kswitch k => call_cont k
719  | _ => k
720  ].
721
722ndefinition is_call_cont : cont → Prop ≝ λk.
723  match k with
724  [ Kstop => True
725  | Kcall _ _ _ _ => True
726  | _ => False
727  ].
728
729(* * States *)
730
731ninductive state: Type :=
732  | State:
733      ∀f: function.
734      ∀s: statement.
735      ∀k: cont.
736      ∀e: env.
737      ∀m: mem.  state
738  | Callstate:
739      ∀fd: fundef.
740      ∀args: list val.
741      ∀k: cont.
742      ∀m: mem. state
743  | Returnstate:
744      ∀res: val.
745      ∀k: cont.
746      ∀m: mem. state.
747                 
748(* * Find the statement and manufacture the continuation
749  corresponding to a label *)
750
751nlet rec find_label (lbl: label) (s: statement) (k: cont)
752                    on s: option (statement × cont) :=
753  match s with
754  [ Ssequence s1 s2 =>
755      match find_label lbl s1 (Kseq s2 k) with
756      [ Some sk => Some ? sk
757      | None => find_label lbl s2 k
758      ]
759  | Sifthenelse a s1 s2 =>
760      match find_label lbl s1 k with
761      [ Some sk => Some ? sk
762      | None => find_label lbl s2 k
763      ]
764  | Swhile a s1 =>
765      find_label lbl s1 (Kwhile a s1 k)
766  | Sdowhile a s1 =>
767      find_label lbl s1 (Kdowhile a s1 k)
768  | Sfor a1 a2 a3 s1 =>
769      match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 s1) k) with
770      [ Some sk => Some ? sk
771      | None =>
772          match find_label lbl s1 (Kfor2 a2 a3 s1 k) with
773          [ Some sk => Some ? sk
774          | None => find_label lbl a3 (Kfor3 a2 a3 s1 k)
775          ]
776      ]
777  | Sswitch e sl =>
778      find_label_ls lbl sl (Kswitch k)
779  | Slabel lbl' s' =>
780      match ident_eq lbl lbl' with
781      [ inl _ ⇒ Some ? 〈s', k〉
782      | inr _ ⇒ find_label lbl s' k
783      ]
784  | _ => None ?
785  ]
786
787and find_label_ls (lbl: label) (sl: labeled_statements) (k: cont)
788                    on sl: option (statement × cont) :=
789  match sl with
790  [ LSdefault s => find_label lbl s k
791  | LScase _ s sl' =>
792      match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with
793      [ Some sk => Some ? sk
794      | None => find_label_ls lbl sl' k
795      ]
796  ].
797
798(* * Transition relation *)
799
800ninductive step (ge:genv) : state -> trace -> state -> Prop :=
801
802  | step_assign:   ∀f,a1,a2,k,e,m,pcl,loc,ofs,v2,m'.
803      eval_lvalue ge e m a1 pcl loc ofs ->
804      eval_expr ge e m a2 v2 ->
805      store_value_of_type (typeof a1) m pcl loc ofs v2 = Some ? m' ->
806      step ge (State f (Sassign a1 a2) k e m)
807           E0 (State f Sskip k e m')
808
809  | step_call_none:   ∀f,a,al,k,e,m,vf,vargs,fd.
810      eval_expr ge e m a vf ->
811      eval_exprlist ge e m al vargs ->
812      find_funct ?? ge vf = Some ? fd ->
813      type_of_fundef fd = typeof a ->
814      step ge (State f (Scall (None ?) a al) k e m)
815           E0 (Callstate fd vargs (Kcall (None ?) f e k) m)
816
817  | step_call_some:   ∀f,lhs,a,al,k,e,m,pcl,loc,ofs,vf,vargs,fd.
818      eval_lvalue ge e m lhs pcl loc ofs ->
819      eval_expr ge e m a vf ->
820      eval_exprlist ge e m al vargs ->
821      find_funct ?? ge vf = Some ? fd ->
822      type_of_fundef fd = typeof a ->
823      step ge (State f (Scall (Some ? lhs) a al) k e m)
824           E0 (Callstate fd vargs (Kcall (Some ? 〈〈〈pcl, loc〉, ofs〉, typeof lhs〉) f e k) m)
825
826  | step_seq:  ∀f,s1,s2,k,e,m.
827      step ge (State f (Ssequence s1 s2) k e m)
828           E0 (State f s1 (Kseq s2 k) e m)
829  | step_skip_seq: ∀f,s,k,e,m.
830      step ge (State f Sskip (Kseq s k) e m)
831           E0 (State f s k e m)
832  | step_continue_seq: ∀f,s,k,e,m.
833      step ge (State f Scontinue (Kseq s k) e m)
834           E0 (State f Scontinue k e m)
835  | step_break_seq: ∀f,s,k,e,m.
836      step ge (State f Sbreak (Kseq s k) e m)
837           E0 (State f Sbreak k e m)
838
839  | step_ifthenelse_true:  ∀f,a,s1,s2,k,e,m,v1.
840      eval_expr ge e m a v1 ->
841      is_true v1 (typeof a) ->
842      step ge (State f (Sifthenelse a s1 s2) k e m)
843           E0 (State f s1 k e m)
844  | step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1.
845      eval_expr ge e m a v1 ->
846      is_false v1 (typeof a) ->
847      step ge (State f (Sifthenelse a s1 s2) k e m)
848           E0 (State f s2 k e m)
849
850  | step_while_false: ∀f,a,s,k,e,m,v.
851      eval_expr ge e m a v ->
852      is_false v (typeof a) ->
853      step ge (State f (Swhile a s) k e m)
854           E0 (State f Sskip k e m)
855  | step_while_true: ∀f,a,s,k,e,m,v.
856      eval_expr ge e m a v ->
857      is_true v (typeof a) ->
858      step ge (State f (Swhile a s) k e m)
859           E0 (State f s (Kwhile a s k) e m)
860  | step_skip_or_continue_while: ∀f,x,a,s,k,e,m.
861      x = Sskip ∨ x = Scontinue ->
862      step ge (State f x (Kwhile a s k) e m)
863           E0 (State f (Swhile a s) k e m)
864  | step_break_while: ∀f,a,s,k,e,m.
865      step ge (State f Sbreak (Kwhile a s k) e m)
866           E0 (State f Sskip k e m)
867
868  | step_dowhile: ∀f,a,s,k,e,m.
869      step ge (State f (Sdowhile a s) k e m)
870        E0 (State f s (Kdowhile a s k) e m)
871  | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v.
872      x = Sskip ∨ x = Scontinue ->
873      eval_expr ge e m a v ->
874      is_false v (typeof a) ->
875      step ge (State f x (Kdowhile a s k) e m)
876           E0 (State f Sskip k e m)
877  | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v.
878      x = Sskip ∨ x = Scontinue ->
879      eval_expr ge e m a v ->
880      is_true v (typeof a) ->
881      step ge (State f x (Kdowhile a s k) e m)
882           E0 (State f (Sdowhile a s) k e m)
883  | step_break_dowhile: ∀f,a,s,k,e,m.
884      step ge (State f Sbreak (Kdowhile a s k) e m)
885           E0 (State f Sskip k e m)
886
887  | step_for_start: ∀f,a1,a2,a3,s,k,e,m.
888      a1 ≠ Sskip ->
889      step ge (State f (Sfor a1 a2 a3 s) k e m)
890           E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
891  | step_for_false: ∀f,a2,a3,s,k,e,m,v.
892      eval_expr ge e m a2 v ->
893      is_false v (typeof a2) ->
894      step ge (State f (Sfor Sskip a2 a3 s) k e m)
895           E0 (State f Sskip k e m)
896  | step_for_true: ∀f,a2,a3,s,k,e,m,v.
897      eval_expr ge e m a2 v ->
898      is_true v (typeof a2) ->
899      step ge (State f (Sfor Sskip a2 a3 s) k e m)
900           E0 (State f s (Kfor2 a2 a3 s k) e m)
901  | step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m.
902      x = Sskip ∨ x = Scontinue ->
903      step ge (State f x (Kfor2 a2 a3 s k) e m)
904           E0 (State f a3 (Kfor3 a2 a3 s k) e m)
905  | step_break_for2: ∀f,a2,a3,s,k,e,m.
906      step ge (State f Sbreak (Kfor2 a2 a3 s k) e m)
907           E0 (State f Sskip k e m)
908  | step_skip_for3: ∀f,a2,a3,s,k,e,m.
909      step ge (State f Sskip (Kfor3 a2 a3 s k) e m)
910           E0 (State f (Sfor Sskip a2 a3 s) k e m)
911
912  | step_return_0: ∀f,k,e,m.
913      fn_return f = Tvoid ->
914      step ge (State f (Sreturn (None ?)) k e m)
915           E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e)))
916  | step_return_1: ∀f,a,k,e,m,v.
917      fn_return f ≠ Tvoid ->
918      eval_expr ge e m a v ->
919      step ge (State f (Sreturn (Some ? a)) k e m)
920           E0 (Returnstate v (call_cont k) (free_list m (blocks_of_env e)))
921  | step_skip_call: ∀f,k,e,m.
922      is_call_cont k ->
923      fn_return f = Tvoid ->
924      step ge (State f Sskip k e m)
925           E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
926
927  | step_switch: ∀f,a,sl,k,e,m,n.
928      eval_expr ge e m a (Vint n) ->
929      step ge (State f (Sswitch a sl) k e m)
930           E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m)
931  | step_skip_break_switch: ∀f,x,k,e,m.
932      x = Sskip ∨ x = Sbreak ->
933      step ge (State f x (Kswitch k) e m)
934           E0 (State f Sskip k e m)
935  | step_continue_switch: ∀f,k,e,m.
936      step ge (State f Scontinue (Kswitch k) e m)
937           E0 (State f Scontinue k e m)
938
939  | step_label: ∀f,lbl,s,k,e,m.
940      step ge (State f (Slabel lbl s) k e m)
941           E0 (State f s k e m)
942
943  | step_goto: ∀f,lbl,k,e,m,s',k'.
944      find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉 ->
945      step ge (State f (Sgoto lbl) k e m)
946           E0 (State f s' k' e m)
947
948  | step_internal_function: ∀f,vargs,k,m,e,m1,m2.
949      alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 ->
950      bind_parameters e m1 (fn_params f) vargs m2 ->
951      step ge (Callstate (Internal f) vargs k m)
952           E0 (State f (fn_body f) k e m2)
953
954  | step_external_function: ∀id,targs,tres,vargs,k,m,vres,t.
955      event_match (external_function id targs tres) vargs t vres ->
956      step ge (Callstate (External id targs tres) vargs k m)
957            t (Returnstate vres k m)
958
959  | step_returnstate_0: ∀v,f,e,k,m.
960      step ge (Returnstate v (Kcall (None ?) f e k) m)
961           E0 (State f Sskip k e m)
962
963  | step_returnstate_1: ∀v,f,e,k,m,m',pcl,loc,ofs,ty.
964      store_value_of_type ty m pcl loc ofs v = Some ? m' ->
965      step ge (Returnstate v (Kcall (Some ? 〈〈〈pcl,loc〉, ofs〉, ty〉) f e k) m)
966           E0 (State f Sskip k e m').
967(*
968(** * Alternate big-step semantics *)
969
970(** ** Big-step semantics for terminating statements and functions *)
971
972(** The execution of a statement produces an ``outcome'', indicating
973  how the execution terminated: either normally or prematurely
974  through the execution of a [break], [continue] or [return] statement. *)
975
976ninductive outcome: Type :=
977   | Out_break: outcome                 (**r terminated by [break] *)
978   | Out_continue: outcome              (**r terminated by [continue] *)
979   | Out_normal: outcome                (**r terminated normally *)
980   | Out_return: option val -> outcome. (**r terminated by [return] *)
981
982ninductive out_normal_or_continue : outcome -> Prop :=
983  | Out_normal_or_continue_N: out_normal_or_continue Out_normal
984  | Out_normal_or_continue_C: out_normal_or_continue Out_continue.
985
986ninductive out_break_or_return : outcome -> outcome -> Prop :=
987  | Out_break_or_return_B: out_break_or_return Out_break Out_normal
988  | Out_break_or_return_R: ∀ov.
989      out_break_or_return (Out_return ov) (Out_return ov).
990
991Definition outcome_switch (out: outcome) : outcome :=
992  match out with
993  | Out_break => Out_normal
994  | o => o
995  end.
996
997Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop :=
998  match out, t with
999  | Out_normal, Tvoid => v = Vundef
1000  | Out_return None, Tvoid => v = Vundef
1001  | Out_return (Some v'), ty => ty <> Tvoid /\ v'=v
1002  | _, _ => False
1003  end.
1004
1005(** [exec_stmt ge e m1 s t m2 out] describes the execution of
1006  the statement [s].  [out] is the outcome for this execution.
1007  [m1] is the initial memory state, [m2] the final memory state.
1008  [t] is the trace of input/output events performed during this
1009  evaluation. *)
1010
1011ninductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop :=
1012  | exec_Sskip:   ∀e,m.
1013      exec_stmt e m Sskip
1014               E0 m Out_normal
1015  | exec_Sassign:   ∀e,m,a1,a2,loc,ofs,v2,m'.
1016      eval_lvalue e m a1 loc ofs ->
1017      eval_expr e m a2 v2 ->
1018      store_value_of_type (typeof a1) m loc ofs v2 = Some m' ->
1019      exec_stmt e m (Sassign a1 a2)
1020               E0 m' Out_normal
1021  | exec_Scall_none:   ∀e,m,a,al,vf,vargs,f,t,m',vres.
1022      eval_expr e m a vf ->
1023      eval_exprlist e m al vargs ->
1024      Genv.find_funct ge vf = Some f ->
1025      type_of_fundef f = typeof a ->
1026      eval_funcall m f vargs t m' vres ->
1027      exec_stmt e m (Scall None a al)
1028                t m' Out_normal
1029  | exec_Scall_some:   ∀e,m,lhs,a,al,loc,ofs,vf,vargs,f,t,m',vres,m''.
1030      eval_lvalue e m lhs loc ofs ->
1031      eval_expr e m a vf ->
1032      eval_exprlist e m al vargs ->
1033      Genv.find_funct ge vf = Some f ->
1034      type_of_fundef f = typeof a ->
1035      eval_funcall m f vargs t m' vres ->
1036      store_value_of_type (typeof lhs) m' loc ofs vres = Some m'' ->
1037      exec_stmt e m (Scall (Some lhs) a al)
1038                t m'' Out_normal
1039  | exec_Sseq_1:   ∀e,m,s1,s2,t1,m1,t2,m2,out.
1040      exec_stmt e m s1 t1 m1 Out_normal ->
1041      exec_stmt e m1 s2 t2 m2 out ->
1042      exec_stmt e m (Ssequence s1 s2)
1043                (t1 ** t2) m2 out
1044  | exec_Sseq_2:   ∀e,m,s1,s2,t1,m1,out.
1045      exec_stmt e m s1 t1 m1 out ->
1046      out <> Out_normal ->
1047      exec_stmt e m (Ssequence s1 s2)
1048                t1 m1 out
1049  | exec_Sifthenelse_true: ∀e,m,a,s1,s2,v1,t,m',out.
1050      eval_expr e m a v1 ->
1051      is_true v1 (typeof a) ->
1052      exec_stmt e m s1 t m' out ->
1053      exec_stmt e m (Sifthenelse a s1 s2)
1054                t m' out
1055  | exec_Sifthenelse_false: ∀e,m,a,s1,s2,v1,t,m',out.
1056      eval_expr e m a v1 ->
1057      is_false v1 (typeof a) ->
1058      exec_stmt e m s2 t m' out ->
1059      exec_stmt e m (Sifthenelse a s1 s2)
1060                t m' out
1061  | exec_Sreturn_none:   ∀e,m.
1062      exec_stmt e m (Sreturn None)
1063               E0 m (Out_return None)
1064  | exec_Sreturn_some: ∀e,m,a,v.
1065      eval_expr e m a v ->
1066      exec_stmt e m (Sreturn (Some a))
1067               E0 m (Out_return (Some v))
1068  | exec_Sbreak:   ∀e,m.
1069      exec_stmt e m Sbreak
1070               E0 m Out_break
1071  | exec_Scontinue:   ∀e,m.
1072      exec_stmt e m Scontinue
1073               E0 m Out_continue
1074  | exec_Swhile_false: ∀e,m,a,s,v.
1075      eval_expr e m a v ->
1076      is_false v (typeof a) ->
1077      exec_stmt e m (Swhile a s)
1078               E0 m Out_normal
1079  | exec_Swhile_stop: ∀e,m,a,v,s,t,m',out',out.
1080      eval_expr e m a v ->
1081      is_true v (typeof a) ->
1082      exec_stmt e m s t m' out' ->
1083      out_break_or_return out' out ->
1084      exec_stmt e m (Swhile a s)
1085                t m' out
1086  | exec_Swhile_loop: ∀e,m,a,s,v,t1,m1,out1,t2,m2,out.
1087      eval_expr e m a v ->
1088      is_true v (typeof a) ->
1089      exec_stmt e m s t1 m1 out1 ->
1090      out_normal_or_continue out1 ->
1091      exec_stmt e m1 (Swhile a s) t2 m2 out ->
1092      exec_stmt e m (Swhile a s)
1093                (t1 ** t2) m2 out
1094  | exec_Sdowhile_false: ∀e,m,s,a,t,m1,out1,v.
1095      exec_stmt e m s t m1 out1 ->
1096      out_normal_or_continue out1 ->
1097      eval_expr e m1 a v ->
1098      is_false v (typeof a) ->
1099      exec_stmt e m (Sdowhile a s)
1100                t m1 Out_normal
1101  | exec_Sdowhile_stop: ∀e,m,s,a,t,m1,out1,out.
1102      exec_stmt e m s t m1 out1 ->
1103      out_break_or_return out1 out ->
1104      exec_stmt e m (Sdowhile a s)
1105                t m1 out
1106  | exec_Sdowhile_loop: ∀e,m,s,a,m1,m2,t1,t2,out,out1,v.
1107      exec_stmt e m s t1 m1 out1 ->
1108      out_normal_or_continue out1 ->
1109      eval_expr e m1 a v ->
1110      is_true v (typeof a) ->
1111      exec_stmt e m1 (Sdowhile a s) t2 m2 out ->
1112      exec_stmt e m (Sdowhile a s)
1113                (t1 ** t2) m2 out
1114  | exec_Sfor_start: ∀e,m,s,a1,a2,a3,out,m1,m2,t1,t2.
1115      a1 <> Sskip ->
1116      exec_stmt e m a1 t1 m1 Out_normal ->
1117      exec_stmt e m1 (Sfor Sskip a2 a3 s) t2 m2 out ->
1118      exec_stmt e m (Sfor a1 a2 a3 s)
1119                (t1 ** t2) m2 out
1120  | exec_Sfor_false: ∀e,m,s,a2,a3,v.
1121      eval_expr e m a2 v ->
1122      is_false v (typeof a2) ->
1123      exec_stmt e m (Sfor Sskip a2 a3 s)
1124               E0 m Out_normal
1125  | exec_Sfor_stop: ∀e,m,s,a2,a3,v,m1,t,out1,out.
1126      eval_expr e m a2 v ->
1127      is_true v (typeof a2) ->
1128      exec_stmt e m s t m1 out1 ->
1129      out_break_or_return out1 out ->
1130      exec_stmt e m (Sfor Sskip a2 a3 s)
1131                t m1 out
1132  | exec_Sfor_loop: ∀e,m,s,a2,a3,v,m1,m2,m3,t1,t2,t3,out1,out.
1133      eval_expr e m a2 v ->
1134      is_true v (typeof a2) ->
1135      exec_stmt e m s t1 m1 out1 ->
1136      out_normal_or_continue out1 ->
1137      exec_stmt e m1 a3 t2 m2 Out_normal ->
1138      exec_stmt e m2 (Sfor Sskip a2 a3 s) t3 m3 out ->
1139      exec_stmt e m (Sfor Sskip a2 a3 s)
1140                (t1 ** t2 ** t3) m3 out
1141  | exec_Sswitch:   ∀e,m,a,t,n,sl,m1,out.
1142      eval_expr e m a (Vint n) ->
1143      exec_stmt e m (seq_of_labeled_statement (select_switch n sl)) t m1 out ->
1144      exec_stmt e m (Sswitch a sl)
1145                t m1 (outcome_switch out)
1146
1147(** [eval_funcall m1 fd args t m2 res] describes the invocation of
1148  function [fd] with arguments [args].  [res] is the value returned
1149  by the call.  *)
1150
1151with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
1152  | eval_funcall_internal: ∀m,f,vargs,t,e,m1,m2,m3,out,vres.
1153      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
1154      bind_parameters e m1 f.(fn_params) vargs m2 ->
1155      exec_stmt e m2 f.(fn_body) t m3 out ->
1156      outcome_result_value out f.(fn_return) vres ->
1157      eval_funcall m (Internal f) vargs t (Mem.free_list m3 (blocks_of_env e)) vres
1158  | eval_funcall_external: ∀m,id,targs,tres,vargs,t,vres.
1159      event_match (external_function id targs tres) vargs t vres ->
1160      eval_funcall m (External id targs tres) vargs t m vres.
1161
1162Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
1163  with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop.
1164
1165(** ** Big-step semantics for diverging statements and functions *)
1166
1167(** Coinductive semantics for divergence.
1168  [execinf_stmt ge e m s t] holds if the execution of statement [s]
1169  diverges, i.e. loops infinitely.  [t] is the possibly infinite
1170  trace of observable events performed during the execution. *)
1171
1172Coninductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop :=
1173  | execinf_Scall_none:   ∀e,m,a,al,vf,vargs,f,t.
1174      eval_expr e m a vf ->
1175      eval_exprlist e m al vargs ->
1176      Genv.find_funct ge vf = Some f ->
1177      type_of_fundef f = typeof a ->
1178      evalinf_funcall m f vargs t ->
1179      execinf_stmt e m (Scall None a al) t
1180  | execinf_Scall_some:   ∀e,m,lhs,a,al,loc,ofs,vf,vargs,f,t.
1181      eval_lvalue e m lhs loc ofs ->
1182      eval_expr e m a vf ->
1183      eval_exprlist e m al vargs ->
1184      Genv.find_funct ge vf = Some f ->
1185      type_of_fundef f = typeof a ->
1186      evalinf_funcall m f vargs t ->
1187      execinf_stmt e m (Scall (Some lhs) a al) t
1188  | execinf_Sseq_1:   ∀e,m,s1,s2,t.
1189      execinf_stmt e m s1 t ->
1190      execinf_stmt e m (Ssequence s1 s2) t
1191  | execinf_Sseq_2:   ∀e,m,s1,s2,t1,m1,t2.
1192      exec_stmt e m s1 t1 m1 Out_normal ->
1193      execinf_stmt e m1 s2 t2 ->
1194      execinf_stmt e m (Ssequence s1 s2) (t1 *** t2)
1195  | execinf_Sifthenelse_true: ∀e,m,a,s1,s2,v1,t.
1196      eval_expr e m a v1 ->
1197      is_true v1 (typeof a) ->
1198      execinf_stmt e m s1 t ->
1199      execinf_stmt e m (Sifthenelse a s1 s2) t
1200  | execinf_Sifthenelse_false: ∀e,m,a,s1,s2,v1,t.
1201      eval_expr e m a v1 ->
1202      is_false v1 (typeof a) ->
1203      execinf_stmt e m s2 t ->
1204      execinf_stmt e m (Sifthenelse a s1 s2) t
1205  | execinf_Swhile_body: ∀e,m,a,v,s,t.
1206      eval_expr e m a v ->
1207      is_true v (typeof a) ->
1208      execinf_stmt e m s t ->
1209      execinf_stmt e m (Swhile a s) t
1210  | execinf_Swhile_loop: ∀e,m,a,s,v,t1,m1,out1,t2.
1211      eval_expr e m a v ->
1212      is_true v (typeof a) ->
1213      exec_stmt e m s t1 m1 out1 ->
1214      out_normal_or_continue out1 ->
1215      execinf_stmt e m1 (Swhile a s) t2 ->
1216      execinf_stmt e m (Swhile a s) (t1 *** t2)
1217  | execinf_Sdowhile_body: ∀e,m,s,a,t.
1218      execinf_stmt e m s t ->
1219      execinf_stmt e m (Sdowhile a s) t
1220  | execinf_Sdowhile_loop: ∀e,m,s,a,m1,t1,t2,out1,v.
1221      exec_stmt e m s t1 m1 out1 ->
1222      out_normal_or_continue out1 ->
1223      eval_expr e m1 a v ->
1224      is_true v (typeof a) ->
1225      execinf_stmt e m1 (Sdowhile a s) t2 ->
1226      execinf_stmt e m (Sdowhile a s) (t1 *** t2)
1227  | execinf_Sfor_start_1: ∀e,m,s,a1,a2,a3,t.
1228      execinf_stmt e m a1 t ->
1229      execinf_stmt e m (Sfor a1 a2 a3 s) t
1230  | execinf_Sfor_start_2: ∀e,m,s,a1,a2,a3,m1,t1,t2.
1231      a1 <> Sskip ->
1232      exec_stmt e m a1 t1 m1 Out_normal ->
1233      execinf_stmt e m1 (Sfor Sskip a2 a3 s) t2 ->
1234      execinf_stmt e m (Sfor a1 a2 a3 s) (t1 *** t2)
1235  | execinf_Sfor_body: ∀e,m,s,a2,a3,v,t.
1236      eval_expr e m a2 v ->
1237      is_true v (typeof a2) ->
1238      execinf_stmt e m s t ->
1239      execinf_stmt e m (Sfor Sskip a2 a3 s) t
1240  | execinf_Sfor_next: ∀e,m,s,a2,a3,v,m1,t1,t2,out1.
1241      eval_expr e m a2 v ->
1242      is_true v (typeof a2) ->
1243      exec_stmt e m s t1 m1 out1 ->
1244      out_normal_or_continue out1 ->
1245      execinf_stmt e m1 a3 t2 ->
1246      execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2)
1247  | execinf_Sfor_loop: ∀e,m,s,a2,a3,v,m1,m2,t1,t2,t3,out1.
1248      eval_expr e m a2 v ->
1249      is_true v (typeof a2) ->
1250      exec_stmt e m s t1 m1 out1 ->
1251      out_normal_or_continue out1 ->
1252      exec_stmt e m1 a3 t2 m2 Out_normal ->
1253      execinf_stmt e m2 (Sfor Sskip a2 a3 s) t3 ->
1254      execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2 *** t3)
1255  | execinf_Sswitch:   ∀e,m,a,t,n,sl.
1256      eval_expr e m a (Vint n) ->
1257      execinf_stmt e m (seq_of_labeled_statement (select_switch n sl)) t ->
1258      execinf_stmt e m (Sswitch a sl) t
1259
1260(** [evalinf_funcall ge m fd args t] holds if the invocation of function
1261    [fd] on arguments [args] diverges, with observable trace [t]. *)
1262
1263with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop :=
1264  | evalinf_funcall_internal: ∀m,f,vargs,t,e,m1,m2.
1265      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
1266      bind_parameters e m1 f.(fn_params) vargs m2 ->
1267      execinf_stmt e m2 f.(fn_body) t ->
1268      evalinf_funcall m (Internal f) vargs t.
1269
1270End SEMANTICS.
1271*)
1272(* * * Whole-program semantics *)
1273
1274(* * Execution of whole programs are described as sequences of transitions
1275  from an initial state to a final state.  An initial state is a [Callstate]
1276  corresponding to the invocation of the ``main'' function of the program
1277  without arguments and with an empty continuation. *)
1278
1279ninductive initial_state (p: program): state -> Prop :=
1280  | initial_state_intro: ∀b,f.
1281      let ge := globalenv Genv ?? p in
1282      let m0 := init_mem Genv ?? p in
1283      find_symbol ?? ge (prog_main ?? p) = Some ? b ->
1284      find_funct_ptr ?? ge b = Some ? f ->
1285      initial_state p (Callstate f (nil ?) Kstop m0).
1286
1287(* * A final state is a [Returnstate] with an empty continuation. *)
1288
1289ninductive final_state: state -> int -> Prop :=
1290  | final_state_intro: ∀r,m.
1291      final_state (Returnstate (Vint r) Kstop m) r.
1292
1293(* * Execution of a whole program: [exec_program p beh]
1294  holds if the application of [p]'s main function to no arguments
1295  in the initial memory state for [p] has [beh] as observable
1296  behavior. *)
1297
1298ndefinition exec_program : program → program_behavior → Prop ≝ λp,beh.
1299  program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv ??? p) beh.
1300(*
1301(** Big-step execution of a whole program.  *)
1302
1303ninductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
1304  | bigstep_program_terminates_intro: ∀b,f,m1,t,r.
1305      let ge := Genv.globalenv p in
1306      let m0 := Genv.init_mem p in
1307      Genv.find_symbol ge p.(prog_main) = Some b ->
1308      Genv.find_funct_ptr ge b = Some f ->
1309      eval_funcall ge m0 f nil t m1 (Vint r) ->
1310      bigstep_program_terminates p t r.
1311
1312ninductive bigstep_program_diverges (p: program): traceinf -> Prop :=
1313  | bigstep_program_diverges_intro: ∀b,f,t.
1314      let ge := Genv.globalenv p in
1315      let m0 := Genv.init_mem p in
1316      Genv.find_symbol ge p.(prog_main) = Some b ->
1317      Genv.find_funct_ptr ge b = Some f ->
1318      evalinf_funcall ge m0 f nil t ->
1319      bigstep_program_diverges p t.
1320
1321(** * Implication from big-step semantics to transition semantics *)
1322
1323Section BIGSTEP_TO_TRANSITIONS.
1324
1325Variable prog: program.
1326Let ge : genv := Genv.globalenv prog.
1327
1328Definition exec_stmt_eval_funcall_ind
1329  (PS: env -> mem -> statement -> trace -> mem -> outcome -> Prop)
1330  (PF: mem -> fundef -> list val -> trace -> mem -> val -> Prop) :=
1331  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 =>
1332  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)
1333       (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).
1334
1335ninductive outcome_state_match
1336       (e: env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop :=
1337  | osm_normal:
1338      outcome_state_match e m f k Out_normal (State f Sskip k e m)
1339  | osm_break:
1340      outcome_state_match e m f k Out_break (State f Sbreak k e m)
1341  | osm_continue:
1342      outcome_state_match e m f k Out_continue (State f Scontinue k e m)
1343  | osm_return_none: ∀k'.
1344      call_cont k' = call_cont k ->
1345      outcome_state_match e m f k
1346        (Out_return None) (State f (Sreturn None) k' e m)
1347  | osm_return_some: ∀a,v,k'.
1348      call_cont k' = call_cont k ->
1349      eval_expr ge e m a v ->
1350      outcome_state_match e m f k
1351        (Out_return (Some v)) (State f (Sreturn (Some a)) k' e m).
1352
1353Lemma is_call_cont_call_cont:
1354  ∀k. is_call_cont k -> call_cont k = k.
1355Proof.
1356  destruct k; simpl; intros; contradiction || auto.
1357Qed.
1358
1359Lemma exec_stmt_eval_funcall_steps:
1360  (∀e,m,s,t,m',out.
1361   exec_stmt ge e m s t m' out ->
1362   ∀f,k. exists S,
1363   star step ge (State f s k e m) t S
1364   /\ outcome_state_match e m' f k out S)
1365/\
1366  (∀m,fd,args,t,m',res.
1367   eval_funcall ge m fd args t m' res ->
1368   ∀k.
1369   is_call_cont k ->
1370   star step ge (Callstate fd args k m) t (Returnstate res k m')).
1371Proof.
1372  apply exec_stmt_eval_funcall_ind; intros.
1373
1374(* skip *)
1375  econstructor; split. apply star_refl. constructor.
1376
1377(* assign *)
1378  econstructor; split. apply star_one. econstructor; eauto. constructor.
1379
1380(* call none *)
1381  econstructor; split.
1382  eapply star_left. econstructor; eauto.
1383  eapply star_right. apply H4. simpl; auto. econstructor. reflexivity. traceEq.
1384  constructor.
1385
1386(* call some *)
1387  econstructor; split.
1388  eapply star_left. econstructor; eauto.
1389  eapply star_right. apply H5. simpl; auto. econstructor; eauto. reflexivity. traceEq.
1390  constructor.
1391
1392(* sequence 2 *)
1393  destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. inv B1.
1394  destruct (H2 f k) as [S2 [A2 B2]].
1395  econstructor; split.
1396  eapply star_left. econstructor.
1397  eapply star_trans. eexact A1.
1398  eapply star_left. constructor. eexact A2.
1399  reflexivity. reflexivity. traceEq.
1400  auto.
1401
1402(* sequence 1 *)
1403  destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]].
1404  set (S2 :=
1405    match out with
1406    | Out_break => State f Sbreak k e m1
1407    | Out_continue => State f Scontinue k e m1
1408    | _ => S1
1409    end).
1410  exists S2; split.
1411  eapply star_left. econstructor.
1412  eapply star_trans. eexact A1.
1413  unfold S2; inv B1.
1414    congruence.
1415    apply star_one. apply step_break_seq.
1416    apply star_one. apply step_continue_seq.
1417    apply star_refl.
1418    apply star_refl.
1419  reflexivity. traceEq.
1420  unfold S2; inv B1; congruence || econstructor; eauto.
1421
1422(* ifthenelse true *)
1423  destruct (H2 f k) as [S1 [A1 B1]].
1424  exists S1; split.
1425  eapply star_left. eapply step_ifthenelse_true; eauto. eexact A1. traceEq.
1426  auto.
1427
1428(* ifthenelse false *)
1429  destruct (H2 f k) as [S1 [A1 B1]].
1430  exists S1; split.
1431  eapply star_left. eapply step_ifthenelse_false; eauto. eexact A1. traceEq.
1432  auto.
1433
1434(* return none *)
1435  econstructor; split. apply star_refl. constructor. auto.
1436
1437(* return some *)
1438  econstructor; split. apply star_refl. econstructor; eauto.
1439
1440(* break *)
1441  econstructor; split. apply star_refl. constructor.
1442
1443(* continue *)
1444  econstructor; split. apply star_refl. constructor.
1445
1446(* while false *)
1447  econstructor; split.
1448  apply star_one. eapply step_while_false; eauto.
1449  constructor.
1450
1451(* while stop *)
1452  destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]].
1453  set (S2 :=
1454    match out' with
1455    | Out_break => State f Sskip k e m'
1456    | _ => S1
1457    end).
1458  exists S2; split.
1459  eapply star_left. eapply step_while_true; eauto.
1460  eapply star_trans. eexact A1.
1461  unfold S2. inversion H3; subst.
1462  inv B1. apply star_one. constructor.   
1463  apply star_refl.
1464  reflexivity. traceEq.
1465  unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto.
1466
1467(* while loop *)
1468  destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]].
1469  destruct (H5 f k) as [S2 [A2 B2]].
1470  exists S2; split.
1471  eapply star_left. eapply step_while_true; eauto.
1472  eapply star_trans. eexact A1.
1473  eapply star_left.
1474  inv H3; inv B1; apply step_skip_or_continue_while; auto.
1475  eexact A2.
1476  reflexivity. reflexivity. traceEq.
1477  auto.
1478
1479(* dowhile false *)
1480  destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
1481  exists (State f Sskip k e m1); split.
1482  eapply star_left. constructor.
1483  eapply star_right. eexact A1.
1484  inv H1; inv B1; eapply step_skip_or_continue_dowhile_false; eauto.
1485  reflexivity. traceEq.
1486  constructor.
1487
1488(* dowhile stop *)
1489  destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
1490  set (S2 :=
1491    match out1 with
1492    | Out_break => State f Sskip k e m1
1493    | _ => S1
1494    end).
1495  exists S2; split.
1496  eapply star_left. apply step_dowhile.
1497  eapply star_trans. eexact A1.
1498  unfold S2. inversion H1; subst.
1499  inv B1. apply star_one. constructor.
1500  apply star_refl.
1501  reflexivity. traceEq.
1502  unfold S2. inversion H1; subst. constructor. inv B1; econstructor; eauto.
1503
1504(* dowhile loop *)
1505  destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]].
1506  destruct (H5 f k) as [S2 [A2 B2]].
1507  exists S2; split.
1508  eapply star_left. apply step_dowhile.
1509  eapply star_trans. eexact A1.
1510  eapply star_left.
1511  inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto.
1512  eexact A2.
1513  reflexivity. reflexivity. traceEq.
1514  auto.
1515
1516(* for start *)
1517  destruct (H1 f (Kseq (Sfor Sskip a2 a3 s) k)) as [S1 [A1 B1]]. inv B1.
1518  destruct (H3 f k) as [S2 [A2 B2]].
1519  exists S2; split.
1520  eapply star_left. apply step_for_start; auto.   
1521  eapply star_trans. eexact A1.
1522  eapply star_left. constructor. eexact A2.
1523  reflexivity. reflexivity. traceEq.
1524  auto.
1525
1526(* for false *)
1527  econstructor; split.
1528  eapply star_one. eapply step_for_false; eauto.
1529  constructor.
1530
1531(* for stop *)
1532  destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]].
1533  set (S2 :=
1534    match out1 with
1535    | Out_break => State f Sskip k e m1
1536    | _ => S1
1537    end).
1538  exists S2; split.
1539  eapply star_left. eapply step_for_true; eauto.
1540  eapply star_trans. eexact A1.
1541  unfold S2. inversion H3; subst.
1542  inv B1. apply star_one. constructor.
1543  apply star_refl.
1544  reflexivity. traceEq.
1545  unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto.
1546
1547(* for loop *)
1548  destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]].
1549  destruct (H5 f (Kfor3 a2 a3 s k)) as [S2 [A2 B2]]. inv B2.
1550  destruct (H7 f k) as [S3 [A3 B3]].
1551  exists S3; split.
1552  eapply star_left. eapply step_for_true; eauto.
1553  eapply star_trans. eexact A1.
1554  eapply star_trans with (s2 := State f a3 (Kfor3 a2 a3 s k) e m1).
1555  inv H3; inv B1.
1556  apply star_one. constructor. auto.
1557  apply star_one. constructor. auto.
1558  eapply star_trans. eexact A2.
1559  eapply star_left. constructor.
1560  eexact A3.
1561  reflexivity. reflexivity. reflexivity. reflexivity. traceEq.
1562  auto.
1563
1564(* switch *)
1565  destruct (H1 f (Kswitch k)) as [S1 [A1 B1]].
1566  set (S2 :=
1567    match out with
1568    | Out_normal => State f Sskip k e m1
1569    | Out_break => State f Sskip k e m1
1570    | Out_continue => State f Scontinue k e m1
1571    | _ => S1
1572    end).
1573  exists S2; split.
1574  eapply star_left. eapply step_switch; eauto.
1575  eapply star_trans. eexact A1.
1576  unfold S2; inv B1.
1577    apply star_one. constructor. auto.
1578    apply star_one. constructor. auto.
1579    apply star_one. constructor.
1580    apply star_refl.
1581    apply star_refl.
1582  reflexivity. traceEq.
1583  unfold S2. inv B1; simpl; econstructor; eauto.
1584
1585(* call internal *)
1586  destruct (H2 f k) as [S1 [A1 B1]].
1587  eapply star_left. eapply step_internal_function; eauto.
1588  eapply star_right. eexact A1.
1589  inv B1; simpl in H3; try contradiction.
1590  (* Out_normal *)
1591  assert (fn_return f = Tvoid /\ vres = Vundef).
1592    destruct (fn_return f); auto || contradiction.
1593  destruct H5. subst vres. apply step_skip_call; auto.
1594  (* Out_return None *)
1595  assert (fn_return f = Tvoid /\ vres = Vundef).
1596    destruct (fn_return f); auto || contradiction.
1597  destruct H6. subst vres.
1598  rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5.
1599  apply step_return_0; auto.
1600  (* Out_return Some *)
1601  destruct H3. subst vres.
1602  rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5.
1603  eapply step_return_1; eauto.
1604  reflexivity. traceEq.
1605
1606(* call external *)
1607  apply star_one. apply step_external_function; auto.
1608Qed.
1609
1610Lemma exec_stmt_steps:
1611   ∀e,m,s,t,m',out.
1612   exec_stmt ge e m s t m' out ->
1613   ∀f,k. exists S,
1614   star step ge (State f s k e m) t S
1615   /\ outcome_state_match e m' f k out S.
1616Proof (proj1 exec_stmt_eval_funcall_steps).
1617
1618Lemma eval_funcall_steps:
1619   ∀m,fd,args,t,m',res.
1620   eval_funcall ge m fd args t m' res ->
1621   ∀k.
1622   is_call_cont k ->
1623   star step ge (Callstate fd args k m) t (Returnstate res k m').
1624Proof (proj2 exec_stmt_eval_funcall_steps).
1625
1626Definition order (x y: unit) := False.
1627
1628Lemma evalinf_funcall_forever:
1629  ∀m,fd,args,T,k.
1630  evalinf_funcall ge m fd args T ->
1631  forever_N step order ge tt (Callstate fd args k m) T.
1632Proof.
1633  cofix CIH_FUN.
1634  assert (∀e,m,s,T,f,k.
1635          execinf_stmt ge e m s T ->
1636          forever_N step order ge tt (State f s k e m) T).
1637  cofix CIH_STMT.
1638  intros. inv H.
1639
1640(* call none *)
1641  eapply forever_N_plus.
1642  apply plus_one. eapply step_call_none; eauto.
1643  apply CIH_FUN. eauto. traceEq.
1644(* call some *)
1645  eapply forever_N_plus.
1646  apply plus_one. eapply step_call_some; eauto.
1647  apply CIH_FUN. eauto. traceEq.
1648
1649(* seq 1 *)
1650  eapply forever_N_plus.
1651  apply plus_one. econstructor.
1652  apply CIH_STMT; eauto. traceEq.
1653(* seq 2 *)
1654  destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kseq s2 k)) as [S1 [A1 B1]].
1655  inv B1.
1656  eapply forever_N_plus.
1657  eapply plus_left. constructor. eapply star_trans. eexact A1.
1658  apply star_one. constructor. reflexivity. reflexivity.
1659  apply CIH_STMT; eauto. traceEq.
1660
1661(* ifthenelse true *)
1662  eapply forever_N_plus.
1663  apply plus_one. eapply step_ifthenelse_true; eauto.
1664  apply CIH_STMT; eauto. traceEq.
1665(* ifthenelse false *)
1666  eapply forever_N_plus.
1667  apply plus_one. eapply step_ifthenelse_false; eauto.
1668  apply CIH_STMT; eauto. traceEq.
1669
1670(* while body *)
1671  eapply forever_N_plus.
1672  eapply plus_one. eapply step_while_true; eauto.
1673  apply CIH_STMT; eauto. traceEq.
1674(* while loop *)
1675  destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kwhile a s0 k)) as [S1 [A1 B1]].
1676  eapply forever_N_plus with (s2 := State f (Swhile a s0) k e m1).
1677  eapply plus_left. eapply step_while_true; eauto.
1678  eapply star_right. eexact A1.
1679  inv H3; inv B1; apply step_skip_or_continue_while; auto.
1680  reflexivity. reflexivity.
1681  apply CIH_STMT; eauto. traceEq.
1682
1683(* dowhile body *)
1684  eapply forever_N_plus.
1685  eapply plus_one. eapply step_dowhile.
1686  apply CIH_STMT; eauto.
1687  traceEq.
1688
1689(* dowhile loop *)
1690  destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kdowhile a s0 k)) as [S1 [A1 B1]].
1691  eapply forever_N_plus with (s2 := State f (Sdowhile a s0) k e m1).
1692  eapply plus_left. eapply step_dowhile.
1693  eapply star_right. eexact A1.
1694  inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto.
1695  reflexivity. reflexivity.
1696  apply CIH_STMT. eauto.
1697  traceEq.
1698
1699(* for start 1 *)
1700  assert (a1 <> Sskip). red; intros; subst. inv H0.
1701  eapply forever_N_plus.
1702  eapply plus_one. apply step_for_start; auto.
1703  apply CIH_STMT; eauto.
1704  traceEq.
1705
1706(* for start 2 *)
1707  destruct (exec_stmt_steps _ _ _ _ _ _ H1 f (Kseq (Sfor Sskip a2 a3 s0) k)) as [S1 [A1 B1]].
1708  inv B1.
1709  eapply forever_N_plus.
1710  eapply plus_left. eapply step_for_start; eauto.
1711  eapply star_right. eexact A1.
1712  apply step_skip_seq.
1713  reflexivity. reflexivity.
1714  apply CIH_STMT; eauto.
1715  traceEq.
1716
1717(* for body *)
1718  eapply forever_N_plus.
1719  apply plus_one. eapply step_for_true; eauto.
1720  apply CIH_STMT; eauto.
1721  traceEq.
1722
1723(* for next *)
1724  destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]].
1725  eapply forever_N_plus.
1726  eapply plus_left. eapply step_for_true; eauto.
1727  eapply star_trans. eexact A1.
1728  apply star_one.
1729  inv H3; inv B1; apply step_skip_or_continue_for2; auto.
1730  reflexivity. reflexivity.
1731  apply CIH_STMT; eauto.
1732  traceEq.
1733
1734(* for body *)
1735  destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]].
1736  destruct (exec_stmt_steps _ _ _ _ _ _ H4 f (Kfor3 a2 a3 s0 k)) as [S2 [A2 B2]].
1737  inv B2.
1738  eapply forever_N_plus.
1739  eapply plus_left. eapply step_for_true; eauto.
1740  eapply star_trans. eexact A1.
1741  eapply star_left. inv H3; inv B1; apply step_skip_or_continue_for2; auto.
1742  eapply star_right. eexact A2.
1743  constructor.
1744  reflexivity. reflexivity. reflexivity. reflexivity. 
1745  apply CIH_STMT; eauto.
1746  traceEq.
1747
1748(* switch *)
1749  eapply forever_N_plus.
1750  eapply plus_one. eapply step_switch; eauto.
1751  apply CIH_STMT; eauto.
1752  traceEq.
1753
1754(* call internal *)
1755  intros. inv H0.
1756  eapply forever_N_plus.
1757  eapply plus_one. econstructor; eauto.
1758  apply H; eauto.
1759  traceEq.
1760Qed.
1761
1762Theorem bigstep_program_terminates_exec:
1763  ∀t,r. bigstep_program_terminates prog t r -> exec_program prog (Terminates t r).
1764Proof.
1765  intros. inv H. unfold ge0, m0 in *.
1766  econstructor.
1767  econstructor. eauto. eauto.
1768  apply eval_funcall_steps. eauto. red; auto.
1769  econstructor.
1770Qed.
1771
1772Theorem bigstep_program_diverges_exec:
1773  ∀T. bigstep_program_diverges prog T ->
1774  exec_program prog (Reacts T) \/
1775  exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T.
1776Proof.
1777  intros. inv H.
1778  set (st := Callstate f nil Kstop m0).
1779  assert (forever step ge0 st T).
1780    eapply forever_N_forever with (order := order).
1781    red; intros. constructor; intros. red in H. elim H.
1782    eapply evalinf_funcall_forever; eauto.
1783  destruct (forever_silent_or_reactive _ _ _ _ _ _ H)
1784  as [A | [t [s' [T' [B [C D]]]]]].
1785  left. econstructor. econstructor. eauto. eauto. auto.
1786  right. exists t. split.
1787  econstructor. econstructor; eauto. eauto. auto.
1788  subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor.
1789Qed.
1790
1791End BIGSTEP_TO_TRANSITIONS.
1792
1793
1794
1795*)
1796
1797 
Note: See TracBrowser for help on using the repository browser.