source: src/Clight/Csem.ma @ 1058

Last change on this file since 1058 was 1058, checked in by campbell, 8 years ago

Evict CompCert? Maps interface in favour of BitVectorTries?.

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