allowing extra data to be packaged along with procCfg

Reviewed By: jeremydubreil

Differential Revision: D3234490

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

infer/src/backend/preanal.ml

@@ -293,7 +293,7 @@ let analyze_and_annotate_proc cfg tenv pname pdesc =
     if !Config.curr_language = Config.Java
     then Vset.empty
     else
-      match AddressTaken.Analyzer.compute_post (ProcData.make pdesc tenv) with
+      match AddressTaken.Analyzer.compute_post (ProcData.make_default pdesc tenv) with
       | Some post -> post
       | None -> Vset.empty in
 

infer/src/checkers/abstractInterpreter.ml

@@ -119,10 +119,10 @@ module Make
 
   module Interprocedural (Summ : Summary.S with type summary = A.astate) = struct
 
-    let checker { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } =
+    let checker { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } extras =
       let post_opt = ref None in
       let analyze_ondemand pdesc =
-        match compute_post (ProcData.make pdesc tenv) with
+        match compute_post (ProcData.make pdesc tenv extras) with
         | Some post ->
             Summ.write_summary (Cfg.Procdesc.get_proc_name pdesc) post;
             post_opt := Some post

infer/src/checkers/addressTaken.ml

@@ -19,6 +19,7 @@ module Domain = AbstractDomain.FiniteSet(PvarSet)
 
 module TransferFunctions = struct
   type astate = Domain.astate
+  type extras = ProcData.no_extras
 
   let rec add_address_taken_pvars exp astate = match exp with
     | Sil.Lvar pvar ->

infer/src/checkers/annotationReachability.ml

@@ -303,6 +303,7 @@ let report_allocations pname loc calls =
 
 module TransferFunctions = struct
   type astate = Domain.astate
+  type extras = ProcData.no_extras
 
   (* This is specific to the @NoAllocation and @PerformanceCritical checker
      and the "unlikely" method is used to guard branches that are expected to run sufficiently
@@ -398,7 +399,7 @@ module Interprocedural = struct
       PatternMatch.proc_iter_overridden_methods
         check_expensive_subtyping_rules tenv proc_name;
 
-    match checker proc_data with
+    match checker proc_data ProcData.empty_extras with
     | Some astate ->
         begin
           match astate with

infer/src/checkers/copyPropagation.ml

@@ -80,8 +80,8 @@ module Domain = struct
 end
 
 module TransferFunctions = struct
-
   type astate = Domain.astate
+  type extras = ProcData.no_extras
 
   let exec_instr astate _ = function
     | Sil.Letderef (lhs_id, Sil.Var rhs_id, _, _) ->
@@ -127,4 +127,4 @@ module Analyzer =
     (TransferFunctions)
 
 let checker { Callbacks.proc_desc; tenv; } =
-  ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv))
+  ignore(Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv))

infer/src/checkers/liveness.ml

@@ -20,6 +20,7 @@ module Domain = AbstractDomain.FiniteSet(Var.Set)
    read, kill the variable when it is assigned *)
 module TransferFunctions = struct
   type astate = Domain.astate
+  type extras = ProcData.no_extras
 
   (* add all of the vars read in [exp] to the live set *)
   let exp_add_live exp astate =
@@ -67,4 +68,4 @@ module Analyzer =
     (TransferFunctions)
 
 let checker { Callbacks.proc_desc; tenv; } =
-  ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv))
+  ignore(Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv))

infer/src/checkers/procData.ml

@@ -9,6 +9,14 @@
 
 open! Utils
 
-type t = { pdesc : Cfg.Procdesc.t; tenv : Tenv.t }
+type 'a t = { pdesc : Cfg.Procdesc.t; tenv : Tenv.t; extras : 'a; }
 
-let make pdesc tenv = { pdesc; tenv }
+type no_extras = unit
+
+let empty_extras = ()
+
+let make pdesc tenv extras =
+  { pdesc; tenv; extras; }
+
+let make_default pdesc tenv =
+  make pdesc tenv empty_extras

infer/src/checkers/procData.mli

@@ -0,0 +1,18 @@
+(*
+ * 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.
+ *)
+
+type 'a t = { pdesc : Cfg.Procdesc.t; tenv : Tenv.t; extras : 'a; }
+
+type no_extras
+
+val empty_extras : no_extras
+
+val make : Cfg.Procdesc.t -> Tenv.t -> 'a -> 'a t
+
+val make_default : Cfg.Procdesc.t -> Tenv.t -> no_extras t

infer/src/checkers/transferFunctions.ml

@@ -11,9 +11,9 @@ open! Utils
 
 
 module type S = sig
-  type astate
+  type astate (* abstract state to propagate *)
+  type extras (* read-only extra state (results of previous analyses, globals, etc.) *)
 
   (* {A} instr {A'}. [caller_pdesc] is the procdesc of the current procedure *)
-  val exec_instr : astate -> ProcData.t -> Sil.instr -> astate
+  val exec_instr : astate -> extras ProcData.t -> Sil.instr -> astate
-
 end

infer/src/unit/abstractInterpreterTests.ml

@@ -50,6 +50,7 @@ end
 
 module PathCountTransferFunctions = struct
   type astate = PathCountDomain.astate
+  type extras = ProcData.no_extras
 
   (* just propagate the current path count *)
   let exec_instr astate _ _ = astate

infer/src/unit/analyzerTester.ml

@@ -136,7 +136,8 @@ module Make
     (C : ProcCfg.Wrapper with type node = Cfg.Node.t)
     (S : Scheduler.S)
     (A : AbstractDomain.S)
-    (T : TransferFunctions.S with type astate = A.astate) = struct
+    (T : TransferFunctions.S
+     with type astate = A.astate and type extras = ProcData.no_extras) = struct
 
   open StructuredSil
 
@@ -225,7 +226,7 @@ module Make
 
   let create_test test_program _ =
     let pdesc, assert_map = structured_program_to_cfg test_program in
-    let inv_map = I.exec_pdesc (ProcData.make pdesc (Tenv.create ())) in
+    let inv_map = I.exec_pdesc (ProcData.make_default pdesc (Tenv.create ())) in
 
     let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc =
       let post_str =