Ignore:
Timestamp:
Mar 2, 2011, 3:27:41 PM (9 years ago)
Author:
ayache
Message:

Update of D2.2 from Paris.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/common/intValue.ml

    r486 r619  
     1
     2(** This module defines functions to manipulate bounded integers. They can be
     3    used to represent sequences of bits. *)
    14
    25open Big_int
    36
    47
     8(* Integers, whatever their size, will be represented using the Big_int
     9   module. This allows immediate conversion, and allows the representation of
     10   any integer (that fits into memory). *)
     11
    512type int_repr = Big_int.big_int
    613
     14(* The parameter module. Bounded integers are characterized by the number of
     15   bits used to represent them. *)
     16   
    717module type INTTYPE =
    818sig
    9   val size      : int (* in bytes *)
    10   val is_signed : bool
     19  val size : int (* in bytes *)
    1120end
     21
     22(* The signature provided to manipulate bounded integers. *)
    1223
    1324module type S = sig
     
    2031  val one       : t
    2132
    22   val succ   : t -> t
    23   val pred   : t -> t
    24   val add    : t -> t -> t
    25   (** [add_of i1 i2] returns true iff adding the unsigned value of [i1] and the
    26       unsigned value of [i2] overflows. *)
    27   val add_of : t -> t -> bool
    28   val sub    : t -> t -> t
    29   (** [sub_of i1 i2] returns true iff substracting the unsigned value of [i1]
    30       and the unsigned value of [i2] underflows. *)
    31   val sub_of : t -> t -> bool
    32   val mul    : t -> t -> t
    33   val div    : t -> t -> t
    34   val modulo : t -> t -> t
    35   val eq     : t -> t -> bool
    36   val neq    : t -> t -> bool
    37   val lt     : t -> t -> bool
    38   val le     : t -> t -> bool
    39   val gt     : t -> t -> bool
    40   val ge     : t -> t -> bool
    41   val neg    : t -> t
    42   val lognot : t -> t
    43   val logand : t -> t -> t
    44   val logor  : t -> t -> t
    45   val logxor : t -> t -> t
    46   val shl    : t -> t -> t
    47   val shr    : t -> t -> t
    48   val shrl   : t -> t -> t
    49   val max    : t -> t -> t
    50   val min    : t -> t -> t
    51   val cast   : int_repr -> t
    52   val of_int : int -> t
    53   val to_int : t -> int
     33  val succ    : t -> t
     34  val pred    : t -> t
     35  val add     : t -> t -> t
     36  (** [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *)
     37  val add_of  : t -> t -> bool
     38  val sub     : t -> t -> t
     39  (** [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2]
     40      underflows. *)
     41  val sub_uf  : t -> t -> bool
     42  val mul     : t -> t -> t
     43  val div     : t -> t -> t
     44  val divu    : t -> t -> t
     45  val modulo  : t -> t -> t
     46  val modulou : t -> t -> t
     47  val eq      : t -> t -> bool
     48  val neq     : t -> t -> bool
     49  val lt      : t -> t -> bool
     50  val ltu     : t -> t -> bool
     51  val le      : t -> t -> bool
     52  val leu     : t -> t -> bool
     53  val gt      : t -> t -> bool
     54  val gtu     : t -> t -> bool
     55  val ge      : t -> t -> bool
     56  val geu     : t -> t -> bool
     57  val neg     : t -> t
     58  val lognot  : t -> t
     59  val logand  : t -> t -> t
     60  val logor   : t -> t -> t
     61  val logxor  : t -> t -> t
     62  val shl     : t -> t -> t
     63  val shr     : t -> t -> t
     64  val shrl    : t -> t -> t
     65  val max     : t -> t -> t
     66  val maxu    : t -> t -> t
     67  val min     : t -> t -> t
     68  val minu    : t -> t -> t
     69  val cast    : int_repr -> t
     70  val of_int  : int -> t
     71  val to_int  : t -> int
     72
     73  (** [zero_ext n a] performs zero extension on [a] where [n] bits are
     74      significant. *)
     75  val zero_ext : int -> t -> t
     76  (** [sign_ext n a] performs sign extension on [a] where [n] bits are
     77      significant. *)
     78  val sign_ext : int -> t -> t
    5479
    5580  (** [break i n] cuts [i] in [n] parts. In the resulting list, the first
    5681      element is the high bits, and the last is the low bits. *)
    5782  val break : t -> int -> t list
    58   (** [merge l] creates an the integer where the first element of [l] is its
     83  (** [merge l] creates the integer where the first element of [l] is its
    5984      high bits, etc, and the last element of [l] is its low bits. *)
    6085  val merge : t list -> t
     
    6388
    6489
    65 (* First, we use a parameter module and a functor where integers may be
    66    unbounded. This will allow to create the Integer module (unbounded integers)
    67    as well as bounded integers. *)
    68 
    69 module type INTTYPE_ARB =
    70 sig
    71   val size      : int
    72   val is_signed : bool
    73   val arbitrary : bool
    74 end
    75 
    76 (* The following functor works for unbounded integers as well as for bounded
    77    intergers. *)
    78 
    79 module Make_Arb (IntType: INTTYPE_ARB) : S =
     90module Make (IntType: INTTYPE) : S =
    8091struct
    8192
     
    90101  let two = succ_big_int unit_big_int
    91102
    92   let half_bound = power_int_positive_int 2 (size-1)
    93 
    94   (* The upper bound of signed integers. *)
    95   let shbound = half_bound
    96   (* The lower bound of signed integers. *)
    97   let slbound = minus_big_int half_bound
    98 
    99   (* The upper bound of unsigned integers. *)
    100   let uhbound = mult_int_big_int 2 half_bound
    101   (* The lower bound of unsigned integers. *)
    102   let ulbound = zero
    103 
    104   (* [unsign a] returns the unsigned value of [a]. *)
    105   let unsign a =
    106     if lt_big_int a zero_big_int then add_big_int uhbound a
    107     else a
    108 
    109   (* [is_in_repr a] returns true iff [a] is a value comprised in the interval of
    110      representation. *)
    111   let is_in_repr a =
    112     if IntType.is_signed then (le_big_int slbound a) && (lt_big_int a shbound)
    113     else (le_big_int ulbound a) && (lt_big_int a uhbound)
     103  (* Integers will all be taken modulo the following value. *)
     104  let _mod = power_int_positive_int 2 size
     105
     106  (* The lower bound (inclusive). *)
     107  let lower_bound = zero
     108  (* The upper bound (inclusive). *)
     109  let upper_bound = pred_big_int _mod
    114110
    115111  (* [cast a] returns a modulo of [a] such that the result fits in the interval
    116112     of representation. *)
    117   let cast a =
    118     if IntType.arbitrary then a
    119     else
    120       if is_in_repr a then a
    121       else
    122         if IntType.is_signed then
    123           sub_big_int
    124             (mod_big_int (add_big_int a half_bound) uhbound)
    125             half_bound
    126         else mod_big_int a uhbound
     113  let cast a = mod_big_int a _mod
     114
     115  (* Half bound (exclusive), i.e. upper bound of signed integers. *)
     116  let half_bound = power_int_positive_int 2 (size-1)
     117
     118  (* Signed value of [a]. *)
     119  let signed a = sub_big_int (cast a) half_bound
     120
     121  let signed_op op a b = op (signed a) (signed b)
    127122
    128123  let succ a = cast (succ_big_int a)
     
    130125  let add a b = cast (add_big_int a b)
    131126
    132   (* [add_of i1 i2] returns true iff adding the unsigned value of [i1] and the
    133      unsigned value of [i2] overflows. *)
    134   let add_of a b =
    135     let u1 = unsign a in
    136     let u2 = unsign b in
    137     let i = add_big_int u1 u2 in
    138     ge_big_int i uhbound
     127  (* [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *)
     128  let add_of a b = gt_big_int (add_big_int a b) upper_bound
    139129
    140130  let sub a b = cast (sub_big_int a b)
    141131
    142   (* [sub_of i1 i2] returns true iff substracting the unsigned value of [i1] and
    143      the unsigned value of [i2] underflows. *)
    144   let sub_of a b =
    145     let u1 = unsign a in
    146     let u2 = unsign b in
    147     let i = sub_big_int u1 u2 in
    148     lt_big_int i zero_big_int
     132  let cast_op op a b = op (cast a) (cast b)
    149133
    150134  let mul a b = cast (mult_big_int a b)
    151   let div a b = cast (div_big_int a b)
    152   let modulo a b = cast (mod_big_int a b)
     135  let div a b = cast (signed_op div_big_int a b)
     136  let divu a b = cast_op div_big_int a b
     137  let modulo a b = cast (signed_op mod_big_int a b)
     138  let modulou a b = cast_op mod_big_int a b
     139
    153140  let eq = eq_big_int
    154141  let neq a b = not (eq a b)
    155   let lt a b = lt_big_int (cast a) (cast b)
    156   let le a b = le_big_int (cast a) (cast b)
    157   let gt a b = gt_big_int (cast a) (cast b)
    158   let ge a b = ge_big_int (cast a) (cast b)
     142  let lt a b = signed_op lt_big_int a b
     143  let le a b = signed_op le_big_int a b
     144  let gt a b = signed_op gt_big_int a b
     145  let ge a b = signed_op ge_big_int a b
     146  let ltu a b = cast_op lt_big_int a b
     147  let leu a b = cast_op le_big_int a b
     148  let gtu a b = cast_op gt_big_int a b
     149  let geu a b = cast_op ge_big_int a b
     150
     151  (* [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2] underflows. *)
     152  let sub_uf a b = lt_big_int (sub_big_int a b) zero
     153
    159154  let of_int i = cast (big_int_of_int i)
    160   let to_int i = int_of_big_int i
     155  let to_int i = int_of_big_int (cast i)
     156
    161157  let neg a = cast (minus_big_int a)
    162158
    163   let lognot a =
    164     let mone = minus_big_int unit_big_int in
    165     if IntType.is_signed then sub mone a
    166     else sub (pred uhbound) a
     159  let lognot = sub upper_bound
    167160
    168161  let shl a b =
    169     let pow = power_int_positive_big_int 2 b in
     162    let pow = power_int_positive_big_int 2 (cast b) in
    170163    cast (mult_big_int a pow)
    171164
    172165  let shr a b =
    173     let pow = power_int_positive_big_int 2 b in
    174     cast (div_big_int a pow)
    175 
    176   let shrl a b =
     166    let a = cast a in
     167    let b = cast b in
    177168    let added =
    178       if IntType.is_signed || (lt_big_int b half_bound) then zero_big_int
     169      if lt_big_int a half_bound then zero
    179170      else half_bound in
    180171    let rec aux acc b =
    181       if eq_big_int b zero_big_int then acc
     172      if eq b zero then acc
    182173      else
    183         let cont_acc = add_big_int added (div_big_int acc two) in
    184         let cont_b = pred_big_int b in
     174        let cont_acc = add added (divu acc two) in
     175        let cont_b = pred b in
    185176        aux cont_acc cont_b
    186177    in
    187178    cast (aux a b)
     179
     180  let shrl a b =
     181    let pow = power_int_positive_big_int 2 (cast b) in
     182    cast (div_big_int (cast a) pow)
    188183
    189184  let max a b = if lt a b then b else a
    190185  let min a b = if gt a b then b else a
    191 
    192   let is_odd a = eq_big_int (mod_big_int a two) unit_big_int
    193   (* [to_bits a] returns the list of bits (0 or 1) that a represents. Signed
    194      integers are represented using the 2-complement representation. *)
     186  let maxu a b = if ltu a b then b else a
     187  let minu a b = if gtu a b then b else a
     188
     189  let is_odd a = eq (modulou a two) one
     190  (* [to_bits a] returns the list of bits (0 or 1) that [a] represents. *)
    195191  let to_bits a =
    196192    let rec aux acc a i =
    197193      if i >= size then acc
    198       else aux ((is_odd a) :: acc) (div_big_int a two) (i+1)
    199     in
    200     aux [] a 0
     194      else aux ((is_odd a) :: acc) (divu a two) (i+1)
     195    in
     196    aux [] (cast a) 0
    201197
    202198  (* [from_bits bits] returns the integer that the list of bits [bits]
    203      represents. Signed integers are represented using the 2-complement
    204      representation. *)
     199     represents. *)
    205200  let from_bits bits =
    206201    let rec aux acc = function
    207202      | [] -> acc
    208203      | b :: bits ->
    209         let next_acc = mult_int_big_int 2 acc in
    210         let next_acc = if b then succ_big_int next_acc else next_acc in
     204        let next_acc = mul acc two in
     205        let next_acc = if b then succ next_acc else next_acc in
    211206        aux next_acc bits
    212207    in
    213     cast (aux zero_big_int bits)
     208    aux zero bits
    214209
    215210  (* [binary_log_op f a b] applies the binary boolean operation [f]
     
    224219  let logxor = binary_log_op xor
    225220
     221
     222  (* [zero_ext n a] performs zero extension on [a] where [n] bits are
     223     significant. *)
     224  let zero_ext n a =
     225    let pow2 = power_int_positive_int 2 n in
     226    cast (mod_big_int a pow2)
     227
     228  (* [sign_ext n a] performs sign extension on [a] where [n] bits are
     229     significant. *)
     230  let sign_ext n a =
     231    let a' = zero_ext n a in
     232    let pow2 = power_int_positive_int 2 (n-1) in
     233    let sign = divu a pow2 in
     234    if is_odd sign then
     235      let added = shr half_bound (of_int (n-1)) in
     236      add a' added
     237    else a'
     238
     239
    226240  (* [break i n] cuts [i] in [n] parts. In the resulting list, the first element
    227241     is the high bits, and the last is the low bits. *)
    228242  let break a n =
    229     let chunk_size = (8 * IntType.size) / n in
     243    let chunk_size = size / n in
    230244    let pow2_chunk_size = power_int_positive_int 2 chunk_size in
    231245    let rec aux acc a i =
    232246      if i = 0 then acc
    233247      else
    234         let (next, chunk) = Big_int.quomod_big_int a pow2_chunk_size in
     248        let (next, chunk) = quomod_big_int a pow2_chunk_size in
    235249        aux ((cast chunk) :: acc) next (i-1)
    236250    in
    237     aux [] a n
     251    aux [] (cast a) n
    238252
    239253  (* [merge l] creates the integer where the first element of [l] is its high
     
    244258      let al = List.rev al in
    245259      let nb_chunks = List.length al in
    246       let chunk_size = (8 * IntType.size) / nb_chunks in
     260      let chunk_size = size / nb_chunks in
    247261      let pow2_chunk_size = power_int_positive_int 2 chunk_size in
    248262      let rec aux pow2 = function
     
    255269
    256270
    257 module Make (IntType : INTTYPE) =
    258   Make_Arb (struct include IntType let arbitrary = false end)
    259 
    260 
    261 module Int8s : S = Make
    262   (struct
    263     let size = 1
    264     let is_signed = true
    265    end)
    266 
    267 module Int8u : S = Make
    268   (struct
    269     let size = 1
    270     let is_signed = false
    271    end)
    272 
    273 module Int16s : S = Make
    274   (struct
    275     let size = 2
    276     let is_signed = true
    277    end)
    278 
    279 module Int16u : S = Make
    280   (struct
    281     let size = 2
    282     let is_signed = false
    283    end)
    284 
    285 module Int32 : S = Make
    286   (struct
    287     let size = 4
    288     let is_signed = true
    289    end)
    290 
    291 module Integer : S = Make_Arb
    292   (struct
    293     let size = 1
    294     let is_signed = true
    295     let arbitrary = true
    296    end)
    297 
    298 
    299 type int8s   = Int8s.t
    300 type int8u   = Int8u.t
    301 type int16s  = Int16s.t
    302 type int16u  = Int16u.t
    303 type int32   = Int32.t
    304 type integer = Integer.t
     271module Int8  : S = Make (struct let size = 1 end)
     272module Int16 : S = Make (struct let size = 2 end)
     273module Int32 : S = Make (struct let size = 4 end)
     274
     275type int8  = Int8.t
     276type int16 = Int16.t
     277type int32 = Int32.t
Note: See TracChangeset for help on using the changeset viewer.