Module Nonrelational.MakeUF

Make the reduced product of a non-relational domain and a labeled union-find. This should then be passed to one of the functions in Union_find, as these are the ones that create relation

Parameters

module _ : Terms.Relations.GROUP_ACTION with type bitvector = SVA.bitvector and type integer = SVA.integer and type boolean = SVA.boolean and type enum = SVA.enum and type ('a, 'b) relation = ('a, 'b) T.Relation.t

Signature

include Term_based_sig.Domain_S with module Query.Boolean_Lattice = SVA.Boolean_Lattice with module Query.Integer_Lattice = SVA.Integer_Lattice with module Terms = T
module Terms = T
val name : string
type t

Type for elements of the abstract domain. The interface is persistent but the implementation can be imperative.

Represent binary, integer and boolean dimensions/variables in the abstract domain.

val equal : t -> t -> bool
val top : t
module Integer_Query : sig ... end

Projection to a non-relational basis.

module Query : sig ... end
val nondet : doma:t -> tupa:Terms.any Immutable_array.t -> domb:t -> tupb:Terms.any Immutable_array.t -> tupres:Terms.any Immutable_array.t -> t
val widened_fixpoint_step : previous:t -> previous_tup:Terms.any Immutable_array.t -> next:t -> next_tup:Terms.any Immutable_array.t -> bool -> res_tup:Terms.any Immutable_array.t -> t * bool

widened_fixpoint_step ~previous ~previous_tup ~next ~next_tup bool ~res_tup where:

  • previous is the previous domain state and previous_tup the tuple of phi arguments;
  • next is the next domain state obtained by joining execution of the function body and initial state and next_tup the phi arguments;
  • bool is false if we know that the fixpoint is not reached yet, and true otherwise;
  • res_tup is the terms corresponding to the phi function;

returns a triple (context,bool) where:

  • context is the new domain state;
  • bool is true if the fixpoint is reached, and false if not reached or we don't know.
val integer_empty : t -> integer -> t
val boolean_empty : t -> boolean -> t
val binary_empty : size:Units.In_bits.t -> t -> binary -> t
val enum_empty : t -> enum -> t
val integer_unknown : t -> integer -> t
val boolean_unknown : t -> boolean -> t
val binary_unknown : size:Units.In_bits.t -> t -> binary -> t
val enum_unknown : enumsize:int -> t -> enum -> t
val assume : t -> boolean -> t option

Returns None if the result is bottom.

module Domain_Arity : sig ... end
module Binary_Forward : Operator.BINARY_FORWARD with module Arity := Domain_Arity and type boolean := boolean and type binary := binary
module Enum_Forward : Operator.ENUM_FORWARD with module Arity := Domain_Arity and type boolean := boolean and type enum := enum
val boolean_pretty : t -> Stdlib.Format.formatter -> boolean -> unit
val integer_pretty : t -> Stdlib.Format.formatter -> integer -> unit
val binary_pretty : size:Units.In_bits.t -> t -> Stdlib.Format.formatter -> binary -> unit
val enum_pretty : t -> Stdlib.Format.formatter -> enum -> unit
val pretty : Stdlib.Format.formatter -> t -> unit
val fixpoint_open : unit -> unit
val fixpoint_step : lvl:int -> iteration:int -> t -> actuals:Terms.any Immutable_array.t -> t -> args:Terms.any Immutable_array.t -> t -> finals:Terms.any Immutable_array.t -> bool * (close:bool -> Terms.any Immutable_array.t -> t)

Tells if fixpoint is reached, and prepare to write the new values. The returned pair (bool,function) allows to decide whether we should end the fixpoint computation; the function represents a continuation, and the boolean tells whether the fixpoint is reached (if yes, we can close, but we don't have to).

val union : t -> 'a Terms.t -> 'b Terms.t -> ('a, 'b) Terms.Relation.t -> t