Pulselib.PulseAbductiveDomain
module BaseDomain = PulseBaseDomain
module Decompiler = PulseDecompiler
module DecompilerExpr = PulseDecompilerExpr
module PathContext = PulsePathContext
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
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 : Pulselib.PulseBasicInterface.Formula.t;
arithmetic facts true along the path (holding for both pre
and post
since abstract values are immutable)
decompiler : Decompiler.t;
topl : PulseTopl.state;
state at of the Topl monitor at the current program point, when Topl is enabled
*)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
*)transitive_info : Pulselib.PulseBasicInterface.TransitiveInfo.t;
record transitive information inter-procedurally
*)recursive_calls : PulseMutualRecursion.Set.t;
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 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 apply_unknown_effect :
?havoc_filter:
(Pulselib.PulseBasicInterface.AbstractValue.t ->
PulseAccess.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
bool) ->
Pulselib.PulseBasicInterface.ValueHistory.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
t ->
t
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 find_post_cell_opt :
Pulselib.PulseBasicInterface.AbstractValue.t ->
t ->
BaseDomain.cell option
val fold_all :
?var_filter:(IR.Var.t -> bool) ->
init:'accum ->
finish:('accum -> 'final) ->
f:
(IR.Var.t ->
'accum ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
Pulselib.PulseBasicInterface.Access.t list ->
('accum, 'final) IStdlib.IStd.Continue_or_stop.t) ->
?f_revisit:
(IR.Var.t ->
'accum ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
Pulselib.PulseBasicInterface.Access.t list ->
'accum) ->
t ->
[ `Post | `Pre ] ->
'final
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_recursive_call :
IBase.Location.t ->
IR.Procname.t ->
t ->
t * PulseMutualRecursion.t
val add_recursive_calls : PulseMutualRecursion.Set.t -> 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 record_call_resolution :
caller:IR.Procdesc.t ->
IBase.Location.t ->
Pulselib.PulseBasicInterface.TransitiveInfo.Callees.call_kind ->
Pulselib.PulseBasicInterface.TransitiveInfo.Callees.resolution ->
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
val incorporate_new_eqs :
Pulselib.PulseBasicInterface.Formula.new_eqs ->
t ->
(t,
[> `PotentialInvalidAccess of
t
* Pulselib.PulseBasicInterface.AbstractValue.t
* (Pulselib.PulseBasicInterface.Trace.t
* Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason
option) ])
IStdlib.IStd.result
Pulselib.PulseBasicInterface.SatUnsat.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 result is Unsat
.
val incorporate_new_eqs_on_val :
Pulselib.PulseBasicInterface.Formula.new_eqs ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
Pulselib.PulseBasicInterface.AbstractValue.t
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