source: Deliverables/D2.2/8051/src/common/value.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: 5.6 KB
Line 
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
9module type DATA_SIZE =
10sig
11  val int_size : int
12  val ptr_size : int
13end
14
15(** This is the signature of the module that provides types and functions to
16    manipulate values. *)
17
18module type S =
19sig
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
176end
177
178
179(** The functor to create bounded values from a size and a signedness. *)
180
181module Make (D : DATA_SIZE) : S
Note: See TracBrowser for help on using the repository browser.