[absint] make Interprocedural functor easier to customize

Summary:
Before, the Interprocedural functor was a bit inflexible. You couldn't do custom postprocessing like normalizing the post state or coverting the post from an astate type to a summary type.
Now, you can do whatever you want by passing a custom `~compute_post` function.
Since `AbstractInterpreter.compute_post` can be used by clients who don't care to do anything custom, this doesn't create too much boilerplate.

Reviewed By: jvillard

Differential Revision: D4309877

fbshipit-source-id: 8d1d85d

infer/src/checkers/AbstractInterpreter.mli

@@ -17,14 +17,6 @@ module type S = sig
 
   module InvariantMap : Map.S with type key = TransferFunctions.CFG.id
 
-  (** create an interprocedural abstract interpreter given logic for handling summaries *)
-  module Interprocedural
-      (Summary : Summary.S with type summary = TransferFunctions.Domain.astate) :
-  sig
-    val checker : Callbacks.proc_callback_args -> TransferFunctions.extras ->
-      TransferFunctions.Domain.astate option
-  end
-
   (** invariant map from node id -> state representing postcondition for node id *)
   type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t
 
@@ -60,3 +52,15 @@ module Make
     (MakeScheduler : Scheduler.Make)
     (MakeTransferFunctions : TransferFunctions.Make) :
   S with module TransferFunctions = MakeTransferFunctions(CFG)
