path: root/abstract/value_domain.ml

(*
  Interface definition for any single-value abstract domain.
  Only implementation of interface is intervals.
*)



type bound = Int of int | PInf | MInf
type itv = Itv of bound * bound | Bot

let string_of_bound = function
    | MInf -> "-oo"
    | PInf -> "+oo"
    | Int i -> string_of_int i
let string_of_itv = function
    | Bot -> "⊥"
    | Itv(a, b) -> "[" ^ (string_of_bound a) ^ "; " ^ (string_of_bound b) ^ "]"


module type VALUE_DOMAIN = sig
    type t

    (* constructors *)
    val top      : t
    val bottom   : t
    val const    : int -> t
    val itv      : int -> int -> t
    val to_itv   : t -> itv
    val as_const : t -> int option

    (* order *)
    val subset   : t -> t -> bool

    (* set-theoretic operations *)
    val join     : t -> t -> t   (* union *)
    val meet     : t -> t -> t   (* intersection *)
    val widen    : t -> t -> t

    (* arithmetic operations *)
    val neg      : t -> t
    val add      : t -> t -> t
    val sub      : t -> t -> t
    val mul      : t -> t -> t
    val div      : t -> t -> t
    val rem      : t -> t -> t

    (* restrict two values considering that the first is smaller than the second *)
    val leq      : t -> t -> t * t

    (* pretty-printing *)
    val to_string : t -> string
end