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 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

}

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 mk_initial : IR.Tenv.t -> IR.Procdesc.t -> t
val get_pre : t -> BaseDomain.t
val get_post : t -> BaseDomain.t
val simplify_instanceof : IR.Tenv.t -> t -> 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 * 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 pre addresses, the live post 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
val is_isl_without_allocation : t -> bool
val is_pre_without_isl_abduced : t -> bool
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 skipped_calls_match_pattern : summary -> bool
val summary_of_post : IR.Tenv.t -> IR.Procdesc.t -> t -> (summary, [> `PotentialInvalidAccessSummary of summary * PulseBasicInterface.AbstractValue.t * (PulseBasicInterface.Trace.t * PulseBasicInterface.Invalidation.must_be_valid_reason option) ]) IStdlib.IStd.result 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 : PulseBasicInterface.PathCondition.new_eqs -> t -> (t, [> `PotentialInvalidAccess of t * PulseBasicInterface.AbstractValue.t * (PulseBasicInterface.Trace.t * PulseBasicInterface.Invalidation.must_be_valid_reason option) ]) IStdlib.IStd.result

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