[absint] kill `AbstractInterpreter.Interprocedural` module

Summary:
After D5245416 I was taking a closer look and decided it's best to get rid of the `Interprocedural` module altogether.
Since jeremydubreil's refactoring to pass the summaries around everywhere, this module doesn't do much (it used to make sure the summary actually got stored to disk).
Client code is shorter and simpler without this module.

Reviewed By: mbouaziz

Differential Revision: D5255400

fbshipit-source-id: acd1c00

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -345,7 +345,6 @@ end
 
 module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctions)
 
-module Interprocedural = AbstractInterpreter.Interprocedural (Summary)
 module CFG = Analyzer.TransferFunctions.CFG
 module Sem = BufferOverrunSemantics.Make (CFG)
 
@@ -539,21 +538,12 @@ let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit
       Dom.Summary.pp_summary s
 
 let checker : Callbacks.proc_callback_args -> Specs.summary
-  = fun ({ proc_desc; tenv; summary } as callback) ->
+  = fun { proc_desc; tenv; summary; get_proc_desc; } ->
     let proc_name = Specs.get_proc_name summary in
-    let make_extras _ = callback.get_proc_desc in
-    let updated_summary : Specs.summary =
-      Interprocedural.compute_summary
-        ~compute_post
-        ~make_extras
-        proc_desc
-        tenv
-        summary in
-    let post =
-      updated_summary.payload.buffer_overrun in
-    begin
-      match post with
-      | Some s when Config.bo_debug >= 1 -> print_summary proc_name s
-      | _ -> ()
-    end;
-    updated_summary
+    let proc_data = ProcData.make proc_desc tenv get_proc_desc in
+    match compute_post proc_data with
+    | Some post ->
+        if Config.bo_debug >= 1 then print_summary proc_name post;
+        Summary.update_summary post summary
+    | None ->
+        summary

infer/src/checkers/AbstractInterpreter.ml

@@ -155,16 +155,6 @@ module MakeNoCFG
     extract_post (CFG.id (CFG.exit_node cfg)) inv_map
 end
 
-module Interprocedural (Summ : Summary.S) = struct
-
-  let compute_summary ~compute_post ~make_extras proc_desc tenv summary =
-    match compute_post (ProcData.make proc_desc tenv (make_extras proc_desc)) with
-    | Some post ->
-        Summ.update_summary post summary
-    | None ->
-        summary
-end
-
 module MakeWithScheduler (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.MakeSIL) =
   MakeNoCFG (S (C)) (T (C))
 

infer/src/checkers/AbstractInterpreter.mli

@@ -63,17 +63,3 @@ module Make
     (CFG : ProcCfg.S)
     (MakeTransferFunctions : TransferFunctions.MakeSIL) :
   S with module TransferFunctions = MakeTransferFunctions(CFG)
