Module Assert_false.Domain

include module type of struct include Assert_false_domain.Domain end
include Sig.Minimal
include Sig.Minimal_No_Boolean
include Sig.With_Id
val unique_id : unit -> Sig.Fresh_id.t
val name : unit -> string
include Sig.With_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.

Guards

include Sig.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.

  • raises Bottom

Joining variables together.

include Sig.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 Sig.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: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
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
include Sig.WITH_QUERIES with module Context := Context and type binary := binary and type enum := enum
include Sig.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 Sig.With_Binary with module Context := Context and type binary := binary and type boolean := boolean
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 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
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 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).

module Types : sig ... end
include module type of struct include Types end
include module type of struct include Types end
module Parse_ctypes = Types.Parse_ctypes
module Type_check_tree = Types.Type_check_tree
module TypedC = Types.TypedC
type memory = unit
type offset = unit
type block = unit
module Block_Forward = Block.Block_Forward
module Memory_Forward = Memory.Memory_Forward
val serialize_memory : widens:'a -> 'b -> 'c
val serialize_block : widens:'a -> 'b -> 'c
val memory_is_bottom : 'a -> 'b
val block_unknown : 'a -> 'b
val block_pretty : 'a -> 'b -> 'c
val memory_pretty : 'a -> 'b -> 'c
val block_empty : 'a -> 'b
val memory_empty : 'a -> 'b
module Query : sig ... end
val memory_is_empty : 'a -> 'b
val assume_memory : 'a -> 'b -> 'c -> 'd
val reachable : 'a -> 'b
val should_focus : size:'a -> 'b -> 'c
val may_alias : ptr_size:'a -> 'b -> size1:'c -> size2:'d -> 'e
val is_weak : size:'a -> 'b -> 'c -> 'd
val global_symbol : 'a -> 'b
val add_global_symbol : size:'a -> 'b -> 'c
val builtin_show_each_in : 'a -> 'b
val check_type : size:'a -> 'b -> 'c
val type_of : size:'a -> 'b -> 'c
val analyze_summary : 'a -> 'b
val addresses_in_block : 'a -> 'b
val addresses_in_memory : 'a -> 'b
val addresses_in_binary : size:'a -> 'b -> 'c

Function relative to offsets (to be removed) *

val offset_pretty : 'a -> 'b
val offset_zero : max:'a -> 'b -> 'c
val offset_shift : offset:'a -> max:'b -> 'c -> 'd
val offset_le : 'a -> 'b
val offset_eq : 'a -> 'b