Separate payloads from different analyses in specs.

Summary: public
Currently payloads for different analyses are stored in a disjoint union.
After this diff, a record is used to enable running different analyses using the same spec files.

Reviewed By: jvillard

Differential Revision: D2695566

fb-gh-sync-id: 3d2886d

infer/src/backend/fork.ml

@@ -65,20 +65,24 @@ let transition_footprint_re_exe proc_name joined_pres =
         Specs.phase = Specs.RE_EXECUTION;
       }
     else
+      let specs =
+        IList.map
+          (fun jp ->
+             Specs.spec_normalize
+               { Specs.pre = jp;
+                 posts = [];
+                 visited = Specs.Visitedset.empty })
+          joined_pres in
+      let payload =
+        { summary.Specs.payload with
+          Specs.preposts = Some specs; } in
+      let dependency_map =
+        Specs.re_initialize_dependency_map summary.Specs.dependency_map in
       { summary with
         Specs.timestamp = 0;
-        Specs.phase = Specs.RE_EXECUTION;
+        phase = Specs.RE_EXECUTION;
-        Specs.dependency_map = Specs.re_initialize_dependency_map summary.Specs.dependency_map;
+        dependency_map;
-        Specs.payload =
+        payload;
-          let specs =
-            IList.map
-              (fun jp ->
-                 Specs.spec_normalize
-                   { Specs.pre = jp;
-                     Specs.posts = [];
-                     Specs.visited = Specs.Visitedset.empty })
-              joined_pres in
-          Specs.PrePosts specs
       } in
   Specs.add_summary proc_name summary'
 
@@ -414,11 +418,14 @@ let interprocedural_algorithm
         let prev_summary = Specs.get_summary_unsafe "interprocedural_algorithm" pname in
         let timestamp = max 1 (prev_summary.Specs.timestamp) in
         let stats = { prev_summary.Specs.stats with Specs.stats_timeout = true } in
+        let payload =
+          { prev_summary.Specs.payload with
+            Specs.preposts = Some []; } in
         let summ =
           { prev_summary with
-            Specs.stats = stats;
+            Specs.stats;
-            Specs.payload = Specs.PrePosts [];
+            payload;
-            Specs.timestamp = timestamp } in
+            timestamp; } in
         summ in
   let process_result exe_env (pname, calls) summary =
     (* wrap _process_result and handle exceptions *)

infer/src/backend/interproc.ml

@@ -1093,10 +1093,14 @@ let update_summary prev_summary specs proc_name elapsed res =
       Specs.stats_time = stats_time;
       Specs.symops = symops;
       Specs.stats_timeout = timeout } in
