ProcCfg: do not include module Node

Summary:
Having the `Node` module including in the `CFG` one is confusing.
Let's keep it separate.

Reviewed By: ngorogiannis

Differential Revision: D8185754

fbshipit-source-id: 62077e6

infer/src/absint/AbstractInterpreter.ml

@@ -13,7 +13,7 @@ type 'a state = {pre: 'a; post: 'a; visit_count: int}
 module type S = sig
   module TransferFunctions : TransferFunctions.SIL
 
-  module InvariantMap : Caml.Map.S with type key = TransferFunctions.CFG.id
+  module InvariantMap = TransferFunctions.CFG.Node.IdMap
 
   type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t
 
@@ -40,8 +40,9 @@ module MakeNoCFG
     (TransferFunctions : TransferFunctions.SIL with module CFG = Scheduler.CFG) =
 struct
   module CFG = Scheduler.CFG
-  module InvariantMap = CFG.IdMap
+  module Node = CFG.Node
   module TransferFunctions = TransferFunctions
+  module InvariantMap = TransferFunctions.CFG.Node.IdMap
   module Domain = TransferFunctions.Domain
 
   type invariant_map = Domain.astate state InvariantMap.t
@@ -60,7 +61,7 @@ struct
 
 
   let exec_node node astate_pre work_queue inv_map ({ProcData.pdesc} as proc_data) ~debug =
-    let node_id = CFG.id node in
+    let node_id = Node.id node in
     let update_inv_map pre ~visit_count =
       let compute_post pre instr = TransferFunctions.exec_instr pre proc_data node instr in
       (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *)
@@ -71,14 +72,14 @@ struct
       if debug then
         NodePrinter.start_session
           ~pp_name:(TransferFunctions.pp_session_name node)
