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

(** This module describes the values manipulated by high level
    languages. *)

(** The representation of values depends on the size of integers and the size of
    addresses.  *)

(** This is the signature of the parameter module. *)

module type DATA_SIZE =
sig
  val int_size : int
  val ptr_size : int
end

(** This is the signature of the module that provides functions and types to
    manipulate values. *)

module type S =
sig

  (** Addresses are represented by a block, i.e. a base address, and an offset
      from this block. Both blocks and offsets are represented using bounded
      integers. *)
  module Block  : IntValue.S
  module Offset : IntValue.S

  (** The type of values. A value may be: a bounded integer, a float (though
      they are not fully supported), an address, or undefined. *)
  type t

  val compare : t -> t -> int
  val equal : t -> t -> bool
  val eq : t -> t -> bool
  val hash : t -> int
  val to_string : t -> string

  (* The functions of this module may raise a Failure exception when
     trying to convert them to their various representation. *)

  val is_int : t -> bool
  val to_int : t -> int
  val of_int : int -> t

  val is_float : t -> bool
  val to_float : t -> float
  val of_float : float -> t

  val to_int_repr : t -> IntValue.int_repr
  val of_int_repr : IntValue.int_repr -> t

  val is_pointer : t -> bool
  val to_pointer : t -> Block.t * Offset.t
  val of_pointer : Block.t * Offset.t -> t

  val of_bool   : bool -> t
  val to_bool   : t -> bool

  val zero      : t
  val val_true  : t
  val val_false : t
  val is_true   : t -> bool
  val is_false  : t -> bool
  val undef     : t


  (** Sign or 0 extensions from various bounded integers. *)
  val cast8unsigned  : t -> t 
  val cast8signed    : t -> t    
  val cast16unsigned : t -> t 
  val cast16signed   : t -> t
  val cast32         : t -> t

  (** Integer opposite *)
  val negint        : t -> t
  (** Boolean negation *)
  val notbool       : t -> t
  (** Bitwise not *)
  val notint        : t -> t         
  val negf          : t -> t           
  val absf          : t -> t           
  val singleoffloat : t -> t  
  val intoffloat    : t -> t     
  val intuoffloat   : t -> t    
  val floatofint    : t -> t     
  val floatofintu   : t -> t    

  val succ       : t -> t
  val pred       : t -> t
  val cmpl       : t -> t

  (** [add_and_of v1 v2] returns the sum of [v1] and [v2], and whether this sum
      overflows. *)
  val add_and_of : t -> t -> (t * t)
  val add        : t -> t -> t
  (** [add_of v1 v2] returns the [1] value if the sum of [v1] and [v2]
      overflows, and [0] otherwise. *)
  val add_of     : t -> t -> t
  (** [sub_and_of v1 v2] returns the substraction of [v1] and [v2], and whether
      this substraction underflows. *)
  val sub_and_uf : t -> t -> (t * t)
  val sub        : t -> t -> t
  (** [sub_of v1 v2] returns the [1] value if the substraction of [v1] and [v2]
      underflows, and [0] otherwise. *)
  val sub_uf     : t -> t -> t
  val mul        : t -> t -> t
  val div        : t -> t -> t
  val divu       : t -> t -> t
  val modulo     : t -> t -> t
  val modulou    : t -> t -> t
  val and_op     : t -> t -> t
  val or_op      : t -> t -> t
  val xor        : t -> t -> t
  val shl        : t -> t -> t
  val shr        : t -> t -> t
  val shru       : t -> t -> t
  val addf       : t -> t -> t
  val subf       : t -> t -> t
  val mulf       : t -> t -> t
  val divf       : t -> t -> t

  (** Unsigned comparisions *)
  val cmp_eq_u : t -> t -> t  
  val cmp_ne_u : t -> t -> t  
  val cmp_lt_u : t -> t -> t  
  val cmp_ge_u : t -> t -> t  
  val cmp_le_u : t -> t -> t  
  val cmp_gt_u : t -> t -> t  

  val cmp_eq_f : t -> t -> t  
  val cmp_ne_f : t -> t -> t  
  val cmp_lt_f : t -> t -> t  
  val cmp_ge_f : t -> t -> t  
  val cmp_le_f : t -> t -> t  
  val cmp_gt_f : t -> t -> t

  val cmp_eq : t -> t -> t  
  val cmp_ne : t -> t -> t  
  val cmp_lt : t -> t -> t  
  val cmp_ge : t -> t -> t  
  val cmp_le : t -> t -> t  
  val cmp_gt : t -> t -> t

  (** [break v n] cuts [v] in [n] parts. In the resulting list, the first
      element is the high bits, and the last is the low bits. *)
  val break : t -> int -> t list
  (** [merge l] creates the value where the first element of [l] is its
      high bits, etc, and the last element of [l] is its low bits. *)
  val merge : t list -> t

end


(** The functor to create bounded values from a size and a signedness. *)

module Make (D : DATA_SIZE) : S