Forcing node ids of procCfg's to be Cfg.Node.id

Summary:
Results of AbsInt checkers are node id -> abstract state maps.
It's hard to compare/combine the results of multiple analyses if the node id types are different.
Needed for the upcoming improvements of the preanalysis.

Reviewed By: jvillard

Differential Revision: D3235669

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

infer/src/IR/cfg.ml

@@ -145,7 +145,12 @@ module Node = struct
       with Not_found -> () in
     Procname.Hash.iter mark_pdesc_if_unchanged new_procs
 
-  let node_id_gen cfg = incr cfg.node_id; !(cfg.node_id)
+
+  let id_of_int__FOR_TESTING_ONLY i = i
+
+  let node_id_gen cfg =
+    incr cfg.node_id;
+    !(cfg.node_id)
 
   let pdesc_tbl_add cfg proc_name proc_desc =
     Procname.Hash.add cfg.name_pdesc_tbl proc_name proc_desc
@@ -223,6 +228,16 @@ module Node = struct
       let compare = compare
     end)
 
+  module IdSet = Set.Make(struct
+      type t = id
+      let compare = id_compare
+    end)
+
+  module IdMap = Map.Make(struct
+      type t = id
+      let compare = id_compare
+    end)
+
   let get_sliced_succs node f =
     let visited = ref NodeSet.empty in
     let rec slice_nodes nodes : NodeSet.t =
@@ -356,8 +371,11 @@ module Node = struct
   (** Set the location of the node *)
   let set_loc n loc = n.nd_loc <- loc
 
+  let pp_id f id =
+    F.fprintf f "%d" id
+
   let pp f node =
-    F.fprintf f "%n" (get_id node)
+    pp_id f (get_id node)
 
   let proc_desc_from_name cfg proc_name =
     try Some (pdesc_tbl_find cfg proc_name)
@@ -819,6 +837,12 @@ module NodeHash = Hashtbl.Make(Node)
 (** Set of nodes. *)
 module NodeSet = Node.NodeSet
 
+(** Set of node ids. *)
+module IdSet = Node.IdSet
+
+(** Map with node id keys. *)
+module IdMap = Node.IdMap
+
 let iter_proc_desc = Node.iter_proc_desc
 
 let rec pp_node_list f = function

infer/src/IR/cfg.mli

@@ -199,6 +199,9 @@ module Node : sig
   (** compare node ids *)
   val id_compare : id -> id -> int
 
+  (** convert an integer to a node id. FOR TESTING ONLY *)
+  val  id_of_int__FOR_TESTING_ONLY : int -> id
+
   (** Get the source location of the node *)
   val get_loc : t -> Location.t
 
@@ -245,6 +248,8 @@ module Node : sig
   (** Pretty print the node *)
   val pp : Format.formatter -> t -> unit
 
+  val pp_id : Format.formatter -> id -> unit
+
   (** Print extended instructions for the node,
       highlighting the given subinstruction if present *)
   val pp_instrs :
@@ -283,6 +288,12 @@ module NodeHash : Hashtbl.S with type key = Node.t
 (** Set of nodes. *)
 module NodeSet : Set.S with type elt = Node.t
 
+(** Map with node id keys. *)
+module IdMap : Map.S with type key = Node.id
+
+(** Set of node ids. *)
+module IdSet : Set.S with type elt = Node.id
+
 val pp_node_list : Format.formatter -> Node.t list -> unit
 
 (** {2 Functions for manipulating an interprocedural CFG} *)

infer/src/checkers/abstractInterpreter.ml

@@ -18,7 +18,7 @@ module Make
     (T : TransferFunctions.S with type astate = A.astate) = struct
 
   module S = Sched (C)
-  module M = ProcCfg.NodeIdMap (C)
+  module M = Cfg.IdMap
 
   type state = { pre: A.astate; post: A.astate; visit_count: int; }
   (* invariant map from node id -> abstract state representing postcondition for node id *)
@@ -29,7 +29,7 @@ module Make
     try
       Some (M.find node_id inv_map)
     with Not_found ->
