Allowing custom procCfg node types

Reviewed By: jberdine

Differential Revision: D3261163

fb-gh-sync-id: 6971a69
fbshipit-source-id: 6971a69

infer/src/IR/cfg.ml

@@ -145,9 +145,6 @@ module Node = struct
       with Not_found -> () in
     Procname.Hash.iter mark_pdesc_if_unchanged new_procs
 
-
-  let id_of_int__FOR_TESTING_ONLY i = i
-
   let node_id_gen cfg =
     incr cfg.node_id;
     !(cfg.node_id)
@@ -228,11 +225,6 @@ 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
@@ -837,9 +829,6 @@ 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
 

infer/src/IR/cfg.mli

@@ -199,9 +199,6 @@ 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
 
@@ -291,9 +288,6 @@ 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

@@ -15,10 +15,10 @@ module Make
     (C : ProcCfg.Wrapper)
     (Sched : Scheduler.S)
     (A : AbstractDomain.S)
-    (T : TransferFunctions.S with type astate = A.astate) = struct
+    (T : TransferFunctions.S with type astate = A.astate and type node_id = C.node_id) = struct
 
   module S = Sched (C)
-  module M = Cfg.IdMap
+  module M = ProcCfg.NodeIdMap (C)
 
   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" Cfg.Node.pp_id node_id;
+      L.err "Warning: No state found for node %a" C.pp_id node_id;
       None
 
   (** extract the postcondition of node [n] from [inv_map] *)
@@ -45,8 +45,8 @@ module Make
     | None -> None
 
   let exec_node node astate_pre work_queue inv_map proc_data =
-    let node_id = C.node_id node in
+    let node_id = C.id node in
-    L.out "Doing analysis of node %a from pre %a@." Cfg.Node.pp_id node_id A.pp astate_pre;
+    L.out "Doing analysis of node %a from pre %a@." C.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 =
@@ -55,7 +55,7 @@ module Make
           else T.exec_instr astate_acc proc_data instr in
         let astate_post_instrs = IList.fold_left exec_instrs astate_pre (C.instrs node) in
         T.postprocess astate_post_instrs node_id proc_data in
-      L.out "Post for node %a is %a@." Cfg.Node.pp_id node_id A.pp astate_post;
+      L.out "Post for node %a is %a@." C.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
@@ -82,10 +82,10 @@ module Make
   let rec exec_worklist cfg work_queue inv_map proc_data =
     let compute_pre node inv_map =
       (* if the [pred] -> [node] transition was normal, use post([pred]) *)
-      let extract_post_ pred = extract_post (C.node_id pred) inv_map in
+      let extract_post_ pred = extract_post (C.id pred) inv_map in
       let normal_posts = IList.map extract_post_ (C.normal_preds cfg node) in
       (* if the [pred] -> [node] transition was exceptional, use pre([pred]) *)
-      let extract_pre_f acc pred = extract_pre (C.node_id pred) inv_map :: acc in
+      let extract_pre_f acc pred = extract_pre (C.id pred) inv_map :: acc in
       let all_posts = IList.fold_left extract_pre_f normal_posts (C.exceptional_preds cfg node) in
       match IList.flatten_options all_posts with
       | post :: posts -> Some (IList.fold_left A.join post posts)
@@ -116,7 +116,7 @@ module Make
   let compute_post ({ ProcData.pdesc; } as proc_data) =
     let cfg = C.from_pdesc pdesc in
     let inv_map = exec_cfg cfg proc_data in
-    extract_post (C.node_id (C.exit_node cfg)) inv_map
+    extract_post (C.id (C.exit_node cfg)) inv_map
 
   module Interprocedural (Summ : Summary.S with type summary = A.astate) = struct
 

infer/src/checkers/addressTaken.ml

@@ -20,6 +20,7 @@ module Domain = AbstractDomain.FiniteSet(PvarSet)
 module TransferFunctions = struct
   type astate = Domain.astate
   type extras = ProcData.no_extras
