Changeset 744 for src/Clight/Csem.ma


Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (9 years ago)
Author:
campbell
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r725 r744  
    170170          if eq_block b1 b2 then
    171171            if eq (repr (sizeof ty)) zero then None ?
    172             else Some ? (Vint (divu (sub_offset ofs1 ofs2) (repr (sizeof ty))))
     172            else match division_u ? (sub_offset ofs1 ofs2) (repr (sizeof ty)) with
     173                 [ None ⇒ None ?
     174                 | Some v ⇒ Some ? (Vint v)
     175                 ]
    173176          else None ?
    174177        | _ ⇒ None ? ]
     
    202205      match v1 with
    203206      [ Vint n1 ⇒ match v2 with
    204         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (divu n1 n2))
    205 (*        [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)*)
     207        [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)
    206208        | _ ⇒ None ? ]
    207209      | _ ⇒ None ? ]
     
    209211      match v1 with
    210212       [ Vint n1 ⇒ match v2 with
    211          [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint(divs n1 n2))
    212 (*         [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)*)
     213         [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)
    213214         | _ ⇒ None ? ]
    214215      | _ ⇒ None ? ]
     
    228229      match v1 with
    229230      [ Vint n1 ⇒ match v2 with
    230         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (modu n1 n2))
    231 (*        [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)*)
     231        [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)
    232232        | _ ⇒ None ? ]
    233233      | _ ⇒ None ? ]
     
    235235      match v1 with
    236236      [ Vint n1 ⇒ match v2 with
    237         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (mods n1 n2))
    238 (*        [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)*)
     237        [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)
    239238        | _ ⇒ None ? ]
    240239      | _ ⇒ None ? ]
Note: See TracChangeset for help on using the changeset viewer.