Module type Sig.BASE_WITH_INTEGER

include BASE
include Minimal
include Minimal_No_Boolean
include With_Id
val unique_id : unit -> Fresh_id.t
val name : unit -> string
include With_Context
module Context : Context
val root_context : unit -> Context.t

Opens a new context, corresponding to the initial scope.

val context_pretty : Stdlib.Format.formatter -> Context.t -> unit

Dumps what is known about the current context: useful for debugging.

type boolean

Guards

include With_Assume with module Context := Context and type boolean := boolean
val assume : Context.t -> boolean -> Context.t option

Corresponds to the creation of a new basic block, accessible only if the condition is met.

Joining variables together.

include With_Nondet with module Context := Context
val typed_nondet2 : Context.t -> Context.t -> 'a Context.in_tuple -> Context.t * 'a Context.out_tuple

This joins two basic blocks and returns a new basic block. The Context.in_tuple and Context.out_tuple corresponds to the phi operations in SSA.

val nondet_same_context : Context.t -> 'a Context.in_tuple -> 'a Context.out_tuple

Additionally, one may compute a non-deterministic choice between two values in the same basic block

It can be seen as equivalent as calling typed_nondet2 by passing the same context twice, which would return the same context.

Fixpoint computation.

include With_Fixpoint_Computation with module Context := Context
val mu_context_open : Context.t -> Context.t

Opening a new context can also be seen as opening a new scope: new variables can be introduced, but variables of the parent scope can still be seen.

val typed_fixpoint_step : iteration:int -> init:Context.t -> arg:Context.t -> body:Context.t -> (bool * 'a Context.in_tuple) -> bool * (close:bool -> 'a Context.out_tuple * Context.t)

Fixpoint step is a combination of inclusion checking + widening.

  • parameter init

    is the context leading to the loop entry,

  • parameter arg

    is the context at the loop entry (obtained by mu_context_open or by the last fixpoint_step operation)

  • parameter body

    is the context at the end of the loop

Also takes a boolean and a tuple of values which is the result of the evaluation of the body (the end of the loop).

Internally, it stores the arguments of the mu.

  • returns

    a boolean which says if the fixpoint is reached, and a function. If the fixpoint is reached, we can "close" the mu, and the function returns a tuple corresponding to the mu. We can always "restart" the mu, in which case the function returns a new arg.

val widened_fixpoint_step : widening_id:Widening_Id.t -> previous:Context.t -> next:Context.t -> (bool * 'a Context.in_tuple) -> Context.t * bool * 'a Context.out_tuple

widened_fixpoint_step ~previous ~next (bool,in_tuple) where:

  • widening_id is a unique representation of the widening point;
  • previous is the previous domain state;
  • next is the next domain state obtained after execution of the function body;
  • bool is false if we know that the fixpoint is not reached yet, and true otherwise;
  • in_tuple is the argument of the SSA phi function;

returns a triple (context,bool,out_tuple) 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;
  • out_tuple is the result of the SSA phi function.

The boolean domain should be present everywhere, as we need it or guards.

include With_Boolean with module Context := Context and type boolean := boolean
module Boolean : Datatype_sig.S with type t = boolean
val boolean_pretty : Context.t -> Stdlib.Format.formatter -> boolean -> unit
val serialize_boolean : Context.t -> boolean -> Context.t -> boolean -> 'a Context.in_acc -> (boolean, 'a) Context.result
val boolean_empty : Context.t -> boolean

Empty denotes that the concretization has no value (or it is the concrete value representing the absence of value). Note that this does not necessarily imply that some error occured; for instance the offset of an uninitialized pointer can be represented with empty. Emptyness testing is a simple way of communicating between domains.

val boolean_unknown : Context.t -> boolean
val query_boolean : Context.t -> boolean -> Lattices.Quadrivalent.t
type binary
type enum
include WITH_QUERIES with module Context := Context and type binary := binary and type enum := enum
module Query : sig ... end
include With_Types with module Context := Context and type binary := binary
val binary_unknown_typed : size:Units.In_bits.t -> Context.t -> Types.TypedC.typ -> binary

Returns an unknown value with a given type.

include With_Binary with module Context := Context and type binary := binary and type boolean := boolean
module Binary : Datatype_sig.S with type t = binary
val binary_pretty : size:Units.In_bits.t -> Context.t -> Stdlib.Format.formatter -> binary -> unit
val serialize_binary : widens:bool -> size:Units.In_bits.t -> Context.t -> binary -> Context.t -> binary -> 'a Context.in_acc -> (binary, 'a) Context.result
val binary_empty : size:Units.In_bits.t -> Context.t -> binary
val binary_unknown : size:Units.In_bits.t -> Context.t -> binary
include With_Binary_Forward with module Context := Context and type binary := binary and type boolean := boolean
include With_Enum with module Context := Context and type enum := enum and type boolean := boolean
module Enum : Datatype_sig.S with type t = enum
val enum_pretty : Context.t -> Stdlib.Format.formatter -> enum -> unit
val serialize_enum : Context.t -> enum -> Context.t -> enum -> 'a Context.in_acc -> (enum, 'a) Context.result
val enum_empty : Context.t -> enum
val enum_unknown : enumsize:int -> Context.t -> enum
include With_Enum_Forward with module Context := Context and type enum := enum and type boolean := boolean

Set operations. Note that we do not distinguish binary from binary sets. Note that union reuses the serialize machinery.

Check if an assertion is satisfiable (i.e. a trace exists that makes it true).

include With_Integer with module Context := Context and type boolean := boolean
type integer
module Integer : Datatype_sig.S with type t = integer
val integer_is_empty : Context.t -> integer -> bool

Can return true if provably empty; false is always safe.

val integer_pretty : Context.t -> Stdlib.Format.formatter -> integer -> unit
val serialize_integer : widens:bool -> Context.t -> integer -> Context.t -> integer -> 'a Context.in_acc -> (integer, 'a) Context.result
val integer_empty : Context.t -> integer
val integer_unknown : Context.t -> integer