From 5a5a865bf45639438a01ba84c97849fa48edf7b0 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Thu, 28 Feb 2019 06:39:34 -0800
Subject: [PATCH] Small refactorings: ReachingDefs

Summary: Adds an mli and don't expose the internal Analyzer.

Reviewed By: ezgicicek

Differential Revision: D14258324

fbshipit-source-id: ecc433226
---
 infer/src/checkers/cost.ml          |  6 +-----
 infer/src/checkers/hoisting.ml      |  6 +-----
 infer/src/checkers/loopInvariant.ml |  2 +-
 infer/src/checkers/reachingDefs.ml  | 15 +++++++++++++--
 infer/src/checkers/reachingDefs.mli | 24 ++++++++++++++++++++++++
 5 files changed, 40 insertions(+), 13 deletions(-)
 create mode 100644 infer/src/checkers/reachingDefs.mli

diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml
index a9721661e..230b902ad 100644
--- a/infer/src/checkers/cost.ml
+++ b/infer/src/checkers/cost.ml
@@ -749,11 +749,7 @@ let checker {Callbacks.tenv; proc_desc; integer_type_widths; summary} : Summary.
   in
   let node_cfg = NodeCFG.from_pdesc proc_desc in
   (* computes reaching defs: node -> (var -> node set) *)
-  let reaching_defs_invariant_map =
-    let proc_data = ProcData.make_default proc_desc tenv in
-    ReachingDefs.Analyzer.exec_cfg node_cfg proc_data
-      ~initial:(ReachingDefs.init_reaching_defs_with_formals proc_desc)
-  in
+  let reaching_defs_invariant_map = ReachingDefs.compute_invariant_map proc_desc tenv in
   (* collect all prune nodes that occur in loop guards, needed for ControlDepAnalyzer *)
   let control_maps, loop_head_to_loop_nodes = Loop_control.get_control_maps node_cfg in
   (* computes the control dependencies: node -> var set *)
diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml
index b7d4416a2..d1e61d78c 100644
--- a/infer/src/checkers/hoisting.ml
+++ b/infer/src/checkers/hoisting.ml
@@ -123,12 +123,8 @@ let get_issue_to_report tenv (Call.({pname}) as call) integer_type_widths inferb
 
 let checker Callbacks.({tenv; summary; proc_desc; integer_type_widths}) : Summary.t =
   let cfg = InstrCFG.from_pdesc proc_desc in
-  let proc_data = ProcData.make_default proc_desc tenv in
   (* computes reaching defs: node -> (var -> node set) *)
-  let reaching_defs_invariant_map =
-    ReachingDefs.Analyzer.exec_cfg cfg proc_data
-      ~initial:(ReachingDefs.init_reaching_defs_with_formals proc_desc)
-  in
+  let reaching_defs_invariant_map = ReachingDefs.compute_invariant_map proc_desc tenv in
   let inferbo_invariant_map =
     lazy (BufferOverrunAnalysis.cached_compute_invariant_map proc_desc tenv integer_type_widths)
   in
diff --git a/infer/src/checkers/loopInvariant.ml b/infer/src/checkers/loopInvariant.ml
index 37b640a75..6b098adba 100644
--- a/infer/src/checkers/loopInvariant.ml
+++ b/infer/src/checkers/loopInvariant.ml
@@ -214,7 +214,7 @@ let get_inv_vars_in_loop tenv reaching_defs_invariant_map ~is_inv_by_default loo
     then (inv_vars, false)
     else
       let loop_head_id = Procdesc.Node.get_id loop_head in
-      ReachingDefs.Analyzer.extract_post loop_head_id reaching_defs_invariant_map
+      ReachingDefs.extract_post loop_head_id reaching_defs_invariant_map
       |> Option.map ~f:(fun reaching_defs ->
              ReachingDefs.ReachingDefsMap.find_opt var reaching_defs
              |> Option.map ~f:(fun def_nodes ->
diff --git a/infer/src/checkers/reachingDefs.ml b/infer/src/checkers/reachingDefs.ml
index 406f151a8..24feec05e 100644
--- a/infer/src/checkers/reachingDefs.ml
+++ b/infer/src/checkers/reachingDefs.ml
@@ -6,6 +6,7 @@
  *)
 open! IStd
 module F = Format
+module NodeCFG = ProcCfg.Normal
 
 (** The node in which the reaching definition x := e is defined.
 
@@ -16,7 +17,7 @@ module Defs = AbstractDomain.FiniteSet (Procdesc.Node)
 
 (* even though we only add singletons (defs), the set is needed for joins *)
 
-(** Map var -> its reaching definition **)
+(** Map var -> its reaching definition *)
 module ReachingDefsMap = AbstractDomain.Map (Var) (Defs)
 
 (* forward transfer function for reaching definitions *)
@@ -64,4 +65,14 @@ let init_reaching_defs_with_formals pdesc =
          ReachingDefsMap.add (Var.of_pvar pvar) start_node_defs acc )
 
 
-module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctionsReachingDefs (ProcCfg.Normal))
+module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctionsReachingDefs (NodeCFG))
+
+type invariant_map = Analyzer.invariant_map
+
+let compute_invariant_map pdesc tenv =
+  let proc_data = ProcData.make_default pdesc tenv in
+  let node_cfg = NodeCFG.from_pdesc pdesc in
+  Analyzer.exec_cfg node_cfg proc_data ~initial:(init_reaching_defs_with_formals pdesc)
+
+
+let extract_post = Analyzer.extract_post
diff --git a/infer/src/checkers/reachingDefs.mli b/infer/src/checkers/reachingDefs.mli
new file mode 100644
index 000000000..5585e84d2
--- /dev/null
+++ b/infer/src/checkers/reachingDefs.mli
@@ -0,0 +1,24 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+(** The node in which the reaching definition x := e is defined.
+
+    A definition x :=e, declared at node N, reaches the current node
+   if there is a path from node N to the current node such that x is
+   not modified along the path **)
+module Defs : module type of AbstractDomain.FiniteSet (Procdesc.Node)
+
+(** Map var -> its reaching definition *)
+module ReachingDefsMap : module type of AbstractDomain.Map (Var) (Defs)
+
+type invariant_map
+
+val compute_invariant_map : Procdesc.t -> Tenv.t -> invariant_map
+
+val extract_post : Procdesc.Node.id -> invariant_map -> ReachingDefsMap.t option