Module Concurrency__StarvationDomain
module ThreadDomain : sig ... end
Domain for thread-type. The main goals are
module Lock : sig ... end
Abstract address for a lock. There are two notions of equality:
module Event : sig ... end
module LockState : Absint.AbstractDomain.WithTop
module Acquisition : sig ... end
a lock acquisition with location information
module Acquisitions : sig ... end
A set of lock acquisitions with source locations and procnames.
module CriticalPairElement : sig ... end
An event and the currently-held locks at the time it occurred.
module CriticalPair : sig ... end
A
CriticalPairElement
equipped with a call stack. The intuition is that if we have a critical pair `(locks, event)` in the summary of a method then there is a trace of that method where `event` occurs, and right before it occurs the locks held are exactly `locks` (no over/under approximation). We call it "critical" because the information here alone determines deadlock conditions.
module CriticalPairs : Absint.AbstractDomain.FiniteSetS with type FiniteSetS.elt = CriticalPair.t
module Attribute : sig ... end
Tracks expression attributes
module AttributeDomain : sig ... end
Tracks all expressions assigned values of
Attribute
module ScheduledWorkItem : sig ... end
A record of scheduled parallel work: the method scheduled to run, where, and on what thread.
module ScheduledWorkDomain : Absint.AbstractDomain.FiniteSetS with type FiniteSetS.elt = ScheduledWorkItem.t
type t
=
{
guard_map : GuardToLockMap.t;
lock_state : LockState.t;
critical_pairs : CriticalPairs.t;
attributes : AttributeDomain.t;
thread : ThreadDomain.t;
scheduled_work : ScheduledWorkDomain.t;
}
include Absint.AbstractDomain.WithBottom with type t := t
include Absint.AbstractDomain.S
include Absint.AbstractDomain.NoJoin
include IStdlib.PrettyPrintable.PrintableType
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val bottom : t
The bottom value of the domain.
val is_bottom : t -> bool
Return true if this is the bottom value
val acquire : ?tenv:IR.Tenv.t -> t -> procname:IR.Procname.t -> loc:IBase.Location.t -> Lock.t list -> t
simultaneously acquire a number of locks, no-op if list is empty
val blocking_call : callee:IR.Procname.t -> Concurrency.StarvationModels.severity -> loc:IBase.Location.t -> t -> t
val wait_on_monitor : loc:IBase.Location.t -> Absint.FormalMap.t -> IR.HilExp.t list -> t -> t
val future_get : callee:IR.Procname.t -> loc:IBase.Location.t -> IR.HilExp.t list -> t -> t
val strict_mode_call : callee:IR.Procname.t -> loc:IBase.Location.t -> t -> t
val add_guard : acquire_now:bool -> procname:IR.Procname.t -> loc:IBase.Location.t -> IR.Tenv.t -> t -> IR.HilExp.t -> Lock.t -> t
Install a mapping from the guard expression to the lock provided, and optionally lock it.
val lock_guard : procname:IR.Procname.t -> loc:IBase.Location.t -> IR.Tenv.t -> t -> IR.HilExp.t -> t
Acquire the lock the guard was constructed with.
val remove_guard : t -> IR.HilExp.t -> t
Destroy the guard and release its lock.
val unlock_guard : t -> IR.HilExp.t -> t
Release the lock the guard was constructed with.
val schedule_work : IBase.Location.t -> Concurrency.StarvationModels.scheduler_thread_constraint -> t -> IR.Procname.t -> t
record the fact that a method is scheduled to run on a certain thread/executor
type summary
=
{
critical_pairs : CriticalPairs.t;
thread : ThreadDomain.t;
scheduled_work : ScheduledWorkDomain.t;
attributes : AttributeDomain.t;
final-state attributes that affect instance variables only
return_attribute : Attribute.t;
}
val empty_summary : summary
val pp_summary : F.formatter -> summary -> unit
val integrate_summary : ?tenv:IR.Tenv.t -> ?lhs:IR.HilExp.AccessExpression.t -> ?subst:Lock.subst -> IR.CallSite.t -> t -> summary -> t
apply a callee summary to the current abstract state;
lhs
is the expression assigned the returned value, if any
val summary_of_astate : IR.Procdesc.t -> t -> summary
val filter_blocking_calls : t -> t