1 | |
---|
2 | (** This module describes the values manipulated by high level languages. *) |
---|
3 | |
---|
4 | (** The representation of values depends on the size of integers and the size of |
---|
5 | addresses. *) |
---|
6 | |
---|
7 | (** This is the signature of the parameter module. *) |
---|
8 | |
---|
9 | module type DATA_SIZE = |
---|
10 | sig |
---|
11 | val int_size : int |
---|
12 | val ptr_size : int |
---|
13 | end |
---|
14 | |
---|
15 | (** This is the signature of the module that provides types and functions to |
---|
16 | manipulate values. *) |
---|
17 | |
---|
18 | module type S = |
---|
19 | sig |
---|
20 | |
---|
21 | val int_size : int |
---|
22 | val ptr_size : int |
---|
23 | |
---|
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. *) |
---|
27 | type t |
---|
28 | |
---|
29 | val compare : t -> t -> int |
---|
30 | val equal : t -> t -> bool |
---|
31 | val eq : t -> t -> bool |
---|
32 | val hash : t -> int |
---|
33 | val to_string : t -> string |
---|
34 | |
---|
35 | (* The functions of this module may raise a Failure exception when |
---|
36 | trying to convert them to their various representation. *) |
---|
37 | |
---|
38 | val is_int : t -> bool |
---|
39 | val to_int : t -> int |
---|
40 | val of_int : int -> t |
---|
41 | |
---|
42 | val of_int_repr : IntValue.int_repr -> t |
---|
43 | val to_int_repr : t -> IntValue.int_repr |
---|
44 | |
---|
45 | val of_bool : bool -> t |
---|
46 | val to_bool : t -> bool |
---|
47 | |
---|
48 | val zero : t |
---|
49 | val val_true : t |
---|
50 | val val_false : t |
---|
51 | val is_true : t -> bool |
---|
52 | val is_false : t -> bool |
---|
53 | val undef : t |
---|
54 | |
---|
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 |
---|
64 | val cast32 : t -> t |
---|
65 | |
---|
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 |
---|
72 | |
---|
73 | (** Integer opposite *) |
---|
74 | val negint : t -> t |
---|
75 | (** Boolean negation *) |
---|
76 | val notbool : t -> t |
---|
77 | (** Bitwise not *) |
---|
78 | val notint : t -> t |
---|
79 | |
---|
80 | val succ : t -> t |
---|
81 | val pred : t -> t |
---|
82 | val cmpl : t -> t |
---|
83 | |
---|
84 | (** [add_and_of v1 v2] returns the sum of [v1] and [v2], and whether this sum |
---|
85 | overflows. *) |
---|
86 | val add_and_of : t -> t -> (t * t) |
---|
87 | val add : 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) |
---|
94 | val sub : 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 |
---|
98 | val mul : t -> t -> t |
---|
99 | val div : 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 rotl : t -> t |
---|
108 | val shr : t -> t -> t |
---|
109 | val shru : t -> t -> t |
---|
110 | |
---|
111 | (** Signed comparisions *) |
---|
112 | val cmp_eq : t -> t -> t |
---|
113 | val cmp_ne : t -> t -> t |
---|
114 | val cmp_lt : t -> t -> t |
---|
115 | val cmp_ge : t -> t -> t |
---|
116 | val cmp_le : t -> t -> t |
---|
117 | val cmp_gt : t -> t -> t |
---|
118 | |
---|
119 | (** Unsigned comparisions *) |
---|
120 | val cmp_eq_u : t -> t -> t |
---|
121 | val cmp_ne_u : t -> t -> t |
---|
122 | val cmp_lt_u : t -> t -> t |
---|
123 | val cmp_ge_u : t -> t -> t |
---|
124 | val cmp_le_u : t -> t -> t |
---|
125 | val cmp_gt_u : t -> t -> t |
---|
126 | |
---|
127 | (** A chunk is a part of a value that has the size of a memory cell. *) |
---|
128 | |
---|
129 | type chunk |
---|
130 | val string_of_chunk : chunk -> string |
---|
131 | val undef_byte : chunk |
---|
132 | val is_undef_byte : chunk -> bool |
---|
133 | |
---|
134 | (** [break v] cuts [v] in chunks that each fits into a memory cell. In the |
---|
135 | resulting list, the first element is the low bits, and the last is the |
---|
136 | high bits (little endian representation). *) |
---|
137 | val break : t -> chunk list |
---|
138 | (** [merge l] creates the value where the first element of [l] is its low |
---|
139 | bits, etc, and the last element of [l] is its high bits (little endian |
---|
140 | representation). *) |
---|
141 | val merge : chunk list -> t |
---|
142 | |
---|
143 | (** Addresses from interpreters point of view. *) |
---|
144 | |
---|
145 | (** Some architectures have pointers bigger than integers. In this case, only |
---|
146 | a chunk of pointer can fit into a machine register. Thus, an address is |
---|
147 | represented by several values (little endian representation). *) |
---|
148 | |
---|
149 | type address = t list |
---|
150 | val string_of_address : address -> string |
---|
151 | val null : address |
---|
152 | |
---|
153 | (** Addresses from the memory point of view. *) |
---|
154 | |
---|
155 | (** Addresses are represented by a block, i.e. a base address, and an offset |
---|
156 | from this block. Both blocks and offsets are represented using bounded |
---|
157 | integers. *) |
---|
158 | module Block : IntValue.S |
---|
159 | module Offset : IntValue.S |
---|
160 | |
---|
161 | type mem_address |
---|
162 | |
---|
163 | val is_mem_address : address -> bool |
---|
164 | |
---|
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 |
---|
171 | |
---|
172 | val change_address_offset : address -> Offset.t -> address |
---|
173 | val add_address : address -> Offset.t -> address |
---|
174 | val eq_address : address -> address -> bool |
---|
175 | |
---|
176 | end |
---|
177 | |
---|
178 | |
---|
179 | (** The functor to create bounded values from a size and a signedness. *) |
---|
180 | |
---|
181 | module Make (D : DATA_SIZE) : S |
---|