Module `StarvationDomain.Lock`

Abstract address for a lock. 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. Locks represented by access paths rooted at method parameters must have equal access paths to compare equal. Paths rooted at locals are ignored.
Equality for comparing two addresses in two distinct threads/traces. Globals and class objects are compared in the same way, but locks represented by access paths rooted at parameters need only have equal access lists (ie x.f.g == y.f.g). This allows demonically aliasing parameters in *distinct* threads. This relation is used in may_deadlock.

include module type of 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

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

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_locks : F.formatter -> t -> unit
val make_java_synchronized : Absint.FormalMap.t -> IR.Procname.t -> t option: create the monitor locked when entering a synchronized java method

val compare_wrt_reporting : t -> t -> int: a stable order for avoiding reporting deadlocks twice based on the root variable type