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

Last change on this file was 1568, checked in by tranquil, 8 years ago
  • Immediates introduced (but not fully used yet in RTLabs to RTL pass)
  • translation streamlined
  • BUGGY: interpretation fails in LTL, trying to fetch a function with incorrect address
File size: 8.4 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
14let print_int_repr = Big_int.string_of_big_int
15
16(* The parameter module. Bounded integers are characterized by the number of
17   bits used to represent them. *)
18   
19module type INTTYPE = 
20sig
21  val size : int (* in bytes *)
22end
23
24(* The signature provided to manipulate bounded integers. *)
25
26module type S = sig
27
28  type t = Big_int.big_int
29
30  val compare   : t -> t -> int
31  val to_string : t -> string
32  val zero      : t
33  val one       : t
34
35  val to_signed_int_repr   : t -> int_repr
36  val to_unsigned_int_repr : t -> int_repr
37
38  val succ    : t -> t
39  val pred    : t -> t
40  val add     : t -> t -> t
41  (** [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *)
42  val add_of  : t -> t -> bool
43  val sub     : t -> t -> t
44  (** [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2]
45      underflows. *)
46  val sub_uf  : t -> t -> bool
47  val mul     : t -> t -> t
48  val div     : t -> t -> t
49  val divu    : t -> t -> t
50  val modulo  : t -> t -> t
51  val modulou : t -> t -> t
52  val eq      : t -> t -> bool
53  val neq     : t -> t -> bool
54  val lt      : t -> t -> bool
55  val ltu     : t -> t -> bool
56  val le      : t -> t -> bool
57  val leu     : t -> t -> bool
58  val gt      : t -> t -> bool
59  val gtu     : t -> t -> bool
60  val ge      : t -> t -> bool
61  val geu     : t -> t -> bool
62  val neg     : t -> t
63  val lognot  : t -> t
64  val logand  : t -> t -> t
65  val logor   : t -> t -> t
66  val logxor  : t -> t -> t
67  val shl     : t -> t -> t
68  val rotl    : t -> t
69  val shr     : t -> t -> t
70  val shrl    : t -> t -> t
71  val max     : t -> t -> t
72  val maxu    : t -> t -> t
73  val min     : t -> t -> t
74  val minu    : t -> t -> t
75  val cast    : int_repr -> t
76  val of_int  : int -> t
77  val to_int  : t -> int
78
79  (** [zero_ext n a] performs zero extension on [a] where [n] bits are
80      significant. *)
81  val zero_ext : int -> t -> t
82  (** [sign_ext n a] performs sign extension on [a] where [n] bits are
83      significant. *)
84  val sign_ext : int -> t -> t
85
86  (** [break i n] cuts [i] in [n] parts. In the resulting list, the first
87      element is the low bits, and the last is the high bits (little endian
88      representation). *)
89  val break : t -> int -> t list
90  (** [merge l] creates the integer where the first element of [l] is its low
91      bits, etc, and the last element of [l] is its high bits (little endian
92      representation). *)
93  val merge : t list -> t
94
95end
96
97
98module Make (IntType: INTTYPE) : S = 
99struct
100
101  type t = Big_int.big_int
102
103  let size = IntType.size * 8 (* real size, i.e. in bits *)
104
105  let compare = compare_big_int
106  let to_string = string_of_big_int
107  let zero = zero_big_int
108  let one = unit_big_int
109  let two = succ_big_int unit_big_int
110
111  (* Integers will all be taken modulo the following value. *)
112  let _mod = power_int_positive_int 2 size
113
114  (* The lower bound (inclusive). *)
115  let lower_bound = zero
116  (* The upper bound (inclusive). *)
117  let upper_bound = pred_big_int _mod
118
119  (* [cast a] returns a modulo of [a] such that the result fits in the interval
120     of representation. *)
121  let cast a = mod_big_int a _mod
122
123  (* Half bound (exclusive), i.e. upper bound of signed integers. *)
124  let half_bound = power_int_positive_int 2 (size-1)
125
126  (* Signed value of [a]. *)
127  let signed a =
128    let a = cast a in
129    if lt_big_int a half_bound then a
130    else sub_big_int a _mod
131
132  let to_signed_int_repr a = signed a
133
134  let to_unsigned_int_repr a = a
135
136  let signed_op op a b = op (signed a) (signed b)
137
138  let succ a = cast (succ_big_int a)
139  let pred a = cast (pred_big_int a)
140  let add a b = cast (add_big_int a b)
141
142  (* [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *)
143  let add_of a b = gt_big_int (add_big_int a b) upper_bound
144
145  let sub a b = cast (sub_big_int a b)
146
147  let cast_op op a b = op (cast a) (cast b)
148
149  let mul a b = cast (mult_big_int a b)
150  let div a b = cast (signed_op div_big_int a b)
151  let divu a b = cast_op div_big_int a b
152  let modulo a b = cast (signed_op mod_big_int a b)
153  let modulou a b = cast_op mod_big_int a b
154
155  let eq = eq_big_int
156  let neq a b = not (eq a b)
157  let lt a b = signed_op lt_big_int a b
158  let le a b = signed_op le_big_int a b
159  let gt a b = signed_op gt_big_int a b
160  let ge a b = signed_op ge_big_int a b
161  let ltu a b = cast_op lt_big_int a b
162  let leu a b = cast_op le_big_int a b
163  let gtu a b = cast_op gt_big_int a b
164  let geu a b = cast_op ge_big_int a b
165
166  (* [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2] underflows. *)
167  let sub_uf a b = lt_big_int (sub_big_int a b) zero
168
169  let of_int i = cast (big_int_of_int i)
170  let to_int i = int_of_big_int (cast i)
171
172  let neg a = cast (minus_big_int a)
173
174  let lognot = sub upper_bound
175
176  let shl a b =
177    let pow = power_int_positive_big_int 2 (cast b) in
178    cast (mult_big_int a pow)
179
180  let rotl a =
181    if ge_big_int a half_bound then
182      cast (add_big_int (mult_big_int a two) one)
183    else
184      cast (mult_big_int a two)
185
186  let shr a b =
187    let a = cast a in
188    let b = cast b in
189    let added =
190      if lt_big_int a half_bound then zero
191      else half_bound in
192    let rec aux acc b =
193      if eq b zero then acc
194      else
195        let cont_acc = add added (divu acc two) in
196        let cont_b = pred b in
197        aux cont_acc cont_b
198    in
199    cast (aux a b)
200
201  let shrl a b =
202    let pow = power_int_positive_big_int 2 (cast b) in
203    cast (div_big_int (cast a) pow)
204
205  let max a b = if lt a b then b else a
206  let min a b = if gt a b then b else a
207  let maxu a b = if ltu a b then b else a
208  let minu a b = if gtu a b then b else a
209
210  let is_odd a = eq (modulou a two) one
211  (* [to_bits a] returns the list of bits (0 or 1) that [a] represents. *)
212  let to_bits a =
213    let rec aux acc a i =
214      if i >= size then acc
215      else aux ((is_odd a) :: acc) (divu a two) (i+1)
216    in
217    aux [] (cast a) 0
218
219  (* [from_bits bits] returns the integer that the list of bits [bits]
220     represents. *)
221  let from_bits bits =
222    let rec aux acc = function
223      | [] -> acc
224      | b :: bits ->
225        let next_acc = mul acc two in
226        let next_acc = if b then succ next_acc else next_acc in
227        aux next_acc bits
228    in
229    aux zero bits
230
231  (* [binary_log_op f a b] applies the binary boolean operation [f]
232     pointwisely to the bits that [a] and [b] represent. *)
233  let binary_log_op f a b =
234    from_bits (List.map2 f (to_bits a) (to_bits b))
235
236  let xor a b = (a || b) && (not (a && b))
237
238  let logand = binary_log_op (&&)
239  let logor = binary_log_op (||)
240  let logxor = binary_log_op xor
241
242
243  (* [zero_ext n a] performs zero extension on [a] where [n] bits are
244     significant. *)
245  let zero_ext n a =
246    let pow2 = power_int_positive_int 2 n in
247    cast (mod_big_int a pow2)
248
249  (* [sign_ext n a] performs sign extension on [a] where [n] bits are
250     significant. *)
251  let sign_ext n a =
252    let a' = zero_ext n a in
253    let pow2 = power_int_positive_int 2 (n-1) in
254    let sign = divu a pow2 in
255    if is_odd sign then
256      let added = shr half_bound (of_int (n-1)) in
257      add a' added
258    else a'
259
260
261  (* [break i n] cuts [i] in [n] parts. In the resulting list, the first element
262     is the low bits, and the last is the high bits (little endian
263     representation). *)
264  let break a n =
265    let chunk_size = size / n in
266    let pow2_chunk_size = power_int_positive_int 2 chunk_size in
267    let rec aux acc a i =
268      if i = 0 then acc
269      else
270        let (next, chunk) = quomod_big_int a pow2_chunk_size in
271        aux ((cast chunk) :: acc) next (i-1)
272    in
273    List.rev (aux [] (cast a) n)
274
275  (* [merge l] creates the integer where the first element of [l] is its low
276     bits, etc, and the last element of [l] is its high bits (little endian
277     representation). *)
278  let merge = function
279    | [] -> zero
280    | al ->
281      let nb_chunks = List.length al in
282      let chunk_size = size / nb_chunks in
283      let pow2_chunk_size = power_int_positive_int 2 chunk_size in
284      let rec aux pow2 = function
285        | [] -> zero
286        | a :: al -> add (mul a pow2) (aux (mul pow2 pow2_chunk_size) al)
287      in
288      aux one al
289
290end
291
292
293module Int8  : S = Make (struct let size = 1 end)
294module Int16 : S = Make (struct let size = 2 end)
295module Int32 : S = Make (struct let size = 4 end)
296
297type int8  = Int8.t
298type int16 = Int16.t
299type int32 = Int32.t
Note: See TracBrowser for help on using the repository browser.