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

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

Update of D2.2 from Paris.

File size: 4.4 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
67  (** Sign or 0 extensions from various bounded integers. *)
68  val cast8unsigned  : t -> t
69  val cast8signed    : t -> t   
70  val cast16unsigned : t -> t
71  val cast16signed   : t -> t
72  val cast32         : t -> t
73
74  (** Integer opposite *)
75  val negint        : t -> t
76  (** Boolean negation *)
77  val notbool       : t -> t
78  (** Bitwise not *)
79  val notint        : t -> t         
80  val negf          : t -> t           
81  val absf          : t -> t           
82  val singleoffloat : t -> t 
83  val intoffloat    : t -> t     
84  val intuoffloat   : t -> t   
85  val floatofint    : t -> t     
86  val floatofintu   : t -> t   
87
88  val succ       : t -> t
89  val pred       : t -> t
90  val cmpl       : t -> t
91
92  (** [add_and_of v1 v2] returns the sum of [v1] and [v2], and whether this sum
93      overflows. *)
94  val add_and_of : t -> t -> (t * t)
95  val add        : t -> t -> t
96  (** [add_of v1 v2] returns the [1] value if the sum of [v1] and [v2]
97      overflows, and [0] otherwise. *)
98  val add_of     : t -> t -> t
99  (** [sub_and_of v1 v2] returns the substraction of [v1] and [v2], and whether
100      this substraction underflows. *)
101  val sub_and_uf : t -> t -> (t * t)
102  val sub        : t -> t -> t
103  (** [sub_of v1 v2] returns the [1] value if the substraction of [v1] and [v2]
104      underflows, and [0] otherwise. *)
105  val sub_uf     : t -> t -> t
106  val mul        : t -> t -> t
107  val div        : t -> t -> t
108  val divu       : t -> t -> t
109  val modulo     : t -> t -> t
110  val modulou    : t -> t -> t
111  val and_op     : t -> t -> t
112  val or_op      : t -> t -> t
113  val xor        : t -> t -> t
114  val shl        : t -> t -> t
115  val shr        : t -> t -> t
116  val shru       : t -> t -> t
117  val addf       : t -> t -> t
118  val subf       : t -> t -> t
119  val mulf       : t -> t -> t
120  val divf       : t -> t -> t
121
122  (** Unsigned comparisions *)
123  val cmp_eq_u : t -> t -> t 
124  val cmp_ne_u : t -> t -> t 
125  val cmp_lt_u : t -> t -> t 
126  val cmp_ge_u : t -> t -> t 
127  val cmp_le_u : t -> t -> t 
128  val cmp_gt_u : t -> t -> t 
129
130  val cmp_eq_f : t -> t -> t 
131  val cmp_ne_f : t -> t -> t 
132  val cmp_lt_f : t -> t -> t 
133  val cmp_ge_f : t -> t -> t 
134  val cmp_le_f : t -> t -> t 
135  val cmp_gt_f : t -> t -> t
136
137  val cmp_eq : t -> t -> t 
138  val cmp_ne : t -> t -> t 
139  val cmp_lt : t -> t -> t 
140  val cmp_ge : t -> t -> t 
141  val cmp_le : t -> t -> t 
142  val cmp_gt : t -> t -> t
143
144  (** [break v n] cuts [v] in [n] parts. In the resulting list, the first
145      element is the high bits, and the last is the low bits. *)
146  val break : t -> int -> t list
147  (** [merge l] creates the value where the first element of [l] is its
148      high bits, etc, and the last element of [l] is its low bits. *)
149  val merge : t list -> t
150
151end
152
153
154(** The functor to create bounded values from a size and a signedness. *)
155
156module Make (D : DATA_SIZE) : S
Note: See TracBrowser for help on using the repository browser.