Changeset 619 for Deliverables/D2.2/8051/src/common/intValue.ml
 Timestamp:
 Mar 2, 2011, 3:27:41 PM (9 years ago)
 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. *) 1 4 2 5 open Big_int 3 6 4 7 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 5 12 type int_repr = Big_int.big_int 6 13 14 (* The parameter module. Bounded integers are characterized by the number of 15 bits used to represent them. *) 16 7 17 module type INTTYPE = 8 18 sig 9 val size : int (* in bytes *) 10 val is_signed : bool 19 val size : int (* in bytes *) 11 20 end 21 22 (* The signature provided to manipulate bounded integers. *) 12 23 13 24 module type S = sig … … 20 31 val one : t 21 32 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 54 79 55 80 (** [break i n] cuts [i] in [n] parts. In the resulting list, the first 56 81 element is the high bits, and the last is the low bits. *) 57 82 val break : t > int > t list 58 (** [merge l] creates anthe integer where the first element of [l] is its83 (** [merge l] creates the integer where the first element of [l] is its 59 84 high bits, etc, and the last element of [l] is its low bits. *) 60 85 val merge : t list > t … … 63 88 64 89 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 = 90 module Make (IntType: INTTYPE) : S = 80 91 struct 81 92 … … 90 101 let two = succ_big_int unit_big_int 91 102 92 let half_bound = power_int_positive_int 2 (size1) 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 114 110 115 111 (* [cast a] returns a modulo of [a] such that the result fits in the interval 116 112 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 (size1) 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) 127 122 128 123 let succ a = cast (succ_big_int a) … … 130 125 let add a b = cast (add_big_int a b) 131 126 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 139 129 140 130 let sub a b = cast (sub_big_int a b) 141 131 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) 149 133 150 134 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 153 140 let eq = eq_big_int 154 141 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 159 154 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 161 157 let neg a = cast (minus_big_int a) 162 158 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 167 160 168 161 let shl a b = 169 let pow = power_int_positive_big_int 2 bin162 let pow = power_int_positive_big_int 2 (cast b) in 170 163 cast (mult_big_int a pow) 171 164 172 165 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 177 168 let added = 178 if IntType.is_signed  (lt_big_int b half_bound) then zero_big_int169 if lt_big_int a half_bound then zero 179 170 else half_bound in 180 171 let rec aux acc b = 181 if eq _big_int b zero_big_intthen acc172 if eq b zero then acc 182 173 else 183 let cont_acc = add _big_int added (div_big_intacc two) in184 let cont_b = pred _big_intb in174 let cont_acc = add added (divu acc two) in 175 let cont_b = pred b in 185 176 aux cont_acc cont_b 186 177 in 187 178 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) 188 183 189 184 let max a b = if lt a b then b else a 190 185 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 2complement 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. *) 195 191 let to_bits a = 196 192 let rec aux acc a i = 197 193 if i >= size then acc 198 else aux ((is_odd a) :: acc) (div _big_inta two) (i+1)199 in 200 aux [] a0194 else aux ((is_odd a) :: acc) (divu a two) (i+1) 195 in 196 aux [] (cast a) 0 201 197 202 198 (* [from_bits bits] returns the integer that the list of bits [bits] 203 represents. Signed integers are represented using the 2complement 204 representation. *) 199 represents. *) 205 200 let from_bits bits = 206 201 let rec aux acc = function 207 202  [] > acc 208 203  b :: bits > 209 let next_acc = mul t_int_big_int 2 accin210 let next_acc = if b then succ _big_intnext_acc else next_acc in204 let next_acc = mul acc two in 205 let next_acc = if b then succ next_acc else next_acc in 211 206 aux next_acc bits 212 207 in 213 cast (aux zero_big_int bits)208 aux zero bits 214 209 215 210 (* [binary_log_op f a b] applies the binary boolean operation [f] … … 224 219 let logxor = binary_log_op xor 225 220 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 (n1) in 233 let sign = divu a pow2 in 234 if is_odd sign then 235 let added = shr half_bound (of_int (n1)) in 236 add a' added 237 else a' 238 239 226 240 (* [break i n] cuts [i] in [n] parts. In the resulting list, the first element 227 241 is the high bits, and the last is the low bits. *) 228 242 let break a n = 229 let chunk_size = (8 * IntType.size)/ n in243 let chunk_size = size / n in 230 244 let pow2_chunk_size = power_int_positive_int 2 chunk_size in 231 245 let rec aux acc a i = 232 246 if i = 0 then acc 233 247 else 234 let (next, chunk) = Big_int.quomod_big_int a pow2_chunk_size in248 let (next, chunk) = quomod_big_int a pow2_chunk_size in 235 249 aux ((cast chunk) :: acc) next (i1) 236 250 in 237 aux [] an251 aux [] (cast a) n 238 252 239 253 (* [merge l] creates the integer where the first element of [l] is its high … … 244 258 let al = List.rev al in 245 259 let nb_chunks = List.length al in 246 let chunk_size = (8 * IntType.size)/ nb_chunks in260 let chunk_size = size / nb_chunks in 247 261 let pow2_chunk_size = power_int_positive_int 2 chunk_size in 248 262 let rec aux pow2 = function … … 255 269 256 270 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 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) 274 275 type int8 = Int8.t 276 type int16 = Int16.t 277 type int32 = Int32.t
Note: See TracChangeset
for help on using the changeset viewer.