Module type `Sig.Minimal_No_Boolean`

This signature is useful when we don't have any new flow-sensitive state and just need all the things on the top of the stack to stay the same.

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.

raises Bottom

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.

Module type Sig.Minimal_No_Boolean

Module type `Sig.Minimal_No_Boolean`