Module Absint__AccessTree.Make

Parameters

Signature

module TraceDomain = TraceDomain
module AccessMap : IStdlib.PrettyPrintable.PPMap with type PPMap.key = Absint.AccessPath.access
module BaseMap = Absint.AccessPath.BaseMap
type node = TraceDomain.t * tree
and tree =
| Subtree of node AccessMap.t

map from access -> nodes. a leaf is encoded as an empty map

| Star

special leaf for starred access paths

map from base var -> access subtree. Here's how to represent a few different kinds of trace * access path associations:

(x, T)               := { x |-> (T, Subtree {}) }
(x.f, T)             := { x |-> (empty, Subtree { f |-> (T, Subtree {}) }) }
(x*, T)              := { x |-> (T, Star) }
(x.f*, T)            := { x |-> (empty, Subtree { f |-> (T, Star) }) }
(x, T1), (y, T2)     := { x |-> (T1, Subtree {}), y |-> (T2, Subtree {}) }
(x.f, T1), (x.g, T2) := { x |-> (empty, Subtree { f |-> (T1, Subtree {}),
                                                  g |-> (T2, Subtree {}) }) }
include Absint.AbstractDomain.WithBottom with type t = node BaseMap.t
include Absint.AbstractDomain.S
include Absint.AbstractDomain.NoJoin
include IStdlib.PrettyPrintable.PrintableType
type t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val leq : lhs:t -> rhs:t -> bool

the implication relation: lhs <= rhs means lhs |- rhs

val join : t -> t -> t
val widen : prev:t -> next:t -> num_iters:int -> t
val bottom : t

The bottom value of the domain.

val is_bottom : t -> bool

Return true if this is the bottom value

val empty_node : node
val make_node : TraceDomain.t -> node AccessMap.t -> node
val make_access_node : TraceDomain.t -> Absint.AccessPath.access -> TraceDomain.t -> node

for testing only

val make_normal_leaf : TraceDomain.t -> node

create a leaf node with no successors

val make_starred_leaf : TraceDomain.t -> node

create a leaf node with a wildcard successor

val get_node : Absint.AccessPath.Abs.t -> t -> node option

retrieve the node associated with the given access path

val get_trace : Absint.AccessPath.Abs.t -> t -> TraceDomain.t option

retrieve the trace associated with the given access path

val add_node : Absint.AccessPath.Abs.t -> node -> t -> t

add the given access path to the tree and associate its last access with the given node. if any of the accesses in the path are not already present in the tree, they will be added with empty traces associated with each of the inner nodes.

val add_trace : Absint.AccessPath.Abs.t -> TraceDomain.t -> t -> t

add the given access path to the tree and associate its last access with the given trace. if any of the accesses in the path are not already present in the tree, they will be added with empty traces associated with each of the inner nodes.

val node_join : node -> node -> node

join two nodes

val fold : ('a -> Absint.AccessPath.Abs.t -> node -> 'a) -> t -> 'a -> 'a

apply a function to each (access path, node) pair in the tree.

val trace_fold : ('a -> Absint.AccessPath.Abs.t -> TraceDomain.t -> 'a) -> t -> 'a -> 'a
val exists : (Absint.AccessPath.Abs.t -> node -> bool) -> t -> bool
val iter : (Absint.AccessPath.Abs.t -> node -> unit) -> t -> unit
val depth : t -> int

number of traces in the tallest branch of the tree

val pp_node : Stdlib.Format.formatter -> node -> unit