-      L.err "Warning: No state found for node %a" C.pp_node_id node_id;
+      L.err "Warning: No state found for node %a" Cfg.Node.pp_id node_id;
       None
 
   (** extract the postcondition of node [n] from [inv_map] *)
@@ -46,7 +46,7 @@ module Make
 
   let exec_node node astate_pre work_queue inv_map proc_data =
     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;
+    L.out "Doing analysis of node %a from pre %a@." Cfg.Node.pp_id node_id A.pp astate_pre;
     let update_inv_map astate_pre visit_count =
       let astate_post =
         let exec_instrs astate_acc instr =
@@ -54,7 +54,7 @@ module Make
           then astate_acc
           else T.exec_instr astate_acc proc_data instr in
         IList.fold_left exec_instrs astate_pre (C.instrs node) in
-      L.out "Post for node %a is %a@." C.pp_node_id node_id A.pp astate_post;
+      L.out "Post for node %a is %a@." Cfg.Node.pp_id node_id A.pp astate_post;
       let inv_map' = M.add node_id { pre=astate_pre; post=astate_post; visit_count; } inv_map in
       inv_map', S.schedule_succs work_queue node in
     if M.mem node_id inv_map then

infer/src/checkers/procCfg.ml

@@ -17,10 +17,9 @@ module F = Format
 module type Base = sig
   type t
   type node
-  type node_id
 
-  val node_id : node -> node_id
-  val node_id_compare : node_id -> node_id -> int
+  val node_id : node -> Cfg.Node.id
+  val node_id_compare : Cfg.Node.id -> Cfg.Node.id -> int
   (** all successors (normal and exceptional) *)
   val succs : t -> node -> node list
   (** all predecessors (normal and exceptional) *)
@@ -49,14 +48,12 @@ module type Wrapper = sig
   val from_pdesc : Cfg.Procdesc.t -> t
 
   val pp_node : F.formatter -> node -> unit
-  val pp_node_id : F.formatter -> node_id -> unit
 end
 
 (** Forward CFG with no exceptional control-flow *)
 module Normal = struct
   type t = Cfg.Procdesc.t
   type node = Cfg.node
-  type node_id = Cfg.Node.id
 
   let node_id = Cfg.Node.get_id
   let normal_succs _ n = Cfg.Node.get_succs n
@@ -78,8 +75,6 @@ module Normal = struct
   let node_id_compare = Cfg.Node.id_compare
 
   let pp_node = Cfg.Node.pp
-
-  let pp_node_id fmt (n : Cfg.Node.id) = F.fprintf fmt "%d" (n :> int)
 end
 
 (** Forward CFG with exceptional control-flow *)
@@ -91,7 +86,6 @@ module Exceptional : Wrapper with type node = Cfg.node = struct
     end)
 
   type node = Cfg.node
-  type node_id = Cfg.Node.id
   type id_node_map = node list NodeIdMap.t
   type t = Cfg.Procdesc.t * id_node_map
 
@@ -154,7 +148,6 @@ module Exceptional : Wrapper with type node = Cfg.node = struct
   let node_id = Cfg.Node.get_id
   let node_id_compare = Cfg.Node.id_compare
   let pp_node = Cfg.Node.pp
-  let pp_node_id fmt (n : Cfg.Node.id) = F.fprintf fmt "%d" (n :> int)
   let kind = Cfg.Node.get_kind
 end
 
@@ -172,13 +165,3 @@ module Backward (W : Wrapper) = struct
   let exceptional_succs = W.exceptional_preds
   let exceptional_preds = W.exceptional_succs
 end
-
-module NodeIdMap (B : Base) = Map.Make(struct
-    type t = B.node_id
-    let compare = B.node_id_compare
-  end)
-
-module NodeIdSet (B : Base) = Set.Make(struct
-    type t = B.node_id
-    let compare = B.node_id_compare
-  end)

infer/src/checkers/procCfg.mli

