[486] | 1 | |
---|
[619] | 2 | (** This module defines functions to manipulate bounded integers. They can be |
---|
| 3 | used to represent sequences of bits. *) |
---|
| 4 | |
---|
[486] | 5 | open Big_int |
---|
| 6 | |
---|
| 7 | |
---|
[619] | 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 | |
---|
[486] | 12 | type int_repr = Big_int.big_int |
---|
| 13 | |
---|
[818] | 14 | let print_int_repr = Big_int.string_of_big_int |
---|
| 15 | |
---|
[619] | 16 | (* The parameter module. Bounded integers are characterized by the number of |
---|
| 17 | bits used to represent them. *) |
---|
| 18 | |
---|
[486] | 19 | module type INTTYPE = |
---|
| 20 | sig |
---|
[619] | 21 | val size : int (* in bytes *) |
---|
[486] | 22 | end |
---|
| 23 | |
---|
[619] | 24 | (* The signature provided to manipulate bounded integers. *) |
---|
| 25 | |
---|
[486] | 26 | module type S = sig |
---|
| 27 | |
---|
| 28 | type t = Big_int.big_int |
---|
| 29 | |
---|
| 30 | val compare : t -> t -> int |
---|
| 31 | val to_string : t -> string |
---|
| 32 | val zero : t |
---|
| 33 | val one : t |
---|
| 34 | |
---|
[818] | 35 | val to_signed_int_repr : t -> int_repr |
---|
| 36 | val to_unsigned_int_repr : t -> int_repr |
---|
| 37 | |
---|
[619] | 38 | val succ : t -> t |
---|
| 39 | val pred : t -> t |
---|
| 40 | val add : t -> t -> t |
---|
| 41 | (** [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *) |
---|
| 42 | val add_of : t -> t -> bool |
---|
| 43 | val sub : t -> t -> t |
---|
| 44 | (** [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2] |
---|
| 45 | underflows. *) |
---|
| 46 | val sub_uf : t -> t -> bool |
---|
| 47 | val mul : t -> t -> t |
---|
| 48 | val div : t -> t -> t |
---|
| 49 | val divu : t -> t -> t |
---|
| 50 | val modulo : t -> t -> t |
---|
| 51 | val modulou : t -> t -> t |
---|
| 52 | val eq : t -> t -> bool |
---|
| 53 | val neq : t -> t -> bool |
---|
| 54 | val lt : t -> t -> bool |
---|
| 55 | val ltu : t -> t -> bool |
---|
| 56 | val le : t -> t -> bool |
---|
| 57 | val leu : t -> t -> bool |
---|
| 58 | val gt : t -> t -> bool |
---|
| 59 | val gtu : t -> t -> bool |
---|
| 60 | val ge : t -> t -> bool |
---|
| 61 | val geu : t -> t -> bool |
---|
| 62 | val neg : t -> t |
---|
| 63 | val lognot : t -> t |
---|
| 64 | val logand : t -> t -> t |
---|
| 65 | val logor : t -> t -> t |
---|
| 66 | val logxor : t -> t -> t |
---|
| 67 | val shl : t -> t -> t |
---|
| 68 | val shr : t -> t -> t |
---|
| 69 | val shrl : t -> t -> t |
---|
| 70 | val max : t -> t -> t |
---|
| 71 | val maxu : t -> t -> t |
---|
| 72 | val min : t -> t -> t |
---|
| 73 | val minu : t -> t -> t |
---|
| 74 | val cast : int_repr -> t |
---|
| 75 | val of_int : int -> t |
---|
| 76 | val to_int : t -> int |
---|
[486] | 77 | |
---|
[619] | 78 | (** [zero_ext n a] performs zero extension on [a] where [n] bits are |
---|
| 79 | significant. *) |
---|
| 80 | val zero_ext : int -> t -> t |
---|
| 81 | (** [sign_ext n a] performs sign extension on [a] where [n] bits are |
---|
| 82 | significant. *) |
---|
| 83 | val sign_ext : int -> t -> t |
---|
| 84 | |
---|
[486] | 85 | (** [break i n] cuts [i] in [n] parts. In the resulting list, the first |
---|
[740] | 86 | element is the low bits, and the last is the high bits (little endian |
---|
| 87 | representation). *) |
---|
[486] | 88 | val break : t -> int -> t list |
---|
[818] | 89 | (** [merge l] creates the integer where the first element of [l] is its low |
---|
| 90 | bits, etc, and the last element of [l] is its high bits (little endian |
---|
[740] | 91 | representation). *) |
---|
[486] | 92 | val merge : t list -> t |
---|
| 93 | |
---|
| 94 | end |
---|
| 95 | |
---|
| 96 | |
---|
[619] | 97 | module Make (IntType: INTTYPE) : S = |
---|
[486] | 98 | struct |
---|
| 99 | |
---|
| 100 | type t = Big_int.big_int |
---|
| 101 | |
---|
| 102 | let size = IntType.size * 8 (* real size, i.e. in bits *) |
---|
| 103 | |
---|
| 104 | let compare = compare_big_int |
---|
| 105 | let to_string = string_of_big_int |
---|
| 106 | let zero = zero_big_int |
---|
| 107 | let one = unit_big_int |
---|
| 108 | let two = succ_big_int unit_big_int |
---|
| 109 | |
---|
[619] | 110 | (* Integers will all be taken modulo the following value. *) |
---|
| 111 | let _mod = power_int_positive_int 2 size |
---|
[486] | 112 | |
---|
[619] | 113 | (* The lower bound (inclusive). *) |
---|
| 114 | let lower_bound = zero |
---|
| 115 | (* The upper bound (inclusive). *) |
---|
| 116 | let upper_bound = pred_big_int _mod |
---|
[486] | 117 | |
---|
[619] | 118 | (* [cast a] returns a modulo of [a] such that the result fits in the interval |
---|
| 119 | of representation. *) |
---|
| 120 | let cast a = mod_big_int a _mod |
---|
[486] | 121 | |
---|
[619] | 122 | (* Half bound (exclusive), i.e. upper bound of signed integers. *) |
---|
| 123 | let half_bound = power_int_positive_int 2 (size-1) |
---|
[486] | 124 | |
---|
[619] | 125 | (* Signed value of [a]. *) |
---|
[630] | 126 | let signed a = |
---|
| 127 | let a = cast a in |
---|
| 128 | if lt_big_int a half_bound then a |
---|
| 129 | else sub_big_int a _mod |
---|
[486] | 130 | |
---|
[818] | 131 | let to_signed_int_repr a = signed a |
---|
| 132 | |
---|
| 133 | let to_unsigned_int_repr a = a |
---|
| 134 | |
---|
[619] | 135 | let signed_op op a b = op (signed a) (signed b) |
---|
[486] | 136 | |
---|
| 137 | let succ a = cast (succ_big_int a) |
---|
| 138 | let pred a = cast (pred_big_int a) |
---|
| 139 | let add a b = cast (add_big_int a b) |
---|
| 140 | |
---|
[619] | 141 | (* [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *) |
---|
| 142 | let add_of a b = gt_big_int (add_big_int a b) upper_bound |
---|
[486] | 143 | |
---|
| 144 | let sub a b = cast (sub_big_int a b) |
---|
| 145 | |
---|
[619] | 146 | let cast_op op a b = op (cast a) (cast b) |
---|
[486] | 147 | |
---|
| 148 | let mul a b = cast (mult_big_int a b) |
---|
[619] | 149 | let div a b = cast (signed_op div_big_int a b) |
---|
| 150 | let divu a b = cast_op div_big_int a b |
---|
| 151 | let modulo a b = cast (signed_op mod_big_int a b) |
---|
| 152 | let modulou a b = cast_op mod_big_int a b |
---|
| 153 | |
---|
[486] | 154 | let eq = eq_big_int |
---|
| 155 | let neq a b = not (eq a b) |
---|
[619] | 156 | let lt a b = signed_op lt_big_int a b |
---|
| 157 | let le a b = signed_op le_big_int a b |
---|
| 158 | let gt a b = signed_op gt_big_int a b |
---|
| 159 | let ge a b = signed_op ge_big_int a b |
---|
| 160 | let ltu a b = cast_op lt_big_int a b |
---|
| 161 | let leu a b = cast_op le_big_int a b |
---|
| 162 | let gtu a b = cast_op gt_big_int a b |
---|
| 163 | let geu a b = cast_op ge_big_int a b |
---|
| 164 | |
---|
| 165 | (* [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2] underflows. *) |
---|
| 166 | let sub_uf a b = lt_big_int (sub_big_int a b) zero |
---|
| 167 | |
---|
[486] | 168 | let of_int i = cast (big_int_of_int i) |
---|
[619] | 169 | let to_int i = int_of_big_int (cast i) |
---|
| 170 | |
---|
[486] | 171 | let neg a = cast (minus_big_int a) |
---|
| 172 | |
---|
[619] | 173 | let lognot = sub upper_bound |
---|
[486] | 174 | |
---|
| 175 | let shl a b = |
---|
[619] | 176 | let pow = power_int_positive_big_int 2 (cast b) in |
---|
[486] | 177 | cast (mult_big_int a pow) |
---|
| 178 | |
---|
| 179 | let shr a b = |
---|
[619] | 180 | let a = cast a in |
---|
| 181 | let b = cast b in |
---|
[486] | 182 | let added = |
---|
[619] | 183 | if lt_big_int a half_bound then zero |
---|
[486] | 184 | else half_bound in |
---|
| 185 | let rec aux acc b = |
---|
[619] | 186 | if eq b zero then acc |
---|
[486] | 187 | else |
---|
[619] | 188 | let cont_acc = add added (divu acc two) in |
---|
| 189 | let cont_b = pred b in |
---|
[486] | 190 | aux cont_acc cont_b |
---|
| 191 | in |
---|
| 192 | cast (aux a b) |
---|
| 193 | |
---|
[619] | 194 | let shrl a b = |
---|
| 195 | let pow = power_int_positive_big_int 2 (cast b) in |
---|
| 196 | cast (div_big_int (cast a) pow) |
---|
| 197 | |
---|
[486] | 198 | let max a b = if lt a b then b else a |
---|
| 199 | let min a b = if gt a b then b else a |
---|
[619] | 200 | let maxu a b = if ltu a b then b else a |
---|
| 201 | let minu a b = if gtu a b then b else a |
---|
[486] | 202 | |
---|
[619] | 203 | let is_odd a = eq (modulou a two) one |
---|
| 204 | (* [to_bits a] returns the list of bits (0 or 1) that [a] represents. *) |
---|
[486] | 205 | let to_bits a = |
---|
| 206 | let rec aux acc a i = |
---|
| 207 | if i >= size then acc |
---|
[619] | 208 | else aux ((is_odd a) :: acc) (divu a two) (i+1) |
---|
[486] | 209 | in |
---|
[619] | 210 | aux [] (cast a) 0 |
---|
[486] | 211 | |
---|
| 212 | (* [from_bits bits] returns the integer that the list of bits [bits] |
---|
[619] | 213 | represents. *) |
---|
[486] | 214 | let from_bits bits = |
---|
| 215 | let rec aux acc = function |
---|
| 216 | | [] -> acc |
---|
| 217 | | b :: bits -> |
---|
[619] | 218 | let next_acc = mul acc two in |
---|
| 219 | let next_acc = if b then succ next_acc else next_acc in |
---|
[486] | 220 | aux next_acc bits |
---|
| 221 | in |
---|
[619] | 222 | aux zero bits |
---|
[486] | 223 | |
---|
| 224 | (* [binary_log_op f a b] applies the binary boolean operation [f] |
---|
| 225 | pointwisely to the bits that [a] and [b] represent. *) |
---|
| 226 | let binary_log_op f a b = |
---|
| 227 | from_bits (List.map2 f (to_bits a) (to_bits b)) |
---|
| 228 | |
---|
| 229 | let xor a b = (a || b) && (not (a && b)) |
---|
| 230 | |
---|
| 231 | let logand = binary_log_op (&&) |
---|
| 232 | let logor = binary_log_op (||) |
---|
| 233 | let logxor = binary_log_op xor |
---|
| 234 | |
---|
[619] | 235 | |
---|
| 236 | (* [zero_ext n a] performs zero extension on [a] where [n] bits are |
---|
| 237 | significant. *) |
---|
| 238 | let zero_ext n a = |
---|
| 239 | let pow2 = power_int_positive_int 2 n in |
---|
| 240 | cast (mod_big_int a pow2) |
---|
| 241 | |
---|
| 242 | (* [sign_ext n a] performs sign extension on [a] where [n] bits are |
---|
| 243 | significant. *) |
---|
| 244 | let sign_ext n a = |
---|
| 245 | let a' = zero_ext n a in |
---|
| 246 | let pow2 = power_int_positive_int 2 (n-1) in |
---|
| 247 | let sign = divu a pow2 in |
---|
| 248 | if is_odd sign then |
---|
| 249 | let added = shr half_bound (of_int (n-1)) in |
---|
| 250 | add a' added |
---|
| 251 | else a' |
---|
| 252 | |
---|
| 253 | |
---|
[486] | 254 | (* [break i n] cuts [i] in [n] parts. In the resulting list, the first element |
---|
[740] | 255 | is the low bits, and the last is the high bits (little endian |
---|
| 256 | representation). *) |
---|
[486] | 257 | let break a n = |
---|
[619] | 258 | let chunk_size = size / n in |
---|
[486] | 259 | let pow2_chunk_size = power_int_positive_int 2 chunk_size in |
---|
| 260 | let rec aux acc a i = |
---|
| 261 | if i = 0 then acc |
---|
| 262 | else |
---|
[619] | 263 | let (next, chunk) = quomod_big_int a pow2_chunk_size in |
---|
[486] | 264 | aux ((cast chunk) :: acc) next (i-1) |
---|
| 265 | in |
---|
[740] | 266 | List.rev (aux [] (cast a) n) |
---|
[486] | 267 | |
---|
[740] | 268 | (* [merge l] creates the integer where the first element of [l] is its low |
---|
| 269 | bits, etc, and the last element of [l] is its high bits (little endian |
---|
| 270 | representation). *) |
---|
[486] | 271 | let merge = function |
---|
| 272 | | [] -> zero |
---|
| 273 | | al -> |
---|
| 274 | let nb_chunks = List.length al in |
---|
[619] | 275 | let chunk_size = size / nb_chunks in |
---|
[486] | 276 | let pow2_chunk_size = power_int_positive_int 2 chunk_size in |
---|
| 277 | let rec aux pow2 = function |
---|
| 278 | | [] -> zero |
---|
| 279 | | a :: al -> add (mul a pow2) (aux (mul pow2 pow2_chunk_size) al) |
---|
| 280 | in |
---|
| 281 | aux one al |
---|
| 282 | |
---|
| 283 | end |
---|
| 284 | |
---|
| 285 | |
---|
[619] | 286 | module Int8 : S = Make (struct let size = 1 end) |
---|
| 287 | module Int16 : S = Make (struct let size = 2 end) |
---|
| 288 | module Int32 : S = Make (struct let size = 4 end) |
---|
[486] | 289 | |
---|
[619] | 290 | type int8 = Int8.t |
---|
| 291 | type int16 = Int16.t |
---|
| 292 | type int32 = Int32.t |
---|