+  let payload =
+    { prev_summary.Specs.payload with
+      Specs.preposts = Some new_specs; } in
   { prev_summary with
-    Specs.stats = stats;
+    Specs.stats;
-    Specs.payload = Specs.PrePosts new_specs;
+    payload;
-    Specs.timestamp = timestamp }
+    timestamp;
+  }
 
 
 (** Analyze [proc_name] and return the updated summary. Use module
@@ -1119,7 +1123,7 @@ let analyze_proc exe_env (proc_name: Procname.t) : Specs.summary =
   let updated_summary =
     update_summary prev_summary specs proc_name elapsed res in
   if (!Config.curr_language <> Config.Java && Config.report_assertion_failure)
-     || !Config.report_runtime_exceptions then
+  || !Config.report_runtime_exceptions then
     report_runtime_exceptions tenv cfg proc_desc updated_summary;
   updated_summary
 

infer/src/backend/specs.ml

@@ -307,9 +307,11 @@ type is_library = Source | Library
 
 (** Payload: results of some analysis *)
 type payload =
-  | PrePosts of NormSpec.t list (** list of specs *)
+  {
-  | TypeState of unit TypeState.t option (** final typestate *)
+    preposts : NormSpec.t list option; (** list of specs *)
-  | Calls of CallTree.t list
+    typestate : unit TypeState.t option; (** final typestate *)
+    calls:  CallTree.t list option;
+  }
 
 type summary =
   { dependency_map: dependency_map_t;  (** maps children procs to timestamp as last seen at the start of an analysys phase for this proc *)
@@ -426,9 +428,10 @@ let pp_summary_no_stats_specs fmt summary =
 let pp_stats_html err_log fmt stats =
   Errlog.pp_html [] fmt err_log
 
-let get_specs_from_payload summary = match summary.payload with
+let get_specs_from_payload summary =
-  | PrePosts specs -> NormSpec.tospecs specs
+  match summary.payload.preposts with
-  | TypeState _ | Calls _ -> []
+  | Some specs -> NormSpec.tospecs specs
+  | None -> []
 
 (** Print the summary *)
 let pp_summary pe whole_seconds fmt summary =
@@ -480,10 +483,14 @@ let rec post_equal pl1 pl2 = match pl1, pl2 with
       if Prop.prop_equal p1 p2 then post_equal pl1' pl2'
       else false
 
-let payload_compact sh payload = match payload with
+let payload_compact sh payload =
-  | PrePosts specs -> PrePosts (IList.map (NormSpec.compact sh) specs)
+  match payload.preposts with
-  | TypeState _ as p -> p
+  | Some specs ->
-  | Calls _ as p -> p
+      { payload with
+        preposts = Some (IList.map (NormSpec.compact sh) specs);
+      }
+  | None ->
+      payload
 
 (** Return a compact representation of the summary *)
 let summary_compact sh summary =
@@ -529,10 +536,12 @@ let summary_serializer : summary Serialization.serializer =
 
 (** Save summary for the procedure into the spec database *)
 let store_summary pname (summ: summary) =
-  let process_payload = function
+  let process_payload payload = match payload.preposts with
-    | PrePosts specs -> PrePosts (IList.map NormSpec.erase_join_info_pre specs)
+    | Some specs ->
-    | TypeState _ as p -> p
+        { payload with
-    | Calls _ as p -> p in
+          preposts = Some (IList.map NormSpec.erase_join_info_pre specs);
+        }
+    | None -> payload in
   let summ1 = { summ with payload = process_payload summ.payload } in
   let summ2 = if !Config.save_compact_summaries
     then summary_compact (Sil.create_sharing_env ()) summ1
@@ -778,6 +787,13 @@ let update_dependency_map proc_name =
           summary.dependency_map in
       set_summary_origin proc_name { summary with dependency_map = current_dependency_map } origin
 
+let empty_payload =
+  {
+    preposts = None;
+    typestate = None;
+    calls = None;
+  }
+
 (** [init_summary (depend_list, nodes,
     proc_flags, calls, cyclomatic, in_out_calls_opt, proc_attributes)]
     initializes the summary for [proc_name] given dependent procs in list [depend_list]. *)
@@ -792,7 +808,7 @@ let init_summary
       nodes = nodes;
       phase = FOOTPRINT;
       sessions = ref 0;
-      payload = PrePosts [];
+      payload = empty_payload;
       stats = empty_stats calls cyclomatic in_out_calls_opt;
       status = INACTIVE;
       timestamp = 0;

infer/src/backend/specs.mli

@@ -119,9 +119,11 @@ type dependency_map_t = int Procname.Map.t
 
 (** Payload: results of some analysis *)
 type payload =
-  | PrePosts of NormSpec.t list (** list of specs *)
+  {
-  | TypeState of unit TypeState.t option (** final typestate *)
+    preposts : NormSpec.t list option; (** list of specs *)
-  | Calls of CallTree.t list (** list of call tree *)
+    typestate : unit TypeState.t option; (** final typestate *)
+    calls:  CallTree.t list option; (** list of call tree *)
+  }
 
 (** Procedure summary *)
 type summary =

infer/src/checkers/codeQuery.ml

@@ -42,16 +42,19 @@ module Err = struct
     let specs =
       let spec =
         { Specs.pre = Specs.Jprop.Prop (1, Prop.prop_emp);
-          Specs.posts = [];
+          posts = [];
-          Specs.visited = Specs.Visitedset.empty
+          visited = Specs.Visitedset.empty
         } in
       [(Specs.spec_normalize spec)] in
     let new_summ = { old_summ with
                      Specs.attributes =
                        { old_summ.Specs.attributes with
                          ProcAttributes.loc = Cfg.Procdesc.get_loc proc_desc };
-                     Specs.nodes = nodes;
+                     nodes = nodes;
-                     Specs.payload = Specs.PrePosts specs } in
+                     payload =
+                       { old_summ.Specs.payload with
+                         Specs.preposts = Some specs; }
+                   } in
     Specs.add_summary proc_name new_summ
 
   let add_error_to_spec proc_name s node loc =

infer/src/checkers/eradicate.ml

@@ -41,7 +41,7 @@ end (* CallBackT *)
 module type ExtensionT = sig
   type extension
   val ext : extension TypeState.ext
-  val mkpayload : extension TypeState.t option -> Specs.payload
+  val update_payload : extension TypeState.t option -> Specs.payload -> Specs.payload
 end
 
 (** Create a module with the toplevel callback. *)
@@ -60,7 +60,8 @@ struct
           {
             old_summ with
             Specs.nodes = nodes;
-            Specs.payload = Extension.mkpayload final_typestate_opt;
+            Specs.payload =
+              Extension.update_payload final_typestate_opt old_summ.Specs.payload;
             Specs.attributes =
               {
                 old_summ.Specs.attributes with
@@ -373,7 +374,9 @@ struct
       join = join;
       pp = pp;
     }
-  let mkpayload typestate_opt = Specs.TypeState typestate_opt
+  let update_payload typestate_opt payload =
+    { payload with
+      Specs.typestate = typestate_opt; }
 end
 
 module Main =

infer/src/checkers/eradicate.mli

@@ -32,7 +32,7 @@ end (* CallBackT *)
 module type ExtensionT = sig
   type extension
   val ext : extension TypeState.ext
-  val mkpayload : extension TypeState.t option -> Specs.payload
+  val update_payload : extension TypeState.t option -> Specs.payload -> Specs.payload
 end
 
 (** Given an extension to the typestate with a check, call the check on each instruction. *)

infer/src/checkers/performanceCritical.ml

@@ -54,9 +54,9 @@ let lookup_call_trees pname =
   | None -> []
   | Some summary ->
       begin
-        match summary.Specs.payload with
+        match summary.Specs.payload.Specs.calls with
-        | Specs.Calls tree -> tree
+        | Some tree -> tree
-        | _ -> []
+        | None -> []
       end
 
 
@@ -80,7 +80,11 @@ let update_summary call_trees pname =
   | None -> ()
   | Some summary ->
       let updated_summary =
-        { summary with Specs.payload = Specs.Calls call_trees } in
+        { summary with
+          Specs.payload =
+            { summary.Specs.payload with
+              Specs.calls = Some call_trees; }
+        } in
       Specs.add_summary pname updated_summary
 
 
@@ -164,7 +168,7 @@ let callback_performance_checker _ get_proc_desc _ tenv pname proc_desc =
       | Some pd -> check_one_procedure tenv pn pd in
     { Ondemand.analyze_ondemand; get_proc_desc; } in
   if !Config.ondemand_enabled
-     || Ondemand.procedure_should_be_analyzed proc_desc pname
+  || Ondemand.procedure_should_be_analyzed proc_desc pname
   then
     begin
       Ondemand.set_callbacks callbacks;

infer/src/checkers/repeatedCallsChecker.ml

@@ -159,7 +159,7 @@ struct
       pp = pp;
     }
 
-  let mkpayload typestate = Specs.TypeState None
+  let update_payload typestate payload = payload
 end (* CheckRepeatedCalls *)
 
 module MainRepeatedCalls =