diff --git a/infer/src/IR/cfg.ml b/infer/src/IR/cfg.ml index 1beb7f5f4..31b7abe5c 100644 --- a/infer/src/IR/cfg.ml +++ b/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 diff --git a/infer/src/IR/cfg.mli b/infer/src/IR/cfg.mli index 3d17182da..5eaf5b68b 100644 --- a/infer/src/IR/cfg.mli +++ b/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} *) diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index c7b56b8d7..a93870a15 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/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 diff --git a/infer/src/checkers/procCfg.ml b/infer/src/checkers/procCfg.ml index 20536b3a8..046b19cd9 100644 --- a/infer/src/checkers/procCfg.ml +++ b/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) diff --git a/infer/src/checkers/procCfg.mli b/infer/src/checkers/procCfg.mli new file mode 100644 index 000000000..9c9d6e4c1 --- /dev/null +++ b/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 diff --git a/infer/src/checkers/scheduler.ml b/infer/src/checkers/scheduler.ml index 2278eb864..ee98c72f4 100644 --- a/infer/src/checkers/scheduler.ml +++ b/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 *) diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index e56221d47..22c2625d7 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/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 diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index a1218023b..f5b577c95 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/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 -> []