AbstractAddress (infer.Concurrency.AbstractAddress)

module F = Stdlib.Format

Type meant to represent abstract addresses based on access paths. It currently distinguishes between paths

rooted at formal parameters (these are identified by the parameter index and the path without the root variable, though that variable is kept for pretty printing);
rooted at global variables;
non access-path expressions representing class objects (java only).

Notably, there are no addresses rooted at locals (because proving aliasing between those is difficult).

There are two notions of equality:

Equality for comparing two addresses within the same thread/process/trace. Under this, identical globals and identical class objects compare equal. Parameter-rooted paths compare equal if their parameter indices, types and lists of accesses are equal.
Equality for comparing two addresses in two distinct threads/traces. Globals and class objects are compared in the same way, but parameter-rooted paths need only have equal access lists (ie x.f.g == y.f.g). This allows demonically aliasing parameters in *distinct* threads.

include IStdlib.PrettyPrintable.PrintableOrderedType

include IStdlib.IStd.Caml.Set.OrderedType

type t

val compare : t -> t -> int

include IStdlib.PrettyPrintable.PrintableType with type t := t

val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit

val describe : F.formatter -> t -> unit

human readable description

val equal : t -> t -> bool

val equal_across_threads : IR.Tenv.t -> t -> t -> bool

val root_class : t -> IR.Typ.name option

Class of the root variable of the expression representing the address

val get_typ : IR.Tenv.t -> t -> IR.Typ.t option

val make : Absint.FormalMap.t -> Absint.HilExp.t -> t option

convert an expression to a canonical form for an address

val is_class_object : t -> bool

is the address a Java class object such as in synchronized(MyClass.class){} or static synchronized void foo()

type subst

A substitution from formal position indices to address options. None is used to for actuals that cannot be resolved to an address (eg local-rooted paths or arithmetic expressions).

val pp_subst : F.formatter -> subst -> unit

val make_subst : Absint.FormalMap.t -> Absint.HilExp.t list -> subst

val apply_subst : subst -> t -> t option