From 41c121bebf1b50c47c3d0d4a6747b8f0e4f6ed3d Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Mon, 12 Sep 2016 21:48:11 -0700
Subject: [PATCH] [quandary] adding quandary summaries to specs

Reviewed By: jeremydubreil

Differential Revision: D3851178

fbshipit-source-id: 8a17357
---
 infer/src/backend/specs.ml          |  2 ++
 infer/src/backend/specs.mli         |  1 +
 infer/src/quandary/TaintAnalysis.ml | 56 ++++++++++++++++++++++-------
 3 files changed, 47 insertions(+), 12 deletions(-)

diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml
index a4e9572ec..ee7bac418 100644
--- a/infer/src/backend/specs.ml
+++ b/infer/src/backend/specs.ml
@@ -324,6 +324,7 @@ type payload =
     typestate : unit TypeState.t option; (** final typestate *)
     calls: call_summary option;
     crashcontext_frame: Stacktree_j.stacktree option;
+    quandary : QuandarySummary.t option;
     (** Proc location and blame_range info for crashcontext analysis *)
   }
 
@@ -758,6 +759,7 @@ let empty_payload =
     typestate = None;
     calls = None;
     crashcontext_frame = None;
+    quandary = None;
   }
 
 (** [init_summary (depend_list, nodes,
diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli
index 9da126530..f5a8a13d5 100644
--- a/infer/src/backend/specs.mli
+++ b/infer/src/backend/specs.mli
@@ -129,6 +129,7 @@ type payload =
     calls:  call_summary option; (** list of calls of the form (call, loc) *)
     crashcontext_frame: Stacktree_j.stacktree option;
     (** Procedure location and blame_range info for crashcontext analysis *)
+    quandary : QuandarySummary.t option;
   }
 
 (** Procedure summary *)
diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml
index bc5e71c5d..976cfc756 100644
--- a/infer/src/quandary/TaintAnalysis.ml
+++ b/infer/src/quandary/TaintAnalysis.ml
@@ -14,6 +14,19 @@ module L = Logging
 
 (** Create a taint analysis from a trace domain *)
 
+module Summary = Summary.Make(struct
+    type summary = QuandarySummary.t
+
+    let update_payload summary payload =
+      { payload with Specs.quandary = Some summary; }
+
+    let read_from_payload payload =
+      match payload.Specs.quandary with
+      | Some summary -> summary
+      | None -> failwith "Failed to load summary"
+  end)
+
+
 module Make (TraceDomain : QuandarySummary.Trace) = struct
 
   module TaintDomain = AccessTree.Make (TraceDomain)
@@ -317,18 +330,37 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
     IList.fold_lefti add_formal_summaries [] formals
     |> add_return_summaries
 
-  let checker { Callbacks.proc_name; proc_desc; tenv; } =
-    let formals =
-      let attrs = Cfg.Procdesc.get_attributes proc_desc in
-      IList.map
-        (fun (name, typ) -> AccessPath.base_of_pvar (Pvar.mk name proc_name) typ)
-        attrs.formals in
-    let proc_data = ProcData.make proc_desc tenv formals in
-    match Analyzer.compute_post proc_data with
-    | Some { access_tree; } ->
-        ignore (make_summary formals access_tree proc_desc)
-    | None ->
-        failwithf "Couldn't compute post for function %a@." Procname.pp proc_name
+  let checker { Callbacks.get_proc_desc; proc_name; proc_desc; tenv; } =
+    let analyze_ondemand pdesc =
+      let make_formal_access_paths pdesc : AccessPath.base list=
+        let pname = Cfg.Procdesc.get_proc_name pdesc in
+        let attrs = Cfg.Procdesc.get_attributes pdesc in
+        IList.map
+          (fun (name, typ) ->
+             let pvar = Pvar.mk name pname in
+             AccessPath.base_of_pvar pvar typ)
+          attrs.ProcAttributes.formals in
+      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 pdesc in
+          Summary.write_summary (Cfg.Procdesc.get_proc_name pdesc) summary;
+      | None ->
+          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 proc_desc;
+        Ondemand.unset_callbacks ();
+      end
+
 end
 
 module Java = Make(struct