package soteria

  1. Overview
  2. Docs
package soteria
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module State_monad.Make

Parameters

module Sym : Symex.Base
module State : sig ... end

Signature

type st = State.t
module Symex = Sym
include sig ... end
type 'a t = State.t -> ('a * State.t) Sym.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 Base_sig with type 'a t := 'a t with module Value = Sym.Value
include Symex.Core with type 'a t := 'a t with module Value = Sym.Value
module Value = Sym.Value
include Soteria.Soteria_std.Monad.Base with type 'a t := 'a 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.

type cons_fail = [
  1. | lfail
  2. | `Missing_subst of Soteria.Symex.Var.t
]
val show_cons_fail : cons_fail -> Ppx_deriving_runtime.string
val assume : Value.sbool Value.t list -> unit t
val vanish : unit -> 'a t
val assert_ : Value.sbool Value.t -> 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 Value.ty -> 'a Value.t

Do not use nondet_UNSAFE.

val nondet : 'a Value.ty -> 'a Value.t t

nondet ty creates a fresh variable of type ty.

val simplify : 'a Value.t -> 'a Value.t t

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

val fresh_var : 'a Value.ty -> Soteria.Symex.Var.t t
val branch_on : ?left_branch_name:string -> ?right_branch_name:string -> Value.sbool Value.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t
val if_sure : ?left_branch_name:string -> ?right_branch_name:string -> Value.sbool Value.t -> 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 -> Value.sbool Value.t -> 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 with_frame : string -> (unit -> 'a t) -> 'a t

Runs the process within a section of execution with given name. Corresponds to frames in the flamegraph.

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

Fuel

val consume_fuel_steps : int -> unit t
val log_solver_state : level:Logs.Level.t -> unit -> unit

Logs the current solver state, at the given log level

include Soteria.Soteria_std.Monad.S with type 'a t := 'a t
include Soteria_std.Monad.Base with type 'a t := 'a t
val return : 'a -> 'a t
val bind : ('a -> 'b t) -> 'a t -> 'b t
val map : ('a -> 'b) -> 'a t -> 'b t
include Soteria_std.Monad.Extension with type 'a t := 'a t
val fold : (module M : Soteria_std.Sigs.Foldable) -> 'elem M.t -> init:'a -> f:('a -> 'elem -> 'a t) -> 'a t
val fold_list : 'elem list -> init:'a -> f:('a -> 'elem -> 'a t) -> 'a t
val fold_iter : 'elem Iter.t -> init:'a -> f:('a -> 'elem -> 'a t) -> 'a t
val iter : (module M : Soteria_std.Sigs.Foldable) -> 'elem M.t -> f:('elem -> unit t) -> unit t
val iter_list : 'elem list -> f:('elem -> unit t) -> unit t
val iter_iter : 'elem Iter.t -> f:('elem -> unit t) -> unit t
val map_m : (module M : Soteria_std.Sigs.Foldable) -> 'elem M.t -> f:('elem -> 'a t) -> 'a list t
val map_list : 'elem list -> f:('elem -> 'a t) -> 'a list t
val map_iter : 'elem Iter.t -> f:('elem -> 'a t) -> 'a list t
val assert_or_error : Value.sbool Value.t -> 'err -> (unit, 'err, 'f) Soteria.Soteria_std.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.

module Result : sig ... end
module Producer : sig ... end
module Consumer : sig ... end
module Syntax : sig ... end