source: src/Clight/Csem.ma @ 725

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

Do some light manual disambiguation to make Clight examples go through more
easily.

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