Import (infer.Pulselib.PulseOperationResult.Import)

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:

X is * if b is a SatUnsat.t and c a SatUnsat.t too (bind)
X is + if b is a SatUnsat.t and c is not (map)
X is = if b is *not* a SatUnsat.t and c is a SatUnsat.t

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

type ('ok, 'err) pulse_result = ('ok, 'err) PulseResult.t =

| Ok of 'ok
| Recoverable of 'ok * 'err list
| 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

val (let=+) : 
  'a Pulselib.PulseDomainInterface.AccessResult.t ->
  ('a -> 'b Pulselib.PulseDomainInterface.AccessResult.t) ->
  'b t

val (>>>|) : 
  'a Pulselib.PulseDomainInterface.AccessResult.t ->
  ('a -> 'b Pulselib.PulseDomainInterface.AccessResult.t) ->
  'b t

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

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 (let<**>) : 
  'a t ->
  ('a -> 'b Pulselib.PulseDomainInterface.AccessResult.t list) ->
  'b Pulselib.PulseDomainInterface.AccessResult.t list

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

val (let<+>) : 
  'a Pulselib.PulseDomainInterface.AccessResult.t ->
  ('a -> Pulselib.PulseDomainInterface.AbductiveDomain.t) ->
  Pulselib.PulseDomainInterface.ExecutionDomain.t
    Pulselib.PulseDomainInterface.AccessResult.t
    list

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

val (let<++>) : 
  'a t ->
  ('a -> Pulselib.PulseDomainInterface.AbductiveDomain.t) ->
  Pulselib.PulseDomainInterface.ExecutionDomain.t
    Pulselib.PulseDomainInterface.AccessResult.t
    list

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

type access_mode =

| Read
| Write
| 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 =

| ContinueProgram of 'abductive_domain_t
| ExceptionRaised of 'abductive_domain_t
| Stopped of Pulselib.PulseDomainInterface.ExecutionDomain.stopped_execution

type base_error = Pulselib.PulseDomainInterface.AccessResult.error =

| PotentialInvalidAccess of {
1. astate : Pulselib.PulseDomainInterface.AbductiveDomain.t;
2. address : Pulselib.PulseDomainInterface.DecompilerExpr.t;
3. must_be_valid : Pulselib.PulseBasicInterface.Trace.t * Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason option;
}
| PotentialInvalidSpecializedCall of {
1. astate : Pulselib.PulseDomainInterface.AbductiveDomain.t;
2. specialized_type : IR.Typ.Name.t;
3. trace : Pulselib.PulseBasicInterface.Trace.t;
}
| ReportableError of {
1. astate : Pulselib.PulseDomainInterface.AbductiveDomain.t;
2. diagnostic : Pulselib.PulseDomainInterface.Diagnostic.t;
}
| WithSummary of base_error * Pulselib.PulseDomainInterface.AbductiveDomain.Summary.t

Monadic operations on the combined monad of SatUnsat and AccessResult.

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

Monadic operations on the combined monad of `SatUnsat` and `AccessResult`.