source: src/Clight/Csem.ma @ 961

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

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

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