-          (CFG.underlying_node node) ;
+          (Node.underlying_node node) ;
       let astate_post = Instrs.fold ~f:compute_post ~init:pre instrs in
       if debug then (
         L.d_strln
           (Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@." Domain.pp pre
              (Instrs.pp Pp.(html Green))
              instrs Domain.pp astate_post) ;
-        NodePrinter.finish_session (CFG.underlying_node node) ) ;
+        NodePrinter.finish_session (Node.underlying_node node) ) ;
       let inv_map' = InvariantMap.add node_id {pre; post= astate_post; visit_count} inv_map in
       (inv_map', Scheduler.schedule_succs work_queue node)
     in
@@ -104,7 +105,7 @@ struct
 
   let rec exec_worklist cfg work_queue inv_map proc_data ~debug =
     let compute_pre node inv_map =
-      let extract_post_ pred = extract_post (CFG.id pred) inv_map in
+      let extract_post_ pred = extract_post (Node.id pred) inv_map in
       CFG.fold_preds cfg node ~init:None ~f:(fun joined_post_opt pred ->
           match extract_post_ pred with
           | None ->
@@ -150,7 +151,7 @@ struct
   let compute_post ?(debug= Config.write_html) ({ProcData.pdesc} as proc_data) ~initial =
     let cfg = CFG.from_pdesc pdesc in
     let inv_map = exec_cfg cfg proc_data ~initial ~debug in
-    extract_post (CFG.id (CFG.exit_node cfg)) inv_map
+    extract_post (Node.id (CFG.exit_node cfg)) inv_map
 end
 
 module MakeWithScheduler (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.MakeSIL) =

infer/src/absint/AbstractInterpreter.mli

@@ -13,7 +13,7 @@ type 'a state = {pre: 'a; post: 'a; visit_count: int}
 module type S = sig
   module TransferFunctions : TransferFunctions.SIL
 
-  module InvariantMap : Caml.Map.S with type key = TransferFunctions.CFG.id
+  module InvariantMap = TransferFunctions.CFG.Node.IdMap
 
   (** invariant map from node id -> state representing postcondition for node id *)
   type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t
@@ -48,9 +48,9 @@ end
 module MakeNoCFG
     (Scheduler : Scheduler.S)
     (TransferFunctions : TransferFunctions.SIL with module CFG = Scheduler.CFG) :
-  S with module TransferFunctions = TransferFunctions and module InvariantMap = Scheduler.CFG.IdMap
+  S with module TransferFunctions = TransferFunctions
 
 (** create an intraprocedural abstract interpreter from a CFG and functors for creating a scheduler/
     transfer functions from a CFG *)
 module Make (CFG : ProcCfg.S) (MakeTransferFunctions : TransferFunctions.MakeSIL) :
-  S with module TransferFunctions = MakeTransferFunctions(CFG) and module InvariantMap = CFG.IdMap
+  S with module TransferFunctions = MakeTransferFunctions(CFG)

infer/src/absint/LowerHil.ml

@@ -31,7 +31,7 @@ struct
 
   let pp_pre_post pre post hil_instr node =
     if Config.write_html then (
-      let underyling_node = CFG.underlying_node node in
+      let underyling_node = CFG.Node.underlying_node node in
       NodePrinter.start_session ~pp_name:(pp_session_name node) underyling_node ;
       L.d_strln
         (Format.asprintf "PRE: %a@.INSTR: %a@.POST: %a@." TransferFunctions.Domain.pp pre

infer/src/absint/LowerHil.mli

@@ -28,9 +28,9 @@ module Make
 
   type extras = TransferFunctions.extras
 
-  val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate
+  val exec_instr : Domain.astate -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Domain.astate
 
-  val pp_session_name : CFG.node -> Format.formatter -> unit
+  val pp_session_name : CFG.Node.t -> Format.formatter -> unit
 end
 
 (** Wrapper around Interpreter to prevent clients from having to deal with IdAccessPathMapDomain *)

infer/src/absint/ProcCfg.ml

@@ -38,7 +38,7 @@ module type Node = sig
   module IdSet : PrettyPrintable.PPSet with type elt = id
 end
 
-module DefaultNode = struct
+module DefaultNode : Node with type t = Procdesc.Node.t and type id = Procdesc.Node.id = struct
   type t = Procdesc.Node.t
 
   type id = Procdesc.Node.id
@@ -71,7 +71,13 @@ module DefaultNode = struct
   module IdSet = PrettyPrintable.MakePPSet (OrderedId)
 end
 
-module InstrNode = struct
+module InstrNode : sig
+  type instr_index = int
+
+  include Node
+          with type t = Procdesc.Node.t * instr_index
+           and type id = Procdesc.Node.id * instr_index
+end = struct
   type instr_index = int [@@deriving compare]
 
   type t = Procdesc.Node.t * instr_index
@@ -107,50 +113,46 @@ end
 module type S = sig
   type t
 
-  type node
+  module Node : Node
-
-  include Node with type t := node
 
-  val instrs : node -> Instrs.t
+  val instrs : Node.t -> Instrs.t
   (** get the instructions from a node *)
 
-  val fold_succs : t -> (node, node, 'accum) Container.fold
+  val fold_succs : t -> (Node.t, Node.t, 'accum) Container.fold
 
-  val fold_preds : t -> (node, node, 'accum) Container.fold
+  val fold_preds : t -> (Node.t, Node.t, 'accum) Container.fold
   (** fold over all predecessors (normal and exceptional) *)
 
-  val fold_normal_succs : t -> (node, node, 'accum) Container.fold
+  val fold_normal_succs : t -> (Node.t, Node.t, 'accum) Container.fold
   (** fold over non-exceptional successors *)
 
-  val fold_normal_preds : t -> (node, node, 'accum) Container.fold
+  val fold_normal_preds : t -> (Node.t, Node.t, 'accum) Container.fold
   (** fold over non-exceptional predecessors *)
 
-  val fold_exceptional_succs : t -> (node, node, 'accum) Container.fold
+  val fold_exceptional_succs : t -> (Node.t, Node.t, 'accum) Container.fold
   (** fold over exceptional successors *)
 
-  val fold_exceptional_preds : t -> (node, node, 'accum) Container.fold
+  val fold_exceptional_preds : t -> (Node.t, Node.t, 'accum) Container.fold
   (** fold over exceptional predecessors *)
 
-  val start_node : t -> node
+  val start_node : t -> Node.t
 
-  val exit_node : t -> node
+  val exit_node : t -> Node.t
 
   val proc_desc : t -> Procdesc.t
 
-  val fold_nodes : (t, node, 'accum) Container.fold
+  val fold_nodes : (t, Node.t, 'accum) Container.fold
 
   val from_pdesc : Procdesc.t -> t
 
-  val is_loop_head : Procdesc.t -> node -> bool
+  val is_loop_head : Procdesc.t -> Node.t -> bool
 end
 
 (** Forward CFG with no exceptional control-flow *)
 module Normal = struct
   type t = Procdesc.t
 
-  type node = DefaultNode.t
+  module Node = DefaultNode
-
-  include (DefaultNode : module type of DefaultNode with type t := node)
 
   let instrs = Procdesc.Node.get_instrs
 
@@ -182,14 +184,12 @@ end
 
 (** Forward CFG with exceptional control-flow *)
 module Exceptional = struct
-  type node = DefaultNode.t
+  module Node = DefaultNode
 
-  type id_node_map = node list Procdesc.IdMap.t
+  type id_node_map = Node.t list Procdesc.IdMap.t
 
   type t = Procdesc.t * id_node_map
 
-  include (DefaultNode : module type of DefaultNode with type t := node)
-
   let fold_exceptional_succs _ n ~init ~f = n |> Procdesc.Node.get_exn |> List.fold ~init ~f
 
   let from_pdesc pdesc =
@@ -234,11 +234,12 @@ module Exceptional = struct
     let acc_normal = fold_normal_alpha t n ~init ~f in
     let normal_set =
       lazy
-        (fold_normal_idset t n ~init:IdSet.empty ~f:(fun set node ->
+        (fold_normal_idset t n ~init:Node.IdSet.empty ~f:(fun set node ->
-             IdSet.add (Procdesc.Node.get_id node) set ))
+             Node.IdSet.add (Procdesc.Node.get_id node) set ))
     in
     let f acc node =
-      if IdSet.mem (Procdesc.Node.get_id node) (Lazy.force_val normal_set) then acc else f acc node
+      if Node.IdSet.mem (Procdesc.Node.get_id node) (Lazy.force_val normal_set) then acc
+      else f acc node
     in
     fold_exceptional t n ~init:acc_normal ~f
 
@@ -285,21 +286,12 @@ module Backward (Base : S) = struct
   let fold_exceptional_preds = Base.fold_exceptional_succs
 end
 
-module OneInstrPerNode (Base : S with type node = Procdesc.Node.t and type id = Procdesc.Node.id) =
+module OneInstrPerNode (Base : S with module Node = DefaultNode) :
+  S with type t = Base.t and module Node = InstrNode =
 struct
   type t = Base.t
 
-  type node = InstrNode.t
+  module Node = InstrNode
-
-  type id = InstrNode.id
-
-  include (
-    InstrNode :
-      Node
-      with type t := node
-       and type id := id
-       and module IdMap = InstrNode.IdMap
-       and module IdSet = InstrNode.IdSet )
 
   let instrs (node, index) =
     let instrs = Base.instrs node in

infer/src/absint/ProcCfg.mli

@@ -40,42 +40,40 @@ end
 module type S = sig
   type t
 
-  type node
+  module Node : Node
 
-  include Node with type t := node
+  val instrs : Node.t -> Instrs.t
-
-  val instrs : node -> Instrs.t
   (** get the instructions from a node *)
 
-  val fold_succs : t -> (node, node, 'accum) Container.fold
+  val fold_succs : t -> (Node.t, Node.t, 'accum) Container.fold
   (** fold over all successors (normal and exceptional) *)
 
-  val fold_preds : t -> (node, node, 'accum) Container.fold
+  val fold_preds : t -> (Node.t, Node.t, 'accum) Container.fold
   (** fold over all predecessors (normal and exceptional) *)
 
-  val fold_normal_succs : t -> (node, node, 'accum) Container.fold
+  val fold_normal_succs : t -> (Node.t, Node.t, 'accum) Container.fold
   (** fold over non-exceptional successors *)
 
-  val fold_normal_preds : t -> (node, node, 'accum) Container.fold
+  val fold_normal_preds : t -> (Node.t, Node.t, 'accum) Container.fold
   (** fold over non-exceptional predecessors *)
 
-  val fold_exceptional_succs : t -> (node, node, 'accum) Container.fold
+  val fold_exceptional_succs : t -> (Node.t, Node.t, 'accum) Container.fold
   (** fold over exceptional successors *)
 
-  val fold_exceptional_preds : t -> (node, node, 'accum) Container.fold
+  val fold_exceptional_preds : t -> (Node.t, Node.t, 'accum) Container.fold
   (** fold over exceptional predescessors *)
 
-  val start_node : t -> node
+  val start_node : t -> Node.t
 
-  val exit_node : t -> node
+  val exit_node : t -> Node.t
 
   val proc_desc : t -> Procdesc.t
 
-  val fold_nodes : (t, node, 'accum) Container.fold
+  val fold_nodes : (t, Node.t, 'accum) Container.fold
 
   val from_pdesc : Procdesc.t -> t
 
-  val is_loop_head : Procdesc.t -> node -> bool
+  val is_loop_head : Procdesc.t -> Node.t -> bool
 end
 
 module DefaultNode : Node with type t = Procdesc.Node.t and type id = Procdesc.Node.id
@@ -89,25 +87,16 @@ module InstrNode : sig
 end
 
 (** Forward CFG with no exceptional control-flow *)
-module Normal :
+module Normal : S with type t = Procdesc.t and module Node = DefaultNode
-  S with type t = Procdesc.t and type node = DefaultNode.t and type id = DefaultNode.id
 
 (** Forward CFG with exceptional control-flow *)
 module Exceptional :
-  S
+  S with type t = Procdesc.t * DefaultNode.t list Procdesc.IdMap.t and module Node = DefaultNode
-  with type t = Procdesc.t * DefaultNode.t list Procdesc.IdMap.t
-   and type node = DefaultNode.t
-   and type id = DefaultNode.id
 
 (** Wrapper that reverses the direction of the CFG *)
-module Backward (Base : S) : S with type t = Base.t and type node = Base.node and type id = Base.id
+module Backward (Base : S) : S with type t = Base.t and module Node = Base.Node
-
+
-module OneInstrPerNode (Base : S with type node = DefaultNode.t and type id = DefaultNode.id) :
+module OneInstrPerNode (Base : S with module Node = DefaultNode) :
-  S
+  S with type t = Base.t and module Node = InstrNode
-  with type t = Base.t
-   and type node = InstrNode.t
-   and type id = InstrNode.id
-   and module IdMap = InstrNode.IdMap
-   and module IdSet = InstrNode.IdSet
 
 module NormalOneInstrPerNode : module type of OneInstrPerNode (Normal)

infer/src/absint/Scheduler.ml

@@ -12,10 +12,10 @@ module type S = sig
 
   type t
 
-  val schedule_succs : t -> CFG.node -> t
+  val schedule_succs : t -> CFG.Node.t -> t
   (** schedule the successors of [node] *)
 
-  val pop : t -> (CFG.node * CFG.id list * t) option
+  val pop : t -> (CFG.Node.t * CFG.Node.id list * t) option
   (** remove and return the node with the highest priority, the ids of its visited
       predecessors, and the new schedule *)
 
@@ -30,13 +30,13 @@ end
     and conditionals; not as good for loops (may visit nodes after a loop multiple times). *)
 module ReversePostorder (CFG : ProcCfg.S) = struct
   module CFG = CFG
-  module M = CFG.IdMap
+  module M = CFG.Node.IdMap
 
   module WorkUnit = struct
-    module IdSet = CFG.IdSet
+    module IdSet = CFG.Node.IdSet
 
     type t =
-      { node: CFG.node  (** node whose instructions will be analyzed *)
+      { node: CFG.Node.t  (** node whose instructions will be analyzed *)
       ; visited_preds: IdSet.t
             (** predecessors of [node] we have already visited in current iter *)
       ; priority: int  (** |preds| - |visited preds|. *) }
@@ -68,10 +68,10 @@ module ReversePostorder (CFG : ProcCfg.S) = struct
 
   (** schedule the succs of [node] for analysis *)
   let schedule_succs t node =
-    let node_id = CFG.id node in
+    let node_id = CFG.Node.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 = CFG.id node_to_schedule in
+      let id_to_schedule = CFG.Node.id node_to_schedule in
       let old_work =
         try M.find id_to_schedule worklist_acc with Caml.Not_found ->
           WorkUnit.make t.cfg node_to_schedule
@@ -100,7 +100,7 @@ module ReversePostorder (CFG : ProcCfg.S) = struct
       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 (CFG.id node) t.worklist} in
+      let t' = {t with worklist= M.remove (CFG.Node.id node) t.worklist} in
       Some (node, WorkUnit.visited_preds max_priority_work, t')
     with Caml.Not_found -> None
 

infer/src/absint/TransferFunctions.ml

@@ -16,9 +16,9 @@ module type S = sig
 
   type instr
 
-  val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> instr -> Domain.astate
+  val exec_instr : Domain.astate -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.astate
 
-  val pp_session_name : CFG.node -> Format.formatter -> unit
+  val pp_session_name : CFG.Node.t -> Format.formatter -> unit
 end
 
 module type SIL = sig

infer/src/absint/TransferFunctions.mli

@@ -22,10 +22,10 @@ module type S = sig
   (** type of the instructions the transfer functions operate on *)
   type instr
 
-  val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> instr -> Domain.astate
+  val exec_instr : Domain.astate -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.astate
   (** {A} instr {A'}. [node] is the node of the current instruction *)
 
-  val pp_session_name : CFG.node -> Format.formatter -> unit
+  val pp_session_name : CFG.Node.t -> Format.formatter -> unit
   (** print session name for HTML debug *)
 end
 

infer/src/backend/preanal.ml

@@ -54,7 +54,7 @@ module NullifyTransferFunctions = struct
   type extras = LivenessAnalysis.invariant_map
 
   let postprocess ((reaching_defs, _) as astate) node {ProcData.extras} =
-    let node_id = Procdesc.Node.get_id (CFG.underlying_node node) in
+    let node_id = Procdesc.Node.get_id (CFG.Node.underlying_node node) in
     match LivenessAnalysis.extract_state node_id extras with
     (* note: because the analysis is backward, post and pre are reversed *)
     | Some {AbstractInterpreter.post= live_before; pre= live_after} ->
@@ -137,7 +137,7 @@ let add_nullify_instrs pdesc tenv liveness_inv_map =
     if ids <> [] then Some (Sil.Remove_temps (List.rev ids, loc)) else None
   in
   Container.iter nullify_proc_cfg ~fold:ProcCfg.Exceptional.fold_nodes ~f:(fun node ->
-      match NullifyAnalysis.extract_post (ProcCfg.Exceptional.id node) nullify_inv_map with
+      match NullifyAnalysis.extract_post (ProcCfg.Exceptional.Node.id node) nullify_inv_map with
       | Some (_, to_nullify) ->
           let pvars_to_nullify, ids_to_remove =
             VarDomain.fold

infer/src/biabduction/SymExec.ml

@@ -1831,7 +1831,7 @@ and sym_exec_wrapper exe_env handle_exn tenv proc_cfg instr ((prop: Prop.normal
         Instrs.exists ~f:instr_is_abstraction (ProcCfg.Exceptional.instrs node)
       in
       let curr_node = State.get_node () in
-      match ProcCfg.Exceptional.kind curr_node with
+      match ProcCfg.Exceptional.Node.kind curr_node with
       | Procdesc.Node.Prune_node _ when not (node_has_abstraction curr_node) ->
           (* don't check for leaks in prune nodes, unless there is abstraction anyway,*)
           (* but force them into either branch *)
@@ -1873,14 +1873,14 @@ and sym_exec_wrapper exe_env handle_exn tenv proc_cfg instr ((prop: Prop.normal
 
 (** {2 Lifted Abstract Transfer Functions} *)
 
-let node handle_exn exe_env tenv proc_cfg (node: ProcCfg.Exceptional.node) (pset: Paths.PathSet.t)
+let node handle_exn exe_env tenv proc_cfg (node: ProcCfg.Exceptional.Node.t)
-    : Paths.PathSet.t =
+    (pset: Paths.PathSet.t) : Paths.PathSet.t =
   let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
   let exe_instr_prop instr p tr (pset1: Paths.PathSet.t) =
     let pset2 =
       if
         Tabulation.prop_is_exn pname p && not (Sil.instr_is_auxiliary instr)
-        && ProcCfg.Exceptional.kind node <> Procdesc.Node.exn_handler_kind
+        && ProcCfg.Exceptional.Node.kind node <> Procdesc.Node.exn_handler_kind
         (* skip normal instructions if an exception was thrown,
             unless this is an exception handler node *)
       then (

infer/src/biabduction/SymExec.mli

@@ -11,7 +11,7 @@ open! IStd
 (** Symbolic Execution *)
 
 val node :
-  (exn -> unit) -> Exe_env.t -> Tenv.t -> ProcCfg.Exceptional.t -> ProcCfg.Exceptional.node
+  (exn -> unit) -> Exe_env.t -> Tenv.t -> ProcCfg.Exceptional.t -> ProcCfg.Exceptional.Node.t
   -> Paths.PathSet.t -> Paths.PathSet.t
 (** Symbolic execution of the instructions of a node, lifted to sets of propositions. *)
 

infer/src/biabduction/interproc.ml

@@ -312,7 +312,7 @@ let propagate_nodes_divergence tenv (proc_cfg: ProcCfg.Exceptional.t) (pset: Pat
 (** Symbolic execution for a Join node *)
 let do_symexec_join proc_cfg tenv wl curr_node (edgeset_todo: Paths.PathSet.t) =
   let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
-  let curr_node_id = ProcCfg.Exceptional.id curr_node in
+  let curr_node_id = ProcCfg.Exceptional.Node.id curr_node in
   let new_dset = edgeset_todo in
   let old_dset = Join_table.find wl.Worklist.join_table curr_node_id in
   let old_dset', new_dset' = Dom.pathset_join pname tenv old_dset new_dset in
@@ -376,7 +376,7 @@ let instrs_get_normal_vars instrs =
 
 
 (** Perform symbolic execution for a node starting from an initial prop *)
-let do_symbolic_execution exe_env proc_cfg handle_exn tenv (node: ProcCfg.Exceptional.node)
+let do_symbolic_execution exe_env proc_cfg handle_exn tenv (node: ProcCfg.Exceptional.Node.t)
     (prop: Prop.normal Prop.t) (path: Paths.Path.t) =
   State.mark_execution_start node ;
   let instrs = ProcCfg.Exceptional.instrs node in
@@ -452,7 +452,7 @@ let forward_tabulate exe_env tenv proc_cfg wl =
     L.d_ln () ;
     L.d_ln ()
   in
-  let do_prop (curr_node: ProcCfg.Exceptional.node) handle_exn prop path cnt num_paths =
+  let do_prop (curr_node: ProcCfg.Exceptional.Node.t) handle_exn prop path cnt num_paths =
     L.d_strln ("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths) ;
     L.d_increase_indent 1 ;
     try
@@ -519,7 +519,7 @@ let remove_locals_formals_and_check tenv proc_cfg p =
   let pname = Procdesc.get_proc_name pdesc in
   let pvars, p' = PropUtil.remove_locals_formals tenv pdesc p in
   let check_pvar pvar =
-    let loc = ProcCfg.Exceptional.loc (ProcCfg.Exceptional.exit_node proc_cfg) in
+    let loc = ProcCfg.Exceptional.Node.loc (ProcCfg.Exceptional.exit_node proc_cfg) in
     let dexp_opt, _ = Errdesc.vpath_find tenv p (Exp.Lvar pvar) in
     let desc = Errdesc.explain_stack_variable_address_escape loc pvar dexp_opt in
     let exn = Exceptions.Stack_variable_address_escape (desc, __POS__) in
@@ -531,7 +531,7 @@ let remove_locals_formals_and_check tenv proc_cfg p =
 (** Collect the analysis results for the exit node. *)
 let collect_analysis_result tenv wl proc_cfg : Paths.PathSet.t =
   let exit_node = ProcCfg.Exceptional.exit_node proc_cfg in
-  let exit_node_id = ProcCfg.Exceptional.id exit_node in
+  let exit_node_id = ProcCfg.Exceptional.Node.id exit_node in
   let pathset = htable_retrieve wl.Worklist.path_set_visited exit_node_id in
   Paths.PathSet.map (remove_locals_formals_and_check tenv proc_cfg) pathset
 

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -209,7 +209,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     L.(debug BufferOverrun Verbose) "================================@\n@."
 
 
-  let exec_instr : Dom.Mem.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Dom.Mem.astate =
+  let exec_instr : Dom.Mem.astate -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.astate =
    fun mem {pdesc; tenv} node instr ->
     let pname = Procdesc.get_proc_name pdesc in
     let output_mem =
@@ -244,7 +244,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | Call (ret, Const (Cfun callee_pname), params, location, _) -> (
         match Models.Call.dispatch callee_pname params with
         | Some {Models.exec} ->
-            let node_hash = CFG.hash node in
+            let node_hash = CFG.Node.hash node in
             let model_env = Models.mk_model_env callee_pname node_hash location tenv ~ret in
             exec model_env mem
         | None ->
@@ -262,7 +262,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               |> Dom.Mem.add_heap Loc.unknown val_unknown )
       | Declare_locals (locals, location) ->
           (* array allocation in stack e.g., int arr[10] *)
-          let node_hash = CFG.hash node in
+          let node_hash = CFG.Node.hash node in
           let rec decl_local pname ~node_hash location loc typ ~inst_num ~dimension mem =
             match typ.Typ.desc with
             | Typ.Tarray {elt= typ; length; stride} ->
@@ -301,7 +301,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     output_mem
 
 
-  let pp_session_name node fmt = F.fprintf fmt "bufferoverrun %a" CFG.pp_id (CFG.id node)
+  let pp_session_name node fmt = F.fprintf fmt "bufferoverrun %a" CFG.Node.pp_id (CFG.Node.id node)
 end
 
 module CFG = ProcCfg.NormalOneInstrPerNode
@@ -331,14 +331,14 @@ module Report = struct
           false
   end
 
-  let check_unreachable_code summary tenv (cfg: CFG.t) (node: CFG.node) instr rem_instrs =
+  let check_unreachable_code summary tenv (cfg: CFG.t) (node: CFG.Node.t) instr rem_instrs =
     match instr with
     | Sil.Prune (_, _, _, (Ik_land_lor | Ik_bexp)) ->
         ()
     | Sil.Prune (cond, location, true_branch, _) ->
         let i = match cond with Exp.Const (Const.Cint i) -> i | _ -> IntLit.zero in
         let desc =
-          Errdesc.explain_condition_always_true_false tenv i cond (CFG.underlying_node node)
+          Errdesc.explain_condition_always_true_false tenv i cond (CFG.Node.underlying_node node)
             location
         in
         let exn = Exceptions.Condition_always_true_false (desc, not true_branch, __POS__) in
@@ -425,7 +425,7 @@ module Report = struct
 
 
   let check_instr
-      : Procdesc.t -> Tenv.t -> CFG.node -> Sil.instr -> Dom.Mem.astate -> PO.ConditionSet.t
+      : Procdesc.t -> Tenv.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.astate -> PO.ConditionSet.t
         -> PO.ConditionSet.t =
    fun pdesc tenv node instr mem cond_set ->
     let pname = Procdesc.get_proc_name pdesc in
@@ -435,7 +435,7 @@ module Report = struct
     | Sil.Call (_, Const (Cfun callee_pname), params, location, _) -> (
       match Models.Call.dispatch callee_pname params with
       | Some {Models.check} ->
-          let node_hash = CFG.hash node in
+          let node_hash = CFG.Node.hash node in
           check (Models.mk_model_env pname node_hash location tenv) mem cond_set
       | None ->
         match Payload.read pdesc callee_pname with
@@ -460,7 +460,7 @@ module Report = struct
 
 
   let check_instrs
-      : Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> CFG.node -> Instrs.t
+      : Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> CFG.Node.t -> Instrs.t
         -> Dom.Mem.astate AbstractInterpreter.state -> PO.ConditionSet.t -> PO.ConditionSet.t =
    fun summary pdesc tenv cfg node instrs state cond_set ->
     match state with
@@ -486,9 +486,9 @@ module Report = struct
 
   let check_node
       : Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t
-        -> CFG.node -> PO.ConditionSet.t =
+        -> CFG.Node.t -> PO.ConditionSet.t =
    fun summary pdesc tenv cfg inv_map cond_set node ->
-    match Analyzer.extract_state (CFG.id node) inv_map with
+    match Analyzer.extract_state (CFG.Node.id node) inv_map with
     | Some state ->
         let instrs = CFG.instrs node in
         check_instrs summary pdesc tenv cfg node instrs state cond_set
@@ -573,8 +573,8 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_
   let pdata = ProcData.make_default proc_desc tenv in
   let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in
   let cfg = CFG.from_pdesc proc_desc in
-  let entry_mem = extract_post (CFG.start_node cfg |> CFG.id) inv_map in
+  let entry_mem = extract_post (CFG.start_node cfg |> CFG.Node.id) inv_map in
-  let exit_mem = extract_post (CFG.exit_node cfg |> CFG.id) inv_map in
+  let exit_mem = extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map in
   let cond_set =
     Report.check_proc summary proc_desc tenv cfg inv_map |> Report.report_errors summary proc_desc
   in

infer/src/bufferoverrun/bufferOverrunChecker.mli

@@ -17,4 +17,4 @@ type invariant_map
 
 val compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t
 
-val extract_pre : CFG.id -> invariant_map -> BufferOverrunDomain.Mem.t option
+val extract_pre : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option

infer/src/checkers/SimpleChecker.ml

@@ -67,7 +67,7 @@ module Make (Spec : Spec) : S = struct
     type extras = ProcData.no_extras
 
     let exec_instr astate_set proc_data node instr =
-      let node_kind = CFG.kind node in
+      let node_kind = CFG.Node.kind node in
       let pname = Procdesc.get_proc_name proc_data.ProcData.pdesc in
       Domain.fold
         (fun astate acc ->
@@ -93,7 +93,7 @@ module Make (Spec : Spec) : S = struct
             nodes
         in
         Domain.iter
-          (fun astate -> Spec.report astate (ProcCfg.Exceptional.loc node) proc_name)
+          (fun astate -> Spec.report astate (ProcCfg.Exceptional.Node.loc node) proc_name)
           astate_set
     in
     let inv_map =

infer/src/checkers/control.ml

@@ -67,7 +67,7 @@ module TransferFunctionsDataDeps (CFG : ProcCfg.S) = struct
 
 
   let pp_session_name node fmt =
-    F.fprintf fmt "data dependency analysis %a" CFG.pp_id (CFG.id node)
+    F.fprintf fmt "data dependency analysis %a" CFG.Node.pp_id (CFG.Node.id node)
 end
 
 module ControlDepSet = VarSet
@@ -109,7 +109,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct
 
 
   let pp_session_name node fmt =
-    F.fprintf fmt "control dependency analysis %a" CFG.pp_id (CFG.id node)
+    F.fprintf fmt "control dependency analysis %a" CFG.Node.pp_id (CFG.Node.id node)
 end
 
 module CFG = ProcCfg.Normal
@@ -156,8 +156,7 @@ let gather_all_deps control_map data_map =
 
 
 let compute_all_deps data_invariant_map control_invariant_map node =
-  let und_node = CFG.underlying_node node in
+  let node_id = CFG.Node.id node in
-  let node_id = Procdesc.Node.get_id und_node in
   let deps = VarSet.empty in
   ControlDepAnalyzer.extract_post node_id control_invariant_map
   |> Option.map ~f:(fun control_deps ->

infer/src/checkers/cost.ml

@@ -67,8 +67,8 @@ module TransferFunctionsNodesBasicCost = struct
 
 
   let exec_instr_cost inferbo_mem (astate: CostDomain.NodeInstructionToCostMap.astate)
-      {ProcData.pdesc; tenv} (node: CFG.node) instr : CostDomain.NodeInstructionToCostMap.astate =
+      {ProcData.pdesc; tenv} (node: CFG.Node.t) instr : CostDomain.NodeInstructionToCostMap.astate =
-    let key = CFG.id node in
+    let key = CFG.Node.id node in
     let astate' =
       match instr with
       | Sil.Call (_, Exp.Const (Const.Cfun callee_pname), params, _, _) ->
@@ -95,12 +95,12 @@ module TransferFunctionsNodesBasicCost = struct
 
 
   let exec_instr costmap ({ProcData.extras= inferbo_invariant_map} as pdata) node instr =
-    let inferbo_mem = BufferOverrunChecker.extract_pre (CFG.id node) inferbo_invariant_map in
+    let inferbo_mem = BufferOverrunChecker.extract_pre (CFG.Node.id node) inferbo_invariant_map in
     let costmap = exec_instr_cost inferbo_mem costmap pdata node instr in
     costmap
 
 
-  let pp_session_name node fmt = F.fprintf fmt "cost(basic) %a" CFG.pp_id (CFG.id node)
+  let pp_session_name node fmt = F.fprintf fmt "cost(basic) %a" CFG.Node.pp_id (CFG.Node.id node)
 end
 
 module AnalyzerNodesBasicCost =
@@ -149,13 +149,13 @@ module BoundMap = struct
       Procdesc.get_formals node_cfg |> List.map ~f:(fun (m, _) -> Pvar.mk m pname)
     in
     let compute_node_upper_bound bound_map node =
-      let node_id = NodeCFG.id node in
+      let node_id = NodeCFG.Node.id node in
       match Procdesc.Node.get_kind node with
       | Procdesc.Node.Exit_node _ ->
           Node.IdMap.add node_id BasicCost.one bound_map
       | _ ->
           let entry_state_opt =
-            let instr_node_id = InstrCFG.of_underlying_node node |> InstrCFG.id in
+            let instr_node_id = InstrCFG.Node.of_underlying_node node |> InstrCFG.Node.id in
             BufferOverrunChecker.extract_pre instr_node_id inferbo_invariant_map
           in
           match entry_state_opt with
@@ -251,17 +251,17 @@ module StructuralConstraints = struct
         | [] ->
             {single= []; sum= []}
         | [single] ->
-            {single= [NodeCFG.id single]; sum= []}
+            {single= [NodeCFG.Node.id single]; sum= []}
         | nodes ->
             let sum =
               List.fold nodes ~init:Node.IdSet.empty ~f:(fun idset node ->
-                  Node.IdSet.add (NodeCFG.id node) idset )
+                  Node.IdSet.add (NodeCFG.Node.id node) idset )
             in
             {single= []; sum= [sum]}
       in
       let preds = constraints_add node Procdesc.Node.get_preds in
       let succs = constraints_add node Procdesc.Node.get_succs in
-      Node.IdMap.add (NodeCFG.id node)
+      Node.IdMap.add (NodeCFG.Node.id node)
         {single= List.append preds.single succs.single; sum= List.append preds.sum succs.sum} acc
     in
     let constraints =
@@ -486,24 +486,24 @@ module TransferFunctionsWCET = struct
         let c_node = BasicCost.mult c t in
         let c_node' = BasicCost.plus acc c_node in
         L.(debug Analysis Medium)
-          "@\n  [AnalyzerWCET] Adding cost: (%a) --> c =%a  t = %a @\n" InstrCFG.pp_id
+          "@\n  [AnalyzerWCET] Adding cost: (%a) --> c =%a  t = %a @\n" InstrCFG.Node.pp_id
           instr_node_id BasicCost.pp c BasicCost.pp t ;
         L.(debug Analysis Medium)
-          "@\n  [AnalyzerWCET] Adding cost: (%a) --> c_node=%a  cost = %a @\n" InstrCFG.pp_id
+          "@\n  [AnalyzerWCET] Adding cost: (%a) --> c_node=%a  cost = %a @\n" InstrCFG.Node.pp_id
           instr_node_id BasicCost.pp c_node BasicCost.pp c_node' ;
         c_node' )
       m BasicCost.zero
 
 
-  let exec_instr ((_, reported_so_far): Domain.astate) {ProcData.extras} (node: CFG.node) instr
+  let exec_instr ((_, reported_so_far): Domain.astate) {ProcData.extras} (node: CFG.Node.t) instr
       : Domain.astate =
     let {basic_cost_map= invariant_map_cost; min_trees_map= trees; summary} = extras in
     let cost_node =
-      let instr_node_id = CFG.id node in
+      let instr_node_id = CFG.Node.id node in
       match AnalyzerNodesBasicCost.extract_post instr_node_id invariant_map_cost with
       | Some node_map ->
           L.(debug Analysis Medium)
-            "@\n [AnalyzerWCET] Final map for node: %a @\n" CFG.pp_id instr_node_id ;
+            "@\n [AnalyzerWCET] Final map for node: %a @\n" CFG.Node.pp_id instr_node_id ;
           map_cost trees node_map
       | _ ->
           assert false
@@ -512,7 +512,7 @@ module TransferFunctionsWCET = struct
       "@\n[>>>AnalyzerWCET] Instr: %a   Cost: %a@\n" (Sil.pp_instr Pp.text) instr BasicCost.pp
       cost_node ;
     let astate' =
-      let und_node = CFG.underlying_node node in
+      let und_node = CFG.Node.underlying_node node in
       let preds = Procdesc.Node.get_preds und_node in
       let reported_so_far =
         if

infer/src/checkers/liveness.ml

@@ -73,7 +73,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         astate
 
 
-  let pp_session_name node fmt = F.fprintf fmt "liveness %a" CFG.pp_id (CFG.id node)
+  let pp_session_name node fmt = F.fprintf fmt "liveness %a" CFG.Node.pp_id (CFG.Node.id node)
 end
 
 module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Backward (ProcCfg.Exceptional))
@@ -183,7 +183,7 @@ let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
     let captured_by_ref_vars =
       match
         CapturedByRefAnalyzer.extract_post
-          (ProcCfg.Exceptional.id (CFG.underlying_node node))
+          (ProcCfg.Exceptional.Node.id (CFG.Node.underlying_node node))
           captured_by_ref_invariant_map
       with
       | Some post ->
@@ -191,7 +191,7 @@ let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
       | None ->
           VarSet.empty
     in
-    let node_id = CFG.id node in
+    let node_id = CFG.Node.id node in
     Instrs.iter (CFG.instrs node) ~f:(fun instr ->
         match Analyzer.extract_pre node_id invariant_map with
         | Some live_vars ->

infer/src/checkers/uninit.ml

@@ -347,7 +347,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         astate
 
 
-  let pp_session_name node fmt = F.fprintf fmt "uninit %a" CFG.pp_id (CFG.id node)
+  let pp_session_name node fmt = F.fprintf fmt "uninit %a" CFG.Node.pp_id (CFG.Node.id node)
 end
 
 module CFG = ProcCfg.NormalOneInstrPerNode
@@ -399,7 +399,7 @@ let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
       (ProcData.make proc_desc tenv (formal_map, summary))
       ~initial:init ~debug:false
   in
-  match Analyzer.extract_post (CFG.id (CFG.exit_node cfg)) invariant_map with
+  match Analyzer.extract_post (CFG.Node.id (CFG.exit_node cfg)) invariant_map with
   | Some
       ( {RecordDomain.uninit_vars= _; RecordDomain.aliased_vars= _; RecordDomain.prepost= pre, post}
       , _ ) ->

infer/src/quandary/TaintAnalysis.ml

@@ -732,7 +732,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
 
     let pp_session_name =
       let name = F.sprintf "quandary(%s)" TaintSpecification.name in
-      fun (_node: CFG.node) fmt -> F.pp_print_string fmt name
+      fun (_node: CFG.Node.t) fmt -> F.pp_print_string fmt name
   end
 
   module HilConfig : LowerHil.HilConfig = struct

infer/src/unit/analyzerTester.ml

@@ -147,7 +147,7 @@ module StructuredSil = struct
     make_call ?return args
 end
 
-module Make (CFG : ProcCfg.S with type node = Procdesc.Node.t) (T : TransferFunctions.MakeSIL) =
+module Make (CFG : ProcCfg.S with type Node.t = Procdesc.Node.t) (T : TransferFunctions.MakeSIL) =
 struct
   open StructuredSil
   module I = AbstractInterpreter.Make (CFG) (T)
@@ -220,7 +220,7 @@ struct
           let node = create_node (Procdesc.Node.Stmt_node "Invariant") [] in
           set_succs last_node [node] ~exn_handlers ;
           (* add the assertion to be checked after analysis converges *)
-          (node, M.add (CFG.id node) (inv_str, inv_label) assert_map)
+          (node, M.add (CFG.Node.id node) (inv_str, inv_label) assert_map)
     and structured_instrs_to_node last_node assert_map exn_handlers instrs =
       List.fold
         ~f:(fun acc instr -> structured_instr_to_node acc exn_handlers instr)

infer/src/unit/procCfgTests.ml

@@ -68,21 +68,21 @@ let tests =
           assert_bool "Second instr should be dummy_instr1" (phys_equal instr2 dummy_instr1)
       | _ ->
           assert_failure "Expected exactly two instructions" ) ;
-      let instr_n1 = InstrCfg.of_underlying_node n1 in
+      let instr_n1 = InstrCfg.Node.of_underlying_node n1 in
       ( match InstrCfg.instrs instr_n1 |> list_of_instrs with
       | [instr] ->
           assert_bool "Only instr should be dummy_instr1" (phys_equal instr dummy_instr1)
       | _ ->
           assert_failure "Expected exactly one instruction" ) ;
-      let n1' = InstrCfg.underlying_node instr_n1 in
+      let n1' = InstrCfg.Node.underlying_node instr_n1 in
       assert_bool "underlying_node should return node of underlying CFG type" (phys_equal n1 n1') ;
-      let backward_instr_n1 = BackwardInstrCfg.of_underlying_node n1 in
+      let backward_instr_n1 = BackwardInstrCfg.Node.of_underlying_node n1 in
       ( match BackwardInstrCfg.instrs backward_instr_n1 |> list_of_instrs with
       | [instr] ->
           assert_bool "Only instr should be dummy_instr1" (phys_equal instr dummy_instr1)
       | _ ->
           assert_failure "Expected exactly one instruction" ) ;
-      let n1'' = BackwardInstrCfg.underlying_node backward_instr_n1 in
+      let n1'' = BackwardInstrCfg.Node.underlying_node backward_instr_n1 in
       assert_bool "underlying_node should return node of underlying CFG type" (phys_equal n1 n1'') ;
       (* test the preds/succs using backward + instr cfg *)
       let check_backward_instr_ fold backward_instr_node expected_instrs =
@@ -94,9 +94,9 @@ let tests =
       in
       check_backward_instr_ BackwardInstrCfg.fold_preds backward_instr_n1
         (Instrs.single dummy_instr2) ;
-      let backward_instr_n2 = BackwardInstrCfg.of_underlying_node n2 in
+      let backward_instr_n2 = BackwardInstrCfg.Node.of_underlying_node n2 in
       check_backward_instr_ BackwardInstrCfg.fold_preds backward_instr_n2 Instrs.empty ;
-      let backward_instr_n3 = BackwardInstrCfg.of_underlying_node n3 in
+      let backward_instr_n3 = BackwardInstrCfg.Node.of_underlying_node n3 in
       check_backward_instr_ BackwardInstrCfg.fold_preds backward_instr_n3 Instrs.empty ;
       check_backward_instr_ BackwardInstrCfg.fold_normal_succs backward_instr_n2
         (Instrs.single dummy_instr2)

infer/src/unit/schedulerTests.ml

@@ -14,12 +14,8 @@ module MockNode = struct
 
   type id = int
 
-  let instrs _ = Instrs.empty
-
   let hash = Hashtbl.hash
 
-  let to_instr_nodes _ = assert false
-
   let id n = n
 
   let loc _ = assert false
@@ -47,25 +43,25 @@ module MockNode = struct
 end
 
 module MockProcCfg = struct
-  type node = int
+  module Node = MockNode
 
-  include (MockNode : module type of MockNode with type t := node)
+  type t = (Node.t * Node.t list) list
 
-  type t = (node * node list) list
+  let instrs _ = Instrs.empty
 
   let equal_id = Int.equal
 
   let fold_succs t n ~init ~f =
-    let node_id = id n in
+    let node_id = Node.id n in
-    List.find ~f:(fun (node, _) -> equal_id (id node) node_id) t
+    List.find ~f:(fun (node, _) -> equal_id (Node.id node) node_id) t
     |> Option.value_map ~f:snd ~default:[] |> List.fold ~init ~f
 
 
   let fold_preds t n ~init ~f =
     try
-      let node_id = id n in
+      let node_id = Node.id n in
       List.filter
-        ~f:(fun (_, succs) -> List.exists ~f:(fun node -> equal_id (id node) node_id) succs)
+        ~f:(fun (_, succs) -> List.exists ~f:(fun node -> equal_id (Node.id node) node_id) succs)
         t
       |> List.map ~f:fst |> List.fold ~init ~f
     with