pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[starvation] reroute access to set of critical pairs of summary through a fold

Browse Source 
Summary:
Another step in the refactoring of the starvation domain:
- Main purpose is to mediate access to the set of critical pairs in a summary through a fold function (`fold_critical_pairs_of_summary`) and not through direct field access to that set.  This will allow eliding storage of critical pairs entirely and dynamically generating those when folding.
- Remove optional arguments as much as possible, as this led to unused arguments not being caught.
- Helper functions distributed more logically among modules.

Reviewed By: skcho

Differential Revision: D24275399

fbshipit-source-id: d23123a48
master
Nikos Gorogiannis 4 years ago committed by Facebook GitHub Bot
parent ae3f1d79c9
commit 8ddc9ee48b
4 changed files with 122 additions and 98 deletions
Show Stats Download Patch File Download Diff File

64
infer/src/backend/StarvationGlobalAnalysis.ml
Unescape View File

@ -9,33 +9,38 @@ open! IStd
module L = Logging module L = Logging
module Domain = StarvationDomain module Domain = StarvationDomain
(* given a scheduled-work item, read the summary of the scheduled method from the disk let iter_scheduled_pair (work_item : Domain.ScheduledWorkItem.t) f =
and adapt its contents to the thread it was scheduled too *) let open Domain in
let get_summary_of_scheduled_work (work_item : Domain.ScheduledWorkItem.t) =
let astate = {Domain.initial with thread= work_item.thread} in
let callsite = CallSite.make work_item.procname work_item.loc in let callsite = CallSite.make work_item.procname work_item.loc in
let open IOption.Let_syntax in fun pair ->
let* {Summary.payloads= {starvation}} = Summary.OnDisk.get work_item.procname in CriticalPair.with_callsite pair callsite
let+ callee_astate = starvation in |> CriticalPair.apply_caller_thread work_item.thread
let ({critical_pairs} : Domain.t) = Domain.integrate_summary callsite astate callee_astate in |> Option.iter ~f
critical_pairs
let iter_critical_pairs_of_summary f summary =
Domain.fold_critical_pairs_of_summary (fun pair () -> f pair) summary ()
let iter_critical_pairs_of_scheduled_work f (work_item : Domain.ScheduledWorkItem.t) =
Summary.OnDisk.get work_item.procname
|> Option.bind ~f:(fun (summary : Summary.t) -> summary.payloads.starvation)
|> Option.iter ~f:(iter_critical_pairs_of_summary (iter_scheduled_pair work_item f))
(* given a summary, do [f work critical_pairs] for each [work] item scheduled in the summary,
where [critical_pairs] are those of the method scheduled, adapted to the thread it's scheduled for *)
let iter_summary ~f exe_env (summary : Summary.t) = let iter_summary ~f exe_env (summary : Summary.t) =
let open Domain in let open Domain in
Payloads.starvation summary.payloads Payloads.starvation summary.payloads
|> Option.iter ~f:(fun ({scheduled_work; critical_pairs} : summary) -> |> Option.iter ~f:(fun (payload : summary) ->
let pname = Summary.get_proc_name summary in let pname = Summary.get_proc_name summary in
let tenv = Exe_env.get_tenv exe_env pname in let tenv = Exe_env.get_tenv exe_env pname in
if if
StarvationModels.is_java_main_method pname StarvationModels.is_java_main_method pname
|| ConcurrencyModels.is_android_lifecycle_method tenv pname || ConcurrencyModels.is_android_lifecycle_method tenv pname
then f pname critical_pairs ; then iter_critical_pairs_of_summary (f pname) payload ;
ScheduledWorkDomain.iter ScheduledWorkDomain.iter
(fun work -> get_summary_of_scheduled_work work |> Option.iter ~f:(f pname)) (iter_critical_pairs_of_scheduled_work (f pname))
scheduled_work ) payload.scheduled_work )
module WorkHashSet = struct module WorkHashSet = struct
@ -52,9 +57,7 @@ module WorkHashSet = struct
include Caml.Hashtbl.Make (T) include Caml.Hashtbl.Make (T)
let add_pairs work_set caller pairs = let add_pair work_set caller pair = replace work_set (caller, pair) ()
let open Domain in
CriticalPairs.iter (fun pair -> replace work_set (caller, pair) ()) pairs
end end
let report exe_env work_set = let report exe_env work_set =
@ -74,19 +77,16 @@ let report exe_env work_set =
(Summary.get_proc_desc summary, starvation) ) ) ) (Summary.get_proc_desc summary, starvation) ) ) )
tenv pattrs pair acc tenv pattrs pair acc
in in
match pair.elem.event with Event.get_acquired_locks pair.elem.event
| LockAcquire {locks} -> |> List.fold ~init:acc ~f:(fun acc lock ->
List.fold locks ~init:acc ~f:(fun acc lock -> let should_report_starvation =
let should_report_starvation = CriticalPair.is_uithread pair && not (Procname.is_constructor procname)
CriticalPair.is_uithread pair && not (Procname.is_constructor procname) in
in WorkHashSet.fold
WorkHashSet.fold (fun (other_procname, (other_pair : CriticalPair.t)) () acc ->
(fun (other_procname, (other_pair : CriticalPair.t)) () acc -> Starvation.report_on_parallel_composition ~should_report_starvation tenv
Starvation.report_on_parallel_composition ~should_report_starvation tenv pattrs pair lock other_procname other_pair acc )
pattrs pair lock other_procname other_pair acc ) work_set acc ) )
work_set acc )
| _ ->
acc )
in in
WorkHashSet.fold wrap_report work_set Starvation.ReportMap.empty WorkHashSet.fold wrap_report work_set Starvation.ReportMap.empty
|> Starvation.ReportMap.store_multi_file |> Starvation.ReportMap.store_multi_file
@ -97,7 +97,7 @@ let whole_program_analysis () =
let work_set = WorkHashSet.create 1 in let work_set = WorkHashSet.create 1 in
let exe_env = Exe_env.mk () in let exe_env = Exe_env.mk () in
L.progress "Processing on-disk summaries...@." ; L.progress "Processing on-disk summaries...@." ;
Summary.OnDisk.iter_specs ~f:(iter_summary exe_env ~f:(WorkHashSet.add_pairs work_set)) ; Summary.OnDisk.iter_specs ~f:(iter_summary exe_env ~f:(WorkHashSet.add_pair work_set)) ;
L.progress "Loaded %d pairs@." (WorkHashSet.length work_set) ; L.progress "Loaded %d pairs@." (WorkHashSet.length work_set) ;
L.progress "Reporting on processed summaries...@." ; L.progress "Reporting on processed summaries...@." ;
report exe_env work_set report exe_env work_set

