source: src/Clight/Csem.ma @ 1231

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

Change SmallstepExec? so that states can depend on global information.
Use less suggestive names for the transition system so that it's obvious
the global information isn't restricted to Genv.
Separate set up of global environment from initialisation so that it never
fails.
Some minimal changes to get Clight execution working; rest to follow.

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