package soteria

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

Module Soteria_std.Compo_res

This module defines a three-way result type for compositional symbolic execution. Unlike standard Result.t which has two cases (Ok/Error), this type adds a third case Missing for bi-abduction scenarios where anti-frame inference is needed, or more generally to represent incompletenesses in the engine.

When performing a function call, the current state may not contain all resources needed by the callee. Rather than immediately failing, we can infer what's missing (the "anti-frame") and continue analysis.

Three Cases:

  • Ok: Operation succeeded, resources matched
  • Error: Definite error found (e.g., null dereference, assertion failure)
  • Missing: Resources needed but not present; includes fixes. Missing contains a list of fixes, providing different ways to resolve the missing resources; for instance, when accessing a location in memory, two options are possible: either the location is allocated, or the location has been freed.

This module also provides a functor to lift this result type into any monadic context.

type ('ok, 'err, 'fix) t =
  1. | Ok of 'ok
  2. | Error of 'err
  3. | Missing of 'fix list
val pp : ok:(Format.formatter -> 'a -> unit) -> err:(Format.formatter -> 'b -> unit) -> miss:'c Fmt.t -> Format.formatter -> ('a, 'b, 'c) t -> unit
val ok : 'a -> ('a, 'b, 'c) t
val error : 'a -> ('b, 'a, 'c) t
val miss : 'a list -> ('b, 'c, 'a) t
val is_ok : ('a, 'b, 'c) t -> bool
val is_error : ('a, 'b, 'c) t -> bool
val is_missing : ('a, 'b, 'c) t -> bool
val get_ok : ('a, 'b, 'c) t -> 'a
val get_error : ('a, 'b, 'c) t -> 'b
val get_missing : ('a, 'b, 'c) t -> 'c list
val only_oks : ('a, 'b, 'c) t list -> 'a list
val only_errors : ('a, 'b, 'c) t list -> 'b list
val only_missings : ('a, 'b, 'c) t list -> 'c list list
val bind : ('a -> ('b, 'c, 'd) t) -> ('a, 'c, 'd) t -> ('b, 'c, 'd) t
val map : ('a -> 'b) -> ('a, 'c, 'd) t -> ('b, 'c, 'd) t
val bind_error : ('a -> ('b, 'c, 'd) t) -> ('b, 'a, 'd) t -> ('b, 'c, 'd) t
val map_error : ('a -> 'b) -> ('c, 'a, 'd) t -> ('c, 'b, 'd) t
val map_missing : ('a -> 'b) -> ('c, 'd, 'a) t -> ('c, 'd, 'b) t
val to_result_opt : ('a, 'b, 'c) t -> ('a, 'b) Result.t option
val of_result : ('a, 'b) Result.t -> ('a, 'b, 'c) t
module Syntax : sig ... end

Module types

Monads with three type parameters

module type Base = sig ... end

Basic interface for the compositional result monad.

module type Syntax = sig ... end
module type S = sig ... end

Complete interface for the compositional result monad, including generic operations and syntax.

Functors

module Extend (M : Base) : S with type ('ok, 'err, 'fix) t = ('ok, 'err, 'fix) M.t

Complete interface for the compositional result monad, including generic operations and syntax.

module Make_syntax (M : Base) : Syntax with type ('ok, 'err, 'fix) t := ('ok, 'err, 'fix) M.t
module T (M : Soteria_std.Monad.Base) : S with type ('ok, 'err, 'fix) t = ('ok, 'err, 'fix) t M.t

Complete interface for the compositional result monad, including generic operations and syntax.