12
infer/src/concurrency/starvation.ml
Unescape View File

@ -776,11 +776,11 @@ let report_on_pair ~analyze_ondemand tenv pattrs (pair : Domain.CriticalPair.t)
then, report on the parallel composition of the current pair and any pair in these then, report on the parallel composition of the current pair and any pair in these
summaries that can indeed run in parallel *) summaries that can indeed run in parallel *)
fold_reportable_summaries analyze_ondemand tenv other_class ~init:acc fold_reportable_summaries analyze_ondemand tenv other_class ~init:acc
~f:(fun acc (other_pname, {critical_pairs}) -> ~f:(fun acc (other_pname, summary) ->
CriticalPairs.fold Domain.fold_critical_pairs_of_summary
(report_on_parallel_composition ~should_report_starvation tenv pattrs pair (report_on_parallel_composition ~should_report_starvation tenv pattrs pair
lock other_pname) lock other_pname)
critical_pairs acc ) ) ) ) summary acc ) ) ) )
| _ -> | _ ->
report_map report_map
@ -788,10 +788,10 @@ let report_on_pair ~analyze_ondemand tenv pattrs (pair : Domain.CriticalPair.t)
let reporting {InterproceduralAnalysis.procedures; file_exe_env; analyze_file_dependency} = let reporting {InterproceduralAnalysis.procedures; file_exe_env; analyze_file_dependency} =
if Config.starvation_whole_program then IssueLog.empty if Config.starvation_whole_program then IssueLog.empty
else else
let report_on_proc tenv proc_desc report_map (payload : Domain.summary) = let report_on_proc tenv proc_desc report_map payload =
Domain.CriticalPairs.fold Domain.fold_critical_pairs_of_summary
(report_on_pair ~analyze_ondemand:analyze_file_dependency tenv proc_desc) (report_on_pair ~analyze_ondemand:analyze_file_dependency tenv proc_desc)
payload.critical_pairs report_map payload report_map
in in
let report_procedure report_map procname = let report_procedure report_map procname =
analyze_file_dependency procname analyze_file_dependency procname

128
infer/src/concurrency/starvationDomain.ml
Unescape View File

