move Var into its own module

Reviewed By: jeremydubreil

Differential Revision: D3140401

fb-gh-sync-id: 750b66a
fbshipit-source-id: 750b66a

infer/src/checkers/copyPropagation.ml

@@ -10,86 +10,61 @@
 module F = Format
 module L = Logging
 
-type var =
-  | ProgramVar of Pvar.t
-  | LogicalVar of Ident.t
-
-let var_compare v1 v2 = match v1, v2 with
-  | ProgramVar pv1, ProgramVar pv2 -> Pvar.compare pv1 pv2
-  | LogicalVar sv1, LogicalVar sv2 -> Ident.compare sv1 sv2
-  | ProgramVar _, _ -> 1
-  | LogicalVar _, _ -> -1
-
-let var_equal v1 v2 =
-  var_compare v1 v2 = 0
-
-let pp_var fmt = function
-  | ProgramVar pv ->
-      (Pvar.pp pe_text) fmt pv
-  | LogicalVar id ->
-      (Ident.pp pe_text) fmt id
-
 module Domain = struct
-  module VarMap = PrettyPrintable.MakePPMap(struct
+  type astate = Var.t Var.Map.t
-      type t = var
-      let compare = var_compare
-      let pp_key = pp_var
-    end)
-
-  type astate = var VarMap.t
 
-  let initial = VarMap.empty
+  let initial = Var.Map.empty
 
   let is_bottom _ = false
 
   (* return true if the key-value bindings in [rhs] are a subset of the key-value bindings in
      [lhs] *)
   let (<=) ~lhs ~rhs =
-    VarMap.for_all
+    Var.Map.for_all
       (fun k v ->
-         try var_equal v (VarMap.find k lhs)
+         try Var.var_equal v (Var.Map.find k lhs)
          with Not_found -> false)
       rhs
 
   let join astate1 astate2 =
     let keep_if_same _ v1_opt v2_opt = match v1_opt, v2_opt with
       | Some v1, Some v2 ->
-          if var_equal v1 v2 then Some v1 else None
+          if Var.var_equal v1 v2 then Some v1 else None
       | _ -> None in
-    VarMap.merge keep_if_same astate1 astate2
+    Var.Map.merge keep_if_same astate1 astate2
 
   let widen ~prev ~next ~num_iters:_=
     join prev next
 
   let pp fmt astate =
-    let pp_value = pp_var in
+    let pp_value = Var.pp_var in
-    VarMap.pp ~pp_value fmt astate
+    Var.Map.pp ~pp_value fmt astate
 
   let gen var1 var2 astate =
     (* don't add tautological copies *)
-    if var_equal var1 var2
+    if Var.var_equal var1 var2
     then astate
-    else VarMap.add var1 var2 astate
+    else Var.Map.add var1 var2 astate
 
   let kill_copies_with_var var astate =
     let do_kill lhs_var rhs_var astate_acc =
-      if var_equal var lhs_var
+      if Var.var_equal var lhs_var
       then astate_acc (* kill copies vith [var] on lhs *)
       else
-      if var_equal var rhs_var
+      if Var.var_equal var rhs_var
       then (* delete [var] = [rhs_var] copy, but add [lhs_var] = M(rhs_var) copy*)
-        try VarMap.add lhs_var (VarMap.find rhs_var astate) astate_acc
+        try Var.Map.add lhs_var (Var.Map.find rhs_var astate) astate_acc
         with Not_found -> astate_acc
       else (* copy is unaffected by killing [var]; keep it *)
-        VarMap.add lhs_var rhs_var astate_acc in
+        Var.Map.add lhs_var rhs_var astate_acc in
-    VarMap.fold do_kill astate VarMap.empty
+    Var.Map.fold do_kill astate Var.Map.empty
 
   (* kill the previous binding for [lhs_var], and add a new [lhs_var] -> [rhs_var] binding *)
   let kill_then_gen lhs_var rhs_var astate =
     let already_has_binding lhs_var rhs_var astate =
-      try var_equal rhs_var (VarMap.find lhs_var astate)
+      try Var.var_equal rhs_var (Var.Map.find lhs_var astate)
       with Not_found -> false in
-    if var_equal lhs_var rhs_var || already_has_binding lhs_var rhs_var astate
+    if Var.var_equal lhs_var rhs_var || already_has_binding lhs_var rhs_var astate
     then astate (* already have this binding; no need to kill or gen *)
     else
       kill_copies_with_var lhs_var astate

infer/src/checkers/liveness.ml

@@ -12,18 +12,11 @@ module L = Logging
 
 (** backward analysis for computing set of maybe-live variables at each program point *)
 
-module VarSet = PrettyPrintable.MakePPSet(struct
+module Domain = AbstractDomain.FiniteSet(Var.Set)
-    type t = CopyPropagation.var
-    let compare = CopyPropagation.var_compare
-    let pp_element = CopyPropagation.pp_var
-  end)
-
-module Domain = AbstractDomain.FiniteSet(VarSet)
 
 (* compilers 101-style backward transfer functions for liveness analysis. gen a variable when it is
    read, kill the variable when it is assigned *)
 module TransferFunctions = struct
-
   type astate = Domain.astate
 
   (* add all of the vars read in [exp] to the live set *)

infer/src/checkers/var.ml

@@ -0,0 +1,41 @@
+(*
+ * 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.
+ *)
+
+(** single abstraction for all the kinds of variables in SIL *)
+
+type var =
+  | ProgramVar of Pvar.t
+  | LogicalVar of Ident.t
+
+type t = var
+
+let var_compare v1 v2 = match v1, v2 with
+  | ProgramVar pv1, ProgramVar pv2 -> Pvar.compare pv1 pv2
+  | LogicalVar sv1, LogicalVar sv2 -> Ident.compare sv1 sv2
+  | ProgramVar _, _ -> 1
+  | LogicalVar _, _ -> -1
+
+let var_equal v1 v2 =
+  var_compare v1 v2 = 0
+
+let pp_var fmt = function
+  | ProgramVar pv -> (Pvar.pp pe_text) fmt pv
+  | LogicalVar id -> (Ident.pp pe_text) fmt id
+
+module Map = PrettyPrintable.MakePPMap(struct
+    type t = var
+    let compare = var_compare
+    let pp_key = pp_var
+  end)
+
+module Set = PrettyPrintable.MakePPSet(struct
+    type t = var
+    let compare = var_compare
+    let pp_element = pp_var
+  end)