Module Pulselib.PulseAbductiveDomain

module F = Stdlib.Format
module BaseAddressAttributes = PulseBaseAddressAttributes
module BaseDomain = PulseBaseDomain
module BaseMemory = PulseBaseMemory
module BaseStack = PulseBaseStack
module type BaseDomainSig = sig ... end

signature common to the "normal" Domain, representing the post at the current program point, and the inverted PreDomain, representing the inferred pre-condition

module PostDomain : BaseDomainSig

The post abstract state at each program point, or current state.

module PreDomain : BaseDomainSig

The inferred pre-condition at each program point, biabduction style.

type isl_status =
| ISLOk

ok triple: the program executes without error

| ISLError

Error specification: an invalid address recorded in the precondition will cause an error

Execution status, similar to PulseExecutionDomain but for ISL (Incorrectness Separation Logic) mode, where PulseExecutionDomain.base_t.ContinueProgram can also contain "error specs" that describe what happens when some addresses are invalid explicitly instead of relying on MustBeValid attributes.

val equal_isl_status : isl_status -> isl_status -> bool
type t = private {
post : PostDomain.t;

state at the current program point

pre : PreDomain.t;

inferred procedure pre-condition leading to the current program point

path_condition : PulseBasicInterface.PathCondition.t;

arithmetic facts true along the path (holding for both pre and post since abstract values are immutable)

topl : PulseTopl.state;

state at of the Topl monitor at the current program point, when Topl is enabled

skipped_calls : PulseBasicInterface.SkippedCalls.t;

metadata: procedure calls for which no summary was found

isl_status : isl_status;
}

pre/post on a single program path

val equal : t -> t -> bool
val leq : lhs:t -> rhs:t -> bool
val pp : Stdlib.Format.formatter -> t -> unit
val set_isl_status : isl_status -> t -> t
val mk_initial : IR.Tenv.t -> IR.Procdesc.t -> t
val get_pre : t -> BaseDomain.t
val get_post : t -> BaseDomain.t
module Stack : sig ... end

stack operations like BaseStack but that also take care of propagating facts to the precondition

module Memory : sig ... end

memory operations like BaseMemory but that also take care of propagating facts to the precondition

module AddressAttributes : sig ... end

attribute operations like BaseAddressAttributes but that also take care of propagating facts to the precondition

val is_local : IR.Var.t -> t -> bool
val find_post_cell_opt : PulseBasicInterface.AbstractValue.t -> t -> BaseDomain.cell option
val discard_unreachable : t -> t * Pulselib.PulseBasicInterface.AbstractValue.Set.t * PulseBasicInterface.AbstractValue.t list

garbage collect unreachable addresses in the state to make it smaller and return the new state, the live addresses, and the discarded addresses that used to have attributes attached

val add_skipped_call : IR.Procname.t -> PulseBasicInterface.Trace.t -> t -> t
val add_skipped_calls : PulseBasicInterface.SkippedCalls.t -> t -> t
val set_path_condition : PulseBasicInterface.PathCondition.t -> t -> t
type summary = private t

private type to make sure summary_of_post is always called when creating summaries

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 summary_of_post : IR.Procdesc.t -> t -> summary PulseBasicInterface.SatUnsat.t

trim the state down to just the procedure's interface (formals and globals), and simplify and normalize the state

val set_post_edges : PulseBasicInterface.AbstractValue.t -> BaseMemory.Edges.t -> t -> t

directly set the edges for the given address, bypassing abduction altogether

val set_post_cell : (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> BaseDomain.cell -> IBase.Location.t -> t -> t

directly set the edges and attributes for the given address, bypassing abduction altogether

val incorporate_new_eqs : t -> (PulseBasicInterface.PathCondition.t * PulseBasicInterface.PathCondition.new_eqs) -> PulseBasicInterface.PathCondition.t

Check that the new equalities discovered are compatible with the current pre and post heaps, e.g. x = 0 is not compatible with x being allocated, and x = y is not compatible with x and y being allocated separately. In those cases, the resulting path condition is PathCondition.false_.

val initialize : PulseBasicInterface.AbstractValue.t -> t -> t

Remove "Uninitialized" attribute of the given address

val set_uninitialized : IR.Tenv.t -> [ `LocalDecl of IR.Pvar.t * PulseBasicInterface.AbstractValue.t option | `Malloc of PulseBasicInterface.AbstractValue.t ] -> IR.Typ.t -> IBase.Location.t -> t -> t

Add "Uninitialized" attributes when a variable is declared or a memory is allocated by malloc.

module Topl : sig ... end