@ -62,24 +62,24 @@ module ThreadDomain = struct
(** given the current thread state [caller_thread] and the thread state under which a critical (** given the current thread state [caller_thread] and the thread state under which a critical
pair occurred, [pair_thread], decide whether to throw away the pair (returning [None]) because pair occurred, [pair_thread], decide whether to throw away the pair (returning [None]) because
it cannot occur within a call from the current state, or adapt its thread state appropriately. *) it cannot occur within a call from the current state, or adapt its thread state appropriately. *)
let apply_to_pair caller_thread pair_thread = let apply_caller_thread ~caller ~callee =
match (caller_thread, pair_thread) with match (caller, callee) with
| UnknownThread, _ -> | UnknownThread, _ ->
(* callee pair knows more than us *) (* callee pair knows more than us *)
Some pair_thread Some callee
| AnyThread, UnknownThread -> | AnyThread, UnknownThread ->
(* callee pair knows nothing and caller has abstracted away info *) (* callee pair knows nothing and caller has abstracted away info *)
Some AnyThread Some AnyThread
| AnyThread, _ -> | AnyThread, _ ->
(* callee pair is UI / BG / Any and caller has abstracted away info so use callee's knowledge *) (* callee pair is UI / BG / Any and caller has abstracted away info so use callee's knowledge *)
Some pair_thread Some callee
| UIThread, BGThread | BGThread, UIThread -> | UIThread, BGThread | BGThread, UIThread ->
(* annotations or assertions are incorrectly used in code, or callee is path-sensitive on (* annotations or assertions are incorrectly used in code, or callee is path-sensitive on
thread-identity, just drop the callee pair *) thread-identity, just drop the callee pair *)
None None
| _, _ -> | _, _ ->
(* caller is UI or BG and callee does not disagree, so use that *) (* caller is UI or BG and callee does not disagree, so use that *)
Some caller_thread Some caller
end end
module Lock = struct module Lock = struct
@ -125,6 +125,18 @@ module Lock = struct
(lock' :: locks', true) ) (lock' :: locks', true) )
in in
apply_subst_to_list_inner l |> fst apply_subst_to_list_inner l |> fst
let is_recursive tenv lock =
let is_class_and_recursive_lock = function
| {Typ.desc= Tptr ({desc= Tstruct name}, _)} | {desc= Tstruct name} ->
ConcurrencyModels.is_recursive_lock_type name
| typ ->
L.debug Analysis Verbose "Asked if non-struct type %a is a recursive lock type.@."
(Typ.pp_full Pp.text) typ ;
true
in
get_typ tenv lock |> Option.exists ~f:is_class_and_recursive_lock
end end
module AccessExpressionDomain = struct module AccessExpressionDomain = struct
@ -223,6 +235,14 @@ module Event = struct
MonitorWait {monitor_wait with thread} MonitorWait {monitor_wait with thread}
let apply_caller_thread caller_thread event =
match ThreadDomain.apply_caller_thread ~caller:caller_thread ~callee:(get_thread event) with
| None ->
None
| Some thread ->
Some (with_thread event thread)
let make_acquire locks thread = LockAcquire {locks; thread} let make_acquire locks thread = LockAcquire {locks; thread}
let make_blocking_call callee severity thread = MayBlock {callee; severity; thread} let make_blocking_call callee severity thread = MayBlock {callee; severity; thread}
@ -231,6 +251,8 @@ module Event = struct
let make_object_wait lock thread = MonitorWait {lock; thread} let make_object_wait lock thread = MonitorWait {lock; thread}
let get_acquired_locks = function LockAcquire {locks} -> locks | _ -> []
let apply_subst subst event = let apply_subst subst event =
match event with match event with
| MayBlock _ | StrictModeCall _ -> | MayBlock _ | StrictModeCall _ ->
@ -251,6 +273,10 @@ module Event = struct
Some event Some event
| locks -> | locks ->
Some (LockAcquire {locks; thread}) ) Some (LockAcquire {locks; thread}) )
let has_recursive_lock tenv event =
get_acquired_locks event |> List.exists ~f:(Lock.is_recursive tenv)
end end
(** A lock acquisition with source location and procname in which it occurs. The location & procname (** A lock acquisition with source location and procname in which it occurs. The location & procname
@ -259,7 +285,9 @@ module Acquisition = struct
type t = {lock: Lock.t; loc: Location.t [@compare.ignore]; procname: Procname.t [@compare.ignore]} type t = {lock: Lock.t; loc: Location.t [@compare.ignore]; procname: Procname.t [@compare.ignore]}
[@@deriving compare] [@@deriving compare]
let pp fmt {lock} = Lock.pp fmt lock let pp fmt {lock; loc; procname} =
F.fprintf fmt "<lock=%a; loc=%a; procname=%a>" Lock.pp lock Location.pp loc Procname.pp procname
let describe fmt {lock} = Lock.pp_locks fmt lock let describe fmt {lock} = Lock.pp_locks fmt lock
@ -419,23 +447,6 @@ module CriticalPairElement = struct
Some {acquisitions; event} Some {acquisitions; event}
end end
let is_recursive_lock event tenv =
let is_class_and_recursive_lock = function
| {Typ.desc= Tptr ({desc= Tstruct name}, _)} | {desc= Tstruct name} ->
ConcurrencyModels.is_recursive_lock_type name
| typ ->
L.debug Analysis Verbose "Asked if non-struct type %a is a recursive lock type.@."
(Typ.pp_full Pp.text) typ ;
true
in
match (event : Event.t) with
| LockAcquire {locks} ->
List.exists locks ~f:(fun lock_path ->
Lock.get_typ tenv lock_path |> Option.exists ~f:is_class_and_recursive_lock )
| _ ->
false
module CriticalPair = struct module CriticalPair = struct
include ExplicitTrace.MakeTraceElem (CriticalPairElement) (ExplicitTrace.DefaultCallPrinter) include ExplicitTrace.MakeTraceElem (CriticalPairElement) (ExplicitTrace.DefaultCallPrinter)
@ -444,11 +455,8 @@ module CriticalPair = struct
let get_thread {elem} = CriticalPairElement.get_thread elem let get_thread {elem} = CriticalPairElement.get_thread elem
let may_deadlock tenv ~(lhs : t) ~lhs_lock ~(rhs : t) = let may_deadlock tenv ~(lhs : t) ~lhs_lock ~(rhs : t) =
let get_acquired_locks {elem= {event}} =
match event with LockAcquire {locks} -> locks | _ -> []
in
if ThreadDomain.can_run_in_parallel (get_thread lhs) (get_thread rhs) then if ThreadDomain.can_run_in_parallel (get_thread lhs) (get_thread rhs) then
get_acquired_locks rhs Event.get_acquired_locks rhs.elem.event
|> List.find ~f:(fun rhs_lock -> |> List.find ~f:(fun rhs_lock ->
(not (Lock.equal_across_threads tenv lhs_lock rhs_lock)) (not (Lock.equal_across_threads tenv lhs_lock rhs_lock))
&& Acquisitions.lock_is_held_in_other_thread tenv rhs_lock lhs.elem.acquisitions && Acquisitions.lock_is_held_in_other_thread tenv rhs_lock lhs.elem.acquisitions
@ -474,7 +482,7 @@ module CriticalPair = struct
let filtered_locks = let filtered_locks =
IList.filter_changed locks ~f:(fun lock -> IList.filter_changed locks ~f:(fun lock ->
(not (Acquisitions.lock_is_held lock held_locks)) (not (Acquisitions.lock_is_held lock held_locks))
|| not (is_recursive_lock pair.elem.event tenv) ) || not (Event.has_recursive_lock tenv pair.elem.event) )
in in
match filtered_locks with match filtered_locks with
| [] -> | [] ->
@ -487,22 +495,27 @@ module CriticalPair = struct
Some pair Some pair
let integrate_summary_opt ?subst ?tenv existing_acquisitions call_site let apply_caller_thread caller_thread callee_pair =
match Event.apply_caller_thread caller_thread callee_pair.elem.event with
| None ->
None
| Some event when phys_equal event callee_pair.elem.event ->
Some callee_pair
| Some event ->
Some (map ~f:(fun (elem : CriticalPairElement.t) -> {elem with event}) callee_pair)
let integrate_summary_opt ~subst ~tenv existing_acquisitions call_site
(caller_thread : ThreadDomain.t) (callee_pair : t) = (caller_thread : ThreadDomain.t) (callee_pair : t) =
let substitute_pair subst callee_pair = apply_subst subst callee_pair
match subst with None -> Some callee_pair | Some subst -> apply_subst subst callee_pair |> Option.bind ~f:(filter_out_reentrant_relocks (Some tenv) existing_acquisitions)
in |> Option.bind ~f:(apply_caller_thread caller_thread)
substitute_pair subst callee_pair |> Option.map ~f:(fun callee_pair ->
|> Option.bind ~f:(filter_out_reentrant_relocks tenv existing_acquisitions) let f (elem : CriticalPairElement.t) =
|> Option.bind ~f:(fun callee_pair -> {elem with acquisitions= Acquisitions.union existing_acquisitions elem.acquisitions}
ThreadDomain.apply_to_pair caller_thread (get_thread callee_pair) in
|> Option.map ~f:(fun thread -> map ~f callee_pair )
let f (elem : CriticalPairElement.t) = |> Option.map ~f:(fun callee_pair -> with_callsite callee_pair call_site)
let acquisitions = Acquisitions.union existing_acquisitions elem.acquisitions in
let event = Event.with_thread elem.event thread in
({acquisitions; event} : elem_t)
in
with_callsite (map ~f callee_pair) call_site ) )
let get_earliest_lock_or_call_loc ~procname ({elem= {acquisitions}} as t) = let get_earliest_lock_or_call_loc ~procname ({elem= {acquisitions}} as t) =
@ -570,13 +583,14 @@ end
module CriticalPairs = struct module CriticalPairs = struct
include CriticalPair.FiniteSet include CriticalPair.FiniteSet
let with_callsite astate ?tenv ?subst lock_state call_site thread = let with_callsite astate ~tenv ~subst lock_state call_site thread =
let existing_acquisitions = LockState.get_acquisitions lock_state in let existing_acquisitions = LockState.get_acquisitions lock_state in
fold fold
(fun critical_pair acc -> (fun critical_pair acc ->
CriticalPair.integrate_summary_opt ?subst ?tenv existing_acquisitions call_site thread CriticalPair.integrate_summary_opt ~subst ~tenv existing_acquisitions call_site thread
critical_pair critical_pair
|> Option.bind ~f:(CriticalPair.filter_out_reentrant_relocks tenv existing_acquisitions) |> Option.bind
~f:(CriticalPair.filter_out_reentrant_relocks (Some tenv) existing_acquisitions)
|> Option.value_map ~default:acc ~f:(fun new_pair -> add new_pair acc) ) |> Option.value_map ~default:acc ~f:(fun new_pair -> add new_pair acc) )
astate empty astate empty
end end
@ -723,18 +737,18 @@ let leq ~lhs ~rhs =
&& VarDomain.leq ~lhs:lhs.var_state ~rhs:rhs.var_state && VarDomain.leq ~lhs:lhs.var_state ~rhs:rhs.var_state
let add_critical_pair ?tenv lock_state event ~loc acc = let add_critical_pair ~tenv_opt lock_state event ~loc acc =
let acquisitions = LockState.get_acquisitions lock_state in let acquisitions = LockState.get_acquisitions lock_state in
let critical_pair = CriticalPair.make ~loc acquisitions event in let critical_pair = CriticalPair.make ~loc acquisitions event in
CriticalPair.filter_out_reentrant_relocks tenv acquisitions critical_pair CriticalPair.filter_out_reentrant_relocks tenv_opt acquisitions critical_pair
|> Option.value_map ~default:acc ~f:(fun pair -> CriticalPairs.add pair acc) |> Option.value_map ~default:acc ~f:(fun pair -> CriticalPairs.add pair acc)
let acquire ?tenv ({lock_state; critical_pairs} as astate) ~procname ~loc locks = let acquire ~tenv ({lock_state; critical_pairs} as astate) ~procname ~loc locks =
{ astate with { astate with
critical_pairs= critical_pairs=
(let event = Event.make_acquire locks astate.thread in (let event = Event.make_acquire locks astate.thread in
add_critical_pair ?tenv lock_state event ~loc critical_pairs ) add_critical_pair ~tenv_opt:(Some tenv) lock_state event ~loc critical_pairs )
; lock_state= ; lock_state=
List.fold locks ~init:lock_state ~f:(fun acc lock -> List.fold locks ~init:lock_state ~f:(fun acc lock ->
LockState.acquire ~procname ~loc lock acc ) } LockState.acquire ~procname ~loc lock acc ) }
@ -744,7 +758,8 @@ let make_call_with_event new_event ~loc astate =
if astate.ignore_blocking_calls then astate if astate.ignore_blocking_calls then astate
else else
{ astate with { astate with
critical_pairs= add_critical_pair astate.lock_state new_event ~loc astate.critical_pairs } critical_pairs=
add_critical_pair ~tenv_opt:None astate.lock_state new_event ~loc astate.critical_pairs }
let blocking_call ~callee sev ~loc astate = let blocking_call ~callee sev ~loc astate =
@ -850,17 +865,15 @@ let pp_summary fmt (summary : summary) =
AttributeDomain.pp summary.attributes AttributeDomain.pp summary.attributes
let integrate_summary ?tenv ?lhs ?subst callsite (astate : t) (summary : summary) = let integrate_summary ~tenv ~lhs ~subst callsite (astate : t) (summary : summary) =
let critical_pairs' = let critical_pairs' =
CriticalPairs.with_callsite summary.critical_pairs ?tenv ?subst astate.lock_state callsite CriticalPairs.with_callsite summary.critical_pairs ~tenv ~subst astate.lock_state callsite
astate.thread astate.thread
in in
{ astate with { astate with
critical_pairs= CriticalPairs.join astate.critical_pairs critical_pairs' critical_pairs= CriticalPairs.join astate.critical_pairs critical_pairs'
; thread= ThreadDomain.integrate_summary ~caller:astate.thread ~callee:summary.thread ; thread= ThreadDomain.integrate_summary ~caller:astate.thread ~callee:summary.thread
; attributes= ; attributes= AttributeDomain.add lhs summary.return_attribute astate.attributes }
Option.value_map lhs ~default:astate.attributes ~f:(fun lhs_exp ->
AttributeDomain.add lhs_exp summary.return_attribute astate.attributes ) }
let summary_of_astate : Procdesc.t -> t -> summary = let summary_of_astate : Procdesc.t -> t -> summary =
@ -912,3 +925,6 @@ let remove_dead_vars (astate : t) deadvars =
let set_ignore_blocking_calls_flag astate = {astate with ignore_blocking_calls= true} let set_ignore_blocking_calls_flag astate = {astate with ignore_blocking_calls= true}
let fold_critical_pairs_of_summary f (summary : summary) acc =
CriticalPairs.fold f summary.critical_pairs acc

16
infer/src/concurrency/starvationDomain.mli
Unescape View File

@ -64,6 +64,8 @@ module Event : sig
[@@deriving compare] [@@deriving compare]
val describe : F.formatter -> t -> unit val describe : F.formatter -> t -> unit
val get_acquired_locks : t -> Lock.t list
end end
module LockState : AbstractDomain.WithTop module LockState : AbstractDomain.WithTop
@ -120,6 +122,10 @@ module CriticalPair : sig
val can_run_in_parallel : t -> t -> bool val can_run_in_parallel : t -> t -> bool
(** can two pairs describe events on two threads that can run in parallel *) (** can two pairs describe events on two threads that can run in parallel *)
val with_callsite : t -> CallSite.t -> t
val apply_caller_thread : ThreadDomain.t -> t -> t option
end end
module CriticalPairs : AbstractDomain.FiniteSetS with type elt = CriticalPair.t module CriticalPairs : AbstractDomain.FiniteSetS with type elt = CriticalPair.t
@ -178,7 +184,7 @@ include AbstractDomain.S with type t := t
val initial : t val initial : t
(** initial domain state *) (** initial domain state *)
val acquire : ?tenv:Tenv.t -> t -> procname:Procname.t -> loc:Location.t -> Lock.t list -> t val acquire : tenv:Tenv.t -> t -> procname:Procname.t -> loc:Location.t -> Lock.t list -> t
(** simultaneously acquire a number of locks, no-op if list is empty *) (** simultaneously acquire a number of locks, no-op if list is empty *)
val release : t -> Lock.t list -> t val release : t -> Lock.t list -> t
@ -228,9 +234,9 @@ val empty_summary : summary
val pp_summary : F.formatter -> summary -> unit val pp_summary : F.formatter -> summary -> unit
val integrate_summary : val integrate_summary :
?tenv:Tenv.t tenv:Tenv.t
-> ?lhs:HilExp.AccessExpression.t -> lhs:HilExp.AccessExpression.t
-> ?subst:Lock.subst -> subst:Lock.subst
-> CallSite.t -> CallSite.t
-> t -> t
-> summary -> summary
@ -243,3 +249,5 @@ val summary_of_astate : Procdesc.t -> t -> summary
val set_ignore_blocking_calls_flag : t -> t val set_ignore_blocking_calls_flag : t -> t
val remove_dead_vars : t -> Var.t list -> t val remove_dead_vars : t -> Var.t list -> t
val fold_critical_pairs_of_summary : (CriticalPair.t -> 'a -> 'a) -> summary -> 'a -> 'a

Write Preview
Loading…
Cancel
Save