Changeset 961 for src/Clight/Csem.ma


Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r816 r961  
    3838inductive is_false: val → type → Prop ≝
    3939  | is_false_int: ∀sz,sg.
    40       is_false (Vint zero) (Tint sz sg)
     40      is_false (Vint sz (zero ?)) (Tint sz sg)
    4141  | is_false_pointer: ∀r,r',t.
    4242      is_false (Vnull r) (Tpointer r' t)
     
    4545
    4646inductive is_true: val → type → Prop ≝
    47   | is_true_int_int: ∀n,sz,sg.
    48       n ≠ zero
    49       is_true (Vint n) (Tint sz sg)
     47  | is_true_int_int: ∀sz,sg,n.
     48      n ≠ (zero ?)
     49      is_true (Vint sz n) (Tint sz sg)
    5050  | is_true_pointer_pointer: ∀r,b,pc,ofs,s,t.
    5151      is_true (Vptr r b pc ofs) (Tpointer s t)
     
    7272let rec sem_neg (v: val) (ty: type) : option val ≝
    7373  match ty with
    74   [ Tint _ _ ⇒
     74  [ Tint sz _ ⇒
    7575      match v with
    76       [ Vint n ⇒ Some ? (Vint (two_complement_negation wordsize n))
     76      [ Vint sz' n ⇒ if eq_intsize sz sz'
     77                     then Some ? (Vint ? (two_complement_negation ? n))
     78                     else None ?
    7779      | _ ⇒ None ?
    7880      ]
     
    8789let rec sem_notint (v: val) : option val ≝
    8890  match v with
    89   [ Vint n ⇒ Some ? (Vint (xor n mone)) (* XXX *)
     91  [ Vint sz n ⇒ Some ? (Vint ? (exclusive_disjunction_bv ? n (mone ?))) (* XXX *)
    9092  | _ ⇒ None ?
    9193  ].
     
    9395let rec sem_notbool (v: val) (ty: type) : option val ≝
    9496  match ty with
    95   [ Tint _ _ ⇒
     97  [ Tint sz _ ⇒
    9698      match v with
    97       [ Vint n ⇒ Some ? (of_bool (eq n zero))
     99      [ Vint sz' n ⇒ if eq_intsize sz sz'
     100                     then Some ? (of_bool (eq_bv ? n (zero ?)))
     101                     else None ?
    98102      | _ ⇒ None ?
    99103      ]
     
    116120  [ add_case_ii ⇒                       (**r integer addition *)
    117121      match v1 with
    118       [ Vint n1 ⇒ match v2 with
    119         [ Vint n2 ⇒ Some ? (Vint (addition_n wordsize n1 n2))
     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 ?)
    120125        | _ ⇒ None ? ]
    121126      | _ ⇒ None ? ]
     
    129134      match v1 with
    130135      [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    131         [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (shift_offset ofs1 (mul (repr (sizeof ty)) n2)))
     136        [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (shift_offset_n ? ofs1 (sizeof ty) n2))
    132137        | _ ⇒ None ? ]
    133138      | Vnull r ⇒ match v2 with
    134         [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
     139        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
    135140        | _ ⇒ None ? ]
    136141      | _ ⇒ None ? ]
    137142  | add_case_ip ty ⇒                    (**r integer plus pointer *)
    138143      match v1 with
    139       [ Vint n1 ⇒ match v2 with
    140         [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset ofs2 (mul (repr (sizeof ty)) n1)))
    141         | Vnull r ⇒ if eq n1 zero then Some ? (Vnull r) else None ?
     144      [ Vint sz1 n1 ⇒ match v2 with
     145        [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset_n ? ofs2 (sizeof ty) n1))
     146        | Vnull r ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ?
    142147        | _ ⇒ None ? ]
    143148      | _ ⇒ None ? ]
     
    149154  [ sub_case_ii ⇒                (**r integer subtraction *)
    150155      match v1 with
    151       [ Vint n1 ⇒ match v2 with
    152         [ Vint n2 ⇒ Some ? (Vint (subtraction wordsize n1 n2))
     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 ?)
    153159        | _ ⇒ None ? ]
    154160      | _ ⇒ None ? ]
     
    162168      match v1 with
    163169      [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    164         [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 (mul (repr (sizeof ty)) n2)))
     170        [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset_n ? ofs1 (sizeof ty) n2))
    165171        | _ ⇒ None ? ]
    166172      | Vnull r ⇒ match v2 with
    167         [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
     173        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
    168174        | _ ⇒ None ? ]
    169175      | _ ⇒ None ? ]
     
    173179        [ Vptr r2 b2 p2 ofs2 ⇒
    174180          if eq_block b1 b2 then
    175             if eq (repr (sizeof ty)) zero then None ?
    176             else match division_u ? (sub_offset ofs1 ofs2) (repr (sizeof ty)) with
     181            if eqb (sizeof ty) 0 then None ?
     182            else match division_u ? (sub_offset ? ofs1 ofs2) (repr (sizeof ty)) with
    177183                 [ None ⇒ None ?
    178                  | Some v ⇒ Some ? (Vint v)
     184                 | Some v ⇒ Some ? (Vint I32 v) (* XXX choose size from result type? *)
    179185                 ]
    180186          else None ?
    181187        | _ ⇒ None ? ]
    182       | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
     188      | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ]
    183189      | _ ⇒ None ? ]
    184190  | sub_default ⇒ None ?
     
    189195  [ mul_case_ii ⇒
    190196      match v1 with
    191       [ Vint n1 ⇒ match v2 with
    192           [ Vint n2 ⇒ Some ? (Vint (mul n1 n2))
    193 (*        [ Vint n2 ⇒ Some ? (Vint (\snd (split ? wordsize wordsize (multiplication ? n1 n2))))*)
     197      [ Vint sz1 n1 ⇒ match v2 with
     198          [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     199                          (λn1. Some ? (Vint sz2 (\snd (split ??? (multiplication ? n1 n2))))) (None ?)
    194200        | _ ⇒ None ? ]
    195201      | _ ⇒ None ? ]
     
    208214  [ div_case_I32unsi ⇒
    209215      match v1 with
    210       [ Vint n1 ⇒ match v2 with
    211         [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)
     216      [ Vint sz1 n1 ⇒ match v2 with
     217        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     218                        (λn1. option_map … (Vint ?) (division_u ? n1 n2)) (None ?)
    212219        | _ ⇒ None ? ]
    213220      | _ ⇒ None ? ]
    214221  | div_case_ii ⇒
    215222      match v1 with
    216        [ Vint n1 ⇒ match v2 with
    217          [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)
     223       [ Vint sz1 n1 ⇒ match v2 with
     224         [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     225                         (λn1. option_map … (Vint ?) (division_s ? n1 n2)) (None ?)
    218226         | _ ⇒ None ? ]
    219227      | _ ⇒ None ? ]
     
    232240  [ mod_case_I32unsi ⇒
    233241      match v1 with
    234       [ Vint n1 ⇒ match v2 with
    235         [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)
     242      [ Vint sz1 n1 ⇒ match v2 with
     243        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     244                        (λn1. option_map … (Vint ?) (modulus_u ? n1 n2)) (None ?)
    236245        | _ ⇒ None ? ]
    237246      | _ ⇒ None ? ]
    238247  | mod_case_ii ⇒
    239248      match v1 with
    240       [ Vint n1 ⇒ match v2 with
    241         [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)
     249      [ Vint sz1 n1 ⇒ match v2 with
     250        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     251                        (λn1. option_map … (Vint ?) (modulus_s ? n1 n2)) (None ?)
    242252        | _ ⇒ None ? ]
    243253      | _ ⇒ None ? ]
     
    248258let rec sem_and (v1,v2: val) : option val ≝
    249259  match v1 with
    250   [ Vint n1 ⇒ match v2 with
    251     [ Vint n2 ⇒ Some ? (Vint (conjunction_bv ? n1 n2))
     260  [ Vint sz1 n1 ⇒ match v2 with
     261    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     262                    (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2))) (None ?)
    252263    | _ ⇒ None ? ]
    253264  | _ ⇒ None ?
     
    256267let rec sem_or (v1,v2: val) : option val ≝
    257268  match v1 with
    258   [ Vint n1 ⇒ match v2 with
    259     [ Vint n2 ⇒ Some ? (Vint (inclusive_disjunction_bv ? n1 n2))
     269  [ Vint sz1 n1 ⇒ match v2 with
     270    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     271                    (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2))) (None ?)
    260272    | _ ⇒ None ? ]
    261273  | _ ⇒ None ?
     
    264276let rec sem_xor (v1,v2: val) : option val ≝
    265277  match v1 with
    266   [ Vint n1 ⇒ match v2 with
    267     [ Vint n2 ⇒ Some ? (Vint (exclusive_disjunction_bv ? n1 n2))
     278  [ Vint sz1 n1 ⇒ match v2 with
     279    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     280                    (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2))) (None ?)
    268281    | _ ⇒ None ? ]
    269282  | _ ⇒ None ?
     
    272285let rec sem_shl (v1,v2: val): option val ≝
    273286  match v1 with
    274   [ Vint n1 ⇒ match v2 with
    275     [ Vint n2 ⇒
    276         if ltu n2 iwordsize then Some ? (Vint(shl n1 n2)) else None ?
     287  [ Vint sz1 n1 ⇒ match v2 with
     288    [ Vint sz2 n2 ⇒
     289        if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     290        then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false))
     291        else None ?
    277292    | _ ⇒ None ? ]
    278293  | _ ⇒ None ? ].
     
    282297  [ shr_case_I32unsi ⇒
    283298      match v1 with
    284       [ Vint n1 ⇒ match v2 with
    285         [ Vint n2 ⇒
    286             if ltu n2 iwordsize then Some ? (Vint (shru n1 n2)) else None ?
     299      [ Vint sz1 n1 ⇒ match v2 with
     300        [ Vint sz2 n2 ⇒
     301            if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     302            then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 false))
     303            else None ?
    287304        | _ ⇒ None ? ]
    288305      | _ ⇒ None ? ]
    289306   | shr_case_ii =>
    290307      match v1 with
    291       [ Vint n1 ⇒ match v2 with
    292         [ Vint n2 ⇒
    293             if ltu n2 iwordsize then Some ? (Vint (shr n1 n2)) else None ?
     308      [ Vint sz1 n1 ⇒ match v2 with
     309        [ Vint sz2 n2 ⇒
     310            if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     311            then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
     312            else None ?
    294313        | _ ⇒ None ? ]
    295314      | _ ⇒ None ? ]
     
    318337  [ cmp_case_I32unsi ⇒
    319338      match v1 with
    320       [ Vint n1 ⇒ match v2 with
    321         [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2))
     339      [ Vint sz1 n1 ⇒ match v2 with
     340        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     341                        (λn1. Some ? (of_bool (cmpu_int ? c n1 n2))) (None ?)
    322342        | _ ⇒ None ? ]
    323343      | _ ⇒ None ? ]
    324344  | cmp_case_ii ⇒
    325345      match v1 with
    326       [ Vint n1 ⇒ match v2 with
    327          [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
     346      [ Vint sz1 n1 ⇒ match v2 with
     347         [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     348                         (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) (None ?)
    328349         | _ ⇒ None ?
    329350         ]
     
    396417  resulting in value [v2].  *)
    397418
    398 let rec cast_int_int (sz: intsize) (sg: signedness) (i: int) : int ≝
    399   match sz with
    400   [ I8 ⇒ match sg with [ Signed ⇒ sign_ext 8 i | Unsigned ⇒ zero_ext 8 i ]
    401   | I16 ⇒ match sg with [ Signed => sign_ext 16 i | Unsigned ⇒ zero_ext 16 i ]
    402   | I32 ⇒ i
    403   ].
    404 
    405 let rec cast_int_float (si : signedness) (i: int) : float ≝
     419let rec cast_int_int (srcsz: intsize) (sz: intsize) (sg: signedness) (i: BitVector (bitsize_of_intsize srcsz)) : BitVector (bitsize_of_intsize sz) ≝
     420  match sg with [ Signed ⇒ sign_ext ?? i | Unsigned ⇒ zero_ext ?? i ].
     421
     422let rec cast_int_float (si : signedness) (n:nat) (i: BitVector n) : float ≝
    406423  match si with
    407   [ Signed ⇒ floatofint i
    408   | Unsigned ⇒ floatofintu i
    409   ].
    410 
    411 let rec cast_float_int (si : signedness) (f: float) : int
     424  [ Signed ⇒ floatofint ? i
     425  | Unsigned ⇒ floatofintu ? i
     426  ].
     427
     428let rec cast_float_int (sz : intsize) (si : signedness) (f: float) : BitVector (bitsize_of_intsize sz)
    412429  match si with
    413   [ Signed ⇒ intoffloat f
    414   | Unsigned ⇒ intuoffloat f
     430  [ Signed ⇒ intoffloat ? f
     431  | Unsigned ⇒ intuoffloat ? f
    415432  ].
    416433
     
    428445
    429446inductive cast : mem → val → type → type → val → Prop ≝
    430   | cast_ii:   ∀m,i,sz2,sz1,si1,si2.            (**r int to int  *)
    431       cast m (Vint i) (Tint sz1 si1) (Tint sz2 si2)
    432            (Vint (cast_int_int sz2 si2 i))
     447  | cast_ii:   ∀m,sz2,sz1,si1,si2,i.            (**r int to int  *)
     448      cast m (Vint sz1 i) (Tint sz1 si1) (Tint sz2 si2)
     449           (Vint sz2 (cast_int_int ? sz2 si2 i))
    433450  | cast_fi:   ∀m,f,sz1,sz2,si2.                (**r float to int *)
    434451      cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
    435            (Vint (cast_int_int sz2 si2 (cast_float_int si2 f)))
    436   | cast_if:   ∀m,i,sz1,sz2,si1.                (**r int to float  *)
    437       cast m (Vint i) (Tint sz1 si1) (Tfloat sz2)
    438           (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
     452           (Vint sz2 (cast_float_int sz2 si2 f))
     453  | cast_if:   ∀m,sz1,sz2,si1,i.                (**r int to float  *)
     454      cast m (Vint sz1 i) (Tint sz1 si1) (Tfloat sz2)
     455          (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))
    439456  | cast_ff:   ∀m,f,sz1,sz2.                    (**r float to float *)
    440457      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
     
    447464  | cast_ip_z: ∀m,sz,sg,ty',r.
    448465      type_region ty' r →
    449       cast m (Vint zero) (Tint sz sg) ty' (Vnull r)
     466      cast m (Vint sz (zero ?)) (Tint sz sg) ty' (Vnull r)
    450467  | cast_pp_z: ∀m,ty,ty',r,r'.
    451468      type_region ty r →
     
    546563(* * Selection of the appropriate case of a [switch], given the value [n]
    547564  of the selector expression. *)
    548 
    549 let rec select_switch (n: int) (sl: labeled_statements)
     565(* FIXME: now that we have several sizes of integer, it isn't clear whether we
     566   should allow case labels to be of a different size to the switch expression. *)
     567let rec select_switch (sz:intsize) (n: BitVector (bitsize_of_intsize sz)) (sl: labeled_statements)
    550568                       on sl : labeled_statements ≝
    551569  match sl with
    552570  [ LSdefault _ ⇒ sl
    553   | LScase c s sl' ⇒ if eq c n then sl else select_switch n sl'
     571  | LScase sz' c s sl' ⇒ intsize_eq_elim ? sz sz' ? n
     572                         (λn. if eq_bv ? c n then sl else select_switch sz' n sl') (select_switch sz n sl')
    554573  ].
    555574
     
    559578  match sl with
    560579  [ LSdefault s ⇒ s
    561   | LScase c s sl' ⇒ Ssequence s (seq_of_labeled_statement sl')
     580  | LScase _ c s sl' ⇒ Ssequence s (seq_of_labeled_statement sl')
    562581  ].
    563582
     
    579598
    580599inductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝
    581   | eval_Econst_int:   ∀i,ty.
    582       eval_expr ge e m (Expr (Econst_int i) ty) (Vint i) E0
     600  | eval_Econst_int:   ∀sz,sg,i.
     601      eval_expr ge e m (Expr (Econst_int sz i) (Tint sz sg)) (Vint sz i) E0
    583602  | eval_Econst_float:   ∀f,ty.
    584603      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0
     
    591610      ∀pc:pointer_compat loc r.
    592611      eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc pc ofs) tr
    593   | eval_Esizeof: ∀ty',ty.
    594       eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0
     612  | eval_Esizeof: ∀ty',sz,sg.
     613      eval_expr ge e m (Expr (Esizeof ty') (Tint sz sg)) (Vint sz (repr ? (sizeof ty'))) E0
    595614  | eval_Eunop:  ∀op,a,ty,v1,v,tr.
    596615      eval_expr ge e m a v1 tr →
     
    663682      typeof a = Tstruct id fList →
    664683      field_offset i fList = OK ? delta →
    665       eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ofs (repr delta)) tr
     684      eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ? ofs (repr I32 delta)) tr
    666685 | eval_Efield_union:   ∀a,i,ty,l,ofs,id,fList,tr.
    667686      eval_lvalue ge e m a l ofs tr →
     
    671690let rec eval_expr_ind (ge:genv) (e:env) (m:mem)
    672691  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
    673   (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
     692  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
    674693  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    675694  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    676695  (ead:∀a,ty,r,loc,pc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty r loc pc ofs tr H))
    677   (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
     696  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
    678697  (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))
    679698  (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))
     
    688707  (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝
    689708  match ev with
    690   [ eval_Econst_int i ty ⇒ eci i ty
     709  [ eval_Econst_int sz sg i ⇒ eci sz sg i
    691710  | eval_Econst_float f ty ⇒ ecF f ty
    692711  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2
    693712  | eval_Eaddrof a ty r loc pc ofs tr H ⇒ ead a ty r loc pc ofs tr H
    694   | eval_Esizeof ty' ty ⇒ esz ty' ty
     713  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
    695714  | 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)
    696715  | 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)
     
    779798  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
    780799  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
    781   (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
     800  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
    782801  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    783802  (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))
    784803  (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))
    785   (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
     804  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
    786805  (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))
    787806  (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))
     
    802821  (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝
    803822  match ev with
    804   [ eval_Econst_int i ty ⇒ eci i ty
     823  [ eval_Econst_int sz sg i ⇒ eci sz sg i
    805824  | eval_Econst_float f ty ⇒ ecF f ty
    806825  | 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)
    807826  | eval_Eaddrof a ty r loc ofs tr H pc ⇒ ead a ty r loc pc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H)
    808   | eval_Esizeof ty' ty ⇒ esz ty' ty
     827  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
    809828  | 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)
    810829  | 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)
     
    821840  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
    822841  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
    823   (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
     842  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
    824843  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    825844  (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))
    826845  (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))
    827   (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
     846  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
    828847  (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))
    829848  (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))
     
    9831002  match sl with
    9841003  [ LSdefault s => find_label lbl s k
    985   | LScase _ s sl' =>
     1004  | LScase _ _ s sl' =>
    9861005      match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with
    9871006      [ Some sk => Some ? sk
     
    11351154           E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
    11361155
    1137   | step_switch: ∀f,a,sl,k,e,m,n,tr.
    1138       eval_expr ge e m a (Vint n) tr →
     1156  | step_switch: ∀f,a,sl,k,e,m,sz,n,tr.
     1157      eval_expr ge e m a (Vint sz n) tr →
    11391158      step ge (State f (Sswitch a sl) k e m)
    1140            tr (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m)
     1159           tr (State f (seq_of_labeled_statement (select_switch ? n sl)) (Kswitch k) e m)
    11411160  | step_skip_break_switch: ∀f,x,k,e,m.
    11421161      x = Sskip ∨ x = Sbreak →
     
    15031522inductive final_state: state -> int -> Prop :=
    15041523  | final_state_intro: ∀r,m.
    1505       final_state (Returnstate (Vint r) Kstop m) r.
     1524      final_state (Returnstate (Vint I32 r) Kstop m) r.
    15061525
    15071526(* * Execution of a whole program: [exec_program p beh]
Note: See TracChangeset for help on using the changeset viewer.