Module Overflow_checks.Make

This functor adds overflow checks to bitvector operations. I.E. for a biadd with ~size=32 it first performs the addition on 33 bits, then checks if the result fits in 32 bits (Checking signedness according to the various flags). Similarly, it adds guards to bisub, bimul, and bisdiv (dividing min_int by -1 underflows). There are no overflow guards on shifts as of yet.

If not, then it assume that it does fit, raising Sig.Bottom if the overflow is guaranteed.

It can also optionaly raise an alarm when a possible overflow is detected.

Specifically:

  • Binary_Forward.biadd ~size ~nsw:true and Binary_Forward.bisub ~size ~nsw:true now check then assume that their results (interpreted as signed) is in range [-2^{size-1} .. 2^{size-1}-1] (using signed comparison Binary_Forward.bisle)
  • Binary_Forward.biadd ~size ~nuw:true and Binary_Forward.bisub ~size ~nuw:true now check then assume that their results (interpreted as unsigned) is smaller than [2^{size}-1] (using unsigned comparison Binary_Forward.biule)
  • Binary_Forward.biadd ~size ~nusw:true and Binary_Forward.bisub ~size ~nusw:true now check then assume that their results (where left argument is unsigned, right argument is signed) is in range [0 .. 2^{size}-1] (fits unsigned result). This flag is assumed to be mutually exclusive with the two previous ones.

Parameters

Signature

include Sig.BASE with type boolean = Sub.boolean with type binary = Sub.binary with type enum = Sub.enum
include Sig.Minimal with type boolean = Sub.boolean
include Sig.Minimal_No_Boolean with type boolean = Sub.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.

type boolean = Sub.boolean

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
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 = Sub.binary
type enum = Sub.enum
include Sig.WITH_QUERIES with module Context := Context and type binary := binary and type enum := enum
module Query : sig ... end
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
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 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
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 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 = Sub.integer
type integer = Sub.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