Source file common.ml

(**************************************************************************)
(*  This file is part of BINSEC.                                          *)
(*                                                                        *)
(*  Copyright (C) 2016-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Binsec

type status = Sat | Unsat | Unknown

module type TERM = sig
  module rec Bl : sig
    type t

    val const : string -> t
    (** [const name]
        creates the (first-order) boolean constant named [name] . *)

    val top : t
    (** The value [true]. *)

    val bot : t
    (** The value [false]. *)

    val lognot : t -> t
    (** [lognot x y]
        creates the boolean [not] operation of [x]. *)

    val logand : t -> t -> t
    (** [logand x y]
        creates the boolean [and] operation between [x] and [y]. *)

    val logor : t -> t -> t
    (** [logor x y]
        creates the boolean [or] operation between [x] and [y]. *)

    val logxor : t -> t -> t
    (** [logxor x y]
        creates the boolean [xor] operation between [x] and [y]. *)

    val ite : t -> t -> t -> t
    (** [ite x y z]
        creates the boolean [ite] operation between [y] and [z]
        according to [x]. *)

    val equal : t -> t -> t
    (** [equal x y ]
        creates the boolean [=] operation between [x] and [y]. *)

    val diff : t -> t -> t
    (** [diff x y ]
        creates the boolean [<>] operation between [x] and [y]. *)

    val implies : t -> t -> t
    (** [implies x y]
        creates the boolean [=>] operation between [x] and [y]. *)

    val to_bv : t -> Bv.t
    (** [to_bv x]
        cast the boolean [x] as a 1-bit bitvector. *)
  end

  and Bv : sig
    type t

    val const : int -> string -> t
    (** [const size name]
        creates the (first-order) constant of [size] bits named [name] . *)

    val value : int -> Z.t -> t
    (** [value sz bv]
        creates a constant from the bitvector value [bv] of size [sz]. *)

    include Sigs.COMPARISON with type t := t and type boolean := Bl.t
    include Sigs.ARITHMETIC with type t := t
    include Sigs.EXTENDED_LOGICAL with type t := t

    val lognand : t -> t -> t
    (** [lognand x y]
        creates the [nand] bitvector operation between [x] and [y]. *)

    val lognor : t -> t -> t
    (** [lognor x y]
        creates the [nor] bitvector operation between [x] and [y]. *)

    val logxnor : t -> t -> t
    (** [logxnor x y]
        creates the [xnor] bitvector operation between [x] and [y]. *)

    include Sigs.SHIFT_ROT with type t := t and type index := t

    val rotate_lefti : t -> int -> t
    (** [rotate_lefti x i]
        same as [rotate_left] but with a constant index. *)

    val rotate_righti : t -> int -> t
    (** [rotate_righti x i]
        same as [rotate_right] but with a constant index. *)

    val append : t -> t -> t
    (** [append x y]
        creates the concatenation of the two bitvectors [x] and [y]. *)

    val extract : hi:int -> lo:int -> t -> t
    (** [extract ~hi ~lo x]
        extracts the sub-bitvector of [x] starting from bit [lo]
        and ending at bit [hi] (included). *)

    val uext : int -> t -> t
    (** [uext n x]
        zero-extends the bitvector [x] by adding [n] bits. *)

    val sext : int -> t -> t
    (** [sext n x]
        sign extends the bitvector [x] copying [n] times
        the most significant bit. *)

    val ite : Bl.t -> t -> t -> t
    (** [ite x y z]
        creates the bitvector [ite] operation between [y] and [z]
        according to [x]. *)

    val succ : t -> t
    (** [succ x]
        creates the bitvector [x + 1] operation. *)

    val to_bl : t -> Bl.t
    (** [to_bl x]
        cast the 1-bit bitvector [x] as a boolean. *)
  end

  and Ax : sig
    type t
    type sort

    val sort : idx:int -> int -> sort
    (** [sort ~idx elm]
        creates a new array kind that maps [idx]-bit bitvector indexes
        to [elm]-bit bitvector values. *)

    val const : sort -> string -> t
    (** [const sort name]
        creates the (first-order) constant array named [name]. *)

    val store : t -> Bv.t -> Bv.t -> t
    (** [store a i x]
        creates the array [store] operation of the byte [x] at index [i]
        in the array [a]. *)

    val select : t -> Bv.t -> Bv.t
    (** [select a i]
        creates the array [select] operation of one byte at index [i]
        in the array [a]. *)

    val equal : t -> t -> Bl.t
    (** [equal x y ]
        creates the array [=] operation between [x] and [y]. *)

    val diff : t -> t -> Bl.t
    (** [diff x y ]
        creates the array [<>] operation between [x] and [y]. *)

    val ite : Bl.t -> t -> t -> t
    (** [ite x y z]
        creates the array [ite] operation between [y] and [z]
        according to [x]. *)
  end
end

module type S = sig
  (** An incremental solver instance. *)

  include TERM

  val assert_formula : Bl.t -> unit
  (** [assert_formula bl] assert the boolean entry in the solver instance.

      @param bl The boolean entry to assert.
  *)

  val push : unit -> unit
  (** [push ()]
      creates a backup point of the current solver context.
  *)

  val pop : unit -> unit
  (** [pop ()]
      discard all the assertions since the last backup point,
      restoring the solver context in the same state as before the [push ()].
      Invalid uses may fail in an unpredictable fashion.
  *)

  val check_sat : ?timeout:float -> unit -> status
  (** [check_sat ()] checks if the current formula is satisfiable.

      @return Sat, Unsat or Unknown.
  *)

  val check_sat_assuming : ?timeout:float -> Bl.t -> status
  (** [check_sat_assuming e] checks if the current formula is satisfiable
      with the assumtion [e].

      @return Sat, Unsat or Unknown.
  *)

  val get_bv_value : Bv.t -> Z.t
  (** [get_bv_value expr] returns the assignment of the
      expression [expr] if [check_sat] returned [Sat].
      Invalid uses may fail in an unpredictable fashion.

      @param expr The expression to get the assignment.

      @return The bitvector assignment of [expr].
  *)

  val fold_ax_values : (Z.t -> Z.t -> 'a -> 'a) -> Ax.t -> 'a -> 'a
  (** [fold_ax_values f ax v] iter through the assignment of the
      array [ax] if [check_sat] returned [Sat].
      Invalid uses may fail in an unpredictable fashion.

      @param ax The expression to get the assignment.
  *)

  val close : unit -> unit
  (** [close ()] will destroy the solver instance and release its ressources.
      Calling any function on this instance afterward is invalid
      and may fail in an unpredictable fashion.
  *)
end

(** A solver instance factory. *)
module type F = functor () -> S

type ('bl, 'bv, 'ax) t =
  (module S with type Bl.t = 'bl and type Bv.t = 'bv and type Ax.t = 'ax)