[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

@@ -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 )
 

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
     "@[<v>%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 =

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
 

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 ())) ;

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