source: Deliverables/D2.3/8051/src/common/intValue.ml @ 453

Last change on this file since 453 was 453, checked in by ayache, 9 years ago

Import of the Paris's sources.

File size: 6.8 KB
Line 
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_uf i1 i2] returns true iff substracting the unsigned value of [i1]
30      and the unsigned value of [i2] underflows. *)
31  val sub_uf : 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
76module Make_Arb (IntType: INTTYPE_ARB) : S = 
77struct
78
79  type t = Big_int.big_int
80
81  let size = IntType.size * 8 (* real size, i.e. in bits *)
82
83  let compare = compare_big_int
84  let to_string = string_of_big_int
85  let zero = zero_big_int
86  let one = unit_big_int
87  let two = succ_big_int unit_big_int
88
89  let half_bound = power_int_positive_int 2 (size-1)
90
91  (* The upper bound of signed integers. *)
92  let shbound = half_bound
93  (* The lower bound of signed integers. *)
94  let slbound = minus_big_int half_bound
95
96  (* The upper bound of unsigned integers. *)
97  let uhbound = mult_int_big_int 2 half_bound
98  (* The lower bound of unsigned integers. *)
99  let ulbound = zero
100
101  (* [unsign a] returns the unsigned value of [a]. *)
102  let unsign a =
103    if lt_big_int a zero_big_int then add_big_int uhbound a
104    else a
105
106  (* [is_in_repr a] returns true iff [a] is a value  *)
107  let is_in_repr a =
108    if IntType.is_signed then (le_big_int slbound a) && (lt_big_int a shbound)
109    else (le_big_int ulbound a) && (lt_big_int a uhbound)
110
111  let cast a =
112    if IntType.arbitrary then a
113    else
114      if is_in_repr a then a
115      else 
116        if IntType.is_signed then
117          sub_big_int
118            (mod_big_int (add_big_int a half_bound) uhbound)
119            half_bound
120        else mod_big_int a uhbound
121
122  let succ a = cast (succ_big_int a)
123  let pred a = cast (pred_big_int a)
124  let add a b = cast (add_big_int a b)
125
126  let add_of a b =
127    let u1 = unsign a in
128    let u2 = unsign b in
129    let i = add_big_int u1 u2 in
130    ge_big_int i uhbound
131
132  let sub a b = cast (sub_big_int a b)
133
134  let sub_uf a b =
135    let u1 = unsign a in
136    let u2 = unsign b in
137    let i = sub_big_int u1 u2 in
138    lt_big_int i zero_big_int
139
140  let mul a b = cast (mult_big_int a b)
141  let div a b = cast (div_big_int a b)
142  let modulo a b = cast (mod_big_int a b)
143  let eq = eq_big_int
144  let neq a b = not (eq a b)
145  let lt a b = lt_big_int (cast a) (cast b)
146  let le a b = le_big_int (cast a) (cast b)
147  let gt a b = gt_big_int (cast a) (cast b)
148  let ge a b = ge_big_int (cast a) (cast b)
149  let of_int i = cast (big_int_of_int i)
150  let to_int i = int_of_big_int i
151  let neg a = cast (minus_big_int a)
152
153  let lognot a =
154    let mone = minus_big_int unit_big_int in
155    if IntType.is_signed then sub mone a
156    else cast (sub (pred uhbound) a)
157
158  let shl a b =
159    let pow = power_int_positive_big_int 2 b in
160    cast (mult_big_int a pow)
161
162  let shr a b =
163    let pow = power_int_positive_big_int 2 b in
164    cast (div_big_int a pow)
165
166  let shrl a b =
167    let added =
168      if IntType.is_signed || (lt_big_int b half_bound) then zero_big_int
169      else half_bound in
170    let rec aux acc b =
171      if eq_big_int b zero_big_int then acc
172      else
173        let cont_acc = add_big_int added (div_big_int acc two) in
174        let cont_b = pred_big_int b in
175        aux cont_acc cont_b
176    in
177    cast (aux a b)
178
179  let max a b = if lt a b then b else a
180  let min a b = if gt a b then b else a
181
182  let is_odd a = eq_big_int (mod_big_int a two) unit_big_int
183  let to_bits a =
184    let rec aux acc a i =
185      if i >= size then acc
186      else aux ((is_odd a) :: acc) (div_big_int a two) (i+1)
187    in
188    aux [] a 0
189
190  let from_bits bs =
191    let rec aux acc = function
192      | [] -> acc
193      | b :: bs ->
194        let next_acc = mult_int_big_int 2 acc in
195        let next_acc = if b then succ_big_int next_acc else next_acc in
196        aux next_acc bs
197    in
198    cast (aux zero_big_int bs)
199
200  let binary_log_op f a b =
201    from_bits (List.map2 f (to_bits a) (to_bits b))
202
203  let xor a b = (a || b) && (not (a && b))
204
205  let logand = binary_log_op (&&)
206  let logor = binary_log_op (||)
207  let logxor = binary_log_op xor
208
209  let break a n =
210    let chunk_size = (8 * IntType.size) / n in
211    let pow2_chunk_size = power_int_positive_int 2 chunk_size in
212    let rec aux acc a i =
213      if i = 0 then acc
214      else
215        let (next, chunk) = Big_int.quomod_big_int a pow2_chunk_size in
216        aux ((cast chunk) :: acc) next (i-1)
217    in
218    aux [] a n
219
220  let merge = function
221    | [] -> zero
222    | al ->
223        let al = List.rev al in
224        let nb_chunks = List.length al in
225        let chunk_size = (8 * IntType.size) / nb_chunks in
226        let pow2_chunk_size = power_int_positive_int 2 chunk_size in
227        let rec aux pow2 = function
228          | [] -> zero
229          | a :: al -> add (mul a pow2) (aux (mul pow2 pow2_chunk_size) al)
230        in
231        aux one al
232
233end
234
235
236module Make (IntType : INTTYPE) =
237  Make_Arb (struct include IntType let arbitrary = false end)
238
239
240module Int8s : S = Make 
241(struct 
242  let size = 1
243  let is_signed = true
244end)
245
246module Int8u : S = Make 
247(struct 
248  let size = 1
249  let is_signed = false
250end)
251
252module Int16s : S = Make 
253(struct 
254  let size = 2
255  let is_signed = true
256end)
257
258module Int16u : S = Make 
259(struct 
260  let size = 2
261  let is_signed = false
262end)
263
264module Int32 : S = Make 
265(struct 
266  let size = 4
267  let is_signed = true
268end)
269
270module Integer : S = Make_Arb
271(struct 
272  let size = 1
273  let is_signed = true
274  let arbitrary = true
275end)
276
277
278type int8s   = Int8s.t
279type int8u   = Int8u.t
280type int16s  = Int16s.t
281type int16u  = Int16u.t
282type int32   = Int32.t
283type integer = Integer.t
Note: See TracBrowser for help on using the repository browser.