From 0becc32a88e37486825f6391e473efc88d1821f5 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 10 May 2016 08:24:31 -0700 Subject: [PATCH] factoring Node module out of CFG Reviewed By: jberdine Differential Revision: D3273314 fbshipit-source-id: fe32f82 --- infer/src/backend/preanal.ml | 2 +- infer/src/checkers/abstractInterpreter.ml | 34 +++--- infer/src/checkers/addressTaken.ml | 2 +- infer/src/checkers/annotationReachability.ml | 2 +- infer/src/checkers/procCfg.ml | 104 +++++++++---------- infer/src/checkers/procCfg.mli | 54 ++++++---- infer/src/checkers/scheduler.ml | 28 ++--- infer/src/unit/analyzerTester.ml | 10 +- infer/src/unit/schedulerTests.ml | 39 +++++-- 9 files changed, 152 insertions(+), 123 deletions(-) diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index ba5fd6bfc..725fa4cbd 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -473,7 +473,7 @@ module NullifyDomain = AbstractDomain.Pair (VarDomain) (VarDomain) module NullifyTransferFunctions = struct type astate = NullifyDomain.astate type extras = LivenessAnalysis.inv_map - type node_id = BackwardCfg.node_id + type node_id = BackwardCfg.id let postprocess ((reaching_defs, _) as astate) node_id { ProcData.extras; } = match LivenessAnalysis.extract_state node_id extras with diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index a71cac752..0be623b09 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/infer/src/checkers/abstractInterpreter.ml @@ -12,13 +12,13 @@ open! Utils module L = Logging module Make - (C : ProcCfg.Wrapper) + (CFG : ProcCfg.S) (Sched : Scheduler.S) (A : AbstractDomain.S) - (T : TransferFunctions.S with type astate = A.astate and type node_id = C.node_id) = struct + (T : TransferFunctions.S with type astate = A.astate and type node_id = CFG.id) = struct - module S = Sched (C) - module M = ProcCfg.NodeIdMap (C) + module S = Sched (CFG) + module M = ProcCfg.NodeIdMap (CFG) 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_id node_id; + L.err "Warning: No state found for node %a" CFG.pp_id node_id; None (** extract the postcondition of node [n] from [inv_map] *) @@ -45,17 +45,17 @@ module Make | None -> None let exec_node node astate_pre work_queue inv_map proc_data = - 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 node_id = CFG.id node in + L.out "Doing analysis of node %a from pre %a@." CFG.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 = if A.is_bottom astate_acc then astate_acc 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 + let astate_post_instrs = IList.fold_left exec_instrs astate_pre (CFG.instrs node) in T.postprocess astate_post_instrs node_id proc_data in - L.out "Post for node %a is %a@." C.pp_id node_id A.pp astate_post; + L.out "Post for node %a is %a@." CFG.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,11 +82,11 @@ 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.id pred) inv_map in - let normal_posts = IList.map extract_post_ (C.normal_preds cfg node) in + let extract_post_ pred = extract_post (CFG.id pred) inv_map in + let normal_posts = IList.map extract_post_ (CFG.normal_preds cfg node) in (* if the [pred] -> [node] transition was exceptional, use pre([pred]) *) - 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 + let extract_pre_f acc pred = extract_pre (CFG.id pred) inv_map :: acc in + let all_posts = IList.fold_left extract_pre_f normal_posts (CFG.exceptional_preds cfg node) in match IList.flatten_options all_posts with | post :: posts -> Some (IList.fold_left A.join post posts) | [] -> None in @@ -103,20 +103,20 @@ module Make (* compute and return an invariant map for [cfg] *) let exec_cfg cfg proc_data = - let start_node = C.start_node cfg in + let start_node = CFG.start_node cfg in let inv_map', work_queue' = exec_node start_node A.initial (S.empty cfg) M.empty proc_data in exec_worklist cfg work_queue' inv_map' proc_data (* compute and return an invariant map for [pdesc] *) let exec_pdesc ({ ProcData.pdesc; } as proc_data) = L.out "Starting analysis of %a@." Procname.pp (Cfg.Procdesc.get_proc_name pdesc); - exec_cfg (C.from_pdesc pdesc) proc_data + exec_cfg (CFG.from_pdesc pdesc) proc_data (* compute and return the postcondition of [pdesc] *) let compute_post ({ ProcData.pdesc; } as proc_data) = - let cfg = C.from_pdesc pdesc in + let cfg = CFG.from_pdesc pdesc in let inv_map = exec_cfg cfg proc_data in - extract_post (C.id (C.exit_node cfg)) inv_map + extract_post (CFG.id (CFG.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 70fd5a341..4c00dea44 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/infer/src/checkers/addressTaken.ml @@ -20,7 +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 + type node_id = ProcCfg.DefaultNode.id let postprocess = TransferFunctions.no_postprocessing diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 0f5a79ee7..f0f9a746e 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -304,7 +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 + type node_id = ProcCfg.DefaultNode.id let postprocess = TransferFunctions.no_postprocessing diff --git a/infer/src/checkers/procCfg.ml b/infer/src/checkers/procCfg.ml index 2584356f5..62b2ee6c9 100644 --- a/infer/src/checkers/procCfg.ml +++ b/infer/src/checkers/procCfg.ml @@ -12,25 +12,39 @@ open! Utils module F = Format (** Control-flow graph for a single procedure (as opposed to cfg.ml, which represents a cfg for a - file). *) + file). Defines useful wrappers that allows us to do tricks like turn a forward cfg into a + backward one, or view a cfg as having a single instruction per node. *) -module type Base = sig +module type Node = sig + type t + type id + + val instrs : t -> Sil.instr list + val kind : t -> Cfg.Node.nodekind + val id : t -> id + val id_compare : id -> id -> int + val pp_id : F.formatter -> id -> unit +end + +module DefaultNode = struct + type t = Cfg.Node.t + type id = Cfg.Node.id + + let instrs = Cfg.Node.get_instrs + let kind = Cfg.Node.get_kind + let id = Cfg.Node.get_id + let id_compare = Cfg.Node.id_compare + let pp_id = Cfg.Node.pp_id +end + +module type S = sig type t type node - type node_id + include (Node with type t := node) - 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) *) 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 *) @@ -41,24 +55,17 @@ module type Wrapper = sig 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 : 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 + type node = DefaultNode.t + include (DefaultNode : module type of DefaultNode with type t := node) - 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 *) @@ -68,25 +75,17 @@ module Normal = struct let preds = normal_preds let start_node = Cfg.Procdesc.get_start_node let exit_node = Cfg.Procdesc.get_exit_node - let instrs = Cfg.Node.get_instrs - let kind = Cfg.Node.get_kind let proc_desc t = t let nodes = Cfg.Procdesc.get_nodes - let from_pdesc pdesc = pdesc - - 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 = struct - type node_id = Cfg.Node.id - type node = Cfg.node + type node = DefaultNode.t type id_node_map = node list Cfg.IdMap.t type t = Cfg.Procdesc.t * id_node_map + include (DefaultNode : module type of DefaultNode with type t := node) let from_pdesc pdesc = (* map from a node to its exceptional predecessors *) @@ -143,34 +142,29 @@ module Exceptional = struct let proc_desc (pdesc, _) = pdesc 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 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 -module Backward (W : Wrapper) = struct - include W - - let succs = W.preds - let preds = W.succs - let start_node = W.exit_node - let exit_node = W.start_node - let instrs t = IList.rev (W.instrs t) - let normal_succs = W.normal_preds - let normal_preds = W.normal_succs - let exceptional_succs = W.exceptional_preds - let exceptional_preds = W.exceptional_succs +(** Wrapper that reverses the direction of the CFG *) +module Backward (Base : S) = struct + include Base + let instrs n = IList.rev (Base.instrs n) + + let succs = Base.preds + let preds = Base.succs + let start_node = Base.exit_node + let exit_node = Base.start_node + let normal_succs = Base.normal_preds + let normal_preds = Base.normal_succs + let exceptional_succs = Base.exceptional_preds + let exceptional_preds = Base.exceptional_succs end -module NodeIdMap (B : Base) = Map.Make(struct - type t = B.node_id - let compare = B.id_compare +module NodeIdMap (CFG : S) = Map.Make(struct + type t = CFG.id + let compare = CFG.id_compare end) -module NodeIdSet (B : Base) = Set.Make(struct - type t = B.node_id - let compare = B.id_compare +module NodeIdSet (CFG : S) = Set.Make(struct + type t = CFG.id + let compare = CFG.id_compare end) diff --git a/infer/src/checkers/procCfg.mli b/infer/src/checkers/procCfg.mli index 3a3551634..02f5c7343 100644 --- a/infer/src/checkers/procCfg.mli +++ b/infer/src/checkers/procCfg.mli @@ -7,23 +7,29 @@ * of patent rights can be found in the PATENTS file in the same directory. *) -module type Base = sig +(** Control-flow graph for a single procedure (as opposed to cfg.ml, which represents a cfg for a + file). Defines useful wrappers that allows us to do tricks like turn a forward cfg to into a + backward one, or view a cfg as having a single instruction per block *) + +module type Node = sig + type t + type id + + val instrs : t -> Sil.instr list + val kind : t -> Cfg.Node.nodekind + val id : t -> id + val id_compare : id -> id -> int + val pp_id : Format.formatter -> id -> unit +end + +module type S = sig type t type node - type node_id + include (Node with type t := node) - 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) *) 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 *) @@ -34,24 +40,28 @@ module type Wrapper = sig 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 - val pp_id : Format.formatter -> node_id -> unit end -module Normal : Wrapper with type node = Cfg.Node.t and type node_id = Cfg.Node.id +module DefaultNode : Node with type t = Cfg.Node.t and type id = Cfg.Node.id -module Exceptional : Wrapper with type node = Cfg.Node.t and type node_id = Cfg.Node.id +(** Forward CFG with no exceptional control-flow *) +module Normal : S with type t = Cfg.Procdesc.t + and type node = DefaultNode.t + and type id = DefaultNode.id -module Backward (W : Wrapper) : Wrapper with type node = W.node and type node_id = W.node_id +(** Forward CFG with exceptional control-flow *) +module Exceptional : S with type t = Cfg.Procdesc.t * DefaultNode.t list Cfg.IdMap.t + and type node = DefaultNode.t + and type id = DefaultNode.id -module NodeIdMap (B : Base) : Map.S with type key = B.node_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 NodeIdSet (B : Base) : Set.S with type elt = B.node_id +module NodeIdMap (CFG : S) : Map.S with type key = CFG.id +module NodeIdSet (CFG : S) : Set.S with type elt = CFG.id diff --git a/infer/src/checkers/scheduler.ml b/infer/src/checkers/scheduler.ml index be9ae84bd..dbbf58bb4 100644 --- a/infer/src/checkers/scheduler.ml +++ b/infer/src/checkers/scheduler.ml @@ -12,28 +12,28 @@ open! Utils module F = Format module L = Logging -module type S = functor (C : ProcCfg.Base) -> sig +module type S = functor (CFG : ProcCfg.S) -> sig type t (* schedule the successors of [node] *) - val schedule_succs : t -> C.node -> t + val schedule_succs : t -> CFG.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 empty : C.t -> t + val pop : t -> (CFG.node * CFG.id list * t) option + val empty : CFG.t -> t 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 ReversePostorder : S = functor (CFG : ProcCfg.S) -> struct + module M = ProcCfg.NodeIdMap (CFG) module WorkUnit = struct - module IdSet = ProcCfg.NodeIdSet (C) + module IdSet = ProcCfg.NodeIdSet (CFG) type t = { - node : C.node; (* node whose instructions will be analyzed *) + node : CFG.node; (* 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|. *) } @@ -45,7 +45,7 @@ module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct let priority t = t.priority let compute_priority cfg node visited_preds = - IList.length (C.preds cfg node) - IdSet.cardinal visited_preds + IList.length (CFG.preds cfg node) - IdSet.cardinal visited_preds let make cfg node = let visited_preds = IdSet.empty in @@ -59,20 +59,20 @@ module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct { t with visited_preds = visited_preds'; priority = priority'; } end - type t = { worklist : WorkUnit.t M.t; cfg : C.t; } + type t = { worklist : WorkUnit.t M.t; cfg : CFG.t; } (* schedule the succs of [node] for analysis *) let schedule_succs t node = - let node_id = C.id node in + let node_id = CFG.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.id node_to_schedule in + let id_to_schedule = CFG.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 let new_work = WorkUnit.add_visited_pred t.cfg old_work node_id in M.add id_to_schedule new_work worklist_acc in - let new_worklist = IList.fold_left schedule_succ t.worklist (C.succs t.cfg node) in + let new_worklist = IList.fold_left schedule_succ t.worklist (CFG.succs t.cfg node) in { t with worklist = new_worklist; } (* remove and return the node with the highest priority (note that smaller integers have higher @@ -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.id node) t.worklist } in + let t' = { t with worklist = M.remove (CFG.id node) t.worklist } in Some (node, WorkUnit.visited_preds max_priority_work, t') with Not_found -> None diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 678f69e91..65ce0b46f 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -138,17 +138,17 @@ module StructuredSil = struct end module Make - (C : ProcCfg.Wrapper with type node = Cfg.Node.t and type node_id = Cfg.Node.id) + (CFG : ProcCfg.S with type node = Cfg.Node.t) (S : Scheduler.S) (A : AbstractDomain.S) (T : TransferFunctions.S with type astate = A.astate and type extras = ProcData.no_extras - and type node_id = C.node_id) = struct + and type node_id = CFG.id) = struct open StructuredSil - module I = AbstractInterpreter.Make (C) (S) (A) (T) - module M = ProcCfg.NodeIdMap (C) + module I = AbstractInterpreter.Make (CFG) (S) (A) (T) + module M = ProcCfg.NodeIdMap (CFG) type assert_map = string M.t @@ -214,7 +214,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.id node) (inv_str, inv_label) assert_map + node, M.add (CFG.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/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index cf40ee019..f2fb6efea 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/infer/src/unit/schedulerTests.ml @@ -12,20 +12,33 @@ open! Utils module F = Format -(* mock for creating CFG's from adjacency lists *) + +(** mocks for creating CFG's from adjacency lists *) +module MockNode = struct + type t = int + type id = int + + let instrs _ = [] + let id n = n + let kind _ = Cfg.Node.Stmt_node "" + let id_compare = int_compare + let pp_id fmt i = + F.fprintf fmt "%i" i +end + module MockProcCfg = struct type node = int + include (MockNode : module type of MockNode with type t := node) type t = (node * node list) list - type node_id = int let id_compare = int_compare - let id n = n - let succs t n = try let node_id = id n in - IList.find (fun (node, _) -> id_compare (id node) node_id = 0) t + IList.find + (fun (node, _) -> id_compare (id node) node_id = 0) + t |> snd with Not_found -> [] @@ -33,12 +46,24 @@ module MockProcCfg = struct try let node_id = id n in IList.filter - (fun (_, succs) -> IList.exists (fun node -> id_compare (id node) 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 -> [] - let from_adjacency_list t = t + let nodes t = IList.map fst t + let normal_succs = succs + let normal_preds = preds + let exceptional_succs _ _ = [] + let exceptional_preds _ _ = [] + let from_adjacency_list t = t + (* not called by the scheduler *) + let start_node _ = assert false + let exit_node _ = assert false + let proc_desc _ = assert false + let from_pdesc _ = assert false end module S = Scheduler.ReversePostorder (MockProcCfg)