Parameter Make.Domain

include Domains.Memory_domains.With_focusing.BASE_WITH_TYPES
include Domains.Memory_sig.Base
include Domains.Sig.BASE
include Domains.Sig.Minimal
include Domains.Sig.Minimal_No_Boolean
include Domains.Sig.With_Id
val unique_id : unit -> Domains.Sig.Fresh_id.t
val name : unit -> string
include Domains.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.

type boolean

Guards

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

type block
type offset
type memory
include Domains.Memory_sig.WITH_QUERIES with module Context := Context and type binary := binary and type memory := memory and type offset := offset and type address := binary and type enum := enum
include Domains.Sig.WITH_QUERIES with module Context := Context with type binary := binary with type enum := enum
module Query : sig ... end
include Domains.Memory_sig.WITH_MEMORY_QUERIES with module Context := Context and type memory := memory and type address := binary and type offset := offset
val should_focus : size:Units.In_bits.t -> Context.t -> memory -> binary -> (binary * offset) option

should_focus ~size ctx mem addr asks the domain whether it is useful to "focus" (or "unfold", i.e. try to represent precisely the memory region pointed to by addr, as long as aliasing info ensures that it is sound) a loaded value. size should be the size of addr. If the answer is yes, then the returned value should contain three things about the region to focus: its base, the offset of the end and the offset of addr in it (in bits).

val may_alias : ptr_size:Units.In_bits.t -> Context.t -> size1:offset -> size2:offset -> binary -> binary -> bool

may_alias ~ptr_size ~size1 ~size2 ctx addr1 addr2 should return whether the region starting at addr1 of size size1 bytes and the region starting at addr2 of size size2 bytes may have a non-empty intersection. This function is used by focusing abstractions to discard a focused region when writing in a possibly aliased address. ptr_size is the size in bits of both addr1 and addr2.

val is_weak : size:Units.In_bits.t -> Context.t -> binary -> bool

is_weak ~size ctx addr asks the domain whether the address addr points to a weak type which indicates that the address will not alias with any other

include Domains.Memory_sig.WITH_BLOCK_OFFSET with module Context := Context and type offset := offset and type boolean := boolean

Transfer functions

val offset_zero : max:int option -> Context.t -> offset

Beginning of a region (offset 0) of size max (in bytes, if known and/or useful).

val offset_shift : offset:int -> max:int option -> Context.t -> offset -> offset

address := address + k

val offset_le : Context.t -> offset -> offset -> boolean

Offset comparison.

val offset_eq : Context.t -> offset -> offset -> boolean
include Domains.Memory_sig.WITH_BLOCK with module Context := Context and type block := block and type offset := offset and type boolean := boolean and type value := binary
val block_empty : Context.t -> block
val block_unknown : Context.t -> block
val block_pretty : Context.t -> Stdlib.Format.formatter -> block -> unit
val serialize_block : widens:bool -> Context.t -> block -> Context.t -> block -> 'a Context.in_acc -> (block, 'a) Context.result
val addresses_in_block : Context.t -> block -> Context.t -> block -> (binary * binary) list
include Domains.Memory_sig.WITH_BLOCK_FORWARD with module Context := Context and type boolean := boolean and type value := binary and type block := block and type offset := offset
val offset_pretty : Context.t -> Stdlib.Format.formatter -> offset -> unit
include Domains.Memory_sig.WITH_MEMORY with module Context := Context and type memory := memory and type address := binary and type boolean := boolean and type block := block and type offset := offset and type value := binary
val serialize_memory : widens:bool -> Context.t -> memory -> Context.t -> memory -> 'a Context.in_acc -> (memory, 'a) Context.result
val memory_pretty : Context.t -> Stdlib.Format.formatter -> memory -> unit
val addresses_in_memory : Context.t -> memory -> Context.t -> memory -> (binary * binary) list
include Domains.Memory_sig.WITH_MEMORY_FORWARD with module Context := Context and type memory := memory and type address := binary and type boolean := boolean and type block := block and type offset := offset and type value := binary
module Memory_Forward : Operator.MEMORY_FORWARD with module Arity := Domains.Sig.Context_Arity_Forward(Context) and type boolean := boolean and type address := binary and type memory := memory and type block := block and type value := binary

Check if the memory is reachable. sat means reachable.

val global_symbol : Context.t -> string -> Units.In_bits.t * binary

Retrieves the value of a global symbol

val add_global_symbol : size:Units.In_bits.t -> Context.t -> string -> binary -> unit

Updates the value of a global symbol

Type check a binary value

val type_of : size:Units.In_bits.t -> Context.t -> binary -> Types.TypedC.typ option

Retrieves the type of value (this only works if it is a pointer and should only be used when looking at function pointers)

val flush_cache : Context.t -> memory -> memory
val serialize_memory_and_cache : 'a. widens:bool -> Context.t -> memory -> Context.t -> memory -> (binary * binary) list -> 'a Context.in_acc -> (memory, 'a) Context.result