Changeset 961 for src/common


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.

Location:
src/common
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r882 r961  
    2020include "common/Integers.ma".
    2121include "common/Floats.ma".
    22 include "ASM/BitVector.ma".
     22include "ASM/Arithmetic.ma".
    2323include "common/Identifiers.ma".
    2424
     
    110110definition SigType_Ptr ≝ ASTptr Any.
    111111
     112(* Define these carefully so that we always know that the result is nonzero,
     113   and can be used in dependent types of the form (S n).
     114   (At the time of writing this is only used for bitsize_of_intsize.) *)
     115
    112116definition size_intsize : intsize → nat ≝
    113 λsz. match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4].
     117λsz. S match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].
     118
     119definition bitsize_of_intsize : intsize → nat ≝
     120λsz. S match sz with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31].
     121
     122definition eq_intsize : intsize → intsize → bool ≝
     123λsz1,sz2.
     124  match sz1 with
     125  [ I8  ⇒ match sz2 with [ I8  ⇒ true | _ ⇒ false ]
     126  | I16 ⇒ match sz2 with [ I16 ⇒ true | _ ⇒ false ]
     127  | I32 ⇒ match sz2 with [ I32 ⇒ true | _ ⇒ false ]
     128  ].
     129
     130lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0].
     131  (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2).
     132* * #P #Hne #Heq whd in ⊢ (?%) try (@Heq @refl) @Hne % #E destruct
     133qed.
     134
     135lemma eq_intsize_true : ∀sz. eq_intsize sz sz = true.
     136* @refl
     137qed.
     138
     139lemma eq_intsize_false : ∀sz,sz'. sz ≠ sz' → eq_intsize sz sz' = false.
     140* * * #NE try @refl @False_ind @NE @refl
     141qed.
     142
     143(* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and
     144   if it is returns [e1] where the type of [n] has its dependency on [sz1]
     145   changed to [sz2], and if not returns [e2]. *)
     146let rec intsize_eq_elim (A:Type[0]) (sz1,sz2:intsize) (P:intsize → Type[0]) on sz1 :
     147  P sz1 → (P sz2 → A) → A → A ≝
     148match sz1 return λsz. P sz → (P sz2 → A) → A → A with
     149[ I8  ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I8  ⇒ λf,d. f x | _ ⇒ λf,d. d ]
     150| I16 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I16 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
     151| I32 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I32 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
     152].
     153
     154lemma intsize_eq_elim_true : ∀A,sz,P,p,f,d.
     155  intsize_eq_elim A sz sz P p f d = f p.
     156#A * //
     157qed.
     158
     159lemma intsize_eq_elim_elim : ∀A,sz1,sz2,P,p,f,d. ∀Q:A → Type[0].
     160  (sz1 ≠ sz2 → Q d) → (∀E:sz1 = sz2. match sym_eq ??? E return λx.λ_.P x → Type[0] with [ refl ⇒ λp. Q (f p) ] p ) → Q (intsize_eq_elim A sz1 sz2 P p f d).
     161#A * * #P #p #f #d #Q #Hne #Heq
     162[ 1,5,9: whd in ⊢ (?%) @(Heq (refl ??))
     163| *: whd in ⊢ (?%) @Hne % #E destruct
     164] qed.
     165
     166
     167(* A type for the integers that appear in the semantics. *)
     168definition bvint : intsize → Type[0] ≝ λsz. BitVector (bitsize_of_intsize sz).
     169
     170definition repr : ∀sz:intsize. nat → bvint sz ≝
     171λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x.
     172
    114173
    115174definition size_floatsize : floatsize → nat ≝
    116 λsz. match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ].
     175λsz. S match sz with [ F32 ⇒ 3 | F64 ⇒ 7 ].
    117176
    118177definition typesize : typ → nat ≝ λty.
     
    187246
    188247inductive init_data: Type[0] ≝
    189   | Init_int8: int → init_data
    190   | Init_int16: int → init_data
    191   | Init_int32: int → init_data
     248  | Init_int8: bvint I8 → init_data
     249  | Init_int16: bvint I16 → init_data
     250  | Init_int32: bvint I32 → init_data
    192251  | Init_float32: float → init_data
    193252  | Init_float64: float → init_data
    194253  | Init_space: nat → init_data
    195254  | Init_null: region → init_data
    196   | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
     255  | Init_addrof: region → ident → nat → init_data.   (*r address of symbol + offset *)
    197256
    198257(* * Whole programs consist of:
  • src/common/Animation.ma

    r879 r961  
    1010λo,ev.
    1111match io_in_typ o return λt. res (eventval_type t) with
    12 [ ASTint _ _ ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? (msg IllTypedEvent) ]
     12[ ASTint sz _ ⇒ match ev with [ EVint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.OK ? i) (Error ? (msg IllTypedEvent)) | _ ⇒ Error ? (msg IllTypedEvent) ]
    1313| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
    1414| ASTptr _ ⇒ Error ? (msg IllTypedEvent)
  • src/common/Events.ma

    r879 r961  
    3737  world. *)
    3838
    39 inductive eventval: Type[0] :=
    40   | EVint: int -> eventval
    41   | EVfloat: float -> eventval.
     39inductive eventval: Type[0]
     40  | EVint: ∀sz. bvint sz → eventval
     41  | EVfloat: float eventval.
    4242
    4343inductive event : Type[0] ≝
     
    193193inductive eventval_match: eventval -> typ -> val -> Prop :=
    194194  | ev_match_int:
    195       ∀i,sz,sg. eventval_match (EVint i) (ASTint sz sg) (Vint i)
     195      ∀sz,sg,i. eventval_match (EVint sz i) (ASTint sz sg) (Vint sz i)
    196196  | ev_match_float:
    197197      ∀f,sz. eventval_match (EVfloat f) (ASTfloat sz) (Vfloat f).
  • src/common/Floats.ma

    r700 r961  
    3434axiom Fabs: float → float.
    3535axiom singleoffloat: float → float.
    36 axiom intoffloat: float → int.
    37 axiom intuoffloat: float → int.
    38 axiom floatofint: int → float.
    39 axiom floatofintu: int → float.
     36axiom intoffloat: ∀n. float → BitVector n.
     37axiom intuoffloat: ∀n. float → BitVector n.
     38axiom floatofint: ∀n. BitVector n → float.
     39axiom floatofintu: ∀n. BitVector n → float.
    4040
    4141axiom Fadd: float → float → float.
  • src/common/FrontEndOps.ma

    r774 r961  
    2121
    2222inductive constant : Type[0] ≝
    23   | Ointconst: int → constant     (**r integer constant *)
    24   | Ofloatconst: float → constant (**r floating-point constant *)
    25   | Oaddrsymbol: ident → int → constant (**r address of the symbol plus the offset *)
    26   | Oaddrstack: int → constant.   (**r stack pointer plus the given offset *)
     23  | Ointconst: ∀sz. bvint sz → constant    (**r integer constant *)
     24  | Ofloatconst: float → constant          (**r floating-point constant *)
     25  | Oaddrsymbol: ident → nat → constant    (**r address of the symbol plus the offset *)
     26  | Oaddrstack: nat → constant.            (**r stack pointer plus the given offset *)
    2727
    2828inductive unary_operation : Type[0] ≝
    29   | Ocast8unsigned: unary_operation        (**r 8-bit zero extension  *)
    30   | Ocast8signed: unary_operation          (**r 8-bit sign extension  *)
    31   | Ocast16unsigned: unary_operation       (**r 16-bit zero extension  *)
    32   | Ocast16signed: unary_operation         (**r 16-bit sign extension *)
     29  | Ocastint: intsize → signedness → unary_operation (**r 8-bit zero extension  *)
    3330  | Onegint: unary_operation               (**r integer opposite *)
    3431  | Onotbool: unary_operation              (**r boolean negation  *)
     
    3734  | Oabsf: unary_operation                 (**r float absolute value *)
    3835  | Osingleoffloat: unary_operation        (**r float truncation *)
    39   | Ointoffloat: unary_operation          (**r signed integer to float *)
    40   | Ointuoffloat: unary_operation          (**r unsigned integer to float *)
     36  | Ointoffloat: intsize → unary_operation (**r signed integer to float *)
     37  | Ointuoffloat: intsize → unary_operation (**r unsigned integer to float *)
    4138  | Ofloatofint: unary_operation           (**r float to signed integer *)
    4239  | Ofloatofintu: unary_operation          (**r float to unsigned integer *)
    4340  | Oid: unary_operation                   (**r identity (used to move between registers *)
    4441  | Optrofint: region → unary_operation    (**r int to pointer with given representation *)
    45   | Ointofptr: unary_operation.            (**r pointer to int *)
     42  | Ointofptr: intsize → unary_operation.  (**r pointer to int *)
    4643
    4744inductive binary_operation : Type[0] ≝
     
    6865  | Oaddp: binary_operation                (**r add an integer to a pointer *)
    6966  | Osubpi: binary_operation               (**r subtract int from a pointers *)
    70   | Osubpp: binary_operation               (**r subtract two pointers *)
     67  | Osubpp: intsize → binary_operation     (**r subtract two pointers *)
    7168  | Ocmpp: comparison → binary_operation.  (**r compare pointers *)
    7269
     
    8077λfind_symbol,sp,cst.
    8178  match cst with
    82   [ Ointconst n ⇒ Some ? (Vint n)
     79  [ Ointconst sz n ⇒ Some ? (Vint sz n)
    8380  | Ofloatconst n ⇒ Some ? (Vfloat n)
    8481  | Oaddrsymbol s ofs ⇒
    8582      match find_symbol s with
    8683      [ None ⇒ None ?
    87       | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset zero_offset ofs))
     84      | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs)))
    8885      ]
    8986  | Oaddrstack ofs ⇒
    90       Some ? (Vptr Any sp ? (shift_offset zero_offset ofs))
     87      Some ? (Vptr Any sp ? (shift_offset ? zero_offset (repr I16 ofs)))
    9188  ]. cases sp // qed.
    9289
     
    9491λop,arg.
    9592  match op with
    96   [ Ocast8unsigned ⇒ Some ? (zero_ext 8 arg)
    97   | Ocast8signed ⇒ Some ? (sign_ext 8 arg)
    98   | Ocast16unsigned ⇒ Some ? (zero_ext 16 arg)
    99   | Ocast16signed ⇒ Some ? (sign_ext 16 arg)
    100   | Onegint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (neg n1)) | _ ⇒ None ? ]
    101   | Onotbool ⇒ match arg with [ Vint n1 ⇒ Some ? (of_bool (eq n1 zero))
     93  [ Ocastint sz sg ⇒
     94      match sg with
     95      [ Unsigned ⇒ Some ? (zero_ext sz arg)
     96      |   Signed ⇒ Some ? (sign_ext sz arg)
     97      ]
     98  | Onegint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (two_complement_negation ? n1)) | _ ⇒ None ? ]
     99  | Onotbool ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (of_bool (eq_bv ? n1 (zero ?)))
    102100                              | Vptr _ _ _ _ ⇒ Some ? Vfalse
    103101                              | Vnull _ ⇒ Some ? Vtrue
    104102                              | _ ⇒ None ?
    105103                              ]
    106   | Onotint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (not n1)) | _ ⇒ None ? ]
     104  | Onotint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (exclusive_disjunction_bv ? n1 (mone ?))) | _ ⇒ None ? ]
    107105  | Onegf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
    108106  | Oabsf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ]
    109107  | Osingleoffloat ⇒ Some ? (singleoffloat arg)
    110   | Ointoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intoffloat f1)) | _ ⇒ None ? ]
    111   | Ointuoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intuoffloat f1)) | _ ⇒ None ? ]
    112   | Ofloatofint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofint n1)) | _ ⇒ None ? ]
    113   | Ofloatofintu ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintu n1)) | _ ⇒ None ? ]
     108  | Ointoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intoffloat ? f1)) | _ ⇒ None ? ]
     109  | Ointuoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intuoffloat ? f1)) | _ ⇒ None ? ]
     110  | Ofloatofint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofint ? n1)) | _ ⇒ None ? ]
     111  | Ofloatofintu ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1)) | _ ⇒ None ? ]
    114112  | Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
    115113  (* Only conversion of null pointers is specified. *)
    116   | Optrofint r ⇒ match arg with [ Vint n1 ⇒ if eq n1 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
    117   | Ointofptr ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
     114  | Optrofint r ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     115  | Ointofptr sz ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
    118116  ].
    119117
     
    122120λc. match c with [ Ceq ⇒ Some ? Vfalse | Cne ⇒ Some ? Vtrue | _ ⇒ None ? ].
    123121
    124 (* Individual operations, adapted from Values. *)
    125 
    126 definition ev_neg : val → option val ≝ λv.
    127   match v with
    128   [ Vint n ⇒ Some ? (Vint (neg n))
    129   | _ ⇒ None ?
    130   ].
    131 
    132 definition ev_negf : val → option val ≝ λv.
    133   match v with
    134   [ Vfloat f ⇒ Some ? (Vfloat (Fneg f))
    135   | _ ⇒ None ?
    136   ].
    137 
    138 definition ev_absf : val → option val ≝ λv.
    139   match v with
    140   [ Vfloat f ⇒ Some ? (Vfloat (Fabs f))
    141   | _ ⇒ None ?
    142   ].
    143 
    144 definition ev_intoffloat : val → option val ≝ λv.
    145   match v with
    146   [ Vfloat f ⇒ Some ? (Vint (intoffloat f))
    147   | _ ⇒ None ?
    148   ].
    149 
    150 definition ev_intuoffloat : val → option val ≝ λv.
    151   match v with
    152   [ Vfloat f ⇒ Some ? (Vint (intuoffloat f))
    153   | _ ⇒ None ?
    154   ].
    155 
    156 definition ev_floatofint : val → option val ≝ λv.
    157   match v with
    158   [ Vint n ⇒ Some ? (Vfloat (floatofint n))
    159   | _ ⇒ None ?
    160   ].
    161 
    162 definition ev_floatofintu : val → option val ≝ λv.
    163   match v with
    164   [ Vint n ⇒ Some ? (Vfloat (floatofintu n))
    165   | _ ⇒ None ?
    166   ].
    167 
    168 definition ev_notint : val → option val ≝ λv.
    169   match v with
    170   [ Vint n ⇒ Some ? (Vint (xor n mone))
    171   | _ ⇒ None ?
    172   ].
    173  
    174 definition ev_notbool : val → option val ≝ λv.
    175   match v with
    176   [ Vint n ⇒ Some ? (of_bool (int_eq n zero))
    177   | Vptr _ b _ ofs ⇒ Some ? Vfalse
    178   | Vnull _ ⇒ Some ? Vtrue
    179   | _ ⇒ None ?
    180   ].
    181 
    182 definition ev_zero_ext ≝ λnbits: nat. λv: val.
    183   match v with
    184   [ Vint n ⇒ Some ? (Vint (zero_ext nbits n))
    185   | _ ⇒ None ?
    186   ].
    187 
    188 definition ev_sign_ext ≝ λnbits:nat. λv:val.
    189   match v with
    190   [ Vint i ⇒ Some ? (Vint (sign_ext nbits i))
    191   | _ ⇒ None ?
    192   ].
    193 
    194 definition ev_singleoffloat : val → option val ≝ λv.
    195   match v with
    196   [ Vfloat f ⇒ Some ? (Vfloat (singleoffloat f))
    197   | _ ⇒ None ?
    198   ].
     122(* Individual operations, adapted from Values.  These differ in that they
     123   implement the plain Cminor/RTLabs operations (e.g., with separate addition
     124   for ints,floats and pointers) and use option rather than Vundef.  The ones
     125   in Value are probably not needed. *)
    199126
    200127definition ev_add ≝ λv1,v2: val.
    201128  match v1 with
    202   [ Vint n1 ⇒ match v2 with
    203     [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2))
     129  [ Vint sz1 n1 ⇒ match v2 with
     130    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     131                    (λn1. Some ? (Vint ? (addition_n ? n1 n2)))
     132                    (None ?)
    204133    | _ ⇒ None ? ]
    205134  | _ ⇒ None ? ].
     
    207136definition ev_sub ≝ λv1,v2: val.
    208137  match v1 with
    209   [ Vint n1 ⇒ match v2 with
    210     [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
     138  [ Vint sz1 n1 ⇒ match v2 with
     139    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     140                    (λn1. Some ? (Vint ? (subtraction ? n1 n2)))
     141                    (None ?)
    211142    | _ ⇒ None ? ]
    212143  | _ ⇒ None ? ].
     
    216147  match v1 with
    217148  [ Vptr r b1 p ofs1 ⇒ match v2 with
    218     [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2))
     149    [ Vint sz2 n2 ⇒ Some ? (Vptr r b1 p (shift_offset ? ofs1 n2))
    219150    | _ ⇒ None ? ]
    220151  | Vnull r ⇒ match v2 with
    221     [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
     152    [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
    222153    | _ ⇒ None ?
    223154    ]
     
    227158  match v1 with
    228159  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    229     [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 n2))
    230     | _ ⇒ None ? ]
    231   | Vnull r ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
    232   | _ ⇒ None ? ].
    233 
    234 definition ev_subpp ≝ λv1,v2: val.
     160    [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2))
     161    | _ ⇒ None ? ]
     162  | Vnull r ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     163  | _ ⇒ None ? ].
     164
     165definition ev_subpp ≝ λsz. λv1,v2: val.
    235166  match v1 with
    236167  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    237168    [ Vptr r2 b2 p2 ofs2 ⇒
    238         if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ?
    239     | _ ⇒ None ? ]
    240   | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
     169        if eq_block b1 b2 then Some ? (Vint sz (sub_offset ? ofs1 ofs2)) else None ?
     170    | _ ⇒ None ? ]
     171  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
    241172  | _ ⇒ None ? ].
    242173
    243174definition ev_mul ≝ λv1, v2: val.
    244175  match v1 with
    245   [ Vint n1 ⇒ match v2 with
    246     [ Vint n2 ⇒ Some ? (Vint (mul n1 n2))
     176  [ Vint sz1 n1 ⇒ match v2 with
     177    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     178                    (λn1. Some ? (Vint ? (\snd (split … (multiplication ? n1 n2)))))
     179                    (None ?)
    247180    | _ ⇒ None ? ]
    248181  | _ ⇒ None ? ].
     
    250183definition ev_divs ≝ λv1, v2: val.
    251184  match v1 with
    252   [ Vint n1 ⇒ match v2 with
    253     [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2)
     185  [ Vint sz1 n1 ⇒ match v2 with
     186    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     187                    (λn1. option_map ?? (Vint ?) (division_s ? n1 n2))
     188                    (None ?)
    254189    | _ ⇒ None ? ]
    255190  | _ ⇒ None ? ].
     
    257192definition ev_mods ≝ λv1, v2: val.
    258193  match v1 with
    259   [ Vint n1 ⇒ match v2 with
    260     [ Vint n2 ⇒ option_map ?? Vint (modulus_s ? n1 n2)
     194  [ Vint sz1 n1 ⇒ match v2 with
     195    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     196                    (λn1. option_map ?? (Vint ?) (modulus_s ? n1 n2))
     197                    (None ?)
    261198    | _ ⇒ None ?
    262199    ]
     
    266203definition ev_divu ≝ λv1, v2: val.
    267204  match v1 with
    268   [ Vint n1 ⇒ match v2 with
    269     [ Vint n2 ⇒ option_map ?? Vint (division_u ? n1 n2)
     205  [ Vint sz1 n1 ⇒ match v2 with
     206    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     207                    (λn1. option_map ?? (Vint ?) (division_u ? n1 n2))
     208                    (None ?)
    270209    | _ ⇒ None ?
    271210    ]
     
    275214definition ev_modu ≝ λv1, v2: val.
    276215  match v1 with
    277   [ Vint n1 ⇒ match v2 with
    278     [ Vint n2 ⇒ option_map ?? Vint (modulus_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 ?) (modulus_u ? n1 n2))
     219                    (None ?)
    279220    | _ ⇒ None ?
    280221    ]
     
    284225definition ev_and ≝ λv1, v2: val.
    285226  match v1 with
    286   [ Vint n1 ⇒ match v2 with
    287     [ Vint n2 ⇒ Some ? (Vint (i_and n1 n2))
     227  [ Vint sz1 n1 ⇒ match v2 with
     228    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     229                    (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2)))
     230                    (None ?)
    288231    | _ ⇒ None ? ]
    289232  | _ ⇒ None ? ].
     
    291234definition ev_or ≝ λv1, v2: val.
    292235  match v1 with
    293   [ Vint n1 ⇒ match v2 with
    294     [ Vint n2 ⇒ Some ? (Vint (or n1 n2))
     236  [ Vint sz1 n1 ⇒ match v2 with
     237    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     238                    (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2)))
     239                    (None ?)
    295240    | _ ⇒ None ? ]
    296241  | _ ⇒ None ? ].
     
    298243definition ev_xor ≝ λv1, v2: val.
    299244  match v1 with
    300   [ Vint n1 ⇒ match v2 with
    301     [ Vint n2 ⇒ Some ? (Vint (xor n1 n2))
     245  [ Vint sz1 n1 ⇒ match v2 with
     246    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     247                    (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2)))
     248                    (None ?)
    302249    | _ ⇒ None ? ]
    303250  | _ ⇒ None ? ].
     
    305252definition ev_shl ≝ λv1, v2: val.
    306253  match v1 with
    307   [ Vint n1 ⇒ match v2 with
    308     [ Vint n2 ⇒
    309        if ltu n2 iwordsize
    310        then Some ? (Vint (shl n1 n2))
     254  [ Vint sz1 n1 ⇒ match v2 with
     255    [ Vint sz2 n2 ⇒
     256       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     257       then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false))
    311258       else None ?
    312259    | _ ⇒ None ? ]
     
    315262definition ev_shr ≝ λv1, v2: val.
    316263  match v1 with
    317   [ Vint n1 ⇒ match v2 with
    318     [ Vint n2 ⇒
    319        if ltu n2 iwordsize
    320        then Some ? (Vint (shr n1 n2))
     264  [ Vint sz1 n1 ⇒ match v2 with
     265    [ Vint sz2 n2 ⇒
     266       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     267       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
    321268       else None ?
    322269    | _ ⇒ None ? ]
    323270  | _ ⇒ None ? ].
    324271
    325 definition ev_shr_carry ≝ λv1, v2: val.
    326   match v1 with
    327   [ Vint n1 ⇒ match v2 with
    328     [ Vint n2 ⇒
    329        if ltu n2 iwordsize
    330        then Some ? (Vint (shr_carry n1 n2))
    331        else None ?
    332     | _ ⇒ None ? ]
    333   | _ ⇒ None ? ].
    334 
    335 definition ev_shrx ≝ λv1, v2: val.
    336   match v1 with
    337   [ Vint n1 ⇒ match v2 with
    338     [ Vint n2 ⇒
    339        if ltu n2 iwordsize
    340        then Some ? (Vint (shrx n1 n2))
    341        else None ?
    342     | _ ⇒ None ? ]
    343   | _ ⇒ None ? ].
    344 
    345272definition ev_shru ≝ λv1, v2: val.
    346273  match v1 with
    347   [ Vint n1 ⇒ match v2 with
    348     [ Vint n2 ⇒
    349        if ltu n2 iwordsize
    350        then Some ? (Vint (shru n1 n2))
    351        else None ?
    352     | _ ⇒ None ? ]
    353   | _ ⇒ None ? ].
    354 
    355 definition ev_rolm ≝
    356 λv: val. λamount, mask: int.
    357   match v with
    358   [ Vint n ⇒ Some ? (Vint (rolm n amount mask))
    359   | _ ⇒ None ?
    360   ].
    361 
    362 definition ev_ror ≝ λv1, v2: val.
    363   match v1 with
    364   [ Vint n1 ⇒ match v2 with
    365     [ Vint n2 ⇒
    366        if ltu n2 iwordsize
    367        then Some ? (Vint (ror n1 n2))
     274  [ Vint sz1 n1 ⇒ match v2 with
     275    [ Vint sz2 n2 ⇒
     276       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     277       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 false))
    368278       else None ?
    369279    | _ ⇒ None ? ]
     
    414324definition ev_cmp ≝ λc: comparison. λv1,v2: val.
    415325  match v1 with
    416   [ Vint n1 ⇒ match v2 with
    417     [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
     326  [ Vint sz1 n1 ⇒ match v2 with
     327    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     328                    (λn1. Some ? (of_bool (cmp_int ? c n1 n2)))
     329                    (None ?)
    418330    | _ ⇒ None ? ]
    419331  | _ ⇒ None ? ].
     
    438350definition ev_cmpu ≝ λc: comparison. λv1,v2: val.
    439351  match v1 with
    440   [ Vint n1 ⇒ match v2 with
    441     [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2))
     352  [ Vint sz1 n1 ⇒ match v2 with
     353    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     354                    (λn1. Some ? (of_bool (cmpu_int ? c n1 n2)))
     355                    (None ?)
    442356    | _ ⇒ None ? ]
    443357  | _ ⇒ None ? ].
     
    475389  | Oaddp ⇒ ev_addp
    476390  | Osubpi ⇒ ev_subpi
    477   | Osubpp ⇒ ev_subpp
     391  | Osubpp sz ⇒ ev_subpp sz
    478392  | Ocmpp c ⇒ ev_cmpp c
    479393  ].
  • src/common/Globalenvs.ma

    r797 r961  
    406406  let r ≝ block_region m b in
    407407  match id with
    408   [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n)
    409   | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint n)
    410   | Init_int32 n ⇒ store Mint32 m r b p (Vint n)
     408  [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint I8 n)
     409  | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint I16 n)
     410  | Init_int32 n ⇒ store Mint32 m r b p (Vint I32 n)
    411411  | Init_float32 n ⇒ store Mfloat32 m r b p (Vfloat n)
    412412  | Init_float64 n ⇒ store Mfloat64 m r b p (Vfloat n)
     
    416416      | Some b' ⇒
    417417        match pointer_compat_dec b' r' with
    418         [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset zero_offset ofs))
     418        [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset ? zero_offset (repr I16 ofs)))
    419419        | inr _ ⇒ None ?
    420420        ]
  • src/common/IO.ma

    r879 r961  
    66
    77definition eventval_type : ∀ty:typ. Type[0] ≝
    8 λty. match ty with [ ASTint _ _ ⇒ int | ASTptr _ ⇒ False | ASTfloat _ ⇒ float ].
     8λty. match ty with [ ASTint sz _ ⇒ bvint sz | ASTptr _ ⇒ False | ASTfloat _ ⇒ float ].
    99
    1010definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    11 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint _ _ ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
     11λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint sz sg ⇒ λv.EVint sz v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
    1212*; qed.
    1313
    1414definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    15 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint _ _ ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
     15λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint sz _ ⇒ λv.Vint sz v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
    1616*; qed.
    1717
     
    2525λev,ty.
    2626match ty with
    27 [ ASTint _ _ ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? (msg IllTypedEvent)]
     27[ ASTint sz _ ⇒ match ev with
     28  [ EVint sz' i ⇒ if eq_intsize sz sz' then OK ? (Vint sz' i) else Error ? (msg IllTypedEvent)
     29  | _ ⇒ Error ? (msg IllTypedEvent)]
    2830| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
    2931| _ ⇒ Error ? (msg IllTypedEvent)
     
    3335λv,ty.
    3436match ty with
    35 [ ASTint _ _ ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? (msg IllTypedEvent) ]
     37[ ASTint sz _ ⇒ match v with
     38  [ Vint sz' i ⇒ if eq_intsize sz sz' then OK ? (EVint sz' i) else Error ? (msg IllTypedEvent)
     39  | _ ⇒ Error ? (msg IllTypedEvent) ]
    3640| ASTfloat _ ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
    3741| _ ⇒ Error ? (msg IllTypedEvent)
  • src/common/Integers.ma

    r889 r961  
    436436#x #y change with (eq_bv ??? = eq_bv ???)
    437437 @eq_bv_elim @eq_bv_elim /2/
    438 [ #NE #E @False_ind >E in NE * /2/
    439 | #E #NE @False_ind >E in NE * /2/
    440 ] qed.
     438#E >E * #NE @False_ind @NE @refl
     439qed.
    441440
    442441theorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y).
  • src/common/Values.ma

    r891 r961  
    1919include "utilities/Coqlib.ma".
    2020include "common/AST.ma".
    21 include "common/Integers.ma".
    2221include "common/Floats.ma".
    2322include "common/Errors.ma".
     
    2726include "basics/logic.ma".
    2827
    29 include "utilities/binary/Z.ma".
    3028include "utilities/extralib.ma".
    3129
     
    9492
    9593definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
    96 definition shift_offset : offset → int → offset ≝
    97   λo,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
    98 definition neg_shift_offset : offset → int → offset ≝
    99   λo,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
    100 definition sub_offset : offset → offset → int ≝
    101   λx,y. bitvector_of_Z ? (offv x - offv y).
     94definition shift_offset : ∀n. offset → BitVector n → offset ≝
     95  λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
     96(* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
     97definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
     98  λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).
     99definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
     100  λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
     101definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
     102  λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)).
     103definition sub_offset : ∀n. offset → offset → BitVector n ≝
     104  λn,x,y. bitvector_of_Z ? (offv x - offv y).
    102105definition zero_offset ≝ mk_offset OZ.
    103106definition lt_offset : offset → offset → bool ≝
     
    117120inductive val: Type[0] ≝
    118121  | Vundef: val
    119   | Vint: int → val
     122  | Vint: ∀sz:intsize. bvint sz → val
    120123  | Vfloat: float → val
    121124  | Vnull: region → val
    122125  | Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val.
    123126
    124 definition Vzero: val ≝ Vint zero.
    125 definition Vone: val ≝ Vint one.
    126 definition Vmone: val ≝ Vint mone.
    127 
    128 definition Vtrue: val ≝ Vint one.
    129 definition Vfalse: val ≝ Vint zero.
     127definition Vzero : intsize → val ≝ λsz. Vint sz (zero ?).
     128definition Vone: intsize → val ≝ λsz. Vint sz (repr sz 1).
     129definition mone ≝ λsz. bitvector_of_Z (bitsize_of_intsize sz) (neg one).
     130definition Vmone: intsize → val ≝ λsz. Vint sz (mone ?).
     131
     132(* XXX 32bit booleans are Clight specific. *)
     133definition Vtrue: val ≝ Vone I32.
     134definition Vfalse: val ≝ Vzero I32.
    130135
    131136(* Values split into bytes.  Ideally we'd use some kind of sizeof for the
     
    140145λv. match v with
    141146[ Vundef ⇒ True
    142 | Vint _ ⇒ True
     147| Vint _ _ ⇒ True
    143148| Vfloat _ ⇒ False
    144149| Vnull r ⇒ ptr_may_be_single r = true
     
    148153definition may_be_split : val → Prop ≝
    149154λv.match v with
    150 [ Vint _ ⇒ False
     155[ Vint _ _ ⇒ False
    151156| Vnull r ⇒ ptr_may_be_single r = false
    152157| Vptr r _ _ _ ⇒ ptr_may_be_single r = false
     
    248253definition is_true : val → Prop ≝ λv.
    249254  match v with
    250   [ Vint n ⇒ n ≠ zero
     255  [ Vint _ n ⇒ n ≠ (zero ?)
    251256  | Vptr _ b _ ofs ⇒ True
    252257  | _ ⇒ False
     
    255260definition is_false : val → Prop ≝ λv.
    256261  match v with
    257   [ Vint n ⇒ n = zero
     262  [ Vint _ n ⇒ n = (zero ?)
    258263  | Vnull _ ⇒ True
    259264  | _ ⇒ False
     
    262267inductive bool_of_val: val → bool → Prop ≝
    263268  | bool_of_val_int_true:
    264       ∀n. n ≠ zero → bool_of_val (Vint n) true
     269      ∀sz,n. n ≠ zero ? → bool_of_val (Vint sz n) true
    265270  | bool_of_val_int_false:
    266       bool_of_val (Vint zero) false
     271      ∀sz. bool_of_val (Vzero sz) false
    267272  | bool_of_val_ptr:
    268273      ∀r,b,p,ofs. bool_of_val (Vptr r b p ofs) true
     
    274279definition eval_bool_of_val : val → res bool ≝
    275280λv. match v with
    276 [ Vint i ⇒ OK ? (notb (eq i zero))
     281[ Vint _ i ⇒ OK ? (notb (eq_bv ? i (zero ?)))
    277282| Vnull _ ⇒ OK ? false
    278283| Vptr _ _ _ _ ⇒ OK ? true
     
    282287definition neg : val → val ≝ λv.
    283288  match v with
    284   [ Vint n ⇒ Vint (neg n)
     289  [ Vint sz n ⇒ Vint sz (two_complement_negation ? n)
    285290  | _ ⇒ Vundef
    286291  ].
     
    298303  ].
    299304
    300 definition intoffloat : val → val ≝ λv.
    301   match v with
    302   [ Vfloat f ⇒ Vint (intoffloat f)
     305definition intoffloat : intsize → val → val ≝ λsz,v.
     306  match v with
     307  [ Vfloat f ⇒ Vint sz (intoffloat ? f)
    303308  | _ ⇒ Vundef
    304309  ].
    305310
    306 definition intuoffloat : val → val ≝ λv.
    307   match v with
    308   [ Vfloat f ⇒ Vint (intuoffloat f)
     311definition intuoffloat : intsize → val → val ≝ λsz,v.
     312  match v with
     313  [ Vfloat f ⇒ Vint sz (intuoffloat ? f)
    309314  | _ ⇒ Vundef
    310315  ].
     
    312317definition floatofint : val → val ≝ λv.
    313318  match v with
    314   [ Vint n ⇒ Vfloat (floatofint n)
     319  [ Vint sz n ⇒ Vfloat (floatofint ? n)
    315320  | _ ⇒ Vundef
    316321  ].
     
    318323definition floatofintu : val → val ≝ λv.
    319324  match v with
    320   [ Vint n ⇒ Vfloat (floatofintu n)
     325  [ Vint sz n ⇒ Vfloat (floatofintu ? n)
    321326  | _ ⇒ Vundef
    322327  ].
     
    324329definition notint : val → val ≝ λv.
    325330  match v with
    326   [ Vint n ⇒ Vint (xor n mone)
     331  [ Vint sz n ⇒ Vint sz (exclusive_disjunction_bv ? n (mone ?))
    327332  | _ ⇒ Vundef
    328333  ].
    329334 
    330 (* FIXME: switch to alias, or rename, or … *)
    331 definition int_eq : int → int → bool ≝ eq.
    332335definition notbool : val → val ≝ λv.
    333336  match v with
    334   [ Vint n ⇒ of_bool (int_eq n zero)
     337  [ Vint sz n ⇒ of_bool (eq_bv ? n (zero ?))
    335338  | Vptr _ b _ ofs ⇒ Vfalse
    336339  | Vnull _ ⇒ Vtrue
     
    338341  ].
    339342
    340 definition zero_ext ≝ λnbits: nat. λv: val.
    341   match v with
    342   [ Vint n ⇒ Vint (zero_ext nbits n)
     343definition zero_ext ≝ λrsz: intsize. λv: val.
     344  match v with
     345  [ Vint sz n ⇒ Vint rsz (zero_ext … n)
    343346  | _ ⇒ Vundef
    344347  ].
    345348
    346 definition sign_ext ≝ λnbits:nat. λv:val.
    347   match v with
    348   [ Vint i ⇒ Vint (sign_ext nbits i)
     349definition sign_ext ≝ λrsz:intsize. λv:val.
     350  match v with
     351  [ Vint sz i ⇒ Vint rsz (sign_ext … i)
    349352  | _ ⇒ Vundef
    350353  ].
     
    359362definition add ≝ λv1,v2: val.
    360363  match v1 with
    361   [ Vint n1 ⇒ match v2 with
    362     [ Vint n2 ⇒ Vint (addition_n ? n1 n2)
    363     | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1)
     364  [ Vint sz1 n1 ⇒ match v2 with
     365    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     366                    (λn1. Vint sz2 (addition_n ? n1 n2))
     367                    Vundef
     368    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ? ofs2 n1)
    364369    | _ ⇒ Vundef ]
    365370  | Vptr r b1 p ofs1 ⇒ match v2 with
    366     [ Vint n2 ⇒ Vptr r b1 p (shift_offset ofs1 n2)
    367     | _ ⇒ Vundef ]
    368   | _ ⇒ Vundef ].
     371    [ Vint _ n2 ⇒ Vptr r b1 p (shift_offset ? ofs1 n2)
     372    | _ ⇒ Vundef ]
     373  | _ ⇒ Vundef ].
     374
     375(* XXX Is I32 the best answer for ptr subtraction? *)
    369376
    370377definition sub ≝ λv1,v2: val.
    371378  match v1 with
    372   [ Vint n1 ⇒ match v2 with
    373     [ Vint n2 ⇒ Vint (subtraction ? n1 n2)
     379  [ Vint sz1 n1 ⇒ match v2 with
     380    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     381                    (λn1. Vint sz2 (subtraction ? n1 n2))
     382                    Vundef
    374383    | _ ⇒ Vundef ]
    375384  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    376     [ Vint n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ofs1 n2)
     385    [ Vint sz2 n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2)
    377386    | Vptr r2 b2 p2 ofs2 ⇒
    378         if eq_block b1 b2 then Vint (sub_offset ofs1 ofs2) else Vundef
    379     | _ ⇒ Vundef ]
    380   | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero | _ ⇒ Vundef ]
     387        if eq_block b1 b2 then Vint I32 (sub_offset ? ofs1 ofs2) else Vundef
     388    | _ ⇒ Vundef ]
     389  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vzero I32 | _ ⇒ Vundef ]
    381390  | _ ⇒ Vundef ].
    382391
    383392definition mul ≝ λv1, v2: val.
    384393  match v1 with
    385   [ Vint n1 ⇒ match v2 with
    386     [ Vint n2 ⇒ Vint (mul n1 n2)
     394  [ Vint sz1 n1 ⇒ match v2 with
     395    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     396                    (λn1. Vint sz2 (\snd (split … (multiplication ? n1 n2))))
     397                    Vundef
    387398    | _ ⇒ Vundef ]
    388399  | _ ⇒ Vundef ].
     
    418429definition v_and ≝ λv1, v2: val.
    419430  match v1 with
    420   [ Vint n1 ⇒ match v2 with
    421     [ Vint n2 ⇒ Vint (i_and n1 n2)
     431  [ Vint sz1 n1 ⇒ match v2 with
     432    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     433                    (λn1. Vint ? (conjunction_bv ? n1 n2))
     434                    Vundef
    422435    | _ ⇒ Vundef ]
    423436  | _ ⇒ Vundef ].
     
    425438definition or ≝ λv1, v2: val.
    426439  match v1 with
    427   [ Vint n1 ⇒ match v2 with
    428     [ Vint n2 ⇒ Vint (or n1 n2)
     440  [ Vint sz1 n1 ⇒ match v2 with
     441    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     442                    (λn1. Vint ? (inclusive_disjunction_bv ? n1 n2))
     443                    Vundef
    429444    | _ ⇒ Vundef ]
    430445  | _ ⇒ Vundef ].
     
    432447definition xor ≝ λv1, v2: val.
    433448  match v1 with
    434   [ Vint n1 ⇒ match v2 with
    435     [ Vint n2 ⇒ Vint (xor n1 n2)
     449  [ Vint sz1 n1 ⇒ match v2 with
     450    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     451                    (λn1. Vint ? (exclusive_disjunction_bv ? n1 n2))
     452                    Vundef
    436453    | _ ⇒ Vundef ]
    437454  | _ ⇒ Vundef ].
     
    550567  ].
    551568
     569definition cmp_int : ∀n. comparison → BitVector n → BitVector n → bool ≝
     570λn,c,x,y.
     571  match c with
     572  [ Ceq ⇒ eq_bv ? x y
     573  | Cne ⇒ notb (eq_bv ? x y)
     574  | Clt ⇒ lt_s ? x y
     575  | Cle ⇒ notb (lt_s ? y x)
     576  | Cgt ⇒ lt_s ? y x
     577  | Cge ⇒ notb (lt_s ? x y)
     578  ].
     579
     580definition cmpu_int : ∀n. comparison → BitVector n → BitVector n → bool ≝
     581λn,c,x,y.
     582  match c with
     583  [ Ceq ⇒ eq_bv ? x y
     584  | Cne ⇒ notb (eq_bv ? x y)
     585  | Clt ⇒ lt_u ? x y
     586  | Cle ⇒ notb (lt_u ? y x)
     587  | Cgt ⇒ lt_u ? y x
     588  | Cge ⇒ notb (lt_u ? x y)
     589  ].
     590
    552591definition cmp ≝ λc: comparison. λv1,v2: val.
    553592  match v1 with
    554   [ Vint n1 ⇒ match v2 with
    555     [ Vint n2 ⇒ of_bool (cmp c n1 n2)
     593  [ Vint sz1 n1 ⇒ match v2 with
     594    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     595                    (λn1. of_bool (cmp_int ? c n1 n2))
     596                    Vundef
    556597    | _ ⇒ Vundef ]
    557598  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     
    571612definition cmpu ≝ λc: comparison. λv1,v2: val.
    572613  match v1 with
    573   [ Vint n1 ⇒ match v2 with
    574     [ Vint n2 ⇒ of_bool (cmpu c n1 n2)
     614  [ Vint sz1 n1 ⇒ match v2 with
     615    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     616                    (λn1. of_bool (cmpu_int ? c n1 n2))
     617                    Vundef
    575618    | _ ⇒ Vundef ]
    576619  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     
    588631  | _ ⇒ Vundef ].
    589632
    590 definition cmpf ≝ λc: comparison. λv1,v2: val.
     633definition cmpf ≝ λc: comparison. λsz:intsize. λv1,v2: val.
    591634  match v1 with
    592635  [ Vfloat f1 ⇒ match v2 with
     
    603646  is performed and [0xFFFFFFFF] is returned.   Type mismatches
    604647  (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *)
     648(* XXX update comment *)
     649(* XXX is this even necessary now?
     650       should we be able to extract bytes? *)
    605651
    606652let rec load_result (chunk: memory_chunk) (v: val) ≝
    607653  match v with
    608   [ Vint n ⇒
     654  [ Vint sz n ⇒
    609655    match chunk with
    610     [ Mint8signed ⇒ Vint (sign_ext 8 n)
    611     | Mint8unsigned ⇒ Vint (zero_ext 8 n)
    612     | Mint16signed ⇒ Vint (sign_ext 16 n)
    613     | Mint16unsigned ⇒ Vint (zero_ext 16 n)
    614     | Mint32 ⇒ Vint n
     656    [ Mint8signed ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
     657    | Mint8unsigned ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
     658    | Mint16signed ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
     659    | Mint16unsigned ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
     660    | Mint32 ⇒  match sz with [ I32 ⇒ v | _ ⇒ Vundef ]
    615661    | _ ⇒ Vundef
    616662    ]
Note: See TracChangeset for help on using the changeset viewer.