source: src/Clight/Csem.ma @ 2896

Last change on this file since 2896 was 2822, checked in by garnier, 7 years ago

A consitent proof state for Clight to Cminor, with some progress (and some temporary regressions)

File size: 53.7 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * Dynamic semantics for the Clight language *)
17
18(*include "Coqlib.ma".*)
19(*include "Errors.ma".*)
20(*include "Integers.ma".*)
21(*include "Floats.ma".*)
22(*include "Values.ma".*)
23(*include "AST.ma".*)
24(*include "Mem.ma".*)
25include "common/Globalenvs.ma".
26include "Clight/Csyntax.ma".
27(*include "Events.ma".*)
28include "common/Smallstep.ma".
29include "Clight/ClassifyOp.ma".
30
31(* * * Semantics of type-dependent operations *)
32
33(* * Interpretation of values as truth values.
34  Non-zero integers, non-zero floats and non-null pointers are
35  considered as true.  The integer zero (which also represents
36  the null pointer) and the float 0.0 are false. *)
37
38inductive is_false: val → type → Prop ≝
39  | is_false_int: ∀sz,sg.
40      is_false (Vint sz (zero ?)) (Tint sz sg)
41  | is_false_pointer: ∀t.
42      is_false Vnull (Tpointer t).
43
44inductive is_true: val → type → Prop ≝
45  | is_true_int_int: ∀sz,sg,n.
46      n ≠ (zero ?) →
47      is_true (Vint sz n) (Tint sz sg)
48  | is_true_pointer_pointer: ∀ptr,t.
49      is_true (Vptr ptr) (Tpointer t).
50
51inductive bool_of_val : val → type → val → Prop ≝
52  | bool_of_val_true: ∀v,ty.
53         is_true v ty →
54         bool_of_val v ty Vtrue
55  | bool_of_val_false: ∀v,ty.
56        is_false v ty →
57        bool_of_val v ty Vfalse.
58
59(* * The following [sem_] functions compute the result of an operator
60  application.  Since operators are overloaded, the result depends
61  both on the static types of the arguments and on their run-time values.
62  Unlike in C, automatic conversions between integers and floats
63  are not performed.  For instance, [e1 + e2] is undefined if [e1]
64  is a float and [e2] an integer.  The Clight producer must have explicitly
65  promoted [e2] to a float. *)
66
67let rec sem_neg (v: val) (ty: type) : option val ≝
68  match ty with
69  [ Tint sz _ ⇒
70      match v with
71      [ Vint sz' n ⇒ if eq_intsize sz sz'
72                     then Some ? (Vint ? (two_complement_negation ? n))
73                     else None ?
74      | _ ⇒ None ?
75      ]
76  | _ ⇒ None ?
77  ].
78
79let rec sem_notint (v: val) : option val ≝
80  match v with
81  [ Vint sz n ⇒ Some ? (Vint ? (exclusive_disjunction_bv ? n (mone ?))) (* XXX *)
82  | _ ⇒ None ?
83  ].
84
85let rec sem_notbool (v: val) (ty: type) : option val ≝
86  match ty with
87  [ Tint sz _ ⇒
88      match v with
89      [ Vint sz' n ⇒ if eq_intsize sz sz'
90                     then Some ? (of_bool (eq_bv ? n (zero ?)))
91                     else None ?
92      | _ ⇒ None ?
93      ]
94  | Tpointer _ ⇒
95      match v with
96      [ Vptr _ ⇒ Some ? Vfalse
97      | Vnull ⇒ Some ? Vtrue
98      | _ ⇒ None ?
99      ]
100  | _ ⇒ None ?
101  ].
102
103let rec sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
104  match classify_add t1 t2 with
105  [ add_case_ii _ _ ⇒                       (**r integer addition *)
106      match v1 with
107      [ Vint sz1 n1 ⇒ match v2 with
108        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
109                        (λn1. Some ? (Vint ? (addition_n ? n1 n2))) (None ?)
110        | _ ⇒ None ? ]
111      | _ ⇒ None ? ]
112  | add_case_pi _ ty _ sg ⇒                    (**r pointer plus integer *)
113      match v1 with
114      [ Vptr ptr1 ⇒ match v2 with
115        [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) sg n2))
116        | _ ⇒ None ? ]
117      | Vnull ⇒ match v2 with
118        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ?
119        | _ ⇒ None ? ]
120      | _ ⇒ None ? ]
121  | add_case_ip _ _ sg ty ⇒                    (**r integer plus pointer *)
122      match v1 with
123      [ Vint sz1 n1 ⇒ match v2 with
124        [ Vptr ptr2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr2 (sizeof ty) sg n1))
125        | Vnull ⇒ if eq_bv ? n1 (zero ?) then Some ? Vnull else None ?
126        | _ ⇒ None ? ]
127      | _ ⇒ None ? ]
128  | add_default _ _ ⇒ None ?
129].
130
131(* Ilias, 16 jan 2013: semantics of pointer/pointer subtraction slightly changed. Matched in toCminor.ma. *)
132let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) (target:type) : option val ≝
133  match classify_sub t1 t2 with
134  [ sub_case_ii _ _ ⇒                (**r integer subtraction *)
135      match v1 with
136      [ Vint sz1 n1 ⇒ match v2 with
137        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
138                        (λn1.Some ? (Vint sz2 (subtraction ? n1 n2))) (None ?)
139        | _ ⇒ None ? ]
140      | _ ⇒ None ? ]
141  | sub_case_pi _ ty _ sg ⇒             (**r pointer minus integer *)
142      match v1 with
143      [ Vptr ptr1 ⇒ match v2 with
144        [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer_n ? ptr1 (sizeof ty) sg n2))
145        | _ ⇒ None ? ]
146      | Vnull ⇒ match v2 with
147        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ?
148        | _ ⇒ None ? ]
149      | _ ⇒ None ? ]
150  | sub_case_pp _ _ ty _ ⇒             (**r pointer minus pointer *)
151      match v1 with
152      [ Vptr ptr1 ⇒
153        match v2 with
154        [ Vptr ptr2 ⇒
155          if eq_block (pblock ptr1) (pblock ptr2) then
156            if eqb (sizeof ty) 0 then None ?
157            else match target with
158                 [ Tint tsz tsg ⇒
159                   match division_u ? (sub_offset ? (poff ptr1) (poff ptr2)) (repr (sizeof ty)) with
160                   [ None ⇒ None ?
161                   | Some v ⇒
162                     Some ? (Vint tsz (zero_ext ?? v))
163                     (*Some ? (Vint tsz v)  XXX choose size from result type? *)
164                   ]
165                 | _ ⇒ None ? ]
166          else None ?
167        | _ ⇒ None ? ]
168      | Vnull ⇒
169        match v2 with
170        [ Vnull ⇒
171          match target with
172          [ Tint tsz tsg ⇒
173            Some ? (Vint tsz (*XXX*) (zero ?))
174          | _ ⇒ None ? ]
175        | _ ⇒ None ? ]
176      | _ ⇒ None ? ]
177  | sub_default _ _ ⇒ None ?
178  ].
179
180
181let rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
182 match classify_aop t1 t2 with
183  [ aop_case_ii _ _ ⇒
184      match v1 with
185      [ Vint sz1 n1 ⇒ match v2 with
186          [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
187                          (λn1. Some ? (Vint sz2 (short_multiplication ? n1 n2))) (None ?)
188        | _ ⇒ None ? ]
189      | _ ⇒ None ? ]
190  | aop_default _ _ ⇒
191      None ?
192  ].
193
194let rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
195  match classify_aop t1 t2 with
196  [ aop_case_ii _ sg ⇒
197      match v1 with
198       [ Vint sz1 n1 ⇒ match v2 with
199         [ Vint sz2 n2 ⇒
200           match sg with
201           [ Signed ⇒  intsize_eq_elim ? sz1 sz2 ? n1
202                         (λn1. option_map … (Vint ?) (division_s ? n1 n2)) (None ?)
203           | Unsigned ⇒  intsize_eq_elim ? sz1 sz2 ? n1
204                         (λn1. option_map … (Vint ?) (division_u ? n1 n2)) (None ?)
205           ]
206         | _ ⇒ None ? ]
207      | _ ⇒ None ? ]
208  | aop_default _ _ ⇒
209      None ?
210  ].
211
212let rec sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
213  match classify_aop t1 t2 with
214  [ aop_case_ii sz sg ⇒
215      match v1 with
216      [ Vint sz1 n1 ⇒ match v2 with
217        [ Vint sz2 n2 ⇒
218          match sg with
219          [ Unsigned ⇒ intsize_eq_elim ? sz1 sz2 ? n1
220                        (λn1. option_map … (Vint ?) (modulus_u ? n1 n2)) (None ?)
221          | Signed ⇒ intsize_eq_elim ? sz1 sz2 ? n1
222                      (λn1. option_map … (Vint ?) (modulus_s ? n1 n2)) (None ?)
223          ]
224        | _ ⇒ None ? ]
225      | _ ⇒ None ? ]
226  | _ ⇒
227      None ?
228  ].
229
230let rec sem_and (v1,v2: val) : option val ≝
231  match v1 with
232  [ Vint sz1 n1 ⇒ match v2 with
233    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
234                    (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2))) (None ?)
235    | _ ⇒ None ? ]
236  | _ ⇒ None ?
237  ].
238
239let rec sem_or (v1,v2: val) : option val ≝
240  match v1 with
241  [ Vint sz1 n1 ⇒ match v2 with
242    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
243                    (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2))) (None ?)
244    | _ ⇒ None ? ]
245  | _ ⇒ None ?
246  ].
247
248let rec sem_xor (v1,v2: val) : option val ≝
249  match v1 with
250  [ Vint sz1 n1 ⇒ match v2 with
251    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
252                    (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2))) (None ?)
253    | _ ⇒ None ? ]
254  | _ ⇒ None ?
255  ].
256
257let rec sem_shl (v1,v2: val): option val ≝
258  match v1 with
259  [ Vint sz1 n1 ⇒ match v2 with
260    [ Vint sz2 n2 ⇒
261        if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
262        then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false))
263        else None ?
264    | _ ⇒ None ? ]
265  | _ ⇒ None ? ].
266
267let rec sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val ≝
268  match classify_aop t1 t2 with
269  [ aop_case_ii _ sg ⇒
270      match v1 with
271      [ Vint sz1 n1 ⇒ match v2 with
272        [ Vint sz2 n2 ⇒
273          match sg with
274          [ Unsigned ⇒
275            if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
276            then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 false))
277            else None ?
278          | Signed ⇒
279            if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
280            then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
281            else None ?
282          ]
283        | _ ⇒ None ? ]
284      | _ ⇒ None ? ]
285   | _ ⇒
286      None ?
287   ].
288
289let rec sem_cmp_mismatch (c: comparison): option val ≝
290  match c with
291  [ Ceq ⇒  Some ? Vfalse
292  | Cne ⇒  Some ? Vtrue
293  | _   ⇒ None ?
294  ].
295
296let rec sem_cmp_match (c: comparison): option val ≝
297  match c with
298  [ Ceq ⇒  Some ? Vtrue
299  | Cne ⇒  Some ? Vfalse
300  | _   ⇒ None ?
301  ].
302
303let rec sem_cmp (c:comparison)
304                  (v1: val) (t1: type) (v2: val) (t2: type)
305                  (m: mem) on m: option val ≝
306  match classify_cmp t1 t2 with
307  [ cmp_case_ii _ sg ⇒
308      match v1 with
309      [ Vint sz1 n1 ⇒ match v2 with
310         [ Vint sz2 n2 ⇒
311           match sg with
312           [ Unsigned ⇒ intsize_eq_elim ? sz1 sz2 ? n1
313                        (λn1. Some ? (of_bool (cmpu_int ? c n1 n2))) (None ?)
314           | Signed ⇒ intsize_eq_elim ? sz1 sz2 ? n1
315                       (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) (None ?)
316           ]
317         | _ ⇒ None ?
318         ]
319      | _ ⇒ None ?     
320      ]
321  | cmp_case_pp _ _ ⇒
322      match v1 with
323      [ Vptr ptr1 ⇒
324        match v2 with
325        [ Vptr ptr2 ⇒
326          if (valid_pointer m ptr1 ∧ valid_pointer m ptr2)
327          then
328            if eq_block (pblock ptr1) (pblock ptr2)
329            then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
330            else sem_cmp_mismatch c
331          else None ?
332        | Vnull ⇒ sem_cmp_mismatch c
333        | _ ⇒ None ? ]
334      | Vnull ⇒
335        match v2 with
336        [ Vptr ptr2 ⇒ sem_cmp_mismatch c
337        | Vnull ⇒ sem_cmp_match c
338        | _ ⇒ None ?
339        ]
340      | _ ⇒ None ? ]
341  | cmp_default _ _ ⇒ None ?
342  ].
343
344definition cast_bool_to_target : type → option val → option val ≝
345  λty,optv.
346  match optv with
347  [ None ⇒ None ?
348  | Some v ⇒
349    match ty with
350    [ Tint sz sg ⇒
351        Some ? (zero_ext sz v)
352    | _ ⇒ None ? ]
353  ].
354
355lemma cast_bool_to_target_inversion : ∀ty,v,vres.
356  cast_bool_to_target ty (Some ? v) = Some ? vres →
357  ∃sz,sg. ty = Tint sz sg ∧ vres = zero_ext sz v.
358#ty #v #vres
359cases ty
360[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
361whd in ⊢ ((??%%) → ?);
362#Heq destruct
363%{sz} %{sg} @conj try @refl
364qed.
365
366definition sem_unary_operation
367            : unary_operation → val → type → option val ≝
368  λop,v,ty.
369  match op with
370  [ Onotbool => sem_notbool v ty
371  | Onotint => sem_notint v
372  | Oneg => sem_neg v ty
373  ].
374
375let rec sem_binary_operation
376    (op: binary_operation)
377    (v1: val) (t1: type) (v2: val) (t2:type)
378    (m: mem)
379    (ty: type): option val ≝
380  match op with
381  [ Oadd ⇒ sem_add v1 t1 v2 t2
382  | Osub ⇒ sem_sub v1 t1 v2 t2 ty
383  | Omul ⇒ sem_mul v1 t1 v2 t2
384  | Omod ⇒ sem_mod v1 t1 v2 t2
385  | Odiv ⇒ sem_div v1 t1 v2 t2
386  | Oand ⇒ sem_and v1 v2 
387  | Oor  ⇒ sem_or v1 v2
388  | Oxor ⇒ sem_xor v1 v2
389  | Oshl ⇒ sem_shl v1 v2
390  | Oshr ⇒ sem_shr v1 t1 v2 t2
391  | Oeq ⇒ cast_bool_to_target ty (sem_cmp Ceq v1 t1 v2 t2 m)
392  | One ⇒ cast_bool_to_target ty (sem_cmp Cne v1 t1 v2 t2 m)
393  | Olt ⇒ cast_bool_to_target ty (sem_cmp Clt v1 t1 v2 t2 m)
394  | Ogt ⇒ cast_bool_to_target ty (sem_cmp Cgt v1 t1 v2 t2 m)
395  | Ole ⇒ cast_bool_to_target ty (sem_cmp Cle v1 t1 v2 t2 m)
396  | Oge ⇒ cast_bool_to_target ty (sem_cmp Cge v1 t1 v2 t2 m)
397  ].
398
399(* * Semantic of casts.  [cast v1 t1 t2 v2] holds if value [v1],
400  viewed with static type [t1], can be cast to type [t2],
401  resulting in value [v2].  *)
402
403let rec cast_int_int (sz: intsize) (sg: signedness) (dstsz: intsize)  (i: BitVector (bitsize_of_intsize sz)) : BitVector (bitsize_of_intsize dstsz) ≝
404  match sg with [ Signed ⇒ sign_ext ?? i | Unsigned ⇒ zero_ext ?? i ].
405
406(* Only for full 8051 memory spaces
407inductive type_region : type → region → Prop ≝
408| type_rgn_pointer : ∀s,t. type_region (Tpointer s t) s
409| type_rgn_array : ∀s,t,n. type_region (Tarray s t n) s
410(* Is the following necessary? *)
411| type_rgn_code : ∀tys,ty. type_region (Tfunction tys ty) Code.
412*)
413
414inductive type_ptr : type → Prop ≝
415| type_pointer : ∀t. type_ptr (Tpointer t)
416| type_array : ∀t,n. type_ptr (Tarray t n)
417| type_fun : ∀tys,ty. type_ptr (Tfunction tys ty).
418
419inductive cast : mem → val → type → type → val → Prop ≝
420  | cast_ii:   ∀m,sz2,sz1,si1,si2,i.            (**r int to int  *)
421      cast m (Vint sz1 i) (Tint sz1 si1) (Tint sz2 si2)
422           (Vint sz2 (cast_int_int sz1 si1 sz2 i))
423  | cast_pp: ∀m,ty,ty',ptr.
424(*      type_region ty (ptype ptr) →
425      type_region ty' r' →
426      ∀pc':pointer_compat (pblock ptr) r'.
427      cast m (Vptr ptr) ty ty' (Vptr (mk_pointer r' (pblock ptr) pc' (poff ptr)))*)
428      type_ptr ty →
429      type_ptr ty' →
430      cast m (Vptr ptr) ty ty' (Vptr ptr)
431  | cast_ip_z: ∀m,sz,sg,ty'.
432(*     type_region ty' r →*)
433      type_ptr ty' →
434      cast m (Vint sz (zero ?)) (Tint sz sg) ty' Vnull
435  | cast_pp_z: ∀m,ty,ty'.
436(*      type_region ty r →
437      type_region ty' r' →*)
438      type_ptr ty →
439      type_ptr ty' →
440      cast m Vnull ty ty' Vnull.
441
442(* * * Operational semantics *)
443
444(* * The semantics uses two environments.  The global environment
445  maps names of functions and global variables to memory block references,
446  and function pointers to their definitions.  (See module [Globalenvs].) *)
447
448definition genv ≝ genv_t clight_fundef.
449
450(* * The local environment maps local variables to block references.
451  The current value of the variable is stored in the associated memory
452  block. *)
453
454definition env ≝ identifier_map SymbolTag block. (* map variable -> location *)
455
456definition empty_env: env ≝ (empty_map …).
457
458(* * [load_value_of_type ty m b ofs] computes the value of a datum
459  of type [ty] residing in memory [m] at block [b], offset [ofs].
460  If the type [ty] indicates an access by value, the corresponding
461  memory load is performed.  If the type [ty] indicates an access by
462  reference, the pointer [Vptr b ofs] is returned. *)
463
464let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: offset) : option val ≝
465  match access_mode ty with
466  [ By_value chunk ⇒ loadv chunk m (Vptr (mk_pointer b ofs))
467  | By_reference  ⇒ Some ? (Vptr (mk_pointer b ofs))
468(*    match pointer_compat_dec b r with
469    [ inl p ⇒ Some ? (Vptr (mk_pointer r b p ofs))
470    | inr _ ⇒ None ?
471    ]*)
472  | By_nothing _ ⇒ None ?
473  ].
474(*cases b //
475qed.*)
476
477(* * Symmetrically, [store_value_of_type ty m b ofs v] returns the
478  memory state after storing the value [v] in the datum
479  of type [ty] residing in memory [m] at block [b], offset [ofs].
480  This is allowed only if [ty] indicates an access by value. *)
481
482let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: offset) (v: val) : option mem ≝
483  match access_mode ty_dest with
484  [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer loc ofs)) v
485  | By_reference  ⇒ None ?
486  | By_nothing _ ⇒ None ?
487  ].
488(*cases loc //
489qed.*)
490
491(* * Allocation of function-local variables.
492  [alloc_variables e1 m1 vars e2 m2] allocates one memory block
493  for each variable declared in [vars], and associates the variable
494  name with this block.  [e1] and [m1] are the initial local environment
495  and memory state.  [e2] and [m2] are the final local environment
496  and memory state. *)
497
498inductive alloc_variables: env → mem →
499                            list (ident × type) →
500                            env → mem → Prop ≝
501  | alloc_variables_nil:
502      ∀e,m.
503      alloc_variables e m (nil ?) e m
504  | alloc_variables_cons:
505      ∀e,m,id,ty,vars,m1,b1,m2,e2.
506      alloc m 0 (sizeof ty) (* XData *) = 〈m1, b1〉 →
507      alloc_variables (add … e id b1) m1 vars e2 m2 →
508      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
509
510(* * Initialization of local variables that are parameters to a function.
511  [bind_parameters e m1 params args m2] stores the values [args]
512  in the memory blocks corresponding to the variables [params].
513  [m1] is the initial memory state and [m2] the final memory state. *)
514
515inductive bind_parameters: env →
516                           mem → list (ident × type) → list val →
517                           mem → Prop ≝
518  | bind_parameters_nil:
519      ∀e,m.
520      bind_parameters e m (nil ?) (nil ?) m
521  | bind_parameters_cons:
522      ∀e,m,id,ty,params,v1,vl,b,m1,m2.
523      lookup ?? e id = Some ? b →
524      store_value_of_type ty m b zero_offset v1 = Some ? m1 →
525      bind_parameters e m1 params vl m2 →
526      bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2.
527
528(* * Return the list of blocks in the codomain of [e]. *)
529
530definition blocks_of_env : env → list block ≝ λe.
531  map ?? (λx. snd ?? x) (elements ?? e).
532
533(* * Selection of the appropriate case of a [switch], given the value [n]
534  of the selector expression.  We fail if any of the cases has an integer of
535  the wrong size.  (NB: ideally, we'd change the syntax so that there is only
536  one size, but we're trying to keep the impact of changes on existing code
537  down.) *)
538
539let rec select_switch (sz:intsize) (n: BitVector (bitsize_of_intsize sz)) (sl: labeled_statements)
540                       on sl : option labeled_statements ≝
541  match sl with
542  [ LSdefault _ ⇒ Some ? sl
543  | LScase sz' c s sl' ⇒ intsize_eq_elim ? sz sz' ? n
544                         (λn. if eq_bv ? c n then Some ? sl else select_switch sz' n sl') (None ?)
545  ].
546
547(* * Turn a labeled statement into a sequence *)
548
549let rec seq_of_labeled_statement (sl: labeled_statements) : statement ≝
550  match sl with
551  [ LSdefault s ⇒ s
552  | LScase _ c s sl' ⇒ Ssequence s (seq_of_labeled_statement sl')
553  ].
554
555(*
556Section SEMANTICS.
557
558Variable ge: genv.
559
560(** ** Evaluation of expressions *)
561
562Section EXPR.
563
564Variable e: env.
565Variable m: mem.
566*)
567(* * [eval_expr ge e m a v] defines the evaluation of expression [a]
568  in r-value position.  [v] is the value of the expression.
569  [e] is the current environment and [m] is the current memory state. *)
570
571inductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝
572  | eval_Econst_int:   ∀sz,sg,i.
573      eval_expr ge e m (Expr (Econst_int sz i) (Tint sz sg)) (Vint sz i) E0
574(*
575  | eval_Econst_float:   ∀f,ty.
576      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0 *)
577  | eval_Elvalue: ∀a,ty,loc,ofs,v,tr.
578      eval_lvalue ge e m (Expr a ty) loc ofs tr →
579      load_value_of_type ty m loc ofs = Some ? v →
580      eval_expr ge e m (Expr a ty) v tr
581  | eval_Eaddrof: ∀a,ty,loc,ofs,tr.
582      eval_lvalue ge e m a loc ofs tr →
583(*      ∀pc:pointer_compat loc r.*)
584      eval_expr ge e m (Expr (Eaddrof a) (Tpointer ty)) (Vptr (mk_pointer loc ofs)) tr
585  | eval_Esizeof: ∀ty',sz,sg.
586      eval_expr ge e m (Expr (Esizeof ty') (Tint sz sg)) (Vint sz (repr ? (sizeof ty'))) E0
587  | eval_Eunop:  ∀op,a,ty,v1,v,tr.
588      eval_expr ge e m a v1 tr →
589      sem_unary_operation op v1 (typeof a) = Some ? v →
590      eval_expr ge e m (Expr (Eunop op a) ty) v tr
591  | eval_Ebinop: ∀op,a1,a2,ty,v1,v2,v,tr1,tr2.
592      eval_expr ge e m a1 v1 tr1 →
593      eval_expr ge e m a2 v2 tr2 →
594      sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m ty = Some ? v →
595      eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v (tr1⧺tr2)
596  | eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2,tr1,tr2.
597      eval_expr ge e m a1 v1 tr1 →
598      is_true v1 (typeof a1) →
599      eval_expr ge e m a2 v2 tr2 →
600      eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v2 (tr1⧺tr2)
601  | eval_Econdition_false: ∀a1,a2,a3,ty,v1,v3,tr1,tr2.
602      eval_expr ge e m a1 v1 tr1 →
603      is_false v1 (typeof a1) →
604      eval_expr ge e m a3 v3 tr2 →
605      eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3 (tr1⧺tr2)
606  | eval_Eorbool_1: ∀a1,a2,ty,v1,tr,vres.
607      eval_expr ge e m a1 v1 tr →
608      is_true v1 (typeof a1) →
609      cast_bool_to_target ty (Some ? Vtrue) = Some ? vres →
610      eval_expr ge e m (Expr (Eorbool a1 a2) ty) vres tr
611  | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2,vres.
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      cast_bool_to_target ty (Some ? v) = Some ? vres →     
617      eval_expr ge e m (Expr (Eorbool a1 a2) ty) vres (tr1⧺tr2)
618  | eval_Eandbool_1: ∀a1,a2,ty,v1,tr,vres.
619      eval_expr ge e m a1 v1 tr →
620      is_false v1 (typeof a1) →
621      cast_bool_to_target ty (Some ? Vfalse) = Some ? vres →           
622      eval_expr ge e m (Expr (Eandbool a1 a2) ty) vres tr
623  | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2,vres.
624      eval_expr ge e m a1 v1 tr1 →
625      is_true v1 (typeof a1) →
626      eval_expr ge e m a2 v2 tr2 →
627      bool_of_val v2 (typeof a2) v →
628      cast_bool_to_target ty (Some ? v) = Some ? vres →                 
629      eval_expr ge e m (Expr (Eandbool a1 a2) ty) vres (tr1⧺tr2)
630  | eval_Ecast:   ∀a,ty,ty',v1,v,tr.
631      eval_expr ge e m a v1 tr →
632      cast m v1 (typeof a) ty v →
633      eval_expr ge e m (Expr (Ecast ty a) ty') v tr
634  | eval_Ecost: ∀a,ty,v,l,tr.
635      eval_expr ge e m a v tr →
636      eval_expr ge e m (Expr (Ecost l a) ty) v ((Echarge l)⧺tr)
637
638(* * [eval_lvalue ge e m a r b ofs] defines the evaluation of expression [a]
639  in l-value position.  The result is the memory location [b, ofs]
640  that contains the value of the expression [a].  The memory location should
641  be representable in a pointer of region r. *)
642
643with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → offset → trace → Prop ≝
644  | eval_Evar_local:   ∀id,l,ty.
645      (* XXX notation? e!id*) lookup ?? e id = Some ? l →
646      eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
647  | eval_Evar_global: ∀id,l,ty.
648      (* XXX e!id *) lookup ?? e id = None ? →
649      find_symbol … ge id = Some ? l →
650      eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
651  | eval_Ederef: ∀a,ty,l,ofs,tr.
652      eval_expr ge e m a (Vptr (mk_pointer  l  ofs)) tr →
653      eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr
654    (* Aside: note that each block of memory is entirely contained within one
655       memory region; hence adding a field offset will not produce a location
656       outside of the original location's region. *)
657 | eval_Efield_struct:   ∀a,i,ty,l,ofs,id,fList,delta,tr.
658      eval_lvalue ge e m a l ofs tr →
659      typeof a = Tstruct id fList →
660      field_offset i fList = OK ? delta →
661      eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ? ofs (repr I16 delta)) tr
662 | eval_Efield_union:   ∀a,i,ty,l,ofs,id,fList,tr.
663      eval_lvalue ge e m a l ofs tr →
664      typeof a = Tunion id fList →
665      eval_lvalue ge e m (Expr (Efield a i) ty) l ofs tr.
666
667let rec eval_expr_ind (ge:genv) (e:env) (m:mem)
668  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
669  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
670(*  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) *)
671  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
672  (ead:∀a,ty,loc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty loc ofs tr H))
673  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
674  (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))
675  (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))
676  (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))
677  (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))
678  (eo1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
679  (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. 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 vres H1 H2 H3 H4 H5))
680  (ea1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
681  (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. 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 vres H1 H2 H3 H4 H5))
682  (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))
683  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
684  (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝
685  match ev with
686  [ eval_Econst_int sz sg i ⇒ eci sz sg i
687(*  | eval_Econst_float f ty ⇒ ecF f ty *)
688  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2
689  | eval_Eaddrof a ty loc ofs tr H ⇒ ead a ty loc ofs tr H
690  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
691  | 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
692  | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H2)
693  | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
694  | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a3 v3 tr2 H3)
695  | eval_Eorbool_1 a1 a2 ty v1 tr vres H1 H2 H3 ⇒ eo1 a1 a2 ty v1 tr vres H1 H2 H3 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
696  | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 (eval_expr_ind ge e m P eci 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
697  | eval_Eandbool_1 a1 a2 ty v1 tr vres H1 H2 H3 ⇒ ea1 a1 a2 ty v1 tr vres H1 H2 H3 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
698  | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 (eval_expr_ind ge e m P eci 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
699  | 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
700  | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v tr H)
701  ].
702(*
703inverter eval_expr_inv_ind for eval_expr : Prop.
704*)
705let rec eval_lvalue_ind (ge:genv) (e:env) (m:mem)
706  (P:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
707  (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H))
708  (lvg:∀id,l,ty,H1,H2. P ???? (eval_Evar_global ge e m id l ty H1 H2))
709  (lde:∀a,ty,l,ofs,tr,H. P ???? (eval_Ederef ge e m a ty l ofs tr H))
710  (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))
711  (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))
712  (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 ≝
713  match ev with
714  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
715  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
716  | eval_Ederef a ty l ofs tr H ⇒ lde a ty l ofs tr H
717  | 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)
718  | 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)
719  ].
720
721(*
722ninverter eval_lvalue_inv_ind for eval_lvalue : Prop.
723*)
724(*
725definition eval_lvalue_inv_ind :
726  ∀x1: genv.
727   ∀x2: env.
728    ∀x3: mem.
729     ∀x4: expr.
730       ∀x6: block.
731        ∀x7: offset.
732         ∀x8: trace.
733          ∀P:
734            ∀_z1430: expr.
735              ∀_z1428: block. ∀_z1427: offset. ∀_z1426: trace. Prop.
736           ∀_H1: ?.
737            ∀_H2: ?.
738             ∀_H3: ?.
739              ∀_H4: ?.
740               ∀_H5: ?.
741                ∀_Hterm: eval_lvalue x1 x2 x3 x4 x6 x7 x8.
742                 P x4 x6 x7 x8
743:=
744  (λx1:genv.
745    (λx2:env.
746      (λx3:mem.
747        (λx4:expr.
748            (λx6:block.
749              (λx7:offset.
750                (λx8:trace.
751                  (λP:∀_z1430: expr.
752                         ∀_z1428: block.
753                          ∀_z1427: offset. ∀_z1426: trace. Prop.
754                    (λH1:?.
755                      (λH2:?.
756                        (λH3:?.
757                          (λH4:?.
758                            (λH5:?.
759                              (λHterm:eval_lvalue x1 x2 x3 x4 x6 x7 x8.
760                                ((λHcut:∀z1435: eq expr x4 x4.
761                                           ∀z1433: eq block x6 x6.
762                                            ∀z1432: eq offset x7 x7.
763                                             ∀z1431: eq trace x8 x8.
764                                              P x4 x6 x7 x8.
765                                   (Hcut (refl expr x4)
766                                     (refl block x6)
767                                     (refl offset x7) (refl trace x8)))
768                                  ?))))))))))))))).
769[ @(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)
770  [ @H1 | @H2 | @H3 | @H4 | @H5 ]
771| *: skip
772] qed.
773*)
774
775let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem)
776  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
777  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
778  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
779  (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))
780  (ead:∀a,ty,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty loc ofs tr H))
781  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
782  (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))
783  (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))
784  (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))
785  (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))
786  (eo1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
787  (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. 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 vres H1 H2 H3 H4 H5))
788  (ea1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
789  (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. 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 vres H1 H2 H3 H4 H5))
790  (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))
791  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
792  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
793  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
794  (lde:∀a,ty,l,ofs,tr,H. P a (Vptr (mk_pointer l ofs)) tr H → Q ???? (eval_Ederef ge e m a ty l ofs tr H))
795  (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))
796  (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))
797 
798  (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝
799  match ev with
800  [ eval_Econst_int sz sg i ⇒ eci sz sg i
801  | 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 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)
802  | eval_Eaddrof a ty loc ofs tr H ⇒ ead a ty loc ofs tr H (eval_lvalue_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H)
803  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
804  | 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
805  | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H2)
806  | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
807  | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a3 v3 tr2 H3)
808  | eval_Eorbool_1 a1 a2 ty v1 tr vres H1 H2 H3 ⇒ eo1 a1 a2 ty v1 tr vres H1 H2 H3 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
809  | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 (eval_expr_ind2 ge e m P Q eci 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
810  | eval_Eandbool_1 a1 a2 ty v1 tr vres H1 H2 H3 ⇒ ea1 a1 a2 ty v1 tr vres H1 H2 H3 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
811  | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 (eval_expr_ind2 ge e m P Q eci 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
812  | 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
813  | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v tr H)
814  ]
815and eval_lvalue_ind2 (ge:genv) (e:env) (m:mem)
816  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
817  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
818  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
819  (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))
820  (ead:∀a,ty,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty loc ofs tr H))
821  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
822  (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))
823  (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))
824  (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))
825  (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))
826  (eo1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
827  (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. 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 vres H1 H2 H3 H4 H5))
828  (ea1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
829  (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. 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 vres H1 H2 H3 H4 H5))
830  (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))
831  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
832  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
833  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
834  (lde:∀a,ty,l,ofs,tr,H. P a (Vptr (mk_pointer l ofs)) tr H → Q ???? (eval_Ederef ge e m a ty l ofs tr H))
835  (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))
836  (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))
837  (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 ≝
838  match ev with
839  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
840  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
841  | eval_Ederef a ty l ofs tr H ⇒ lde a ty l ofs tr H (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr (mk_pointer l ofs)) tr H)
842  | 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
843  | 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
844  ].
845
846definition combined_expr_lvalue_ind ≝
847λge,e,m,P,Q,eci,elv,ead,esz,eun,ebi,ect,ecf,eo1,eo2,ea1,ea2,ecs,eco,lvl,lvg,lde,lfs,lfu. 
848conj ??
849  (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu)
850  (eval_lvalue_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu).
851
852(* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]
853  in l-value position.  The result is the memory location [b, ofs]
854  that contains the value of the expression [a]. *)
855
856(*
857Scheme eval_expr_ind22 := Minimality for eval_expr Sort Prop
858  with eval_lvalue_ind2 := Minimality for eval_lvalue Sort Prop.
859*)
860
861(* * [eval_exprlist ge e m al vl] evaluates a list of r-value
862  expressions [al] to their values [vl]. *)
863
864inductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝
865  | eval_Enil:
866      eval_exprlist ge e m (nil ?) (nil ?) E0
867  | eval_Econs:   ∀a,bl,v,vl,tr1,tr2.
868      eval_expr ge e m a v tr1 →
869      eval_exprlist ge e m bl vl tr2 →
870      eval_exprlist ge e m (a :: bl) (v :: vl) (tr1⧺tr2).
871
872(*End EXPR.*)
873
874(* * ** Transition semantics for statements and functions *)
875
876(* * Continuations *)
877
878inductive cont: Type[0] :=
879  | Kstop: cont
880  | Kseq: statement -> cont -> cont
881       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
882  | Kwhile: expr -> statement -> cont -> cont
883       (**r [Kwhile e s k] = after [s] in [while (e) s] *)
884  | Kdowhile: expr -> statement -> cont -> cont
885       (**r [Kdowhile e s k] = after [s] in [do s while (e)] *)
886  | Kfor2: expr -> statement -> statement -> cont -> cont
887       (**r [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *)
888  | Kfor3: expr -> statement -> statement -> cont -> cont
889       (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *)
890  | Kswitch: cont -> cont
891       (**r catches [break] statements arising out of [switch] *)
892  | Kcall: option (block × offset × type) -> (**r where to store result *)
893           function ->                       (**r calling function *)
894           env ->                            (**r local env of calling function *)
895           cont -> cont.
896
897(* * Pop continuation until a call or stop *)
898
899let rec call_cont (k: cont) : cont :=
900  match k with
901  [ Kseq s k => call_cont k
902  | Kwhile e s k => call_cont k
903  | Kdowhile e s k => call_cont k
904  | Kfor2 e2 e3 s k => call_cont k
905  | Kfor3 e2 e3 s k => call_cont k
906  | Kswitch k => call_cont k
907  | _ => k
908  ].
909
910definition is_call_cont : cont → Prop ≝ λk.
911  match k with
912  [ Kstop => True
913  | Kcall _ _ _ _ => True
914  | _ => False
915  ].
916
917(* * States *)
918
919inductive state: Type[0] :=
920  | State:
921      ∀f: function.
922      ∀s: statement.
923      ∀k: cont.
924      ∀e: env.
925      ∀m: mem.  state
926  | Callstate:
927      ∀id: ident. (* function name; used by stack instrumentation, but not the semantics *)
928      ∀fd: clight_fundef.
929      ∀args: list val.
930      ∀k: cont.
931      ∀m: mem. state
932  | Returnstate:
933      ∀res: val.
934      ∀k: cont.
935      ∀m: mem. state
936  | Finalstate:
937      ∀r: int.
938      state.
939                 
940(* * Find the statement and manufacture the continuation
941  corresponding to a label *)
942
943let rec find_label (lbl: label) (s: statement) (k: cont)
944                    on s: option (statement × cont) :=
945  match s with
946  [ Ssequence s1 s2 =>
947      match find_label lbl s1 (Kseq s2 k) with
948      [ Some sk => Some ? sk
949      | None => find_label lbl s2 k
950      ]
951  | Sifthenelse a s1 s2 =>
952      match find_label lbl s1 k with
953      [ Some sk => Some ? sk
954      | None => find_label lbl s2 k
955      ]
956  | Swhile a s1 =>
957      find_label lbl s1 (Kwhile a s1 k)
958  | Sdowhile a s1 =>
959      find_label lbl s1 (Kdowhile a s1 k)
960  | Sfor a1 a2 a3 s1 =>
961      match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 s1) k) with
962      [ Some sk => Some ? sk
963      | None =>
964          match find_label lbl s1 (Kfor2 a2 a3 s1 k) with
965          [ Some sk => Some ? sk
966          | None => find_label lbl a3 (Kfor3 a2 a3 s1 k)
967          ]
968      ]
969  | Sswitch e sl =>
970      find_label_ls lbl sl (Kswitch k)
971  | Slabel lbl' s' =>
972      match ident_eq lbl lbl' with
973      [ inl _ ⇒ Some ? 〈s', k〉
974      | inr _ ⇒ find_label lbl s' k
975      ]
976  | Scost c s' ⇒
977      find_label lbl s' k
978  | _ => None ?
979  ]
980
981and find_label_ls (lbl: label) (sl: labeled_statements) (k: cont)
982                    on sl: option (statement × cont) :=
983  match sl with
984  [ LSdefault s => find_label lbl s k
985  | LScase _ _ s sl' =>
986      match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with
987      [ Some sk => Some ? sk
988      | None => find_label_ls lbl sl' k
989      ]
990  ].
991
992(* * Transition relation *)
993
994(* Strip off outer pointer for use when comparing function types. *)
995definition fun_typeof ≝
996λe. match typeof e with
997[ Tvoid ⇒ Tvoid
998| Tint a b ⇒ Tint a b
999(*| Tfloat a ⇒ Tfloat a*)
1000| Tpointer ty ⇒ ty
1001| Tarray a b ⇒ Tarray a b
1002| Tfunction a b ⇒ Tfunction a b
1003| Tstruct a b ⇒ Tstruct a b
1004| Tunion a b ⇒ Tunion a b
1005| Tcomp_ptr a ⇒ Tcomp_ptr a
1006].
1007
1008(* XXX: note that cost labels in exprs expose a particular eval order. *)
1009
1010inductive step (ge:genv) : state → trace → state → Prop ≝
1011
1012  | step_assign:   ∀f,a1,a2,k,e,m,loc,ofs,v2,m',tr1,tr2.
1013      eval_lvalue ge e m a1 loc ofs tr1 →
1014      eval_expr ge e m a2 v2 tr2 →
1015      store_value_of_type (typeof a1) m loc ofs v2 = Some ? m' →
1016      step ge (State f (Sassign a1 a2) k e m)
1017           (tr1⧺tr2) (State f Sskip k e m')
1018
1019  | step_call_none:   ∀f,a,al,k,e,m,vf,vargs,fd,id,tr1,tr2.
1020      eval_expr ge e m a vf tr1 →
1021      eval_exprlist ge e m al vargs tr2 →
1022      find_funct_id … ge vf = Some ? 〈fd,id〉 →
1023      type_of_fundef fd = fun_typeof a →
1024      step ge (State f (Scall (None ?) a al) k e m)
1025           (tr1⧺tr2) (Callstate id fd vargs (Kcall (None ?) f e k) m)
1026
1027  | step_call_some:   ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,id,tr1,tr2,tr3.
1028      eval_lvalue ge e m lhs loc ofs tr1 →
1029      eval_expr ge e m a vf tr2 →
1030      eval_exprlist ge e m al vargs tr3 →
1031      find_funct_id … ge vf = Some ? 〈fd,id〉 →
1032      type_of_fundef fd = fun_typeof a →
1033      step ge (State f (Scall (Some ? lhs) a al) k e m)
1034           (tr1⧺tr2⧺tr3) (Callstate id fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)
1035
1036  | step_seq:  ∀f,s1,s2,k,e,m.
1037      step ge (State f (Ssequence s1 s2) k e m)
1038           E0 (State f s1 (Kseq s2 k) e m)
1039  | step_skip_seq: ∀f,s,k,e,m.
1040      step ge (State f Sskip (Kseq s k) e m)
1041           E0 (State f s k e m)
1042  | step_continue_seq: ∀f,s,k,e,m.
1043      step ge (State f Scontinue (Kseq s k) e m)
1044           E0 (State f Scontinue k e m)
1045  | step_break_seq: ∀f,s,k,e,m.
1046      step ge (State f Sbreak (Kseq s k) e m)
1047           E0 (State f Sbreak k e m)
1048
1049  | step_ifthenelse_true:  ∀f,a,s1,s2,k,e,m,v1,tr.
1050      eval_expr ge e m a v1 tr →
1051      is_true v1 (typeof a) →
1052      step ge (State f (Sifthenelse a s1 s2) k e m)
1053           tr (State f s1 k e m)
1054  | step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1,tr.
1055      eval_expr ge e m a v1 tr →
1056      is_false v1 (typeof a) →
1057      step ge (State f (Sifthenelse a s1 s2) k e m)
1058           tr (State f s2 k e m)
1059
1060  | step_while_false: ∀f,a,s,k,e,m,v,tr.
1061      eval_expr ge e m a v tr →
1062      is_false v (typeof a) →
1063      step ge (State f (Swhile a s) k e m)
1064           tr (State f Sskip k e m)
1065  | step_while_true: ∀f,a,s,k,e,m,v,tr.
1066      eval_expr ge e m a v tr →
1067      is_true v (typeof a) →
1068      step ge (State f (Swhile a s) k e m)
1069           tr (State f s (Kwhile a s k) e m)
1070  | step_skip_or_continue_while: ∀f,x,a,s,k,e,m.
1071      x = Sskip ∨ x = Scontinue →
1072      step ge (State f x (Kwhile a s k) e m)
1073           E0 (State f (Swhile a s) k e m)
1074  | step_break_while: ∀f,a,s,k,e,m.
1075      step ge (State f Sbreak (Kwhile a s k) e m)
1076           E0 (State f Sskip k e m)
1077
1078  | step_dowhile: ∀f,a,s,k,e,m.
1079      step ge (State f (Sdowhile a s) k e m)
1080        E0 (State f s (Kdowhile a s k) e m)
1081  | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v,tr.
1082      x = Sskip ∨ x = Scontinue →
1083      eval_expr ge e m a v tr →
1084      is_false v (typeof a) →
1085      step ge (State f x (Kdowhile a s k) e m)
1086           tr (State f Sskip k e m)
1087  | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v,tr.
1088      x = Sskip ∨ x = Scontinue →
1089      eval_expr ge e m a v tr →
1090      is_true v (typeof a) →
1091      step ge (State f x (Kdowhile a s k) e m)
1092           tr (State f (Sdowhile a s) k e m)
1093  | step_break_dowhile: ∀f,a,s,k,e,m.
1094      step ge (State f Sbreak (Kdowhile a s k) e m)
1095           E0 (State f Sskip k e m)
1096
1097  | step_for_start: ∀f,a1,a2,a3,s,k,e,m.
1098      a1 ≠ Sskip →
1099      step ge (State f (Sfor a1 a2 a3 s) k e m)
1100           E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
1101  | step_for_false: ∀f,a2,a3,s,k,e,m,v,tr.
1102      eval_expr ge e m a2 v tr →
1103      is_false v (typeof a2) →
1104      step ge (State f (Sfor Sskip a2 a3 s) k e m)
1105           tr (State f Sskip k e m)
1106  | step_for_true: ∀f,a2,a3,s,k,e,m,v,tr.
1107      eval_expr ge e m a2 v tr →
1108      is_true v (typeof a2) →
1109      step ge (State f (Sfor Sskip a2 a3 s) k e m)
1110           tr (State f s (Kfor2 a2 a3 s k) e m)
1111  | step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m.
1112      x = Sskip ∨ x = Scontinue →
1113      step ge (State f x (Kfor2 a2 a3 s k) e m)
1114           E0 (State f a3 (Kfor3 a2 a3 s k) e m)
1115  | step_break_for2: ∀f,a2,a3,s,k,e,m.
1116      step ge (State f Sbreak (Kfor2 a2 a3 s k) e m)
1117           E0 (State f Sskip k e m)
1118  | step_skip_for3: ∀f,a2,a3,s,k,e,m.
1119      step ge (State f Sskip (Kfor3 a2 a3 s k) e m)
1120           E0 (State f (Sfor Sskip a2 a3 s) k e m)
1121
1122  | step_return_0: ∀f,k,e,m.
1123      fn_return f = Tvoid →
1124      step ge (State f (Sreturn (None ?)) k e m)
1125           E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e)))
1126  | step_return_1: ∀f,a,k,e,m,v,tr.
1127      fn_return f ≠ Tvoid →
1128      eval_expr ge e m a v tr →
1129      step ge (State f (Sreturn (Some ? a)) k e m)
1130           tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e)))
1131  | step_skip_call: ∀f,k,e,m.
1132      is_call_cont k →
1133      fn_return f = Tvoid →
1134      step ge (State f Sskip k e m)
1135           E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
1136
1137  | step_switch: ∀f,a,sl,sl',k,e,m,sz,sg,n,tr.
1138      eval_expr ge e m a (Vint sz n) tr →
1139      typeof a = Tint sz sg →
1140      select_switch sz n sl = Some ? sl' →
1141      step ge (State f (Sswitch a sl) k e m)
1142           tr (State f (seq_of_labeled_statement sl') (Kswitch k) e m)
1143  | step_skip_break_switch: ∀f,x,k,e,m.
1144      x = Sskip ∨ x = Sbreak →
1145      step ge (State f x (Kswitch k) e m)
1146           E0 (State f Sskip k e m)
1147  | step_continue_switch: ∀f,k,e,m.
1148      step ge (State f Scontinue (Kswitch k) e m)
1149           E0 (State f Scontinue k e m)
1150
1151  | step_label: ∀f,lbl,s,k,e,m.
1152      step ge (State f (Slabel lbl s) k e m)
1153           E0 (State f s k e m)
1154
1155  | step_goto: ∀f,lbl,k,e,m,s',k'.
1156      find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉 →
1157      step ge (State f (Sgoto lbl) k e m)
1158           E0 (State f s' k' e m)
1159
1160  | step_internal_function: ∀id,f,vargs,k,m,e,m1,m2.
1161      alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 →
1162      bind_parameters e m1 (fn_params f) vargs m2 →
1163      step ge (Callstate id (CL_Internal f) vargs k m)
1164           E0 (State f (fn_body f) k e m2)
1165
1166  | step_external_function: ∀fid,id,targs,tres,vargs,k,m,vres,t.
1167      event_match (external_function id targs tres) vargs t vres →
1168      step ge (Callstate fid (CL_External id targs tres) vargs k m)
1169            t (Returnstate vres k m)
1170
1171  | step_returnstate_0: ∀v,f,e,k,m.
1172      step ge (Returnstate v (Kcall (None ?) f e k) m)
1173           E0 (State f Sskip k e m)
1174
1175  | step_returnstate_1: ∀v,f,e,k,m,m',loc,ofs,ty.
1176      store_value_of_type ty m loc ofs v = Some ? m' →
1177      step ge (Returnstate v (Kcall (Some ? 〈〈loc, ofs〉, ty〉) f e k) m)
1178           E0 (State f Sskip k e m')
1179           
1180  | step_cost: ∀f,lbl,s,k,e,m.
1181      step ge (State f (Scost lbl s) k e m)
1182           (Echarge lbl) (State f s k e m)
1183 
1184  | step_final: ∀r,m.
1185      step ge (Returnstate (Vint I32 r) Kstop m)
1186           E0 (Finalstate r).
1187
1188(*
1189End SEMANTICS.
1190*)
1191
1192(* * * Whole-program semantics *)
1193
1194(* * Execution of whole programs are described as sequences of transitions
1195  from an initial state to a final state.  An initial state is a [Callstate]
1196  corresponding to the invocation of the ``main'' function of the program
1197  without arguments and with an empty continuation. *)
1198
1199inductive initial_state (p: clight_program): state -> Prop :=
1200  | initial_state_intro: ∀b,f,ge,m0.
1201      globalenv … (fst ??) p = ge →
1202      init_mem … (fst ??) p = OK ? m0 →
1203      find_symbol … ge (prog_main ?? p) = Some ? b →
1204      find_funct_ptr … ge b = Some ? f →
1205      initial_state p (Callstate (prog_main ?? p) f (nil ?) Kstop m0).
1206
1207(* * A final state is a [Returnstate] with an empty continuation. *)
1208
1209inductive final_state: state -> int -> Prop :=
1210  | final_state_intro: ∀r.
1211      final_state (Finalstate r) r.
1212
1213(* * Execution of a whole program: [exec_program p beh]
1214  holds if the application of [p]'s main function to no arguments
1215  in the initial memory state for [p] has [beh] as observable
1216  behavior. *)
1217
1218definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
1219  ∀ge. globalenv … (fst ??) p = ge →
1220  program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.
1221 
Note: See TracBrowser for help on using the repository browser.