src/common/value.mli

   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 shr        : t -> t -> t
 108   val shru       : t -> t -> t
 109
 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
 117
 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
 125
 126   (** A chunk is a part of a value that has the size of a memory cell. *)
 127
 128   type chunk
 129   val string_of_chunk : chunk -> string
 130   val undef_byte : chunk
 131   val is_undef_byte : chunk -> bool
 132
 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
 139       representation). *)
 140   val merge : chunk list -> t
 141
 142   (** Addresses from interpreters point of view. *)
 143
 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). *)
 147
 148   type address = t list
 149   val string_of_address : address -> string
 150   val null : address
 151
 152   (** Addresses from the memory point of view. *)
 153
 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
 156       integers. *)
 157   module Block  : IntValue.S
 158   module Offset : IntValue.S
 159
 160   type mem_address
 161   val string_of_mem_address : mem_address -> string
 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