Module PulseOperationResult.Import

For opening in other modules.

Monadic operations on the combined monad of SatUnsat and AccessResult.

let operators produce _ t values following the naming convention letXY where X and Y depend on the types of the inputs: in letXY a = b in c, X is according to the SatUnsat.t behaviour and Y about the AccessResult.t behaviour:

Similarly Y is * or + depending on whether the operation on the underlying AccessResult.t is a map or or bind.

We also define inline operations >>UV with U being =, |, or > corresponding to *, +, or = above, and similarly for V.

In practice, to figure out which let binder or operator is right for your call site, just have a look at the types! To figure out which letXY to use for letXY a = b in c, pick the one with the type type_of_b -> (type_of_a -> type_of_c) -> type_of_letXY_a_equal_b_in_c.

include module type of PulseResult.Let_syntax
include module type of PulseResult.Monad_infix
include module type of PulseResult.Type

for opening locally

type ('ok, 'err) pulse_result = ('ok, 'err) PulseResult.t =
  1. | Ok of 'ok
  2. | Recoverable of 'ok * 'err list
  3. | FatalError of 'err * 'err list
val (>>|) : ('ok, 'err) PulseResult.t -> ('ok -> 'okk) -> ('okk, 'err) PulseResult.t
val (>>=) : ('ok, 'err) PulseResult.t -> ('ok -> ('okk, 'err) PulseResult.t) -> ('okk, 'err) PulseResult.t
val let+ : ('ok, 'err) PulseResult.t -> ('ok -> 'okk) -> ('okk, 'err) PulseResult.t
val let* : ('ok, 'err) PulseResult.t -> ('ok -> ('okk, 'err) PulseResult.t) -> ('okk, 'err) PulseResult.t
val let** : 'a t -> ('a -> 'b t) -> 'b t
val (>>==) : 'a t -> ('a -> 'b t) -> 'b t
val let++ : 'a t -> ('a -> 'b) -> 'b t
val (>>||) : 'a t -> ('a -> 'b) -> 'b t
val let+* : 'a t -> ('a -> 'b Pulselib.PulseDomainInterface.AccessResult.t) -> 'b t
val (>>|=) : 'a t -> ('a -> 'b Pulselib.PulseDomainInterface.AccessResult.t) -> 'b t
val let=* : 'a Pulselib.PulseDomainInterface.AccessResult.t -> ('a -> 'b t) -> 'b t
val (>>>=) : 'a Pulselib.PulseDomainInterface.AccessResult.t -> ('a -> 'b t) -> 'b t

monadic "bind" but not really that turns an AccessResult.t into a list of AccessResult.ts (not really because the first type is not an AccessResult.t list but just an AccessResult.t)

val bind_sat_result : 'c -> 'a t -> ('a -> 'b Pulselib.PulseDomainInterface.AccessResult.t list * 'c) -> 'b Pulselib.PulseDomainInterface.AccessResult.t list * 'c

monadic "map" but even less really that turns a AccessResult.t into an analysis result

Imported types for ease of use and so we can write variants without the corresponding module prefix

type access_mode =
  1. | Read
  2. | Write
  3. | NoAccess
    (*

    The initialized-ness of the address is not checked when it evaluates a heap address without actual memory access, for example, when evaluating &x.f we need to check initialized-ness of x, not that of x.f.

    *)
type 'abductive_domain_t execution_domain_base_t = 'abductive_domain_t Pulselib.PulseDomainInterface.ExecutionDomain.base_t =
  1. | ContinueProgram of 'abductive_domain_t
  2. | ExceptionRaised of 'abductive_domain_t
  3. | ExitProgram of Pulselib.PulseDomainInterface.AbductiveDomain.Summary.t
  4. | AbortProgram of Pulselib.PulseDomainInterface.AbductiveDomain.Summary.t
  5. | LatentAbortProgram of {
    1. astate : Pulselib.PulseDomainInterface.AbductiveDomain.Summary.t;
    2. latent_issue : Pulselib.PulseDomainInterface.LatentIssue.t;
    }
  6. | LatentInvalidAccess of {
    1. astate : Pulselib.PulseDomainInterface.AbductiveDomain.Summary.t;
    2. address : Pulselib.PulseDomainInterface.DecompilerExpr.t;
    3. must_be_valid : Pulselib.PulseBasicInterface.Trace.t * Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason option;
    4. calling_context : (Pulselib.PulseBasicInterface.CallEvent.t * IBase.Location.t) list;
    }
  7. | LatentSpecializedTypeIssue of {
    1. astate : Pulselib.PulseDomainInterface.AbductiveDomain.Summary.t;
    2. specialized_type : IR.Typ.Name.t;
    3. trace : Pulselib.PulseBasicInterface.Trace.t;
    }