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

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
  • deprecated unsafe, obviously; please add a comment why you need to use this and suppress this warning locally with [@alert "-deprecated"]
type needs_canon

an abstract value that needs to be normalized; just AbstractValue.t under the hood too

type astate

PulseAbductiveDomain.t but we cannot mention it there otherwise it would create a circular dependency.

Functions to normalize abstract values

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

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!

  • deprecated unsafe, obviously; please add a comment why you need to use this and suppress this warning locally with [@alert "-deprecated"]

Domain elements, revisited to be safe wrt value normalization

module Stack : sig ... end
val canon_access : astate -> PulseAccess.t -> Memory.Access.t