Module Concurrency.StarvationDomain

module F = Stdlib.Format
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 AccessExpressionOrConst : sig ... end
module VarDomain : sig ... end
module Event : sig ... end
module AcquisitionElem : sig ... end

a lock acquisition with location information

module Acquisition : sig ... end
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 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.

type t = {
  1. ignore_blocking_calls : bool;
  2. guard_map : GuardToLockMap.t;
  3. lock_state : LockState.t;
  4. critical_pairs : NullLocsCriticalPairs.t;
  5. attributes : AttributeDomain.t;
  6. thread : ThreadDomain.t;
  7. scheduled_work : ScheduledWorkDomain.t;
  8. var_state : VarDomain.t;
  9. null_locs : NullLocs.t;
  10. lazily_initalized : LazilyInitialized.t;
}
include Absint.AbstractDomain.S with type t := t
include Absint.AbstractDomain.Comparable with type t := t
include IStdlib.PrettyPrintable.PrintableType with type t := 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 initial : t

initial domain state

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 release : t -> Lock.t list -> t

simultaneously release a number of locks, no-op if list is empty

val blocking_call : callee:IR.Procname.t -> loc:IBase.Location.t -> t -> t
val ipc : callee:IR.Procname.t -> loc:IBase.Location.t -> t -> t
val wait_on_monitor : loc:IBase.Location.t -> Absint.FormalMap.t -> Absint.HilExp.t list -> t -> t
val future_get : callee:IR.Procname.t -> loc:IBase.Location.t -> Absint.HilExp.t list -> t -> t
val regex_op : callee:IR.Procname.t -> loc:IBase.Location.t -> t -> t
val strict_mode_call : callee:IR.Procname.t -> loc:IBase.Location.t -> t -> t
val arbitrary_code_execution : 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 -> Absint.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 -> Absint.HilExp.t -> t

Acquire the lock the guard was constructed with.

val remove_guard : t -> Absint.HilExp.t -> t

Destroy the guard and release its lock.

val unlock_guard : t -> Absint.HilExp.t -> t

Release the lock the guard was constructed with.

record the fact that a method is scheduled to run on a certain thread/executor

type summary = {
  1. critical_pairs : CriticalPairs.t;
  2. thread : ThreadDomain.t;
  3. scheduled_work : ScheduledWorkDomain.t;
  4. lock_state : LockState.t;
  5. attributes : AttributeDomain.t;
    (*

    final-state attributes that affect instance variables only

    *)
  6. return_attribute : Attribute.t;
}
val empty_summary : summary
val pp_summary : F.formatter -> summary -> unit
val integrate_summary : tenv:IR.Tenv.t -> procname:IR.Procname.t -> lhs:Absint.HilExp.AccessExpression.t -> subst:Lock.subst -> Absint.FormalMap.t -> Absint.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 set_ignore_blocking_calls_flag : t -> t
val remove_dead_vars : t -> IR.Var.t list -> t
val fold_critical_pairs_of_summary : (CriticalPair.t -> 'a -> 'a) -> summary -> 'a -> 'a
val null_check : Absint.FormalMap.t -> Absint.HilExp.t -> t -> t

if expression is a heap location, mark it as null in this branch

if expression is a heap location, mark it as set to non-null in this branch