From 9c8db94e7da973fe531f62e250ae8494af8e51fe Mon Sep 17 00:00:00 2001 From: David Pichardie Date: Wed, 24 Jan 2024 07:54:34 -0800 Subject: [PATCH] [pulse][transitive-info] refactoring (part 2 of 2) Summary: now that NonDisj domain is split between intra/inter informations, we can eliminate some code duplication between AbductiveDomain and NonDisjDomain Reviewed By: geralt-encore Differential Revision: D52999404 Privacy Context Container: L1208441 fbshipit-source-id: 72e72a9729aa958e43e07ebde19a26f14722064c --- infer/src/pulse/Pulse.ml | 6 +- infer/src/pulse/PulseAbductiveDomain.ml | 80 +++++--------- infer/src/pulse/PulseAbductiveDomain.mli | 23 +--- infer/src/pulse/PulseInterproc.ml | 25 +---- infer/src/pulse/PulseNonDisjunctiveDomain.ml | 103 ++---------------- infer/src/pulse/PulseNonDisjunctiveDomain.mli | 8 +- .../src/pulse/PulseTransitiveAccessChecker.ml | 22 +--- infer/src/pulse/PulseTransitiveInfo.ml | 43 ++++++++ infer/src/pulse/PulseTransitiveInfo.mli | 21 +++- 9 files changed, 117 insertions(+), 214 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index ca0dfa77d0d..09b3cc94c84 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -1597,10 +1597,8 @@ module PulseTransferFunctions = struct let remember_dropped_disjuncts disjuncts non_disj = List.fold disjuncts ~init:non_disj ~f:(fun non_disj (exec, _) -> match exec with - | ContinueProgram - {AbductiveDomain.transitive_accesses; transitive_callees; transitive_missed_captures} -> - NonDisjDomain.remember_dropped_elements transitive_accesses transitive_callees - transitive_missed_captures non_disj + | ContinueProgram {AbductiveDomain.transitive_info} -> + NonDisjDomain.remember_dropped_elements transitive_info non_disj | _ -> non_disj ) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index c4b1408af33..835b65fa1f6 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -79,9 +79,7 @@ type t = ; topl: (PulseTopl.state[@yojson.opaque]) ; need_closure_specialization: bool ; need_dynamic_type_specialization: (AbstractValue.Set.t[@yojson.opaque]) - ; transitive_accesses: (Trace.Set.t[@yojson.opaque]) - ; transitive_callees: (TransitiveInfo.Callees.t[@yojson.opaque]) - ; transitive_missed_captures: (Typ.Name.Set.t[@yojson.opaque]) + ; transitive_info: (TransitiveInfo.t[@yojson.opaque]) ; skipped_calls: SkippedCalls.t } [@@deriving compare, equal, yojson_of] @@ -92,9 +90,7 @@ let pp_ ~is_summary f ; decompiler ; need_closure_specialization ; need_dynamic_type_specialization - ; transitive_accesses - ; transitive_callees - ; transitive_missed_captures + ; transitive_info ; topl ; skipped_calls } = let pp_decompiler f = @@ -106,20 +102,16 @@ let pp_ ~is_summary f if is_summary then F.fprintf f "PRE=@[%a@]@;POST=@[%a@]" PreDomain.pp pre PostDomain.pp post else F.fprintf f "%a@;PRE=[%a]" PostDomain.pp post PreDomain.pp pre in - let pp_transitive_acces fmt set = Trace.Set.pp fmt set in F.fprintf f "@[%a@;\ %t@;\ %tneed_closure_specialization=%b@;\ need_dynamic_type_specialization=%a@;\ - transitive_accesses=%a@;\ - transitive_callees=%a@;\ - transitive_missed_captures=%a@;\ + transitive_info=%a@;\ skipped_calls=%a@;\ Topl=%a@]" Formula.pp path_condition pp_pre_post pp_decompiler need_closure_specialization - AbstractValue.Set.pp need_dynamic_type_specialization pp_transitive_acces transitive_accesses - TransitiveInfo.Callees.pp transitive_callees Typ.Name.Set.pp transitive_missed_captures + AbstractValue.Set.pp need_dynamic_type_specialization TransitiveInfo.pp transitive_info SkippedCalls.pp skipped_calls PulseTopl.pp_state topl @@ -133,16 +125,19 @@ let unset_need_closure_specialization astate = {astate with need_closure_special let record_transitive_access location astate = let trace = Trace.Immediate {location; history= ValueHistory.epoch} in - {astate with transitive_accesses= Trace.Set.add trace astate.transitive_accesses} + let accesses = Trace.Set.add trace astate.transitive_info.accesses in + let transitive_info = {astate.transitive_info with accesses} in + {astate with transitive_info} let record_call_resolution ~caller_name ~caller_loc ~callsite_loc call_kind resolution astate = - let {transitive_callees} = astate in - let transitive_callees = + let {TransitiveInfo.callees} = astate.transitive_info in + let callees = TransitiveInfo.Callees.record ~caller_name ~caller_loc ~callsite_loc call_kind resolution - transitive_callees + callees in - {astate with transitive_callees} + let transitive_info = {astate.transitive_info with callees} in + {astate with transitive_info} let map_decompiler astate ~f = {astate with decompiler= f astate.decompiler} @@ -1581,9 +1576,7 @@ let mk_initial tenv (proc_attrs : ProcAttributes.t) specialization = ; need_closure_specialization= false ; need_dynamic_type_specialization= AbstractValue.Set.empty ; topl= PulseTopl.start () - ; transitive_accesses= Trace.Set.empty - ; transitive_callees= TransitiveInfo.Callees.bottom - ; transitive_missed_captures= Typ.Name.Set.empty + ; transitive_info= TransitiveInfo.bottom ; skipped_calls= SkippedCalls.empty } in let astate = @@ -2213,33 +2206,7 @@ module Summary = struct let add_need_dynamic_type_specialization = add_need_dynamic_type_specialization - let transfer_accesses_to_caller astate callee_proc_name call_loc summary = - let transitive_accesses = - Trace.Set.map_callee (Call callee_proc_name) call_loc summary.transitive_accesses - |> Trace.Set.union astate.transitive_accesses - in - {astate with transitive_accesses} - - - let transfer_transitive_callees_to_caller astate summary = - let transitive_callees = - TransitiveInfo.Callees.join astate.transitive_callees summary.transitive_callees - in - {astate with transitive_callees} - - - let transfer_transitive_missed_captures_to_caller astate summary = - let transitive_missed_captures = - Typ.Name.Set.union astate.transitive_missed_captures summary.transitive_missed_captures - in - {astate with transitive_missed_captures} - - - let get_transitive_accesses summary = summary.transitive_accesses - - let get_transitive_callees summary = summary.transitive_callees - - let get_transitive_missed_captures summary = summary.transitive_missed_captures + let get_transitive_info {transitive_info} = transitive_info let heap_paths_that_need_dynamic_type_specialization summary = let rec mk_heap_path var rev_accesses = @@ -2318,12 +2285,11 @@ module Topl = struct PulseTopl.report_errors proc_desc err_log ~pulse_is_manifest astate.topl end -let add_missed_captures missed_captures ({transitive_missed_captures} as astate) = +let add_missed_captures missed_captures ({transitive_info} as astate) = if Config.pulse_monitor_transitive_missed_captures then - let transitive_missed_captures = - Typ.Name.Set.union missed_captures transitive_missed_captures - in - {astate with transitive_missed_captures} + let missed_captures = Typ.Name.Set.union missed_captures transitive_info.missed_captures in + let transitive_info = {transitive_info with TransitiveInfo.missed_captures} in + {astate with transitive_info} else astate @@ -2343,6 +2309,16 @@ let add_skipped_calls new_skipped_calls astate = if phys_equal skipped_calls astate.skipped_calls then astate else {astate with skipped_calls} +let transfer_transitive_info_to_caller callee_proc_name call_loc summary caller_astate = + let caller = caller_astate.transitive_info in + let callee_summary = summary.transitive_info in + let transitive_info = + TransitiveInfo.transfer_transitive_info_to_caller ~caller callee_proc_name call_loc + ~callee_summary + in + {caller_astate with transitive_info} + + let is_local = is_local let is_allocated_this_pointer proc_attrs astate address = diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index c2fb1fea69e..c014bfb3717 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -69,12 +69,7 @@ type t = private ; need_dynamic_type_specialization: AbstractValue.Set.t (** a set of abstract values that are used as receiver of method calls in the instructions reached so far *) - ; transitive_accesses: Trace.Set.t (** record specific acceses inter-procedurally *) - ; transitive_callees: TransitiveInfo.Callees.t - (** record all call resolutions that were transitively performed *) - ; transitive_missed_captures: Typ.Name.Set.t - (** record types that were missing during name resolution (fields/methods) while analysing - this function and its transitive callees *) + ; transitive_info: TransitiveInfo.t (** record transitive information inter-procedurally *) ; skipped_calls: SkippedCalls.t (** metadata: procedure calls for which no summary was found *) } [@@deriving equal] @@ -346,18 +341,6 @@ module Summary : sig val add_need_dynamic_type_specialization : AbstractValue.t -> summary -> summary - val get_transitive_accesses : summary -> Trace.Set.t - - val get_transitive_callees : summary -> TransitiveInfo.Callees.t - - val get_transitive_missed_captures : summary -> Typ.Name.Set.t - - val transfer_accesses_to_caller : t -> Procname.t -> Location.t -> summary -> t - - val transfer_transitive_callees_to_caller : t -> summary -> t - - val transfer_transitive_missed_captures_to_caller : t -> summary -> t - val of_post : Tenv.t -> Procname.t @@ -414,8 +397,12 @@ module Summary : sig have made. *) type t = summary [@@deriving compare, equal, yojson_of] + + val get_transitive_info : t -> TransitiveInfo.t end +val transfer_transitive_info_to_caller : Procname.t -> Location.t -> Summary.t -> t -> t + module Topl : sig val small_step : Location.t -> PulseTopl.event -> t -> t diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 4d5443edd10..47f8607db9d 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -832,25 +832,10 @@ let record_need_closure_specialization callee_summary call_state = else call_state -let record_transitive_accesses callee_proc_name call_loc callee_summary call_state = +let record_transitive_info callee_proc_name call_location callee_summary call_state = let astate = - AbductiveDomain.Summary.transfer_accesses_to_caller call_state.astate callee_proc_name call_loc - callee_summary - in - {call_state with astate} - - -let record_transitive_callees callee_summary call_state = - let astate = - AbductiveDomain.Summary.transfer_transitive_callees_to_caller call_state.astate callee_summary - in - {call_state with astate} - - -let record_transitive_missed_captures callee_summary call_state = - let astate = - AbductiveDomain.Summary.transfer_transitive_missed_captures_to_caller call_state.astate - callee_summary + AbductiveDomain.transfer_transitive_info_to_caller callee_proc_name call_location callee_summary + call_state.astate in {call_state with astate} @@ -949,9 +934,7 @@ let apply_post path callee_proc_name call_location callee_summary call_state = (AbductiveDomain.Summary.get_post callee_summary).attrs >>| record_skipped_calls callee_proc_name call_location callee_summary >>| record_need_closure_specialization callee_summary - >>| record_transitive_accesses callee_proc_name call_location callee_summary - >>| record_transitive_callees callee_summary - >>| record_transitive_missed_captures callee_summary + >>| record_transitive_info callee_proc_name call_location callee_summary >>| read_return_value path callee_proc_name call_location callee_summary in PerfEvent.(log (fun logger -> log_end_event logger ())) ; diff --git a/infer/src/pulse/PulseNonDisjunctiveDomain.ml b/infer/src/pulse/PulseNonDisjunctiveDomain.ml index bd52c35c76e..547f57046bb 100644 --- a/infer/src/pulse/PulseNonDisjunctiveDomain.ml +++ b/infer/src/pulse/PulseNonDisjunctiveDomain.ml @@ -627,81 +627,21 @@ module IntraDom = struct not (CalleesWithLoc.is_empty callees) end -module DroppedTransitiveAccesses = AbstractDomain.FiniteSetOfPPSet (Trace.Set) -module TransitiveMissedCapture = AbstractDomain.FiniteSetOfPPSet (Typ.Name.Set) - -module InterDomElt = struct - type t = - { dropped_transitive_accesses: DroppedTransitiveAccesses.t - ; transitive_callees: TransitiveInfo.Callees.t - ; transitive_missed_captures: TransitiveMissedCapture.t } - [@@deriving abstract_domain] - - let pp fmt {dropped_transitive_accesses; transitive_callees; transitive_missed_captures} = - F.fprintf fmt - "@[@[dropped transitive accesses: %a@],@ @[transitive callees: %a@],@ @[transitive missed \ - captures: %a@]@]" - DroppedTransitiveAccesses.pp dropped_transitive_accesses TransitiveInfo.Callees.pp - transitive_callees Typ.Name.Set.pp transitive_missed_captures - - - let bottom = - { dropped_transitive_accesses= DroppedTransitiveAccesses.empty - ; transitive_callees= TransitiveInfo.Callees.bottom - ; transitive_missed_captures= Typ.Name.Set.empty } - - - let is_bottom {dropped_transitive_accesses; transitive_callees; transitive_missed_captures} = - DroppedTransitiveAccesses.is_bottom dropped_transitive_accesses - && TransitiveInfo.Callees.is_bottom transitive_callees - && Typ.Name.Set.is_empty transitive_missed_captures - - - let remember_dropped_elements accesses callees missed_captures - {dropped_transitive_accesses; transitive_callees; transitive_missed_captures} = - let dropped_transitive_accesses = - DroppedTransitiveAccesses.union accesses dropped_transitive_accesses - in - let transitive_callees = TransitiveInfo.Callees.join callees transitive_callees in - let transitive_missed_captures = - Typ.Name.Set.union missed_captures transitive_missed_captures - in - {dropped_transitive_accesses; transitive_callees; transitive_missed_captures} - - - let apply_summary ~callee_pname ~call_loc ~summary - {dropped_transitive_accesses; transitive_callees; transitive_missed_captures} = - let dropped_transitive_accesses = - Trace.Set.map_callee (CallEvent.Call callee_pname) call_loc - summary.dropped_transitive_accesses - |> Trace.Set.union dropped_transitive_accesses - in - let transitive_callees = - TransitiveInfo.Callees.join transitive_callees summary.transitive_callees - in - let transitive_missed_captures = - TransitiveMissedCapture.join transitive_missed_captures summary.transitive_missed_captures - in - {dropped_transitive_accesses; transitive_callees; transitive_missed_captures} -end - module InterDom = struct - include AbstractDomain.TopLifted (InterDomElt) - - let bottom = NonTop InterDomElt.bottom + include AbstractDomain.TopLifted (TransitiveInfo) - let is_bottom = get ~default:false InterDomElt.is_bottom + let bottom = NonTop TransitiveInfo.bottom - let remember_dropped_elements accesses callees missed_captures = - map (InterDomElt.remember_dropped_elements accesses callees missed_captures) + let is_bottom = get ~default:false TransitiveInfo.is_bottom + let remember_dropped_elements dropped = map (TransitiveInfo.remember_dropped_elements ~dropped) let apply_summary ~callee_pname ~call_loc ~summary non_disj = match (non_disj, summary) with | Top, _ | _, Top -> Top | NonTop non_disj, NonTop summary -> - NonTop (InterDomElt.apply_summary ~callee_pname ~call_loc ~summary non_disj) + NonTop (TransitiveInfo.apply_summary ~callee_pname ~call_loc ~summary non_disj) end type t = {intra: IntraDom.t; inter: InterDom.t} [@@deriving abstract_domain] @@ -771,9 +711,7 @@ let set_passed_to loc timestamp call_exp actuals = let is_lifetime_extended var {intra} = IntraDom.is_lifetime_extended var intra -let remember_dropped_elements accesses callees missed_captures = - map_inter (InterDom.remember_dropped_elements accesses callees missed_captures) - +let remember_dropped_elements dropped = map_inter (InterDom.remember_dropped_elements dropped) let quick_join lhs rhs = if phys_equal lhs bottom then rhs else if phys_equal rhs bottom then lhs else join lhs rhs @@ -800,35 +738,14 @@ module Summary = struct let pp fmt = function | Top -> AbstractDomain.TopLiftedUtils.pp_top fmt - | NonTop - {InterDomElt.dropped_transitive_accesses; transitive_callees; transitive_missed_captures} -> - F.fprintf fmt - "@[@[calls history: %a@],@ @[dropped transitive accesses: %a@],@ @[transitive missed \ - captures: %a@]@]" - TransitiveInfo.Callees.pp transitive_callees DroppedTransitiveAccesses.pp - dropped_transitive_accesses Typ.Name.Set.pp transitive_missed_captures + | NonTop transitive_info -> + TransitiveInfo.pp fmt transitive_info let bottom = InterDom.bottom let is_bottom = InterDom.is_bottom - let iter_on_transitive_accesses_if_not_top (x : t) ~f = - match x with - | Top -> - () - | NonTop {dropped_transitive_accesses} -> - DroppedTransitiveAccesses.iter f dropped_transitive_accesses - - - let get_transitive_callees_if_not_top (x : t) = - match x with Top -> None | NonTop {transitive_callees} -> Some transitive_callees - - - let get_transitive_missed_capture_if_not_top (x : t) = - match x with - | Top -> - None - | NonTop {transitive_missed_captures} -> - Some transitive_missed_captures + let get_transitive_info_if_not_top (x : t) = + match x with Top -> None | NonTop transitive_info -> Some transitive_info end diff --git a/infer/src/pulse/PulseNonDisjunctiveDomain.mli b/infer/src/pulse/PulseNonDisjunctiveDomain.mli index 4efaa21170f..c220768234b 100644 --- a/infer/src/pulse/PulseNonDisjunctiveDomain.mli +++ b/infer/src/pulse/PulseNonDisjunctiveDomain.mli @@ -42,11 +42,7 @@ val make_summary : t -> summary module Summary : sig include AbstractDomain.WithBottom with type t = summary - val iter_on_transitive_accesses_if_not_top : t -> f:(Trace.t -> unit) -> unit - - val get_transitive_callees_if_not_top : t -> TransitiveInfo.Callees.t option - - val get_transitive_missed_capture_if_not_top : t -> Typ.Name.Set.t option + val get_transitive_info_if_not_top : t -> TransitiveInfo.t option end val add_var : @@ -102,7 +98,7 @@ val set_passed_to : Location.t -> Timestamp.t -> Exp.t -> (Exp.t * Typ.t) list - val is_lifetime_extended : Var.t -> t -> bool -val remember_dropped_elements : Trace.Set.t -> TransitiveInfo.Callees.t -> Typ.Name.Set.t -> t -> t +val remember_dropped_elements : TransitiveInfo.t -> t -> t val apply_summary : callee_pname:Procname.t -> call_loc:Location.t -> t -> summary -> t diff --git a/infer/src/pulse/PulseTransitiveAccessChecker.ml b/infer/src/pulse/PulseTransitiveAccessChecker.ml index e5c45049735..2039f5dcabb 100644 --- a/infer/src/pulse/PulseTransitiveAccessChecker.ml +++ b/infer/src/pulse/PulseTransitiveAccessChecker.ml @@ -177,24 +177,14 @@ let report_errors tenv proc_desc err_log {PulseSummary.pre_post_list; non_disj} in List.iter pre_post_list ~f:(function | ContinueProgram astate -> - let transitive_callees = AbductiveDomain.Summary.get_transitive_callees astate in - let transitive_missed_captures = - AbductiveDomain.Summary.get_transitive_missed_captures astate + let {PulseTransitiveInfo.accesses; callees; missed_captures} = + AbductiveDomain.Summary.get_transitive_info astate in - PulseTrace.Set.iter - (report transitive_callees transitive_missed_captures) - (AbductiveDomain.Summary.get_transitive_accesses astate) + PulseTrace.Set.iter (report callees missed_captures) accesses | _ -> () ) ; - let non_disj_transitive_callees = - NonDisjDomain.Summary.get_transitive_callees_if_not_top non_disj - |> Option.value ~default:PulseTransitiveInfo.Callees.bottom - in - let non_disj_transitive_missed_captures = - NonDisjDomain.Summary.get_transitive_missed_capture_if_not_top non_disj - |> Option.value ~default:Typ.Name.Set.empty - in - NonDisjDomain.Summary.iter_on_transitive_accesses_if_not_top non_disj - ~f:(report non_disj_transitive_callees non_disj_transitive_missed_captures) + NonDisjDomain.Summary.get_transitive_info_if_not_top non_disj + |> Option.iter ~f:(fun {PulseTransitiveInfo.accesses; callees; missed_captures} -> + PulseTrace.Set.iter (report callees missed_captures) accesses ) | None -> () diff --git a/infer/src/pulse/PulseTransitiveInfo.ml b/infer/src/pulse/PulseTransitiveInfo.ml index d9b54c62415..3e47964ba4a 100644 --- a/infer/src/pulse/PulseTransitiveInfo.ml +++ b/infer/src/pulse/PulseTransitiveInfo.ml @@ -90,3 +90,46 @@ module Callees = struct {callsite_loc; caller_name; caller_loc; kind; resolution} :: acc ) history [] end + +module Accesses = AbstractDomain.FiniteSetOfPPSet (PulseTrace.Set) +module MissedCaptures = AbstractDomain.FiniteSetOfPPSet (Typ.Name.Set) + +type t = {accesses: Accesses.t; callees: Callees.t; missed_captures: MissedCaptures.t} +[@@deriving abstract_domain, compare, equal] + +let pp fmt {accesses; callees; missed_captures} = + F.fprintf fmt "@[@[accesses: %a@],@ @[callees: %a@],@ @[missed captures: %a@]@]" Accesses.pp + accesses Callees.pp callees Typ.Name.Set.pp missed_captures + + +let bottom = {accesses= Accesses.empty; callees= Callees.bottom; missed_captures= Typ.Name.Set.empty} + +let is_bottom {accesses; callees; missed_captures} = + Accesses.is_bottom accesses && Callees.is_bottom callees && Typ.Name.Set.is_empty missed_captures + + +let remember_dropped_elements ~dropped {accesses; callees; missed_captures} = + let accesses = Accesses.union dropped.accesses accesses in + let callees = Callees.join dropped.callees callees in + let missed_captures = Typ.Name.Set.union dropped.missed_captures missed_captures in + {accesses; callees; missed_captures} + + +let apply_summary ~callee_pname ~call_loc ~summary {accesses; callees; missed_captures} = + let accesses = + PulseTrace.Set.map_callee (PulseCallEvent.Call callee_pname) call_loc summary.accesses + |> PulseTrace.Set.union accesses + in + let callees = Callees.join callees summary.callees in + let missed_captures = MissedCaptures.join missed_captures summary.missed_captures in + {accesses; callees; missed_captures} + + +let transfer_transitive_info_to_caller ~caller callee_proc_name call_loc ~callee_summary = + let accesses = + PulseTrace.Set.map_callee (Call callee_proc_name) call_loc callee_summary.accesses + |> PulseTrace.Set.union caller.accesses + in + let callees = Callees.join caller.callees callee_summary.callees in + let missed_captures = Typ.Name.Set.union caller.missed_captures callee_summary.missed_captures in + {accesses; callees; missed_captures} diff --git a/infer/src/pulse/PulseTransitiveInfo.mli b/infer/src/pulse/PulseTransitiveInfo.mli index 4f0bf97575a..1b72e6caf8d 100644 --- a/infer/src/pulse/PulseTransitiveInfo.mli +++ b/infer/src/pulse/PulseTransitiveInfo.mli @@ -12,10 +12,6 @@ module Callees : sig include AbstractDomain.WithBottom - val compare : t -> t -> int - - val equal : t -> t -> bool - val pp : Format.formatter -> t -> unit type call_kind = Static | Virtual | Closure @@ -40,3 +36,20 @@ module Callees : sig val report_as_extra_info : t -> item list end + +type t = + { accesses: PulseTrace.Set.t (** record specific accesses inter-procedurally *) + ; callees: Callees.t (** record all call resolutions that were transitively performed *) + ; missed_captures: Typ.Name.Set.t + (** record types that were missing during name resolution (fields/methods) while analysing + this function and its transitive callees *) } +[@@deriving compare, equal] + +include AbstractDomain.WithBottom with type t := t + +val apply_summary : callee_pname:Procname.t -> call_loc:Location.t -> summary:t -> t -> t + +val remember_dropped_elements : dropped:t -> t -> t + +val transfer_transitive_info_to_caller : + caller:t -> Procname.t -> Location.t -> callee_summary:t -> t