+  type node_id = Cfg.Node.id
 
   let postprocess = TransferFunctions.no_postprocessing
 

infer/src/checkers/annotationReachability.ml

@@ -304,6 +304,7 @@ let report_allocations pname loc calls =
 module TransferFunctions = struct
   type astate = Domain.astate
   type extras = ProcData.no_extras
+  type node_id = Cfg.Node.id
 
   let postprocess = TransferFunctions.no_postprocessing
 

infer/src/checkers/copyPropagation.ml

@@ -82,6 +82,7 @@ end
 module TransferFunctions = struct
   type astate = Domain.astate
   type extras = ProcData.no_extras
+  type node_id = Cfg.Node.id
 
   let postprocess = TransferFunctions.no_postprocessing
 

infer/src/checkers/liveness.ml

@@ -21,6 +21,7 @@ module Domain = AbstractDomain.FiniteSet(Var.Set)
 module TransferFunctions = struct
   type astate = Domain.astate
   type extras = ProcData.no_extras
+  type node_id = Cfg.Node.id
 
   let postprocess = TransferFunctions.no_postprocessing
 

infer/src/checkers/procCfg.ml

@@ -17,9 +17,10 @@ module F = Format
 module type Base = sig
   type t
   type node
+  type node_id
 
-  val node_id : node -> Cfg.Node.id
+  val id : node -> node_id
-  val node_id_compare : Cfg.Node.id -> Cfg.Node.id -> int
+  val id_compare : node_id -> node_id -> int
   (** all successors (normal and exceptional) *)
   val succs : t -> node -> node list
   (** all predecessors (normal and exceptional) *)
@@ -48,14 +49,16 @@ module type Wrapper = sig
   val from_pdesc : Cfg.Procdesc.t -> t
 
   val pp_node : F.formatter -> node -> unit
+  val pp_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 id = Cfg.Node.get_id
   let normal_succs _ n = Cfg.Node.get_succs n
   let normal_preds _ n = Cfg.Node.get_preds n
   (* prune away exceptional control flow *)
@@ -72,21 +75,17 @@ module Normal = struct
 
   let from_pdesc pdesc = pdesc
 
-  let node_id_compare = Cfg.Node.id_compare
+  let id_compare = Cfg.Node.id_compare
 
   let pp_node = Cfg.Node.pp
+  let pp_id = Cfg.Node.pp_id
 end
 
 (** Forward CFG with exceptional control-flow *)
-module Exceptional : Wrapper with type node = Cfg.node = struct
+module Exceptional = struct
-
+  type node_id = Cfg.Node.id
-  module NodeIdMap = Map.Make(struct
-      type t = Cfg.Node.id
-      let compare = Cfg.Node.id_compare
-    end)
-
   type node = Cfg.node
-  type id_node_map = node list NodeIdMap.t
+  type id_node_map = node list Cfg.IdMap.t
   type t = Cfg.Procdesc.t * id_node_map
 
   let from_pdesc pdesc =
@@ -95,16 +94,16 @@ module Exceptional : Wrapper with type node = Cfg.node = struct
       let add_exn_pred exn_preds_acc exn_succ_node =
         let exn_succ_node_id = Cfg.Node.get_id exn_succ_node in
         let existing_exn_preds =
