Module Pulselib.PulseExecutionDomain

module F = Stdlib.Format
module AbductiveDomain = PulseAbductiveDomain
module DecompilerExpr = PulseDecompilerExpr
module LatentIssue = PulseLatentIssue
type 'abductive_domain_t base_t =
  1. | ContinueProgram of 'abductive_domain_t
    (*

    represents the state at the program point

    *)
  2. | ExceptionRaised of 'abductive_domain_t
    (*

    state after an exception has been thrown

    *)
  3. | ExitProgram of AbductiveDomain.Summary.t
    (*

    represents the state originating at exit/divergence.

    *)
  4. | AbortProgram of AbductiveDomain.Summary.t
    (*

    represents the state at the program point that caused an error

    *)
  5. | LatentAbortProgram of {
    1. astate : AbductiveDomain.Summary.t;
    2. latent_issue : LatentIssue.t;
    }
    (*

    this path leads to an error but we don't have conclusive enough data to report it yet

    *)
  6. | LatentInvalidAccess of {
    1. astate : AbductiveDomain.Summary.t;
    2. address : 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;
    }
    (*

    if address is ever observed to be invalid then there is an invalid access because it must_be_valid

    *)
  7. | LatentSpecializedTypeIssue of {
    1. astate : AbductiveDomain.Summary.t;
    2. specialized_type : IR.Typ.Name.t;
    3. trace : Pulselib.PulseBasicInterface.Trace.t;
    }
    (*

    this path leads to an error but we need to know where type specialization happened to report it

    *)
include Absint.AbstractDomain.Disjunct with type t := t
include Absint.AbstractDomain.Comparable with type t := t
include IStdlib.PrettyPrintable.PrintableType with type t := t
val leq : lhs:t -> rhs:t -> bool

the implication relation: lhs <= rhs means lhs |- rhs

val equal_fast : t -> t -> bool

equal_fast x y must imply x <=> y; it's a good idea for this function to be "fast", e.g. not depend on the size of its input

val is_normal : t -> bool

test if the abstract state represents exactly concrete states

val is_exceptional : t -> bool

test if the abstract state represents exactly exceptional concrete states

val is_executable : t -> bool

test if the abstract state represents executable states, e.g. ContinueProgram or ExceptionRaised.

val exceptional_to_normal : t -> t

convert all exceptional states into normal states (used when reaching a handler)

val pp_with_kind : IStdlib.Pp.print_kind -> PulsePathContext.t option -> F.formatter -> t -> unit
val pp : F.formatter -> t -> unit
val continue : AbductiveDomain.t -> t
val compare_summary : summary -> summary -> int
val equal_summary : summary -> summary -> bool
val yojson_of_summary : summary -> Ppx_yojson_conv_lib.Yojson.Safe.t
val pp_summary : F.formatter -> summary -> unit
val to_name : 'a base_t -> string