pass tenv to the transfer functions

Reviewed By: cristianoc

Differential Revision: D3153716

fb-gh-sync-id: 855fc41
fbshipit-source-id: 855fc41

infer/src/backend/preanal.ml

@@ -281,7 +281,7 @@ let add_dead_pvars_after_conditionals_join cfg n deads =
 
 (** Find the set of dead variables for the procedure pname and add nullify instructions.
     The variables whose addresses may be taken are only considered just before the exit node. *)
-let analyze_and_annotate_proc cfg pname pdesc =
+let analyze_and_annotate_proc cfg tenv pname pdesc =
   let exit_node = Cfg.Procdesc.get_exit_node pdesc in
   let exit_node_is_succ node =
     match Cfg.Node.get_succs node with
@@ -293,7 +293,7 @@ let analyze_and_annotate_proc cfg pname pdesc =
     if !Config.curr_language = Config.Java
     then Vset.empty
     else
-      match AddressTaken.Analyzer.compute_post pdesc with
+      match AddressTaken.Analyzer.compute_post (ProcData.make pdesc tenv) with
       | Some post -> post
       | None -> Vset.empty in
 
@@ -445,7 +445,7 @@ let add_removetemps_instructions cfg =
 let doit ?(f_translate_typ=None) cfg cg tenv =
   add_removetemps_instructions cfg;
   AllPreds.mk_table cfg;
-  Cfg.iter_proc_desc cfg (analyze_and_annotate_proc cfg);
+  Cfg.iter_proc_desc cfg (analyze_and_annotate_proc cfg tenv);
   AllPreds.clear_table ();
   if !Config.curr_language = Config.Java
   then add_dispatch_calls cfg cg tenv f_translate_typ;

infer/src/checkers/abstractInterpreter.ml

@@ -22,11 +22,11 @@ module Make
   (* invariant map from node id -> abstract state representing postcondition for node id *)
   type inv_map = state M.t
 
-  let exec_node node astate_pre work_queue inv_map pdesc =
+  let exec_node node astate_pre work_queue inv_map proc_data =
     let exec_instrs astate_acc instr =
       if A.is_bottom astate_acc
       then astate_acc
-      else T.exec_instr astate_acc pdesc instr in
+      else T.exec_instr astate_acc proc_data instr in
     let node_id = C.node_id node in
     L.out "Doing analysis of node %a from pre %a@." C.pp_node_id node_id A.pp astate_pre;
     let instrs = C.instrs node in
@@ -59,10 +59,10 @@ module Make
         M.add node_id { post=astate_post; visit_count; } inv_map in
       inv_map', S.schedule_succs work_queue node
 
-  let rec exec_worklist work_queue inv_map pdesc =
+  let rec exec_worklist work_queue inv_map proc_data =
     match S.pop work_queue with
     | Some (_, [], work_queue') ->
-        exec_worklist work_queue' inv_map pdesc
+        exec_worklist work_queue' inv_map proc_data
     | Some (node, visited_pred :: visited_preds, work_queue') ->
         let get_post pred_id =
           (M.find pred_id inv_map).post in
@@ -70,25 +70,25 @@ module Make
         let join_pred_posts astate_acc pred_id =
           A.join (get_post pred_id) astate_acc in
         let astate_pre = IList.fold_left join_pred_posts (get_post visited_pred) visited_preds in
-        let inv_map', work_queue'' = exec_node node astate_pre work_queue' inv_map pdesc in
+        let inv_map', work_queue'' = exec_node node astate_pre work_queue' inv_map proc_data in
-        exec_worklist work_queue'' inv_map' pdesc
+        exec_worklist work_queue'' inv_map' proc_data
     | None -> inv_map
 
   (* compute and return an invariant map for [cfg] *)
-  let exec_cfg cfg pdesc =
+  let exec_cfg cfg proc_data =
     let start_node = C.start_node cfg in
-    let inv_map', work_queue' = exec_node start_node A.initial (S.empty cfg) M.empty pdesc in
+    let inv_map', work_queue' = exec_node start_node A.initial (S.empty cfg) M.empty proc_data in
-    exec_worklist work_queue' inv_map' pdesc
+    exec_worklist work_queue' inv_map' proc_data
 
   (* compute and return an invariant map for [pdesc] *)
-  let exec_pdesc pdesc =
+  let exec_pdesc ({ ProcData.pdesc; } as proc_data) =
     L.out "Starting analysis of %a@." Procname.pp (Cfg.Procdesc.get_proc_name pdesc);
-    exec_cfg (C.from_pdesc pdesc) pdesc
+    exec_cfg (C.from_pdesc pdesc) proc_data
 
   (* compute and return the postcondition of [pdesc] *)
-  let compute_post pdesc =
+  let compute_post ({ ProcData.pdesc; } as proc_data) =
     let cfg = C.from_pdesc pdesc in
-    let inv_map = exec_cfg cfg pdesc in
+    let inv_map = exec_cfg cfg proc_data in
     try
       let end_state = M.find (C.node_id (C.exit_node cfg)) inv_map in
       Some (end_state.post)
@@ -102,9 +102,9 @@ module Make
 
   module Interprocedural (Summ : Summary.S with type summary = A.astate) = struct
 
-    let checker { Callbacks.get_proc_desc; proc_desc; proc_name; } =
+    let checker { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } =
       let analyze_ondemand pdesc =
-        match compute_post pdesc with
+        match compute_post (ProcData.make pdesc tenv) with
         | Some post ->
             Summ.write_summary (Cfg.Procdesc.get_proc_name pdesc) post
         | None -> () in

infer/src/checkers/copyPropagation.ml

@@ -118,4 +118,5 @@ module Analyzer =
     (Domain)
     (TransferFunctions)
 
-let checker { Callbacks.proc_desc; } = ignore(Analyzer.exec_pdesc proc_desc)
+let checker { Callbacks.proc_desc; tenv; } =
+  ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv))

infer/src/checkers/liveness.ml

@@ -64,4 +64,5 @@ module Analyzer =
     (Domain)
     (TransferFunctions)
 
-let checker { Callbacks.proc_desc; } = ignore(Analyzer.exec_pdesc proc_desc)
+let checker { Callbacks.proc_desc; tenv; } =
+  ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv))

infer/src/checkers/procData.ml

@@ -0,0 +1,12 @@
+(*
+ * 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 t = { pdesc : Cfg.Procdesc.t; tenv : Tenv.t }
+
+let make pdesc tenv = { pdesc; tenv }

infer/src/checkers/transferFunctions.ml

@@ -12,6 +12,6 @@ module type S = sig
   type astate
 
   (* {A} instr {A'}. [caller_pdesc] is the procdesc of the current procedure *)
-  val exec_instr : astate -> Cfg.Procdesc.t -> Sil.instr -> astate
+  val exec_instr : astate -> ProcData.t -> Sil.instr -> astate
 
 end

infer/src/unit/analyzerTester.ml

@@ -200,7 +200,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 pdesc in
+    let inv_map = I.exec_pdesc (ProcData.make pdesc (Tenv.create ())) in
 
     let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc =
       let post_str =