Small refactorings: Control

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

Reviewed By: ezgicicek

Differential Revision: D14258273

fbshipit-source-id: a000e5286

infer/src/checkers/control.ml

@@ -161,6 +161,14 @@ end
 
 module ControlDepAnalyzer = AbstractInterpreter.MakeRPO (TransferFunctionsControlDeps (CFG))
 
+type invariant_map = ControlDepAnalyzer.invariant_map
+
+let compute_invariant_map pdesc tenv control_maps : invariant_map =
+  let proc_data = ProcData.make pdesc tenv control_maps in
+  let node_cfg = CFG.from_pdesc pdesc in
+  ControlDepAnalyzer.exec_cfg node_cfg proc_data ~initial:ControlDepSet.empty
+
+
 (* Filter CVs which are invariant in the loop where the CV originated from *)
 let remove_invariant_vars control_vars loop_inv_map =
   ControlDepSet.fold

infer/src/checkers/control.mli

@@ -0,0 +1,35 @@
+(*
+ * 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
+module LoopHead = Procdesc.Node
+module LoopHeads = Procdesc.NodeSet
+
+(** Map control var -> loop head location  *)
+module ControlMap : module type of PrettyPrintable.MakePPMap (Var)
+
+module GuardNodes : module type of AbstractDomain.FiniteSet (Procdesc.Node)
+
+(** Map exit node -> loop head set  *)
+module ExitNodeToLoopHeads = Procdesc.NodeMap
+
+(** Map loop head -> prune nodes in the loop guard  *)
+module LoopHeadToGuardNodes = Procdesc.NodeMap
+
+type invariant_map
+
+type loop_control_maps =
+  { exit_map: LoopHeads.t ExitNodeToLoopHeads.t
+  ; loop_head_to_guard_nodes: GuardNodes.t LoopHeadToGuardNodes.t }
+
+val compute_invariant_map : Procdesc.t -> Tenv.t -> loop_control_maps -> invariant_map
+
+val compute_control_vars :
+     invariant_map
+  -> LoopInvariant.VarsInLoop.t LoopHeadToGuardNodes.t
+  -> LoopHead.t
+  -> Location.t ControlMap.t

infer/src/checkers/cost.ml

@@ -757,10 +757,7 @@ let checker {Callbacks.tenv; proc_desc; integer_type_widths; summary} : Summary.
   (* 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 *)
-  let control_dep_invariant_map =
-    let proc_data = ProcData.make proc_desc tenv control_maps in
-    Control.ControlDepAnalyzer.exec_cfg node_cfg proc_data ~initial:Control.ControlDepSet.empty
-  in
+  let control_dep_invariant_map = Control.compute_invariant_map proc_desc tenv control_maps in
   (* compute loop invariant map for control var analysis *)
   let loop_inv_map =
     LoopInvariant.get_loop_inv_var_map tenv reaching_defs_invariant_map loop_head_to_loop_nodes