-
-(** create an interprocedural abstract interpreter given logic for handling summaries *)
-module Interprocedural (Summary : Summary.S) : sig
-
-  (** compute a summary for the given procedure using [compute_post] and write it into the
-      aggregated [Specs.summary] *)
-  val compute_summary :
-    compute_post: ('a ProcData.t -> Summary.payload option) ->
-    make_extras : (Procdesc.t -> 'a) ->
-    Procdesc.t ->
-    Tenv.t ->
-    Specs.summary ->
-    Specs.summary
-end

infer/src/checkers/NullabilitySuggest.ml

@@ -40,15 +40,7 @@ module UseDefChain = struct
 end
 module Domain = AbstractDomain.Map (AccessPath.Raw) (UseDefChain)
 
-(* Right now this is just a placeholder. We'll change it to something useful when necessary *)
-module Summary = Summary.Make(struct
-    type payload = unit
-
-    let update_payload _ summary = summary
-    let read_payload _ = None
-  end)
-
-type extras = unit
+type extras = ProcData.no_extras
 
 module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
@@ -116,7 +108,6 @@ module Analyzer =
   AbstractInterpreter.Make
     (ProcCfg.Exceptional)
     (LowerHil.Make (TransferFunctions))
-module Interprocedural = AbstractInterpreter.Interprocedural (Summary)
 
 let make_error_trace astate ap ud =
   let name_of ap =
@@ -187,16 +178,14 @@ let checker { Callbacks.summary; proc_desc; tenv; } =
     in
     Domain.iter report_access_path astate
   in
-  let compute_post (proc_data : extras ProcData.t) =
   (* Assume all fields are not null in the beginning *)
   let initial = Domain.empty, IdAccessPathMapDomain.empty in
+  let proc_data = ProcData.make_default proc_desc tenv in
   match Analyzer.compute_post proc_data ~initial ~debug:false with
   | Some (post, _) ->
       report post proc_data;
-        Some ()
+      summary
   | None ->
       failwithf
         "Analyzer failed to compute post for %a"
         Typ.Procname.pp (Procdesc.get_proc_name proc_data.pdesc)
-  in
-  Interprocedural.compute_summary ~compute_post ~make_extras:(fun _ -> ()) proc_desc tenv summary

infer/src/checkers/Siof.ml

@@ -172,9 +172,6 @@ end
 
 module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctions)
 
-module Interprocedural = AbstractInterpreter.Interprocedural (Summary)
-
-
 let is_foreign tu_opt (v, _) =
   match Pvar.get_translation_unit v, tu_opt with
   | TUFile v_tu, Some current_tu ->
@@ -239,25 +236,16 @@ let siof_check pdesc gname (summary : Specs.summary) =
   | Some (SiofDomain.BottomSiofTrace.Bottom, _) | None ->
       ()
 
-let compute_post proc_data =
-  Analyzer.compute_post proc_data
-    ~initial:(SiofDomain.BottomSiofTrace.Bottom, SiofDomain.VarNames.empty)
-  |> Option.map ~f:SiofDomain.normalize
-
-let checker { Callbacks.proc_desc; tenv; summary } : Specs.summary =
+let checker { Callbacks.proc_desc; tenv; summary; } : Specs.summary =
+  let proc_data = ProcData.make_default proc_desc tenv in
+  let initial = SiofDomain.BottomSiofTrace.Bottom, SiofDomain.VarNames.empty in
   let updated_summary =
-    Interprocedural.compute_summary
-      ~compute_post
-      ~make_extras:ProcData.make_empty_extras
-      proc_desc
-      tenv
-      summary in
-  let pname = Procdesc.get_proc_name proc_desc in
+    match Analyzer.compute_post proc_data ~initial with
+    | Some post -> Summary.update_summary (SiofDomain.normalize post) summary
+    | None -> summary in
   begin
-    match Typ.Procname.get_global_name_of_initializer pname with
-    | Some gname ->
-        siof_check proc_desc gname updated_summary
-    | None ->
-        ()
+    match Typ.Procname.get_global_name_of_initializer (Procdesc.get_proc_name proc_desc) with
+    | Some gname -> siof_check proc_desc gname updated_summary
+    | None -> ()
   end;
   updated_summary

infer/src/checkers/ThreadSafety.ml

@@ -761,8 +761,6 @@ end
 
 module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (LowerHil.Make(TransferFunctions))
 
-module Interprocedural = AbstractInterpreter.Interprocedural (Summary)
-
 (* similarly, we assume that immutable classes safely encapsulate their state *)
 let is_immutable_collection_class class_name tenv =
   let immutable_collections = [
@@ -871,14 +869,15 @@ let analyze_procedure { Callbacks.proc_desc; tenv; summary; } =
     Typ.Procname.is_constructor proc_name || FbThreadSafety.is_custom_init tenv proc_name in
   let open ThreadSafetyDomain in
   (* convert the abstract state to a summary by dropping the id map *)
-  let compute_post ({ ProcData.pdesc; tenv; extras; } as proc_data) =
-    if should_analyze_proc pdesc tenv
+  if should_analyze_proc proc_desc tenv
   then
     begin
-        if not (Procdesc.did_preanalysis pdesc) then Preanal.do_liveness pdesc tenv;
+      if not (Procdesc.did_preanalysis proc_desc) then Preanal.do_liveness proc_desc tenv;
+      let extras = FormalMap.make proc_desc in
+      let proc_data = ProcData.make proc_desc tenv extras in
       let initial =
-          let threads = runs_on_ui_thread pdesc || is_thread_confined_method tenv pdesc in
-          if is_initializer tenv (Procdesc.get_proc_name pdesc)
+        let threads = runs_on_ui_thread proc_desc || is_thread_confined_method tenv proc_desc in
+        if is_initializer tenv (Procdesc.get_proc_name proc_desc)
         then
           let add_owned_formal acc formal_index =
             match FormalMap.get_formal_base formal_index extras with
@@ -890,8 +889,8 @@ let analyze_procedure { Callbacks.proc_desc; tenv; summary; } =
             (* if a constructer is called via DI, all of its formals will be freshly allocated
                and therefore owned. we assume that constructors annotated with @Inject will only
                be called via DI or using fresh parameters. *)
-              if Annotations.pdesc_has_return_annot pdesc Annotations.ia_is_inject
-              then List.mapi ~f:(fun i _ -> i)  (Procdesc.get_formals pdesc)
+            if Annotations.pdesc_has_return_annot proc_desc Annotations.ia_is_inject
+            then List.mapi ~f:(fun i _ -> i)  (Procdesc.get_formals proc_desc)
             else [0] (* express that the constructor owns [this] *) in
           let attribute_map =
             List.fold
@@ -906,18 +905,18 @@ let analyze_procedure { Callbacks.proc_desc; tenv; summary; } =
       | Some ({ thumbs_up; threads; locks; accesses; attribute_map; }, _) ->
           let return_var_ap =
             AccessPath.of_pvar
-                (Pvar.get_ret_pvar (Procdesc.get_proc_name pdesc))
-                (Procdesc.get_ret_type pdesc) in
+              (Pvar.get_ret_pvar (Procdesc.get_proc_name proc_desc))
+              (Procdesc.get_ret_type proc_desc) in
           let return_attributes =
             try AttributeMapDomain.find return_var_ap attribute_map
             with Not_found -> AttributeSetDomain.empty in
-            Some (thumbs_up, threads, locks, accesses, return_attributes)
+          let post = thumbs_up, threads, locks, accesses, return_attributes in
+          Summary.update_summary post summary
       | None ->
-            None
+          summary
     end
   else
-      Some empty_post in
-  Interprocedural.compute_summary ~compute_post ~make_extras:FormalMap.make proc_desc tenv summary
+    Summary.update_summary empty_post summary
 
 (* we assume two access paths can alias if their access parts are equal (we ignore the base). *)
 let can_alias access_path1 access_path2 =

infer/src/checkers/annotationReachability.ml

@@ -389,37 +389,20 @@ let check_expensive_subtyping_rules { Callbacks.proc_desc; tenv; summary } overr
         (expensive_overrides_unexpensive, Localise.verbatim_desc description) in
     Reporting.log_error summary ~loc exn
 
-module Interprocedural = struct
-  include AbstractInterpreter.Interprocedural(Summary)
 
-  let check_and_report ({ Callbacks.proc_desc; tenv; summary} as callback) : Specs.summary =
+let checker ({ Callbacks.proc_desc; tenv; summary} as callback) : Specs.summary =
   let proc_name = Procdesc.get_proc_name proc_desc in
   if is_expensive tenv proc_name then
     PatternMatch.override_iter (check_expensive_subtyping_rules callback) tenv proc_name;
-
   let initial =
     (AnnotReachabilityDomain.empty, Domain.TrackingDomain.NonBottom Domain.TrackingVar.empty) in
-    let compute_post proc_data =
-      Option.map ~f:fst (Analyzer.compute_post ~initial proc_data) in
-    let updated_summary : Specs.summary =
-      compute_summary
-        ~compute_post:compute_post
-        ~make_extras:ProcData.make_empty_extras
-        proc_desc
-        tenv
-        summary in
-    begin
-      match updated_summary.payload.annot_map with
-      | Some annot_map ->
-          List.iter ~f:(report_src_snk_paths callback annot_map) src_snk_pairs
+  let proc_data = ProcData.make_default proc_desc tenv in
+  match Analyzer.compute_post proc_data ~initial with
+  | Some (annot_map, _) ->
+      List.iter ~f:(report_src_snk_paths callback annot_map) src_snk_pairs;
+      Summary.update_summary annot_map summary
   | None ->
-          ()
-    end;
-    updated_summary
-
-end
-
-let checker = Interprocedural.check_and_report
+      summary
 
 (* New implementation starts here *)
 

infer/src/labs/ResourceLeaks.ml

@@ -92,10 +92,6 @@ module Analyzer =
     (ProcCfg.Normal) (* 5(a) *)
     (LowerHil.Make(TransferFunctions))
 
-(* Lift our intraprocedural abstract interpreter into an interprocedural one that computes
-   summaries of the type we defined earlier *)
-module Interprocedural = AbstractInterpreter.Interprocedural (Summary)
-
 (* Callback for invoking the checker from the outside--registered in RegisterCheckers *)
 let checker { Callbacks.summary; proc_desc; tenv; } : Specs.summary =
   (* Report an error when we have acquired more resources than we have released *)
@@ -107,20 +103,20 @@ let checker { Callbacks.summary; proc_desc; tenv; } : Specs.summary =
       let message = F.asprintf "Leaked %d resource(s)" leak_count in
       let exn = Exceptions.Checkers (issue_kind, Localise.verbatim_desc message) in
       Reporting.log_error summary ~loc:last_loc exn in
+
   (* Convert the abstract state to a summary. for now, just the identity function *)
   let convert_to_summary (post : Domain.astate) : Domain.summary =
     (* 4(a) *)
     post in
-  let compute_post (proc_data : extras ProcData.t) =
+  let extras = FormalMap.make proc_desc in
+  let proc_data = ProcData.make proc_desc tenv extras in
   let initial = ResourceLeakDomain.initial, IdAccessPathMapDomain.empty in
   match Analyzer.compute_post proc_data ~initial ~debug:false with
   | Some (post, _) ->
       (* 1(c) *)
       report post proc_data;
-        Some (convert_to_summary post)
+      Summary.update_summary (convert_to_summary post) summary
   | None ->
       failwithf
         "Analyzer failed to compute post for %a"
-          Typ.Procname.pp (Procdesc.get_proc_name proc_data.pdesc) in
-
-  Interprocedural.compute_summary ~compute_post ~make_extras:FormalMap.make proc_desc tenv summary
+        Typ.Procname.pp (Procdesc.get_proc_name proc_data.pdesc)

infer/src/quandary/TaintAnalysis.ml

@@ -612,8 +612,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct
 
     TaintSpecification.to_summary_access_tree with_footprint_vars
 
-  module Interprocedural = AbstractInterpreter.Interprocedural(Summary)
-
   let checker { Callbacks.tenv; summary; proc_desc; } : Specs.summary =
 
     (* bind parameters to a trace with a tainted source (if applicable) *)
@@ -631,24 +629,22 @@ module Make (TaintSpecification : TaintSpec.S) = struct
           (TraceDomain.Source.get_tainted_formals pdesc tenv) in
       access_tree, IdAccessPathMapDomain.empty in
 
-    let compute_post (proc_data : extras ProcData.t) =
-      if not (Procdesc.did_preanalysis proc_data.pdesc)
+    if not (Procdesc.did_preanalysis proc_desc)
     then
       begin
-          Preanal.do_liveness proc_data.pdesc proc_data.tenv;
-          Preanal.do_dynamic_dispatch
-            proc_data.pdesc (Cg.create (SourceFile.invalid __FILE__)) proc_data.tenv;
+        Preanal.do_liveness proc_desc tenv;
+        Preanal.do_dynamic_dispatch proc_desc (Cg.create (SourceFile.invalid __FILE__)) tenv;
       end;
-      let initial = make_initial proc_data.pdesc in
+    let initial = make_initial proc_desc in
+    let extras =
+      let formal_map = FormalMap.make proc_desc in
+      { formal_map; summary; } in
+    let proc_data = ProcData.make proc_desc tenv extras in
     match Analyzer.compute_post proc_data ~initial ~debug:false with
     | Some (access_tree, _) ->
-          Some (make_summary proc_data access_tree)
+        Summary.update_summary (make_summary proc_data access_tree) summary
     | None ->
-          if Procdesc.Node.get_succs (Procdesc.get_start_node proc_data.pdesc) <> []
+        if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> []
         then failwith "Couldn't compute post"
-          else None in
-    let make_extras pdesc =
-      let formal_map = FormalMap.make pdesc in
-      { formal_map; summary; } in
-    Interprocedural.compute_summary ~compute_post ~make_extras proc_desc tenv summary
+        else summary
 end