Ignore:
Timestamp:
Feb 22, 2011, 11:35:16 AM (9 years ago)
Author:
campbell
Message:

Use bit vector operations widely instead of round-trips through Z.
Implement more efficient addition, subtraction and comparison on bit vectors.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Csem.ma

    r502 r582  
    7474  [ Tint _ _ ⇒
    7575      match v with
    76       [ Vint n ⇒ Some ? (Vint (neg n))
     76      [ Vint n ⇒ Some ? (Vint (negation_bv wordsize n))
    7777      | _ => None ?
    7878      ]
     
    8787let rec sem_notint (v: val) : option val ≝
    8888  match v with
    89   [ Vint n ⇒ Some ? (Vint (xor n mone))
     89  [ Vint n ⇒ Some ? (Vint (xor n mone)) (* XXX *)
    9090  | _ ⇒ None ?
    9191  ].
     
    117117      match v1 with
    118118      [ Vint n1 ⇒ match v2 with
    119         [ Vint n2 ⇒ Some ? (Vint (add n1 n2))
     119        [ Vint n2 ⇒ Some ? (Vint (addition_n wordsize n1 n2))
    120120        | _ ⇒ None ? ]
    121121      | _ ⇒ None ? ]
     
    149149      match v1 with
    150150      [ Vint n1 ⇒ match v2 with
    151         [ Vint n2 ⇒ Some ? (Vint (sub n1 n2))
     151        [ Vint n2 ⇒ Some ? (Vint (subtraction wordsize n1 n2))
    152152        | _ ⇒ None ? ]
    153153      | _ ⇒ None ? ]
     
    183183      match v1 with
    184184      [ Vint n1 ⇒ match v2 with
    185         [ Vint n2 ⇒ Some ? (Vint (mul n1 n2))
     185        [ Vint n2 ⇒ Some ? (Vint (\snd (split ? wordsize wordsize (multiplication ? n1 n2))))
    186186        | _ ⇒ None ? ]
    187187      | _ ⇒ None ? ]
     
    201201      match v1 with
    202202      [ Vint n1 ⇒ match v2 with
    203         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (divu n1 n2))
     203        [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)
    204204        | _ ⇒ None ? ]
    205205      | _ ⇒ None ? ]
     
    207207      match v1 with
    208208       [ Vint n1 ⇒ match v2 with
    209          [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint(divs n1 n2))
     209         [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)
    210210         | _ ⇒ None ? ]
    211211      | _ ⇒ None ? ]
     
    225225      match v1 with
    226226      [ Vint n1 ⇒ match v2 with
    227         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (modu n1 n2))
     227        [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)
    228228        | _ ⇒ None ? ]
    229229      | _ ⇒ None ? ]
     
    231231      match v1 with
    232232      [ Vint n1 ⇒ match v2 with
    233         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (mods n1 n2))
     233        [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)
    234234        | _ ⇒ None ? ]
    235235      | _ ⇒ None ? ]
     
    241241  match v1 with
    242242  [ Vint n1 ⇒ match v2 with
    243     [ Vint n2 ⇒ Some ? (Vint(i_and n1 n2))
     243    [ Vint n2 ⇒ Some ? (Vint (conjunction_bv ? n1 n2))
    244244    | _ ⇒ None ? ]
    245245  | _ ⇒ None ?
     
    249249  match v1 with
    250250  [ Vint n1 ⇒ match v2 with
    251     [ Vint n2 ⇒ Some ? (Vint(or n1 n2))
     251    [ Vint n2 ⇒ Some ? (Vint (inclusive_disjunction_bv ? n1 n2))
    252252    | _ ⇒ None ? ]
    253253  | _ ⇒ None ?
     
    257257  match v1 with
    258258  [ Vint n1 ⇒ match v2 with
    259     [ Vint n2 ⇒ Some ? (Vint(xor n1 n2))
     259    [ Vint n2 ⇒ Some ? (Vint (exclusive_disjunction_bv ? n1 n2))
    260260    | _ ⇒ None ? ]
    261261  | _ ⇒ None ?
Note: See TracChangeset for help on using the changeset viewer.