Module Pulselib.PulseAbductiveDomain

module F = Stdlib.Format
module BaseDomain = PulseBaseDomain
module Decompiler = PulseDecompiler
module DecompilerExpr = PulseDecompilerExpr
module PathContext = PulsePathContext

Abductive, value-normalizing layer on top of BaseDomain

The operations in this module take care of two things that are important for the safety of domain operations:

1. Propagate operations on the current state to the pre-condition when necessary. This is the "abductive" part of the domain and follows the principles of biabduction as laid out in *Compositional Shape Analysis by Means of Bi-Abduction*, JACM, 2011, https://doi.org/10.1145/2049697.2049700. Simply put, a read from a memory location that is reachable from the precondition for the first time is taken to mean that this memory location had better been allocated since the beginning of the function for the operation to be safe, hence we "abduce" that this was the case and add it to the pre-condition (unless we already know that address to be invalid of course).

2. Normalize values (AbstractValue.t) in and out of the state according to their canonical representatives as per the current path condition. The idea is that one can ask about any abstract value and functions in this API will normalize it as needed first before querying the abstract state, and normalize any value found in the abstract state as needed too. For example, values in the raw map corresponding to the memory are not necessarily normalized at all times but the API allows one to pretend they are by normalizing them on the fly. On the other hand, *keys* in the memory map are always normalized so values must be normalized before being looked up in the map and this module takes care of that transparently too. See also PulseCanonValue.

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

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

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

type t = private {
  1. post : PostDomain.t;
    (*

    state at the current program point

    *)
  2. pre : PreDomain.t;
    (*

    inferred procedure pre-condition leading to the current program point

    *)
  3. path_condition : Pulselib.PulseBasicInterface.Formula.t;
    (*

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

    *)
  4. decompiler : Decompiler.t;
  5. topl : PulseTopl.state;
    (*

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

    *)
  6. need_dynamic_type_specialization : Pulselib.PulseBasicInterface.AbstractValue.Set.t;
    (*

    a set of abstract values that are used as receiver of method calls in the instructions reached so far

    *)
  7. transitive_info : Pulselib.PulseBasicInterface.TransitiveInfo.t;
    (*

    record transitive information inter-procedurally

    *)
  8. skipped_calls : Pulselib.PulseBasicInterface.SkippedCalls.t;
    (*

    metadata: procedure calls for which no summary was found

    *)
}

pre/post on a single program path

include Ppx_compare_lib.Equal.S with type t := t
val equal : t Base__Ppx_compare_lib.equal
val leq : lhs:t -> rhs:t -> bool
val pp : Stdlib.Format.formatter -> t -> unit
val mk_initial : IR.Tenv.t -> IR.ProcAttributes.t -> t
module Stack : sig ... end

Safe version of PulseBaseStack

module Memory : sig ... end

Safe version of PulseBaseMemory

module AddressAttributes : sig ... end

Safe version of PulseBaseAddressAttributes

val should_havoc_if_unknown : unit -> [> `ShouldHavoc | `ShouldOnlyHavocResources ]

do as much as possible to assume "the best" happened at that location: deallocate and initialize everything reachable from the address, then havoc all the edges starting from the address passing havoc_filter (by default everything passes the filter)

val is_local : IR.Var.t -> t -> bool
val find_post_cell_opt : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> BaseDomain.cell option
val reachable_addresses_from : ?edge_filter:(Pulselib.PulseBasicInterface.Access.t -> bool) -> Pulselib.PulseBasicInterface.AbstractValue.t Stdlib.Seq.t -> t -> [ `Pre | `Post ] -> Pulselib.PulseBasicInterface.AbstractValue.Set.t

Compute the set of abstract addresses that are reachable from given abstract addresses.

val get_unreachable_attributes : t -> Pulselib.PulseBasicInterface.AbstractValue.t list

collect the addresses that have attributes but are unreachable in the current post-condition

val mark_potential_leaks : IBase.Location.t -> dead_roots:IR.Var.t list -> t -> t
val add_skipped_call : IR.Procname.t -> Pulselib.PulseBasicInterface.Trace.t -> t -> t
val add_skipped_calls : Pulselib.PulseBasicInterface.SkippedCalls.t -> t -> t
val add_missed_captures : IR.Typ.Name.Set.t -> t -> t
val set_path_condition : Pulselib.PulseBasicInterface.Formula.t -> t -> t
val record_transitive_access : IBase.Location.t -> t -> t
val add_need_dynamic_type_specialization : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> t
val map_decompiler : t -> f:(Decompiler.t -> Decompiler.t) -> t
val add_block_source : Pulselib.PulseBasicInterface.AbstractValue.t -> string -> t -> t
val set_post_edges : Pulselib.PulseBasicInterface.AbstractValue.t -> PulseBaseMemory.Edges.t -> t -> t

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

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

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

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 result is Unsat.

Similar to incorporate_new_eqs, but apply to an abstract value.

module Summary : sig ... end
val transfer_transitive_info_to_caller : IR.Procname.t -> IBase.Location.t -> Summary.t -> t -> t
module Topl : sig ... end
module CanonValue : sig ... end

see PulseCanonValue