@@ -0,0 +1,50 @@
+(*
+ * 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.
+ *)
+
+module type Base = sig
+  type t
+  type node
+
+  val node_id : node -> Cfg.Node.id
+  val node_id_compare : Cfg.Node.id -> Cfg.Node.id -> int
+  (** all successors (normal and exceptional) *)
+  val succs : t -> node -> node list
+  (** all predecessors (normal and exceptional) *)
+  val preds : t -> node -> node list
+end
+
+(** Wrapper that allows us to do tricks like turn a forward cfg to into a backward one *)
+module type Wrapper = sig
+  include Base
+
+  (** non-exceptional successors *)
+  val normal_succs : t -> node -> node list
+  (** non-exceptional predecessors *)
+  val normal_preds : t -> node -> node list
+  (** exceptional successors *)
+  val exceptional_succs : t -> node -> node list
+  (** exceptional predescessors *)
+  val exceptional_preds : t -> node -> node list
+  val start_node : t -> node
+  val exit_node : t -> node
+  val instrs : node -> Sil.instr list
+  val kind : node -> Cfg.Node.nodekind
+  val proc_desc : t -> Cfg.Procdesc.t
+  val nodes : t -> node list
+
+  val from_pdesc : Cfg.Procdesc.t -> t
+
+  val pp_node : Format.formatter -> node -> unit
+end
+
+module Normal : Wrapper with type node = Cfg.Node.t
+
+module Exceptional : Wrapper with type node = Cfg.Node.t
+
+module Backward : functor (W : Wrapper) -> Wrapper with type node = W.node

infer/src/checkers/scheduler.ml

@@ -19,7 +19,7 @@ module type S = functor (C : ProcCfg.Base) -> sig
   val schedule_succs : t -> C.node -> t
   (* remove and return the node with the highest priority, the ids of its visited
      predecessors, and the new schedule *)
-  val pop : t -> (C.node * C.node_id list * t) option
+  val pop : t -> (C.node * Cfg.Node.id list * t) option
   val empty : C.t -> t
 
 end
@@ -27,10 +27,10 @@ end
 (* simple scheduler that visits CFG nodes in reverse postorder. fast/precise for straightline code
    and conditionals; not as good for loops (may visit nodes after a loop multiple times). *)
 module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct
-  module M = ProcCfg.NodeIdMap (C)
+  module M = Cfg.IdMap
 
   module WorkUnit = struct
-    module IdSet = ProcCfg.NodeIdSet(C)
+    module IdSet = Cfg.IdSet
 
     type t = {
       node : C.node; (* node whose instructions will be analyzed *)

infer/src/unit/analyzerTester.ml

@@ -141,7 +141,7 @@ module Make
   open StructuredSil
 
   module I = AbstractInterpreter.Make (C) (S) (A) (T)
-  module M = ProcCfg.NodeIdMap (C)
+  module M = Cfg.IdMap
 
   type assert_map = string M.t
 

infer/src/unit/schedulerTests.ml

@@ -15,23 +15,24 @@ module F = Format
 (* mock for creating CFG's from adjacency lists *)
 module MockProcCfg = struct
   type node = int
-  type node_id = int
   type t = (node * node list) list
 
-  let node_id_compare = int_compare
+  let node_id_compare = Cfg.Node.id_compare
 
-  let node_id n = n
+  let node_id n = Cfg.Node.id_of_int__FOR_TESTING_ONLY n
 
   let succs t n =
     try
-      IList.find (fun (node, _) -> node_id_compare node n = 0) t
+      let id = node_id n in
+      IList.find (fun (node, _) -> node_id_compare (node_id node) id = 0) t
       |> snd
     with Not_found -> []
 
   let preds t n =
     try
+      let id = node_id n in
       IList.filter
-        (fun (_, succs) -> IList.exists (fun node -> node_id_compare node n = 0) succs) t
+        (fun (_, succs) -> IList.exists (fun node -> node_id_compare (node_id node) id = 0) succs) t
       |> IList.map fst
     with Not_found -> []