Module Codom.SM

type st = t option
module Symex = CSYMEX
include sig ... end
type 'a t = st -> ('a * st) Symex.t
val get_state : unit -> st t
val set_state : st -> unit t
val map_state : (st -> st) -> unit t
val run_with_state : state:st -> 'a t -> ('a * st) Symex.t
val with_state : state:st -> 'a t -> 'a t
val lift : 'a Symex.t -> 'a t
include Soteria.Sym_states.State_monad.Base_sig with type 'a t := 'a t with module Value = CSYMEX.Value
include Soteria.Symex.Core with type 'a t := 'a t with module Value = CSYMEX.Value
module Value = CSYMEX.Value
include Soteria.Soteria_std.Monad.Base with type 'a t := 'a t
val return : 'a -> 'a t
val bind : 'a t -> ('a -> 'b t) -> 'b t
val map : 'a t -> ('a -> 'b) -> 'b t
type lfail = [
  1. | `Lfail of Value.sbool Value.t
]

Type of error that corresponds to a logical failure (i.e. a logical mismatch during consumption).

Use this instead of `Lfail directly in type signatures to avoid potential typos such as `LFail which will take precious time to debug... trust me.

val pp_lfail : Ppx_deriving_runtime.Format.formatter -> lfail -> Ppx_deriving_runtime.unit
val show_lfail : lfail -> Ppx_deriving_runtime.string
type cons_fail = [
  1. | lfail
  2. | `Missing_subst of Soteria.Symex.Var.t
]
val pp_cons_fail : Ppx_deriving_runtime.Format.formatter -> cons_fail -> Ppx_deriving_runtime.unit
val show_cons_fail : cons_fail -> Ppx_deriving_runtime.string
type 'a v := 'a Value.t
type 'a vt := 'a Value.ty
type sbool := Value.sbool
val assume : sbool v list -> unit t
val vanish : unit -> 'a t
val assert_ : sbool v -> bool t

Assert is a symbolic process that does not branch but tests for the feasibility of the input symbolic value.

  • In UX, assert_ returns false if and only if not value is satisfiable.
  • In OX, assert_ returns true if and only if not value is unsatisfiable.
val nondet_UNSAFE : 'a vt -> 'a v

Do not use nondet_UNSAFE.

val nondet : 'a vt -> 'a v t

nondet ty creates a fresh variable of type ty.

val simplify : 'a v -> 'a v t

simplify v simplifies the value v according to the current path condition.

val fresh_var : 'a vt -> Soteria.Symex.Var.t t
val branch_on : ?left_branch_name:string -> ?right_branch_name:string -> sbool v -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t
val if_sure : ?left_branch_name:string -> ?right_branch_name:string -> sbool v -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t

if_sure cond ~then_ ~else_ evaluates the ~then_ branch if cond is guaranteed to hold in the current context, and otherwise evaluates ~else_.

This is to be used with caution: the ~then_ branch should always describe a behaviour that is semantically equivalent to that of the ~else_ branch when cond holds.

val branch_on_take_one : ?left_branch_name:string -> ?right_branch_name:string -> sbool v -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t

Branches on value, and (in UX only) takes at most one branch, starting with the then branch. This means that if the then_ branch is SAT, it is taken and the else_ branch is ignored, otherwise the else_ branch is taken. In OX mode, this behaves exactly as branch_on.

val give_up : string -> 'a t

Gives up on this path of execution for incompleteness reason. For instance, if a give feature is unsupported.

val branches : (unit -> 'a t) list -> 'a t

Fuel

val consume_fuel_steps : int -> unit t
val assert_or_error : Value.sbool Value.t -> 'err -> (unit, 'err, 'f) Soteria.Symex.Compo_res.t t

assert_or_error guard err asserts guard is true, and otherwise returns Compo_res.Error err. Biased towards the assertion being false to reduce SAT-checks.

This is provided as a utility, and is equivalent to

  branch_on (not guard)
    ~then_:(fun () -> return (Compo_res.error err))
    ~else_:(fun () -> return (Compo_res.ok ()))
val some_or_give_up : string -> 'a option -> 'a t

If the given option is None, gives up execution, otherwise continues, unwrapping the option.

val all : ('a -> 'b t) -> 'a list -> 'b list t
val fold_list : 'a list -> init:'b -> f:('b -> 'a -> 'b t) -> 'b t
val fold_iter : 'a Soteria.Soteria_std.Iter.t -> init:'b -> f:('b -> 'a -> 'b t) -> 'b t
val fold_seq : 'a Soteria.Soteria_std.Seq.t -> init:'b -> f:('b -> 'a -> 'b t) -> 'b t
val iter_list : 'a list -> f:('a -> unit t) -> unit t
val iter_iter : 'a Soteria.Soteria_std.Iter.t -> f:('a -> unit t) -> unit t
val map_list : 'a list -> f:('a -> 'b t) -> 'b list t
module Producer : sig ... end
module Consumer : sig ... end
module Result : sig ... end
module Syntax : sig ... end