package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Integer2binary.MakeSource

Parameters

Signature

include Sig.BASE with type binary = I.integer with type boolean = I.boolean with module Context = I.Context
include Sig.Minimal with type boolean = I.boolean with module Context = I.Context
include Sig.Minimal_No_Boolean with type boolean = I.boolean with module Context = I.Context
include Sig.With_Id
Sourceval unique_id : unit -> Sig.Fresh_id.t
Sourceval name : unit -> string
include Sig.With_Context with module Context = I.Context
Sourcemodule Context = I.Context
Sourceval root_context : unit -> Context.t

Opens a new context, corresponding to the initial scope.

Sourceval context_pretty : Format.formatter -> Context.t -> unit

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

Sourcetype boolean = I.boolean

Guards

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

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

  • raises Bottom

Joining variables together.

include Sig.With_Nondet with module Context := Context

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.

Sourceval 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 Sig.With_Fixpoint_Computation with module Context := Context
Sourceval 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.

Sourceval 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.

Sourceval widened_fixpoint_step : widening_id:Sig.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 Sig.With_Boolean with module Context := Context and type boolean := boolean
Sourcemodule Boolean : Datatype_sig.S with type t = boolean
Sourceval boolean_pretty : Context.t -> Format.formatter -> boolean -> unit
Sourceval serialize_boolean : Context.t -> boolean -> Context.t -> boolean -> 'a Context.in_acc -> (boolean, 'a) Context.result
Sourceval 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.

Sourceval boolean_unknown : Context.t -> boolean
Sourcetype binary = I.integer
Sourcetype enum
include Sig.WITH_QUERIES with module Context := Context and type binary := binary and type enum := enum
Sourcemodule Query : sig ... end
include Sig.With_Types with module Context := Context and type binary := binary
Sourceval binary_unknown_typed : size:Units.In_bits.t -> Context.t -> Types.TypedC.typ -> binary

Returns an unknown value with a given type.

include Sig.With_Binary with module Context := Context and type binary := binary and type boolean := boolean
Sourcemodule Binary : Datatype_sig.S with type t = binary
Sourceval binary_pretty : size:Units.In_bits.t -> Context.t -> Format.formatter -> binary -> unit
Sourceval serialize_binary : widens:bool -> size:Units.In_bits.t -> Context.t -> binary -> Context.t -> binary -> 'a Context.in_acc -> (binary, 'a) Context.result
Sourceval binary_empty : size:Units.In_bits.t -> Context.t -> binary
Sourceval binary_unknown : size:Units.In_bits.t -> Context.t -> binary
include Sig.With_Binary_Forward with module Context := Context and type binary := binary and type boolean := boolean
include Sig.With_Enum with module Context := Context and type enum := enum and type boolean := boolean
Sourcemodule Enum : Datatype_sig.S with type t = enum
Sourceval enum_pretty : Context.t -> Format.formatter -> enum -> unit
Sourceval serialize_enum : Context.t -> enum -> Context.t -> enum -> 'a Context.in_acc -> (enum, 'a) Context.result
Sourceval enum_empty : Context.t -> enum
Sourceval enum_unknown : enumsize:int -> Context.t -> enum
include Sig.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 Sig.With_Integer with module Context := Context and type boolean := boolean with type integer = I.integer with module Integer_Query = I.Integer_Query
Sourcetype integer = I.integer
Sourcemodule Integer : Datatype_sig.S with type t = integer
Sourceval integer_is_empty : Context.t -> integer -> bool

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

Sourceval integer_pretty : Context.t -> Format.formatter -> integer -> unit
Sourceval serialize_integer : widens:bool -> Context.t -> integer -> Context.t -> integer -> 'a Context.in_acc -> (integer, 'a) Context.result
Sourceval integer_empty : Context.t -> integer
Sourceval integer_unknown : Context.t -> integer
Sourcemodule Integer_Query = I.Integer_Query