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

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

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File size: 8.0 KB
Line 
1
2(** This module defines functions to manipulate bounded integers. They can be
3    used to represent sequences of bits. *)
4
5open Big_int
6
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
12type int_repr = Big_int.big_int
13
14(* The parameter module. Bounded integers are characterized by the number of
15   bits used to represent them. *)
16   
17module type INTTYPE = 
18sig
19  val size : int (* in bytes *)
20end
21
22(* The signature provided to manipulate bounded integers. *)
23
24module 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
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
79
80  (** [break i n] cuts [i] in [n] parts. In the resulting list, the first
81      element is the low bits, and the last is the high bits (little endian
82      representation). *)
83  val break : t -> int -> t list
84  (** [merge l] creates the integer where the first element of [l] is its
85      low bits, etc, and the last element of [l] is its high bits (little endian
86      representation). *)
87  val merge : t list -> t
88
89end
90
91
92module Make (IntType: INTTYPE) : S = 
93struct
94
95  type t = Big_int.big_int
96
97  let size = IntType.size * 8 (* real size, i.e. in bits *)
98
99  let compare = compare_big_int
100  let to_string = string_of_big_int
101  let zero = zero_big_int
102  let one = unit_big_int
103  let two = succ_big_int unit_big_int
104
105  (* Integers will all be taken modulo the following value. *)
106  let _mod = power_int_positive_int 2 size
107
108  (* The lower bound (inclusive). *)
109  let lower_bound = zero
110  (* The upper bound (inclusive). *)
111  let upper_bound = pred_big_int _mod
112
113  (* [cast a] returns a modulo of [a] such that the result fits in the interval
114     of representation. *)
115  let cast a = mod_big_int a _mod
116
117  (* Half bound (exclusive), i.e. upper bound of signed integers. *)
118  let half_bound = power_int_positive_int 2 (size-1)
119
120  (* Signed value of [a]. *)
121  let signed a =
122    let a = cast a in
123    if lt_big_int a half_bound then a
124    else sub_big_int a _mod
125
126  let signed_op op a b = op (signed a) (signed b)
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 [i1] and [i2] overflows. *)
133  let add_of a b = gt_big_int (add_big_int a b) upper_bound
134
135  let sub a b = cast (sub_big_int a b)
136
137  let cast_op op a b = op (cast a) (cast b)
138
139  let mul a b = cast (mult_big_int a b)
140  let div a b = cast (signed_op div_big_int a b)
141  let divu a b = cast_op div_big_int a b
142  let modulo a b = cast (signed_op mod_big_int a b)
143  let modulou a b = cast_op mod_big_int a b
144
145  let eq = eq_big_int
146  let neq a b = not (eq a b)
147  let lt a b = signed_op lt_big_int a b
148  let le a b = signed_op le_big_int a b
149  let gt a b = signed_op gt_big_int a b
150  let ge a b = signed_op ge_big_int a b
151  let ltu a b = cast_op lt_big_int a b
152  let leu a b = cast_op le_big_int a b
153  let gtu a b = cast_op gt_big_int a b
154  let geu a b = cast_op ge_big_int a b
155
156  (* [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2] underflows. *)
157  let sub_uf a b = lt_big_int (sub_big_int a b) zero
158
159  let of_int i = cast (big_int_of_int i)
160  let to_int i = int_of_big_int (cast i)
161
162  let neg a = cast (minus_big_int a)
163
164  let lognot = sub upper_bound
165
166  let shl a b =
167    let pow = power_int_positive_big_int 2 (cast b) in
168    cast (mult_big_int a pow)
169
170  let shr a b =
171    let a = cast a in
172    let b = cast b in
173    let added =
174      if lt_big_int a half_bound then zero
175      else half_bound in
176    let rec aux acc b =
177      if eq b zero then acc
178      else
179        let cont_acc = add added (divu acc two) in
180        let cont_b = pred b in
181        aux cont_acc cont_b
182    in
183    cast (aux a b)
184
185  let shrl a b =
186    let pow = power_int_positive_big_int 2 (cast b) in
187    cast (div_big_int (cast a) pow)
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  let maxu a b = if ltu a b then b else a
192  let minu a b = if gtu a b then b else a
193
194  let is_odd a = eq (modulou a two) one
195  (* [to_bits a] returns the list of bits (0 or 1) that [a] represents. *)
196  let to_bits a =
197    let rec aux acc a i =
198      if i >= size then acc
199      else aux ((is_odd a) :: acc) (divu a two) (i+1)
200    in
201    aux [] (cast a) 0
202
203  (* [from_bits bits] returns the integer that the list of bits [bits]
204     represents. *)
205  let from_bits bits =
206    let rec aux acc = function
207      | [] -> acc
208      | b :: bits ->
209        let next_acc = mul acc two in
210        let next_acc = if b then succ next_acc else next_acc in
211        aux next_acc bits
212    in
213    aux zero 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
227  (* [zero_ext n a] performs zero extension on [a] where [n] bits are
228     significant. *)
229  let zero_ext n a =
230    let pow2 = power_int_positive_int 2 n in
231    cast (mod_big_int a pow2)
232
233  (* [sign_ext n a] performs sign extension on [a] where [n] bits are
234     significant. *)
235  let sign_ext n a =
236    let a' = zero_ext n a in
237    let pow2 = power_int_positive_int 2 (n-1) in
238    let sign = divu a pow2 in
239    if is_odd sign then
240      let added = shr half_bound (of_int (n-1)) in
241      add a' added
242    else a'
243
244
245  (* [break i n] cuts [i] in [n] parts. In the resulting list, the first element
246     is the low bits, and the last is the high bits (little endian
247     representation). *)
248  let break a n =
249    let chunk_size = size / n in
250    let pow2_chunk_size = power_int_positive_int 2 chunk_size in
251    let rec aux acc a i =
252      if i = 0 then acc
253      else
254        let (next, chunk) = quomod_big_int a pow2_chunk_size in
255        aux ((cast chunk) :: acc) next (i-1)
256    in
257    List.rev (aux [] (cast a) n)
258
259  (* [merge l] creates the integer where the first element of [l] is its low
260     bits, etc, and the last element of [l] is its high bits (little endian
261     representation). *)
262  let merge = function
263    | [] -> zero
264    | al ->
265      let nb_chunks = List.length al in
266      let chunk_size = size / nb_chunks in
267      let pow2_chunk_size = power_int_positive_int 2 chunk_size in
268      let rec aux pow2 = function
269        | [] -> zero
270        | a :: al -> add (mul a pow2) (aux (mul pow2 pow2_chunk_size) al)
271      in
272      aux one al
273
274end
275
276
277module Int8  : S = Make (struct let size = 1 end)
278module Int16 : S = Make (struct let size = 2 end)
279module Int32 : S = Make (struct let size = 4 end)
280
281type int8  = Int8.t
282type int16 = Int16.t
283type int32 = Int32.t
Note: See TracBrowser for help on using the repository browser.