source: Deliverables/D2.2/8051/src/common/intValue.mli @ 1568

Last change on this file since 1568 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: 3.2 KB
Line 
1
2(** This module defines functions to manipulate bounded integers. They can be
3    used to represent sequences of bits. *)
4
5(* Integers, whatever their size, will be represented using the Big_int
6   module. This allows immediate conversion, and allows the representation of
7   any integer (that fits into memory). *)
8
9type int_repr = Big_int.big_int
10val print_int_repr : int_repr -> string
11
12(* The parameter module. Bounded integers are characterized by the number of
13   bits used to represent them. *)
14   
15module type INTTYPE = 
16sig
17  val size : int (* in bytes *)
18end
19
20(* The signature provided to manipulate bounded integers. *)
21
22module type S = sig
23
24  type t = Big_int.big_int
25
26  val compare   : t -> t -> int
27  val to_string : t -> string
28  val zero      : t
29  val one       : t
30
31  val to_signed_int_repr   : t -> int_repr
32  val to_unsigned_int_repr : t -> int_repr
33
34  val succ    : t -> t
35  val pred    : t -> t
36  val add     : t -> t -> t
37  (** [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *)
38  val add_of  : t -> t -> bool
39  val sub     : t -> t -> t
40  (** [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2]
41      underflows. *)
42  val sub_uf  : t -> t -> bool
43  val mul     : t -> t -> t
44  val div     : t -> t -> t
45  val divu    : t -> t -> t
46  val modulo  : t -> t -> t
47  val modulou : t -> t -> t
48  val eq      : t -> t -> bool
49  val neq     : t -> t -> bool
50  val lt      : t -> t -> bool
51  val ltu     : t -> t -> bool
52  val le      : t -> t -> bool
53  val leu     : t -> t -> bool
54  val gt      : t -> t -> bool
55  val gtu     : t -> t -> bool
56  val ge      : t -> t -> bool
57  val geu     : t -> t -> bool
58  val neg     : t -> t
59  val lognot  : t -> t
60  val logand  : t -> t -> t
61  val logor   : t -> t -> t
62  val logxor  : t -> t -> t
63  val shl     : t -> t -> t
64  val rotl    : t -> t
65  val shr     : t -> t -> t
66  val shrl    : t -> t -> t
67  val max     : t -> t -> t
68  val maxu    : t -> t -> t
69  val min     : t -> t -> t
70  val minu    : t -> t -> t
71  val cast    : int_repr -> t
72  val of_int  : int -> t
73  val to_int  : t -> int
74
75  (** [zero_ext n a] performs zero extension on [a] where [n] bits are
76      significant. *)
77  val zero_ext : int -> t -> t
78  (** [sign_ext n a] performs sign extension on [a] where [n] bits are
79      significant. *)
80  val sign_ext : int -> t -> t
81
82  (** [break i n] cuts [i] in [n] parts. In the resulting list, the first
83      element is the low bits, and the last is the high bits (little endian
84      representation). *)
85  val break : t -> int -> t list
86  (** [merge l] creates the integer where the first element of [l] is its low
87      bits, etc, and the last element of [l] is its high bits (little endian
88      representation). *)
89  val merge : t list -> t
90
91end
92
93(** The functor to create bounded integers from a size. *)
94
95module Make: functor (IntType: INTTYPE) -> S
96
97module Int8  : S
98module Int16 : S
99module Int32 : S
100
101type int8  = Int8.t
102type int16 = Int16.t
103type int32 = Int32.t
104
105
106(*
107module Int8s   : S
108module Int8u   : S
109module Int16s  : S
110module Int16u  : S
111module Int32   : S
112
113(** Unbounded integers. *)
114module Integer : S
115
116type int8s   = Int8s.t
117type int8u   = Int8u.t
118type int16s  = Int16s.t
119type int16u  = Int16u.t
120type int32   = Int32.t
121type integer = Integer.t
122*)
Note: See TracBrowser for help on using the repository browser.