source: src/Clight/Csem.ma @ 2324

Last change on this file since 2324 was 2263, checked in by garnier, 8 years ago

Finished proving semantics preservation under memory injections for unary and binary ops. Had to tweak a definition in Csem.ma to circumvent lack of unfold.

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