source: Deliverables/D2.2/8051/src/common/intValue.ml @ 486

Last change on this file since 486 was 486, checked in by ayache, 8 years ago

Deliverable D2.2

File size: 8.1 KB
RevLine 
[486]1
2open Big_int
3
4
5type int_repr = Big_int.big_int
6
7module type INTTYPE = 
8sig
9  val size      : int (* in bytes *)
10  val is_signed : bool 
11end
12
13module type S = sig
14
15  type t = Big_int.big_int
16
17  val compare   : t -> t -> int
18  val to_string : t -> string
19  val zero      : t
20  val one       : t
21
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
54
55  (** [break i n] cuts [i] in [n] parts. In the resulting list, the first
56      element is the high bits, and the last is the low bits. *)
57  val break : t -> int -> t list
58  (** [merge l] creates an the integer where the first element of [l] is its
59      high bits, etc, and the last element of [l] is its low bits. *)
60  val merge : t list -> t
61
62end
63
64
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
69module type INTTYPE_ARB =
70sig
71  val size      : int
72  val is_signed : bool
73  val arbitrary : bool
74end
75
76(* The following functor works for unbounded integers as well as for bounded
77   intergers. *)
78
79module Make_Arb (IntType: INTTYPE_ARB) : S = 
80struct
81
82  type t = Big_int.big_int
83
84  let size = IntType.size * 8 (* real size, i.e. in bits *)
85
86  let compare = compare_big_int
87  let to_string = string_of_big_int
88  let zero = zero_big_int
89  let one = unit_big_int
90  let two = succ_big_int unit_big_int
91
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)
114
115  (* [cast a] returns a modulo of [a] such that the result fits in the interval
116     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
127
128  let succ a = cast (succ_big_int a)
129  let pred a = cast (pred_big_int a)
130  let add a b = cast (add_big_int a b)
131
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
139
140  let sub a b = cast (sub_big_int a b)
141
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
149
150  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)
153  let eq = eq_big_int
154  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)
159  let of_int i = cast (big_int_of_int i)
160  let to_int i = int_of_big_int i
161  let neg a = cast (minus_big_int a)
162
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
167
168  let shl a b =
169    let pow = power_int_positive_big_int 2 b in
170    cast (mult_big_int a pow)
171
172  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 =
177    let added =
178      if IntType.is_signed || (lt_big_int b half_bound) then zero_big_int
179      else half_bound in
180    let rec aux acc b =
181      if eq_big_int b zero_big_int then acc
182      else
183        let cont_acc = add_big_int added (div_big_int acc two) in
184        let cont_b = pred_big_int b in
185        aux cont_acc cont_b
186    in
187    cast (aux a b)
188
189  let max a b = if lt a b then b else a
190  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. *)
195  let to_bits a =
196    let rec aux acc a i =
197      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
201
202  (* [from_bits bits] returns the integer that the list of bits [bits]
203     represents. Signed integers are represented using the 2-complement
204     representation. *)
205  let from_bits bits =
206    let rec aux acc = function
207      | [] -> acc
208      | 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
211        aux next_acc bits
212    in
213    cast (aux zero_big_int bits)
214
215  (* [binary_log_op f a b] applies the binary boolean operation [f]
216     pointwisely to the bits that [a] and [b] represent. *)
217  let binary_log_op f a b =
218    from_bits (List.map2 f (to_bits a) (to_bits b))
219
220  let xor a b = (a || b) && (not (a && b))
221
222  let logand = binary_log_op (&&)
223  let logor = binary_log_op (||)
224  let logxor = binary_log_op xor
225
226  (* [break i n] cuts [i] in [n] parts. In the resulting list, the first element
227     is the high bits, and the last is the low bits. *)
228  let break a n =
229    let chunk_size = (8 * IntType.size) / n in
230    let pow2_chunk_size = power_int_positive_int 2 chunk_size in
231    let rec aux acc a i =
232      if i = 0 then acc
233      else
234        let (next, chunk) = Big_int.quomod_big_int a pow2_chunk_size in
235        aux ((cast chunk) :: acc) next (i-1)
236    in
237    aux [] a n
238
239  (* [merge l] creates the integer where the first element of [l] is its high
240     bits, etc, and the last element of [l] is its low bits. *)
241  let merge = function
242    | [] -> zero
243    | al ->
244      let al = List.rev al in
245      let nb_chunks = List.length al in
246      let chunk_size = (8 * IntType.size) / nb_chunks in
247      let pow2_chunk_size = power_int_positive_int 2 chunk_size in
248      let rec aux pow2 = function
249        | [] -> zero
250        | a :: al -> add (mul a pow2) (aux (mul pow2 pow2_chunk_size) al)
251      in
252      aux one al
253
254end
255
256
257module Make (IntType : INTTYPE) =
258  Make_Arb (struct include IntType let arbitrary = false end)
259
260
261module Int8s : S = Make 
262  (struct 
263    let size = 1
264    let is_signed = true
265   end)
266
267module Int8u : S = Make 
268  (struct 
269    let size = 1
270    let is_signed = false
271   end)
272
273module Int16s : S = Make 
274  (struct 
275    let size = 2
276    let is_signed = true
277   end)
278
279module Int16u : S = Make 
280  (struct 
281    let size = 2
282    let is_signed = false
283   end)
284
285module Int32 : S = Make 
286  (struct 
287    let size = 4
288    let is_signed = true
289   end)
290
291module Integer : S = Make_Arb
292  (struct 
293    let size = 1
294    let is_signed = true
295    let arbitrary = true
296   end)
297
298
299type int8s   = Int8s.t
300type int8u   = Int8u.t
301type int16s  = Int16s.t
302type int16u  = Int16u.t
303type int32   = Int32.t
304type integer = Integer.t
Note: See TracBrowser for help on using the repository browser.