diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 35e664497..57cb7ee4b 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/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) = diff --git a/infer/src/absint/AbstractInterpreter.mli b/infer/src/absint/AbstractInterpreter.mli index c6e82dc14..596f0fff5 100644 --- a/infer/src/absint/AbstractInterpreter.mli +++ b/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) diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 8c7cff682..440b1a51f 100644 --- a/infer/src/absint/LowerHil.ml +++ b/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 diff --git a/infer/src/absint/LowerHil.mli b/infer/src/absint/LowerHil.mli index 91ca4f015..65f56e153 100644 --- a/infer/src/absint/LowerHil.mli +++ b/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 *) diff --git a/infer/src/absint/ProcCfg.ml b/infer/src/absint/ProcCfg.ml index f3365b323..bd01c0893 100644 --- a/infer/src/absint/ProcCfg.ml +++ b/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 - - include Node with type t := node + module Node : 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 - - include (DefaultNode : module type of DefaultNode with type t := node) + module Node = DefaultNode 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 -> - IdSet.add (Procdesc.Node.get_id node) set )) + (fold_normal_idset t n ~init:Node.IdSet.empty ~f:(fun set node -> + 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 - - 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 ) + module Node = InstrNode let instrs (node, index) = let instrs = Base.instrs node in diff --git a/infer/src/absint/ProcCfg.mli b/infer/src/absint/ProcCfg.mli index 08958f66b..20d1120cb 100644 --- a/infer/src/absint/ProcCfg.mli +++ b/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 -> 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 (** 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 : - S with type t = Procdesc.t and type node = DefaultNode.t and type id = DefaultNode.id +module Normal : S with type t = Procdesc.t and module Node = DefaultNode (** Forward CFG with exceptional control-flow *) module Exceptional : - S - with type t = Procdesc.t * DefaultNode.t list Procdesc.IdMap.t - and type node = DefaultNode.t - and type id = DefaultNode.id + S with type t = Procdesc.t * DefaultNode.t list Procdesc.IdMap.t and module Node = DefaultNode (** 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 OneInstrPerNode (Base : S with type node = DefaultNode.t and type id = DefaultNode.id) : - S - 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 Backward (Base : S) : S with type t = Base.t and module Node = Base.Node + +module OneInstrPerNode (Base : S with module Node = DefaultNode) : + S with type t = Base.t and module Node = InstrNode module NormalOneInstrPerNode : module type of OneInstrPerNode (Normal) diff --git a/infer/src/absint/Scheduler.ml b/infer/src/absint/Scheduler.ml index b60fea742..4a3654ea8 100644 --- a/infer/src/absint/Scheduler.ml +++ b/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 diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index 10430ad4b..4c974e38a 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/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 diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index 655249a77..2d54136dc 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/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 diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index ac2582b0f..71163a054 100644 --- a/infer/src/backend/preanal.ml +++ b/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 diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 647ab365d..88e3355a9 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/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) - : Paths.PathSet.t = +let node handle_exn exe_env tenv proc_cfg (node: ProcCfg.Exceptional.Node.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 ( diff --git a/infer/src/biabduction/SymExec.mli b/infer/src/biabduction/SymExec.mli index f5113b184..7486e3797 100644 --- a/infer/src/biabduction/SymExec.mli +++ b/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. *) diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 3777d543d..4e1905410 100644 --- a/infer/src/biabduction/interproc.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 23478d3ab..e8e10ec10 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 exit_mem = extract_post (CFG.exit_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.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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.mli b/infer/src/bufferoverrun/bufferOverrunChecker.mli index d26d92239..f09c3576f 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.mli +++ b/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 diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml index 3d366590e..be24df249 100644 --- a/infer/src/checkers/SimpleChecker.ml +++ b/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 = diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml index c38109f44..562a50c30 100644 --- a/infer/src/checkers/control.ml +++ b/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 = Procdesc.Node.get_id und_node in + let node_id = CFG.Node.id node in let deps = VarSet.empty in ControlDepAnalyzer.extract_post node_id control_invariant_map |> Option.map ~f:(fun control_deps -> diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index d0395a56c..b83a256f0 100644 --- a/infer/src/checkers/cost.ml +++ b/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 = - let key = CFG.id node in + {ProcData.pdesc; tenv} (node: CFG.Node.t) instr : CostDomain.NodeInstructionToCostMap.astate = + 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 diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 2d5e3411b..a2876bf55 100644 --- a/infer/src/checkers/liveness.ml +++ b/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 -> diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index adf3fb31f..e1649d838 100644 --- a/infer/src/checkers/uninit.ml +++ b/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} , _ ) -> diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index fcd045442..6952834ff 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/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 diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index d6056f914..3ee2c3f44 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/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) diff --git a/infer/src/unit/procCfgTests.ml b/infer/src/unit/procCfgTests.ml index 837bc4a25..c5dde4cc2 100644 --- a/infer/src/unit/procCfgTests.ml +++ b/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) diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index d503f87b1..92c10bac1 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/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 - List.find ~f:(fun (node, _) -> equal_id (id node) node_id) t + let node_id = Node.id n in + 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