support for interprocedural checkers

Reviewed By: jvillard

Differential Revision: D3083347

fb-gh-sync-id: f7e3bc7
fbshipit-source-id: f7e3bc7

infer/src/checkers/abstractInterpreter.ml

@@ -77,11 +77,49 @@ module Make
         exec_worklist work_queue'' inv_map'
     | None -> inv_map
 
-  let exec_pdesc pdesc =
+  (* compute and return an invariant map for [cfg] *)
-    L.out "Starting analysis of %a@." Procname.pp (Cfg.Procdesc.get_proc_name pdesc);
+  let exec_cfg cfg =
-    let cfg = C.from_pdesc pdesc in
     let start_node = C.start_node cfg in
     let inv_map', work_queue' = exec_node start_node A.initial (S.empty cfg) M.empty in
     exec_worklist work_queue' inv_map'
+
+  (* compute and return an invariant map for [pdesc] *)
+  let exec_pdesc pdesc =
+    L.out "Starting analysis of %a@." Procname.pp (Cfg.Procdesc.get_proc_name pdesc);
+    exec_cfg (C.from_pdesc pdesc)
+
+  (* compute and return the postcondition of [pdesc] *)
+  let compute_post pdesc =
+    let cfg = C.from_pdesc pdesc in
+    let inv_map = exec_cfg cfg in
+    let end_state =
+      try M.find (C.node_id (C.exit_node cfg)) inv_map
+      with Not_found ->
+        failwith
+          (Printf.sprintf
+             "No postcondition found for exit node of %s; this should never happen"
+             (Procname.to_string (Cfg.Procdesc.get_proc_name pdesc))) in
+    end_state.post
+
+  module Interprocedural (Summ : Summary.S with type summary = A.astate) = struct
+
+    let checker { Callbacks.get_proc_desc; proc_desc; proc_name; } =
+      let analyze_ondemand pdesc =
+        let post = compute_post pdesc in
+        Summ.write_summary (Cfg.Procdesc.get_proc_name pdesc) 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 proc_desc;
+          Ondemand.unset_callbacks ()
+        end
+  end
+
 end
 

infer/src/checkers/summary.ml

@@ -0,0 +1,49 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+module type Helper = sig
+  type summary
+
+  (* 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
+end
+
+module type S = sig
+  type summary
+
+  (* write the summary for [name] to persistent storage *)
+  val write_summary : Procname.t -> summary -> unit
+  (* read and return the summary for [pname]. does the analysis to create the summary if needed *)
+  val read_summary : Procname.t -> summary option
+end
+
+module Make (H : Helper) = struct
+  type summary = H.summary
+
+  let write_summary pname summary =
+    match Specs.get_summary pname with
+    | Some global_summary ->
+        let payload = H.update_payload summary global_summary.Specs.payload in
+        Specs.add_summary pname { global_summary with payload }
+    | None ->
+        Printf.sprintf "Summary for %s should exist, but does not!@." (Procname.to_string pname)
+        |> failwith
+
+  let read_summary pname =
+    (* this is reprehensible. but the caller_pdesc is only used for debug printing *)
+    (* TODO: fix the ondemand API so we can choose to pass a pdesc option *)
+    let dummy_caller_pdesc =
+      Cfg.Procdesc.create (Cfg.Node.create_cfg ()) (ProcAttributes.default pname Config.Java) in
+    Ondemand.analyze_proc_name ~propagate_exceptions:false dummy_caller_pdesc pname;
+    match Specs.get_summary pname with
+    | None -> None
+    | Some summary -> Some (H.read_from_payload summary.Specs.payload)
+end