PulseOperationResult.Import
For open
ing in other modules.
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
for opening locally
type ('ok, 'err) pulse_result = ('ok, 'err) PulseResult.t =
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 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.t
s (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
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
| ExitProgram of Pulselib.PulseDomainInterface.AbductiveDomain.Summary.t
| AbortProgram of Pulselib.PulseDomainInterface.AbductiveDomain.Summary.t
| LatentAbortProgram of {
astate : Pulselib.PulseDomainInterface.AbductiveDomain.Summary.t;
latent_issue : Pulselib.PulseDomainInterface.LatentIssue.t;
}
| LatentInvalidAccess of {
astate : Pulselib.PulseDomainInterface.AbductiveDomain.Summary.t;
address : Pulselib.PulseDomainInterface.DecompilerExpr.t;
must_be_valid : Pulselib.PulseBasicInterface.Trace.t
* Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason
option;
calling_context : (Pulselib.PulseBasicInterface.CallEvent.t * IBase.Location.t)
list;
}
| LatentSpecializedTypeIssue of {
astate : Pulselib.PulseDomainInterface.AbductiveDomain.Summary.t;
specialized_type : IR.Typ.Name.t;
trace : Pulselib.PulseBasicInterface.Trace.t;
}
type base_error = Pulselib.PulseDomainInterface.AccessResult.error =
| PotentialInvalidAccess of {
astate : Pulselib.PulseDomainInterface.AbductiveDomain.t;
address : Pulselib.PulseDomainInterface.DecompilerExpr.t;
must_be_valid : Pulselib.PulseBasicInterface.Trace.t
* Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason
option;
}
| PotentialInvalidSpecializedCall of {
astate : Pulselib.PulseDomainInterface.AbductiveDomain.t;
specialized_type : IR.Typ.Name.t;
trace : Pulselib.PulseBasicInterface.Trace.t;
}
| ReportableError of {
astate : Pulselib.PulseDomainInterface.AbductiveDomain.t;
diagnostic : Pulselib.PulseDomainInterface.Diagnostic.t;
}
| WithSummary of base_error
* Pulselib.PulseDomainInterface.AbductiveDomain.Summary.t