-          try NodeIdMap.find exn_succ_node_id exn_preds_acc
+          try Cfg.IdMap.find exn_succ_node_id exn_preds_acc
           with Not_found -> [] in
         if not (IList.mem Cfg.Node.equal n existing_exn_preds)
         then (* don't add duplicates *)
-          NodeIdMap.add exn_succ_node_id (n :: existing_exn_preds) exn_preds_acc
+          Cfg.IdMap.add exn_succ_node_id (n :: existing_exn_preds) exn_preds_acc
         else
           exn_preds_acc in
       IList.fold_left add_exn_pred exn_preds_acc (Cfg.Node.get_exn n) in
     let exceptional_preds =
-      IList.fold_left add_exn_preds NodeIdMap.empty (Cfg.Procdesc.get_nodes pdesc) in
+      IList.fold_left add_exn_preds Cfg.IdMap.empty (Cfg.Procdesc.get_nodes pdesc) in
     pdesc, exceptional_preds
 
   let nodes (t, _) = Cfg.Procdesc.get_nodes t
@@ -116,7 +115,7 @@ module Exceptional : Wrapper with type node = Cfg.node = struct
   let exceptional_succs _ n = Cfg.Node.get_exn n
 
   let exceptional_preds (_, exn_pred_map) n =
-    try NodeIdMap.find (Cfg.Node.get_id n) exn_pred_map
+    try Cfg.IdMap.find (Cfg.Node.get_id n) exn_pred_map
     with Not_found -> []
 
   (** get all normal and exceptional successors of [n]. *)
@@ -145,13 +144,13 @@ module Exceptional : Wrapper with type node = Cfg.node = struct
   let start_node (pdesc, _) = Cfg.Procdesc.get_start_node pdesc
   let exit_node (pdesc, _) = Cfg.Procdesc.get_exit_node pdesc
   let instrs = Cfg.Node.get_instrs
-  let node_id = Cfg.Node.get_id
+  let id = Cfg.Node.get_id
-  let node_id_compare = Cfg.Node.id_compare
+  let id_compare = Cfg.Node.id_compare
   let pp_node = Cfg.Node.pp
+  let pp_id = Cfg.Node.pp_id
   let kind = Cfg.Node.get_kind
 end
 
-(** Turn a forward CFG into a backward cfg *)
 module Backward (W : Wrapper) = struct
   include W
 
@@ -165,3 +164,13 @@ 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.id_compare
+  end)
+
+module NodeIdSet (B : Base) = Set.Make(struct
+    type t = B.node_id
+    let compare = B.id_compare
+  end)

infer/src/checkers/procCfg.mli

@@ -10,9 +10,10 @@
 module type Base = sig
   type t
   type node
+  type node_id
 
-  val node_id : node -> Cfg.Node.id
+  val id : node -> node_id
-  val node_id_compare : Cfg.Node.id -> Cfg.Node.id -> int
+  val id_compare : node_id -> node_id -> int
   (** all successors (normal and exceptional) *)
   val succs : t -> node -> node list
   (** all predecessors (normal and exceptional) *)
@@ -41,10 +42,16 @@ module type Wrapper = sig
   val from_pdesc : Cfg.Procdesc.t -> t
 
   val pp_node : Format.formatter -> node -> unit
+  val pp_id : Format.formatter -> node_id -> unit
 end
 
-module Normal : Wrapper with type node = Cfg.Node.t
+module Normal : Wrapper with type node = Cfg.Node.t and type node_id = Cfg.Node.id
 
-module Exceptional : Wrapper with type node = Cfg.Node.t
+module Exceptional : Wrapper with type node = Cfg.Node.t and type node_id = Cfg.Node.id
+
+module Backward (W : Wrapper) : Wrapper with type node = W.node and type node_id = W.node_id
+
+module NodeIdMap (B : Base) : Map.S with type key = B.node_id
+
+module NodeIdSet (B : Base) : Set.S with type elt = B.node_id
 
