diff --git a/infer/src/IR/cfg.ml b/infer/src/IR/cfg.ml index 31b7abe5c..92ea869aa 100644 --- a/infer/src/IR/cfg.ml +++ b/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 diff --git a/infer/src/IR/cfg.mli b/infer/src/IR/cfg.mli index 5eaf5b68b..acbf63837 100644 --- a/infer/src/IR/cfg.mli +++ b/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} *) diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index 7299b155c..a71cac752 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/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 - L.out "Doing analysis of node %a from pre %a@." Cfg.Node.pp_id node_id A.pp astate_pre; + let node_id = C.id node in + 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 diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index 54ae565fd..70fd5a341 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/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 diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 4f018ee9a..0f5a79ee7 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/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 diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml index aa2edb9d7..a57cb3d4a 100644 --- a/infer/src/checkers/copyPropagation.ml +++ b/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 diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 7b11295e7..ff5acfa2a 100644 --- a/infer/src/checkers/liveness.ml +++ b/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 diff --git a/infer/src/checkers/procCfg.ml b/infer/src/checkers/procCfg.ml index 046b19cd9..2584356f5 100644 --- a/infer/src/checkers/procCfg.ml +++ b/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 node_id_compare : Cfg.Node.id -> Cfg.Node.id -> int + val id : node -> node_id + 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 NodeIdMap = Map.Make(struct - type t = Cfg.Node.id - let compare = Cfg.Node.id_compare - end) - +module Exceptional = struct + type node_id = Cfg.Node.id 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 node_id_compare = Cfg.Node.id_compare + let id = Cfg.Node.get_id + 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) diff --git a/infer/src/checkers/procCfg.mli b/infer/src/checkers/procCfg.mli index 9c9d6e4c1..3a3551634 100644 --- a/infer/src/checkers/procCfg.mli +++ b/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 node_id_compare : Cfg.Node.id -> Cfg.Node.id -> int + val id : node -> node_id + 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 diff --git a/infer/src/checkers/scheduler.ml b/infer/src/checkers/scheduler.ml index ee98c72f4..be9ae84bd 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 * 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 diff --git a/infer/src/checkers/transferFunctions.ml b/infer/src/checkers/transferFunctions.ml index aafefbcfb..f8e5e09f1 100644 --- a/infer/src/checkers/transferFunctions.ml +++ b/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 *) diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index eb1cf10d2..a73daf675 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/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 diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 376b992a3..0e4d2c094 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/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) diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml index 6793ac05a..000b44b27 100644 --- a/infer/src/unit/livenessTests.ml +++ b/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) diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index f5b577c95..cf40ee019 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/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 - IList.find (fun (node, _) -> node_id_compare (node_id node) id = 0) t + let node_id = id n in + 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 -> []