[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 | |
---|
[619] | 14 | (* The parameter module. Bounded integers are characterized by the number of |
---|
| 15 | bits used to represent them. *) |
---|
| 16 | |
---|
[486] | 17 | module type INTTYPE = |
---|
| 18 | sig |
---|
[619] | 19 | val size : int (* in bytes *) |
---|
[486] | 20 | end |
---|
| 21 | |
---|
[619] | 22 | (* The signature provided to manipulate bounded integers. *) |
---|
| 23 | |
---|
[486] | 24 | module type S = sig |
---|
| 25 | |
---|
| 26 | type t = Big_int.big_int |
---|
| 27 | |
---|
| 28 | val compare : t -> t -> int |
---|
| 29 | val to_string : t -> string |
---|
| 30 | val zero : t |
---|
| 31 | val one : t |
---|
| 32 | |
---|
[619] | 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 |
---|
[486] | 72 | |
---|
[619] | 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 |
---|
| 79 | |
---|
[486] | 80 | (** [break i n] cuts [i] in [n] parts. In the resulting list, the first |
---|
| 81 | element is the high bits, and the last is the low bits. *) |
---|
| 82 | val break : t -> int -> t list |
---|
[619] | 83 | (** [merge l] creates the integer where the first element of [l] is its |
---|
[486] | 84 | high bits, etc, and the last element of [l] is its low bits. *) |
---|
| 85 | val merge : t list -> t |
---|
| 86 | |
---|
| 87 | end |
---|
| 88 | |
---|
| 89 | |
---|
[619] | 90 | module Make (IntType: INTTYPE) : S = |
---|
[486] | 91 | struct |
---|
| 92 | |
---|
| 93 | type t = Big_int.big_int |
---|
| 94 | |
---|
| 95 | let size = IntType.size * 8 (* real size, i.e. in bits *) |
---|
| 96 | |
---|
| 97 | let compare = compare_big_int |
---|
| 98 | let to_string = string_of_big_int |
---|
| 99 | let zero = zero_big_int |
---|
| 100 | let one = unit_big_int |
---|
| 101 | let two = succ_big_int unit_big_int |
---|
| 102 | |
---|
[619] | 103 | (* Integers will all be taken modulo the following value. *) |
---|
| 104 | let _mod = power_int_positive_int 2 size |
---|
[486] | 105 | |
---|
[619] | 106 | (* The lower bound (inclusive). *) |
---|
| 107 | let lower_bound = zero |
---|
| 108 | (* The upper bound (inclusive). *) |
---|
| 109 | let upper_bound = pred_big_int _mod |
---|
[486] | 110 | |
---|
[619] | 111 | (* [cast a] returns a modulo of [a] such that the result fits in the interval |
---|
| 112 | of representation. *) |
---|
| 113 | let cast a = mod_big_int a _mod |
---|
[486] | 114 | |
---|
[619] | 115 | (* Half bound (exclusive), i.e. upper bound of signed integers. *) |
---|
| 116 | let half_bound = power_int_positive_int 2 (size-1) |
---|
[486] | 117 | |
---|
[619] | 118 | (* Signed value of [a]. *) |
---|
| 119 | let signed a = sub_big_int (cast a) half_bound |
---|
[486] | 120 | |
---|
[619] | 121 | let signed_op op a b = op (signed a) (signed b) |
---|
[486] | 122 | |
---|
| 123 | let succ a = cast (succ_big_int a) |
---|
| 124 | let pred a = cast (pred_big_int a) |
---|
| 125 | let add a b = cast (add_big_int a b) |
---|
| 126 | |
---|
[619] | 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 |
---|
[486] | 129 | |
---|
| 130 | let sub a b = cast (sub_big_int a b) |
---|
| 131 | |
---|
[619] | 132 | let cast_op op a b = op (cast a) (cast b) |
---|
[486] | 133 | |
---|
| 134 | let mul a b = cast (mult_big_int a b) |
---|
[619] | 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 | |
---|
[486] | 140 | let eq = eq_big_int |
---|
| 141 | let neq a b = not (eq a b) |
---|
[619] | 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 | |
---|
[486] | 154 | let of_int i = cast (big_int_of_int i) |
---|
[619] | 155 | let to_int i = int_of_big_int (cast i) |
---|
| 156 | |
---|
[486] | 157 | let neg a = cast (minus_big_int a) |
---|
| 158 | |
---|
[619] | 159 | let lognot = sub upper_bound |
---|
[486] | 160 | |
---|
| 161 | let shl a b = |
---|
[619] | 162 | let pow = power_int_positive_big_int 2 (cast b) in |
---|
[486] | 163 | cast (mult_big_int a pow) |
---|
| 164 | |
---|
| 165 | let shr a b = |
---|
[619] | 166 | let a = cast a in |
---|
| 167 | let b = cast b in |
---|
[486] | 168 | let added = |
---|
[619] | 169 | if lt_big_int a half_bound then zero |
---|
[486] | 170 | else half_bound in |
---|
| 171 | let rec aux acc b = |
---|
[619] | 172 | if eq b zero then acc |
---|
[486] | 173 | else |
---|
[619] | 174 | let cont_acc = add added (divu acc two) in |
---|
| 175 | let cont_b = pred b in |
---|
[486] | 176 | aux cont_acc cont_b |
---|
| 177 | in |
---|
| 178 | cast (aux a b) |
---|
| 179 | |
---|
[619] | 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) |
---|
| 183 | |
---|
[486] | 184 | let max a b = if lt a b then b else a |
---|
| 185 | let min a b = if gt a b then b else a |
---|
[619] | 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 |
---|
[486] | 188 | |
---|
[619] | 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. *) |
---|
[486] | 191 | let to_bits a = |
---|
| 192 | let rec aux acc a i = |
---|
| 193 | if i >= size then acc |
---|
[619] | 194 | else aux ((is_odd a) :: acc) (divu a two) (i+1) |
---|
[486] | 195 | in |
---|
[619] | 196 | aux [] (cast a) 0 |
---|
[486] | 197 | |
---|
| 198 | (* [from_bits bits] returns the integer that the list of bits [bits] |
---|
[619] | 199 | represents. *) |
---|
[486] | 200 | let from_bits bits = |
---|
| 201 | let rec aux acc = function |
---|
| 202 | | [] -> acc |
---|
| 203 | | b :: bits -> |
---|
[619] | 204 | let next_acc = mul acc two in |
---|
| 205 | let next_acc = if b then succ next_acc else next_acc in |
---|
[486] | 206 | aux next_acc bits |
---|
| 207 | in |
---|
[619] | 208 | aux zero bits |
---|
[486] | 209 | |
---|
| 210 | (* [binary_log_op f a b] applies the binary boolean operation [f] |
---|
| 211 | pointwisely to the bits that [a] and [b] represent. *) |
---|
| 212 | let binary_log_op f a b = |
---|
| 213 | from_bits (List.map2 f (to_bits a) (to_bits b)) |
---|
| 214 | |
---|
| 215 | let xor a b = (a || b) && (not (a && b)) |
---|
| 216 | |
---|
| 217 | let logand = binary_log_op (&&) |
---|
| 218 | let logor = binary_log_op (||) |
---|
| 219 | let logxor = binary_log_op xor |
---|
| 220 | |
---|
[619] | 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 | |
---|
[486] | 240 | (* [break i n] cuts [i] in [n] parts. In the resulting list, the first element |
---|
| 241 | is the high bits, and the last is the low bits. *) |
---|
| 242 | let break a n = |
---|
[619] | 243 | let chunk_size = size / n in |
---|
[486] | 244 | let pow2_chunk_size = power_int_positive_int 2 chunk_size in |
---|
| 245 | let rec aux acc a i = |
---|
| 246 | if i = 0 then acc |
---|
| 247 | else |
---|
[619] | 248 | let (next, chunk) = quomod_big_int a pow2_chunk_size in |
---|
[486] | 249 | aux ((cast chunk) :: acc) next (i-1) |
---|
| 250 | in |
---|
[619] | 251 | aux [] (cast a) n |
---|
[486] | 252 | |
---|
| 253 | (* [merge l] creates the integer where the first element of [l] is its high |
---|
| 254 | bits, etc, and the last element of [l] is its low bits. *) |
---|
| 255 | let merge = function |
---|
| 256 | | [] -> zero |
---|
| 257 | | al -> |
---|
| 258 | let al = List.rev al in |
---|
| 259 | let nb_chunks = List.length al in |
---|
[619] | 260 | let chunk_size = size / nb_chunks in |
---|
[486] | 261 | let pow2_chunk_size = power_int_positive_int 2 chunk_size in |
---|
| 262 | let rec aux pow2 = function |
---|
| 263 | | [] -> zero |
---|
| 264 | | a :: al -> add (mul a pow2) (aux (mul pow2 pow2_chunk_size) al) |
---|
| 265 | in |
---|
| 266 | aux one al |
---|
| 267 | |
---|
| 268 | end |
---|
| 269 | |
---|
| 270 | |
---|
[619] | 271 | module Int8 : S = Make (struct let size = 1 end) |
---|
| 272 | module Int16 : S = Make (struct let size = 2 end) |
---|
| 273 | module Int32 : S = Make (struct let size = 4 end) |
---|
[486] | 274 | |
---|
[619] | 275 | type int8 = Int8.t |
---|
| 276 | type int16 = Int16.t |
---|
| 277 | type int32 = Int32.t |
---|