source: src/Clight/Csem.ma @ 2588

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

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

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