-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 * Cfg.Node.id list * t) option
+  val pop : t -> (C.node * C.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 = Cfg.IdMap
+  module M = ProcCfg.NodeIdMap (C)
 
   module WorkUnit = struct
-    module IdSet = Cfg.IdSet
+    module IdSet = ProcCfg.NodeIdSet (C)
 
     type t = {
       node : C.node; (* node whose instructions will be analyzed *)
@@ -63,10 +63,10 @@ module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct
 
   (* schedule the succs of [node] for analysis *)
   let schedule_succs t node =
-    let node_id = C.node_id node in
+    let node_id = C.id node in
     (* mark [node] as a visited pred of [node_to_schedule] and schedule it *)
     let schedule_succ worklist_acc node_to_schedule =
-      let id_to_schedule = C.node_id node_to_schedule in
+      let id_to_schedule = C.id node_to_schedule in
       let old_work =
         try M.find id_to_schedule worklist_acc
         with Not_found -> WorkUnit.make t.cfg node_to_schedule in
@@ -94,7 +94,7 @@ module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct
           (init_id, init_priority) in
       let max_priority_work = M.find max_priority_id t.worklist in
       let node = WorkUnit.node max_priority_work in
-      let t' = { t with worklist = M.remove (C.node_id node) t.worklist } in
+      let t' = { t with worklist = M.remove (C.id node) t.worklist } in
       Some (node, WorkUnit.visited_preds max_priority_work, t')
     with Not_found -> None
 

infer/src/checkers/transferFunctions.ml

@@ -12,12 +12,13 @@ open! Utils
 module type S = sig
   type astate (* abstract state to propagate *)
   type extras (* read-only extra state (results of previous analyses, globals, etc.) *)
+  type node_id
 
   (* {A} instr {A'}. [caller_pdesc] is the procdesc of the current procedure *)
   val exec_instr : astate -> extras ProcData.t -> Sil.instr -> astate
 
   (* optional postprocessing step to be performed after executing node [id]. *)
-  val postprocess : astate -> Cfg.Node.id -> extras ProcData.t -> astate
+  val postprocess : astate -> node_id -> extras ProcData.t -> astate
 end
 
 (* default postprocessing: do nothing *)

infer/src/unit/abstractInterpreterTests.ml

@@ -51,6 +51,7 @@ end
 module PathCountTransferFunctions = struct
   type astate = PathCountDomain.astate
   type extras = ProcData.no_extras
+  type node_id = Cfg.Node.id
 
   let postprocess = TransferFunctions.no_postprocessing
 

infer/src/unit/analyzerTester.ml

@@ -133,16 +133,17 @@ module StructuredSil = struct
 end
 
 module Make
-    (C : ProcCfg.Wrapper with type node = Cfg.Node.t)
+    (C : ProcCfg.Wrapper with type node = Cfg.Node.t and type node_id = Cfg.Node.id)
     (S : Scheduler.S)
     (A : AbstractDomain.S)
     (T : TransferFunctions.S
-     with type astate = A.astate and type extras = ProcData.no_extras) = struct
+     with type astate = A.astate and type extras = ProcData.no_extras
+                                 and type node_id = C.node_id) = struct
 
   open StructuredSil
 
   module I = AbstractInterpreter.Make (C) (S) (A) (T)
-  module M = Cfg.IdMap
+  module M = ProcCfg.NodeIdMap (C)
 
   type assert_map = string M.t
 
@@ -208,7 +209,7 @@ module Make
           let node = create_node (Cfg.Node.Stmt_node "Invariant") [] in
           set_succs last_node [node] ~exn_handlers;
           (* add the assertion to be checked after analysis converges *)
-          node, M.add (C.node_id node) (inv_str, inv_label) assert_map
+          node, M.add (C.id node) (inv_str, inv_label) assert_map
     and structured_instrs_to_node last_node assert_map exn_handlers instrs =
       IList.fold_left
         (fun acc instr -> structured_instr_to_node acc exn_handlers instr)

infer/src/unit/livenessTests.ml

@@ -12,7 +12,7 @@ open! Utils
 module F = Format
 
 module TestInterpreter = AnalyzerTester.Make
-    (ProcCfg.Backward (ProcCfg.Exceptional))
+    (ProcCfg.Backward(ProcCfg.Normal))
     (Scheduler.ReversePostorder)
     (Liveness.Domain)
     (Liveness.TransferFunctions)

infer/src/unit/schedulerTests.ml

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