2 (** This module describes the values manipulated by high level languages. *)
4 (** The representation of values depends on the size of integers and the size of
7 (** This is the signature of the parameter module. *)
9 module type DATA_SIZE =
15 (** This is the signature of the module that provides types and functions to
24 (** The type of values. A value may be: a bounded integer, a chunk of an
25 address (exactly an address when they have the same size as a machine
26 register), or undefined. *)
29 val compare : t -> t -> int
30 val equal : t -> t -> bool
31 val eq : t -> t -> bool
33 val to_string : t -> string
35 (* The functions of this module may raise a Failure exception when
36 trying to convert them to their various representation. *)
38 val is_int : t -> bool
42 val of_int_repr : IntValue.int_repr -> t
43 val to_int_repr : t -> IntValue.int_repr
45 val of_bool : bool -> t
46 val to_bool : t -> bool
51 val is_true : t -> bool
52 val is_false : t -> bool
55 (** The cast operations below returns the undefined value for non-integer
56 values. For integer values, it will return the integer value that
57 represents the same quantity, but using every bits (sign or zero
58 extension) of an integer value. For example, the function [cast8unsigned]
59 should be read as "cast from an 8 bits unsigned integer". *)
60 val cast8unsigned : t -> t
61 val cast8signed : t -> t
62 val cast16unsigned : t -> t
63 val cast16signed : t -> t
66 (** [zero_ext v n m] performs a zero extension on [v] where [n] bytes are
67 significant to a value where [m] bytes are significant. *)
68 val zero_ext : t -> int -> int -> t
69 (** [sign_ext v n m] performs a sign extension on [v] where [n] bytes are
70 significant to a value where [m] bytes are significant. *)
71 val sign_ext : t -> int -> int -> t
73 (** Integer opposite *)
75 (** Boolean negation *)
84 (** [add_and_of v1 v2] returns the sum of [v1] and [v2], and whether this sum
86 val add_and_of : t -> t -> (t * t)
88 (** [add_of v1 v2] returns the [1] value if the sum of [v1] and [v2]
89 overflows, and [0] otherwise. *)
90 val add_of : t -> t -> t
91 (** [sub_and_uf v1 v2] returns the substraction of [v1] and [v2], and whether
92 this substraction underflows. *)
93 val sub_and_uf : t -> t -> (t * t)
95 (** [sub_uf v1 v2] returns the [1] value if the substraction of [v1] and [v2]
96 underflows, and [0] otherwise. *)
97 val sub_uf : t -> t -> t
100 val divu : t -> t -> t
101 val modulo : t -> t -> t
102 val modulou : t -> t -> t
103 val and_op : t -> t -> t
104 val or_op : t -> t -> t
105 val xor : t -> t -> t
106 val shl : t -> t -> t
107 val shr : t -> t -> t
108 val shru : t -> t -> t
110 (** Signed comparisions *)
111 val cmp_eq : t -> t -> t
112 val cmp_ne : t -> t -> t
113 val cmp_lt : t -> t -> t
114 val cmp_ge : t -> t -> t
115 val cmp_le : t -> t -> t
116 val cmp_gt : t -> t -> t
118 (** Unsigned comparisions *)
119 val cmp_eq_u : t -> t -> t
120 val cmp_ne_u : t -> t -> t
121 val cmp_lt_u : t -> t -> t
122 val cmp_ge_u : t -> t -> t
123 val cmp_le_u : t -> t -> t
124 val cmp_gt_u : t -> t -> t
126 (** A chunk is a part of a value that has the size of a memory cell. *)
129 val string_of_chunk : chunk -> string
130 val undef_byte : chunk
131 val is_undef_byte : chunk -> bool
133 (** [break v] cuts [v] in chunks that each fits into a memory cell. In the
134 resulting list, the first element is the low bits, and the last is the
135 high bits (little endian representation). *)
136 val break : t -> chunk list
137 (** [merge l] creates the value where the first element of [l] is its low
138 bits, etc, and the last element of [l] is its high bits (little endian
140 val merge : chunk list -> t
142 (** Addresses from interpreters point of view. *)
144 (** Some architectures have pointers bigger than integers. In this case, only
145 a chunk of pointer can fit into a machine register. Thus, an address is
146 represented by several values (little endian representation). *)
148 type address = t list
149 val string_of_address : address -> string
152 (** Addresses from the memory point of view. *)
154 (** Addresses are represented by a block, i.e. a base address, and an offset
155 from this block. Both blocks and offsets are represented using bounded
157 module Block : IntValue.S
158 module Offset : IntValue.S
161 val string_of_mem_address : mem_address -> string
163 val is_mem_address : address -> bool
165 val of_mem_address : mem_address -> address
166 val to_mem_address : address -> mem_address
167 val make_mem_address : Block.t -> Offset.t -> mem_address
168 val decompose_mem_address : mem_address -> Block.t * Offset.t
169 val block_of_address : address -> Block.t
170 val offset_of_address : address -> Offset.t
172 val change_address_offset : address -> Offset.t -> address
173 val add_address : address -> Offset.t -> address
174 val eq_address : address -> address -> bool
179 (** The functor to create bounded values from a size and a signedness. *)
181 module Make (D : DATA_SIZE) : S