PulseCanonValue.S
elements of the base abstract domain (stack, heap, attributes) with a type-safe interface that reflects the expected normalization status of the abstract values they mention
type t = private Pulselib.PulseBasicInterface.AbstractValue.t
an abstract value that is the canonical representative of its equivalence class (of other abstract values that are equal to it) in the current state (this may not be true if more equalities are added or generally any time the formula inside the state changes)
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
include Ppx_compare_lib.Equal.S with type t := t
val equal : t Base__Ppx_compare_lib.equal
val pp : F.formatter -> t -> unit
module Set : IStdlib.PrettyPrintable.PPSet with type elt = t
val downcast_set : Set.t -> Pulselib.PulseBasicInterface.AbstractValue.Set.t
val unsafe_cast_set : Pulselib.PulseBasicInterface.AbstractValue.Set.t -> Set.t
an abstract value that needs to be normalized; just AbstractValue.t
under the hood too
PulseAbductiveDomain.t
but we cannot mention it there otherwise it would create a circular dependency.
Also provided are helper functions that normalize inside of more complex values such as tuples. In that case the functions take care to preserve physical equality if the input value is already its own canonical representative.
We need separate functions for AbstractValue.t
and needs_canon
values because of the type system. By convention functions that end in '
are the same as the non-primed ones but operate on AbstractValue.t
instead of needs_canon
ones.
val canon : astate -> needs_canon -> t
fetch the canonical representative of the given needs_canon
val canon' : astate -> Pulselib.PulseBasicInterface.AbstractValue.t -> t
fetch the canonical representative of the given AbstractValue.t
val canon_fst : astate -> (needs_canon * 'a) -> t * 'a
val canon_fst' :
astate ->
(Pulselib.PulseBasicInterface.AbstractValue.t * 'a) ->
t * 'a
val canon_snd_fst : astate -> ('a * (needs_canon * 'b)) -> 'a * (t * 'b)
val canon_opt : astate -> needs_canon option -> t option
val canon_opt' :
astate ->
Pulselib.PulseBasicInterface.AbstractValue.t option ->
t option
val canon_opt_fst : astate -> (needs_canon * 'a) option -> (t * 'a) option
val canon_opt_fst4' :
astate ->
(Pulselib.PulseBasicInterface.AbstractValue.t * 'a * 'b * 'c) option ->
(t * 'a * 'b * 'c) option
val mk_fresh : unit -> t
This is just AbstractValue.mk_fresh
so technically is only guaranteed to produce a canonical representative if the value is not immediately made equal to another one... Use with caution!
val unsafe_cast : Pulselib.PulseBasicInterface.AbstractValue.t -> t
module Stack : sig ... end
module Memory :
PulseBaseMemory.S
with type key := t
and type in_map_t :=
Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t
and type out_of_map_t :=
needs_canon * Pulselib.PulseBasicInterface.ValueHistory.t
and type t = PulseBaseMemory.t
and type Edges.t = PulseBaseMemory.Edges.t
val canon_access : astate -> PulseAccess.t -> Memory.Access.t
module Attributes :
PulseBaseAddressAttributes.S
with type key := t
and type t = PulseBaseAddressAttributes.t