package soteria

You can search for identifiers within the package.

in-package search v0.2.0

Soteria is a toolkit for writing symbolic bug-finding tools

Install

dune-project

Dependency

github.com Readme Changelog Edit opam file Versions (2)

Authors

Maintainers

Sources

v0.2.3.tar.gz

md5=22e0fc3f97555ac35b96fae10817a887

sha512=10457c9d1302e3f3018dca652cdf81f0cdfd461a79eca1a8a8b754e964a47f7f35c10a8c07aff8f5193ee7e794440635d788d91925ce75fb8280b60b4f0d6663

doc/soteria/Soteria/Symex/module-type-Base/index.html

Module type `Symex.Base`

include Core

module Value : Value.S

type 'a t

Represents a yet-to-be-executed symbolic process which terminates with a value of type 'a.

include Soteria.Soteria_std.Monad.Base with type 'a t := 'a t

type lfail = [

| `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 = [

| lfail
| `Missing_subst of 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

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 -> 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 Syntax : sig ... end

module Producer : sig ... end

module Consumer : sig ... end