source: Deliverables/D2.2/8051/src/common/value.mli @ 486

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

Deliverable D2.2

File size: 4.6 KB
Line 
1
2(** This module describes the values manipulated by high level
3    languages. *)
4
5(** The representation of values depends on the size of integers and the size of
6    addresses.  *)
7
8(** This is the signature of the parameter module. *)
9
10module type DATA_SIZE =
11sig
12  val int_size : int
13  val ptr_size : int
14end
15
16(** This is the signature of the module that provides functions and types to
17    manipulate values. *)
18
19module type S =
20sig
21
22  (** Addresses are represented by a block, i.e. a base address, and an offset
23      from this block. Both blocks and offsets are represented using bounded
24      integers. *)
25  module Block  : IntValue.S
26  module Offset : IntValue.S
27
28  (** The type of values. A value may be: a bounded integer, a float (though
29      they are not fully supported), an address, or undefined. *)
30  type t
31
32  val compare : t -> t -> int
33  val equal : t -> t -> bool
34  val eq : t -> t -> bool
35  val hash : t -> int
36  val to_string : t -> string
37
38  (* The functions of this module may raise a Failure exception when
39     trying to convert them to their various representation. *)
40
41  val is_int : t -> bool
42  val to_int : t -> int
43  val of_int : int -> t
44
45  val is_float : t -> bool
46  val to_float : t -> float
47  val of_float : float -> t
48
49  val to_int_repr : t -> IntValue.int_repr
50  val of_int_repr : IntValue.int_repr -> t
51
52  val is_pointer : t -> bool
53  val to_pointer : t -> Block.t * Offset.t
54  val of_pointer : Block.t * Offset.t -> t
55
56  val of_bool   : bool -> t
57  val to_bool   : t -> bool
58
59  val zero      : t
60  val val_true  : t
61  val val_false : t
62  val is_true   : t -> bool
63  val is_false  : t -> bool
64  val undef     : t
65
66  (** [cast8unsigned v] returns undefined for non-integer values. For integer
67      values, it supposes that the value is a 8 bit unsigned integer. It will
68      return the integer value that represents the same quantity, but using
69      every bits. The other cast operations behave the same way. *)
70  val cast8unsigned  : t -> t
71  val cast8signed    : t -> t   
72  val cast16unsigned : t -> t
73  val cast16signed   : t -> t
74  val cast32         : t -> t
75
76  (** Integer opposite *)
77  val negint        : t -> t
78  (** Boolean negation *)
79  val notbool       : t -> t
80  (** Bitwise not *)
81  val notint        : t -> t         
82  val negf          : t -> t           
83  val absf          : t -> t           
84  val singleoffloat : t -> t 
85  val intoffloat    : t -> t     
86  val intuoffloat   : t -> t   
87  val floatofint    : t -> t     
88  val floatofintu   : t -> t   
89
90  val succ       : t -> t
91  val pred       : t -> t
92  val cmpl       : t -> t
93
94  (** [add_and_of v1 v2] returns the sum of [v1] and [v2], and whether this sum
95      overflows. *)
96  val add_and_of : t -> t -> (t * t)
97  val add        : t -> t -> t
98  (** [add_of v1 v2] returns the 1 value if the sum of [v1] and [v2]
99      overflows, and 0 otherwise. *)
100  val add_of     : t -> t -> t
101  (** [sub_and_of v1 v2] returns the substraction of [v1] and [v2], and whether
102      this substraction overflows. *)
103  val sub_and_of : t -> t -> (t * t)
104  val sub        : t -> t -> t
105  (** [sub_of v1 v2] returns the 1 value if the substraction of [v1] and [v2]
106      overflows, and 0 otherwise. *)
107  val sub_of     : t -> t -> t
108  val mul        : t -> t -> t
109  val div        : t -> t -> t
110  val divu       : t -> t -> t
111  val modulo     : t -> t -> t
112  val modu       : t -> t -> t
113  val and_op     : t -> t -> t
114  val or_op      : t -> t -> t
115  val xor        : t -> t -> t
116  val shl        : t -> t -> t
117  val shr        : t -> t -> t
118  val shru       : t -> t -> t
119  val addf       : t -> t -> t
120  val subf       : t -> t -> t
121  val mulf       : t -> t -> t
122  val divf       : t -> t -> t
123
124  (** Unsigned comparisions *)
125  val cmp_eq_u : t -> t -> t 
126  val cmp_ne_u : t -> t -> t 
127  val cmp_lt_u : t -> t -> t 
128  val cmp_ge_u : t -> t -> t 
129  val cmp_le_u : t -> t -> t 
130  val cmp_gt_u : t -> t -> t 
131
132  val cmp_eq_f : t -> t -> t 
133  val cmp_ne_f : t -> t -> t 
134  val cmp_lt_f : t -> t -> t 
135  val cmp_ge_f : t -> t -> t 
136  val cmp_le_f : t -> t -> t 
137  val cmp_gt_f : t -> t -> t
138
139  val cmp_eq : t -> t -> t 
140  val cmp_ne : t -> t -> t 
141  val cmp_lt : t -> t -> t 
142  val cmp_ge : t -> t -> t 
143  val cmp_le : t -> t -> t 
144  val cmp_gt : t -> t -> t
145
146  (** [break v n] cuts [v] in [n] parts. In the resulting list, the first
147      element is the high bits, and the last is the low bits. *)
148  val break : t -> int -> t list
149  (** [merge l] creates the value where the first element of [l] is its
150      high bits, etc, and the last element of [l] is its low bits. *)
151  val merge : t list -> t
152
153end
154
155
156(** The functor to create bounded values from a size and a signedness. *)
157
158module Make (D : DATA_SIZE) : S
Note: See TracBrowser for help on using the repository browser.