source: Deliverables/D3.1/C-semantics/Csem.ma @ 496

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

First pass at moving regions to block type.

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