+
+(** create an interprocedural abstract interpreter given logic for handling summaries *)
+module Interprocedural (Summary : Summary.S) : sig
+
+  (** compute and return the summary for the given procedure and store it on disk using
+      [compute_post]. *)
+  val compute_and_store_post :
+    compute_post: ('a ProcData.t -> Summary.summary option) ->
+    make_extras : (Procdesc.t -> 'a) ->
+    Callbacks.proc_callback_args ->
+    Summary.summary option
+end

infer/src/checkers/Siof.ml

@@ -103,7 +103,7 @@ module Analyzer =
     (Scheduler.ReversePostorder)
     (TransferFunctions)
 
-module Interprocedural = Analyzer.Interprocedural (Summary)
+module Interprocedural = AbstractInterpreter.Interprocedural (Summary)
 
 
 let is_foreign tu_opt v =
@@ -176,7 +176,11 @@ let siof_check pdesc gname = function
       ()
 
 let checker ({ Callbacks.proc_desc; } as callback) =
-  let post = Interprocedural.checker callback ProcData.empty_extras in
+  let post =
+    Interprocedural.compute_and_store_post
+      ~compute_post:Analyzer.compute_post
+      ~make_extras:ProcData.make_empty_extras
+      callback in
   let pname = Procdesc.get_proc_name proc_desc in
   match Procname.get_global_name_of_initializer pname with
   | Some gname ->

infer/src/checkers/ThreadSafety.ml

@@ -157,12 +157,16 @@ module Analyzer =
     (Scheduler.ReversePostorder)
     (TransferFunctions)
 
-module Interprocedural = Analyzer.Interprocedural (Summary)
+module Interprocedural = AbstractInterpreter.Interprocedural (Summary)
 
 (*This is a "checker"*)
 let method_analysis callback =
   let proc_desc = callback.Callbacks.proc_desc in
-  let opost = Interprocedural.checker callback ProcData.empty_extras in
+  let opost =
+    Interprocedural.compute_and_store_post
+      ~compute_post:Analyzer.compute_post
+      ~make_extras:ProcData.make_empty_extras
+      callback in
   match opost with
   | Some post ->  (* I am printing to commandline and out to cater to javac and buck*)
       (L.stdout  "\n Procedure: %s@ "
@@ -201,7 +205,11 @@ let make_results_table get_proc_desc file_env =
       let callback_arg =
         {Callbacks.get_proc_desc; get_procs_in_file = (fun _ -> []);
          idenv; tenv; proc_name; proc_desc} in
-      match Interprocedural.checker callback_arg ProcData.empty_extras with
+      match
+        Interprocedural.compute_and_store_post
+          ~compute_post:Analyzer.compute_post
+          ~make_extras:ProcData.make_empty_extras
+          callback_arg with
       | Some post -> post
       | None -> ThreadSafetyDomain.initial
   in

infer/src/checkers/abstractInterpreter.ml

@@ -19,8 +19,14 @@ module type S = sig
   module Interprocedural
       (Summary : Summary.S with type summary = TransferFunctions.Domain.astate) :
   sig
-    val checker : Callbacks.proc_callback_args -> TransferFunctions.extras ->
-      TransferFunctions.Domain.astate option
+
+    (** compute and return the summary for the given procedure and store it on disk using
+        [compute_post]. *)
+    val compute_and_store_post :
+      compute_post: ('a ProcData.t -> Summary.summary option) ->
+      make_extras : (Procdesc.t -> 'a) ->
+      Callbacks.proc_callback_args ->
+      Summary.summary option
   end
 
   type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t
@@ -129,11 +135,14 @@ module MakeNoCFG
     let inv_map = exec_cfg cfg proc_data in
     extract_post (CFG.id (CFG.exit_node cfg)) inv_map
 
-  module Interprocedural (Summ : Summary.S with type summary = Domain.astate) = struct
+end
+
+module Interprocedural (Summ : Summary.S) = struct
 
-    let checker { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } extras =
+  let compute_and_store_post
+      ~compute_post ~make_extras { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } =
     let analyze_ondemand_ _ pdesc =
-        match compute_post (ProcData.make pdesc tenv extras) with
+      match compute_post (ProcData.make pdesc tenv (make_extras pdesc)) with
       | Some post ->
           Summ.write_summary (Procdesc.get_proc_name pdesc) post;
           Some post
@@ -157,7 +166,7 @@ module MakeNoCFG
     else
       Summ.read_summary proc_desc proc_name
 end
-end
+
 
 module Make (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.Make) =
   MakeNoCFG (S (C)) (T (C))

infer/src/checkers/annotationReachability.ml

@@ -353,7 +353,7 @@ module Analyzer =
     (TransferFunctions)
 
 module Interprocedural = struct
-  include Analyzer.Interprocedural(Summary)
+  include AbstractInterpreter.Interprocedural(Summary)
 
   let is_expensive tenv pname =
     check_attributes Annotations.ia_is_expensive tenv pname
@@ -403,7 +403,10 @@ module Interprocedural = struct
       if not (IList.length calls = 0)
       then IList.iter (report_src_snk_path calls) src_annot_list in
 
-    match checker proc_data ProcData.empty_extras with
+    match compute_and_store_post
+            ~compute_post:Analyzer.compute_post
+            ~make_extras:ProcData.make_empty_extras
+            proc_data with
     | Some Domain.NonBottom (call_map, _) ->
         IList.iter (report_src_snk_paths call_map) (src_snk_pairs ())
     | Some Domain.Bottom | None ->

infer/src/checkers/procData.ml

@@ -15,6 +15,8 @@ type no_extras = unit
 
 let empty_extras = ()
 
+let make_empty_extras _ = ()
+
 let make pdesc tenv extras =
   { pdesc; tenv; extras; }
 

infer/src/checkers/procData.mli

@@ -17,4 +17,6 @@ val empty_extras : no_extras
 
 val make : Procdesc.t -> Tenv.t -> 'a -> 'a t
 
+val make_empty_extras : Procdesc.t -> no_extras
+
 val make_default : Procdesc.t -> Tenv.t -> no_extras t

infer/src/checkers/summary.ml

@@ -11,21 +11,27 @@ open! IStd
 
 module type Helper = sig
   type summary
+  (*  type astate*)
 
   (* update the specs payload with [summary] *)
   val update_payload : summary -> Specs.payload -> Specs.payload
   (* extract [summmary] from the specs payload *)
   val read_from_payload : Specs.payload -> summary option
+
+  (*val to_summary : astate -> summary*)
 end
 
 module type S = sig
   type summary
+  (*  type astate*)
 
   (* write the summary for [name] to persistent storage *)
   val write_summary : Procname.t -> summary -> unit
   (* read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis to
      create the summary if needed *)
   val read_summary : Procdesc.t -> Procname.t -> summary option
+
+  (*  val to_summary : astate -> summary*)
 end
 
 module Make (H : Helper) = struct

infer/src/quandary/TaintAnalysis.ml

@@ -35,6 +35,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct
   module TaintDomain = AccessTree.Make (TraceDomain)
   module IdMapDomain = IdAccessPathMapDomain
 
+  (** map from formals to their position *)
+  type formal_map = int AccessPath.BaseMap.t
+
   module Domain = struct
     type astate =
       {
@@ -83,8 +86,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct
     module CFG = CFG
     module Domain = Domain
 
-    (** map from formals to their position *)
-    type formal_map = int AccessPath.BaseMap.t
     type extras = formal_map
 
     let is_formal base formal_map =
@@ -547,11 +548,21 @@ module Make (TaintSpecification : TaintSpec.S) = struct
       TraceDomain.Source.Set.fold add_summary_for_source (TraceDomain.sources trace) summary_acc in
     TaintDomain.fold add_summaries_for_trace access_tree []
 
-  let dummy_cg = Cg.create None
+  module Interprocedural = AbstractInterpreter.Interprocedural(Summary)
+
+  let checker callback =
+
+    let compute_post (proc_data : formal_map ProcData.t) =
+      Preanal.doit ~handle_dynamic_dispatch:true proc_data.pdesc (Cg.create None) proc_data.tenv;
+      match Analyzer.compute_post proc_data with
+      | Some { access_tree; } ->
+          Some (make_summary proc_data.extras access_tree)
+      | None ->
+          if Procdesc.Node.get_succs (Procdesc.get_start_node proc_data.pdesc) <> []
+          then failwith "Couldn't compute post"
+          else None in
 
-  let checker { Callbacks.get_proc_desc; proc_name; proc_desc; tenv; } =
-    let analyze_ondemand _ pdesc =
-      let make_formal_access_paths pdesc =
+    let make_extras pdesc =
       let pname = Procdesc.get_proc_name pdesc in
       let attrs = Procdesc.get_attributes pdesc in
       let formals_with_nums =
@@ -565,28 +576,5 @@ module Make (TaintSpecification : TaintSpec.S) = struct
         AccessPath.BaseMap.empty
         formals_with_nums in
 
-      Preanal.doit ~handle_dynamic_dispatch:true pdesc dummy_cg tenv;
-      let formals = make_formal_access_paths pdesc in
-      let proc_data = ProcData.make pdesc tenv formals in
-      match Analyzer.compute_post proc_data with
-      | Some { access_tree; } ->
-          let summary = make_summary formals access_tree in
-          Summary.write_summary (Procdesc.get_proc_name pdesc) summary;
-      | None ->
-          if Procdesc.Node.get_succs (Procdesc.get_start_node pdesc) <> []
-          then failwith "Couldn't compute post" in
-
-    let callbacks =
-      {
-        Ondemand.analyze_ondemand;
-        get_proc_desc;
-      } in
-    if Ondemand.procedure_should_be_analyzed proc_name
-    then
-      begin
-        Ondemand.set_callbacks callbacks;
-        analyze_ondemand SourceFile.empty proc_desc;
-        Ondemand.unset_callbacks ();
-      end
-
+    ignore(Interprocedural.compute_and_store_post ~compute_post ~make_extras callback)
 end