From 8948b08bf275c54626072f5a8bea8ff6cf52d996 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Wed, 15 Feb 2017 23:16:36 -0800 Subject: [PATCH] [infer][backend] The dependency map with the list of children is no longer used by the ondemand analysis Summary: This does not seem to be used anymore Reviewed By: sblackshear Differential Revision: D4557781 fbshipit-source-id: 7deac40 --- infer/src/backend/interproc.ml | 11 +++--- infer/src/backend/specs.ml | 61 ++++++++-------------------------- infer/src/backend/specs.mli | 45 ++++++++++--------------- 3 files changed, 34 insertions(+), 83 deletions(-) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 6492a933a..be896698f 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1351,12 +1351,9 @@ let transition_footprint_re_exe tenv proc_name joined_pres = let payload = { summary.Specs.payload with Specs.preposts = Some specs; } in - let dependency_map = - Specs.re_initialize_dependency_map summary.Specs.dependency_map in { summary with Specs.timestamp = 0; phase = Specs.RE_EXECUTION; - dependency_map; payload; } in Specs.add_summary proc_name summary' @@ -1437,7 +1434,7 @@ let do_analysis exe_env = let f (callee_pname, loc) = calls := (callee_pname, loc) :: !calls in Procdesc.iter_calls f caller_pdesc; IList.rev !calls in - let init_proc (pname, dep) = + let init_proc pname = let pdesc = match Exe_env.get_proc_desc exe_env pname with | Some pdesc -> pdesc @@ -1454,15 +1451,15 @@ let do_analysis exe_env = if Config.dynamic_dispatch = `Lazy then Some pdesc else None in - Specs.init_summary (dep, nodes, proc_flags, calls, None, attributes, proc_desc_option) in + Specs.init_summary (nodes, proc_flags, calls, None, attributes, proc_desc_option) in IList.iter - (fun ((pn, _) as x) -> + (fun (pn, _) -> let should_init () = Config.models_mode || is_none (Specs.get_summary pn) in if should_init () - then init_proc x) + then init_proc pn) procs_and_defined_children; let callbacks = diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index cc24616fb..f1c4d0494 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -312,8 +312,6 @@ type phase = FOOTPRINT | RE_EXECUTION [@@deriving compare] let equal_phase = [%compare.equal : phase] -type dependency_map_t = int Procname.Map.t - type call_summary = CallSite.Set.t Annot.Map.t (** Payload: results of some analysis *) @@ -330,18 +328,17 @@ type payload = buffer_overrun : BufferOverrunDomain.Summary.t option; } -type summary = - { dependency_map: dependency_map_t; (** maps children procs to timestamp as last seen at the start of an analysys phase for this proc *) - nodes: Procdesc.Node.id list; (** ids of cfg nodes of the procedure *) - phase: phase; (** in FOOTPRINT phase or in RE_EXECUTION PHASE *) - payload: payload; (** payload containing the result of some analysis *) - sessions: int ref; (** Session number: how many nodes went trough symbolic execution *) - stats: stats; (** statistics: execution time and list of errors *) - status: status; (** ACTIVE when the proc is being analyzed *) - timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *) - attributes : ProcAttributes.t; (** Attributes of the procedure *) - proc_desc_option : Procdesc.t option; - } +type summary = { + nodes: Procdesc.Node.id list; (** ids of cfg nodes of the procedure *) + phase: phase; (** in FOOTPRINT phase or in RE_EXECUTION PHASE *) + payload: payload; (** payload containing the result of some analysis *) + sessions: int ref; (** Session number: how many nodes went trough symbolic execution *) + stats: stats; (** statistics: execution time and list of errors *) + status: status; (** ACTIVE when the proc is being analyzed *) + timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *) + attributes : ProcAttributes.t; (** Attributes of the procedure *) + proc_desc_option : Procdesc.t option; +} type spec_tbl = summary Procname.Hash.t @@ -409,11 +406,6 @@ let pp_specs pe fmt specs = F.fprintf fmt "\\subsection*{Spec %d of %d}@\n\\(%a\\)@\n" !cnt total (pp_spec pe None) spec) specs -(** Print the decpendency map *) -let pp_dependency_map fmt dependency_map = - let pp_entry fmt proc_name n = F.fprintf fmt "%a=%d " Procname.pp proc_name n in - Procname.Map.iter (pp_entry fmt) dependency_map - let describe_timestamp summary = ("Timestamp", Printf.sprintf "%d" summary.timestamp) @@ -453,8 +445,7 @@ let pp_summary_no_stats_specs fmt summary = F.fprintf fmt "%s@\n" (get_signature summary); F.fprintf fmt "%a@\n" pp_pair (describe_timestamp summary); F.fprintf fmt "%a@\n" pp_pair (describe_status summary); - F.fprintf fmt "%a@\n" pp_pair (describe_phase summary); - F.fprintf fmt "Dependency_map: @[%a@]@\n" pp_dependency_map summary.dependency_map + F.fprintf fmt "%a@\n" pp_pair (describe_phase summary) let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof; threadsafety; buffer_overrun } = let pp_opt pp fmt = function @@ -724,28 +715,6 @@ let set_status proc_name status = | None -> raise (Failure ("Specs.set_status: " ^ (Procname.to_string proc_name) ^ " Not_found")) | Some summary -> add_summary proc_name { summary with status = status } -(** Create the initial dependency map with the given list of dependencies *) -let mk_initial_dependency_map proc_list : dependency_map_t = - IList.fold_left (fun map pname -> Procname.Map.add pname (- 1) map) Procname.Map.empty proc_list - -(** Re-initialize a dependency map *) -let re_initialize_dependency_map dependency_map = - Procname.Map.map (fun _ -> - 1) dependency_map - -(** Update the dependency map of [proc_name] with the current - timestamps of the dependents *) -let update_dependency_map proc_name = - match get_summary proc_name with - | None -> - raise - (Failure ("Specs.update_dependency_map: " ^ (Procname.to_string proc_name) ^ " Not_found")) - | Some summary -> - let current_dependency_map = - Procname.Map.mapi - (fun _ _ -> get_timestamp summary) - summary.dependency_map in - add_summary proc_name { summary with dependency_map = current_dependency_map } - let empty_payload = { preposts = None; @@ -762,14 +731,12 @@ let empty_payload = proc_flags, calls, in_out_calls_opt, proc_attributes)] initializes the summary for [proc_name] given dependent procs in list [depend_list]. *) let init_summary - (depend_list, nodes, + (nodes, proc_flags, calls, in_out_calls_opt, proc_attributes, proc_desc_option) = - let dependency_map = mk_initial_dependency_map depend_list in let summary = { - dependency_map = dependency_map; nodes = nodes; phase = FOOTPRINT; sessions = ref 0; @@ -786,14 +753,12 @@ let init_summary (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *) let reset_summary call_graph proc_name attributes_opt proc_desc_option = - let dependents = Cg.get_defined_children call_graph proc_name in let proc_attributes = match attributes_opt with | Some attributes -> attributes | None -> ProcAttributes.default proc_name !Config.curr_language in init_summary ( - Procname.Set.elements dependents, [], ProcAttributes.proc_flags_empty (), [], diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 3f7d1d3f0..2fae294e9 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -121,8 +121,6 @@ type phase = FOOTPRINT | RE_EXECUTION val equal_phase : phase -> phase -> bool -type dependency_map_t = int Procname.Map.t - type call_summary = CallSite.Set.t Annot.Map.t (** Payload: results of some analysis *) @@ -140,18 +138,17 @@ type payload = } (** Procedure summary *) -type summary = - { dependency_map: dependency_map_t; (** maps children procs to timestamp as last seen at the start of an analysys phase for this proc *) - nodes: Procdesc.Node.id list; (** ids of cfg nodes of the procedure *) - phase: phase; (** in FOOTPRINT phase or in RE_EXECUTION PHASE *) - payload: payload; (** payload containing the result of some analysis *) - sessions: int ref; (** Session number: how many nodes went trough symbolic execution *) - stats: stats; (** statistics: execution time and list of errors *) - status: status; (** ACTIVE when the proc is being analyzed *) - timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *) - attributes : ProcAttributes.t; (** Attributes of the procedure *) - proc_desc_option : Procdesc.t option; - } +type summary = { + nodes: Procdesc.Node.id list; (** ids of cfg nodes of the procedure *) + phase: phase; (** in FOOTPRINT phase or in RE_EXECUTION PHASE *) + payload: payload; (** payload containing the result of some analysis *) + sessions: int ref; (** Session number: how many nodes went trough symbolic execution *) + stats: stats; (** statistics: execution time and list of errors *) + status: status; (** ACTIVE when the proc is being analyzed *) + timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *) + attributes : ProcAttributes.t; (** Attributes of the procedure *) + proc_desc_option : Procdesc.t option; +} (** Add the summary to the table for the given function *) val add_summary : Procname.t -> summary -> unit @@ -213,13 +210,12 @@ val is_active : summary -> bool (** Initialize the summary for [proc_name] given dependent procs in list [depend_list]. Do nothing if a summary exists already. *) val init_summary : - (Procname.t list * (* depend list *) - Procdesc.Node.id list * (* nodes *) - ProcAttributes.proc_flags * (* procedure flags *) - (Procname.t * Location.t) list * (* calls *) - (Cg.in_out_calls option) * (* in and out calls *) - ProcAttributes.t * (* attributes of the procedure *) - Procdesc.t option) (* procdesc option *) + ( Procdesc.Node.id list * (* nodes *) + ProcAttributes.proc_flags * (* procedure flags *) + (Procname.t * Location.t) list * (* calls *) + (Cg.in_out_calls option) * (* in and out calls *) + ProcAttributes.t * (* attributes of the procedure *) + Procdesc.t option) (* procdesc option *) -> unit (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *) @@ -264,9 +260,6 @@ val proc_resolve_attributes : Procname.t -> ProcAttributes.t option It's not defined, and there is no spec file for it. *) val proc_is_library : ProcAttributes.t -> bool -(** Re-initialize a dependency map *) -val re_initialize_dependency_map : dependency_map_t -> dependency_map_t - (** Set the current status for the proc *) val set_status : Procname.t -> status -> unit @@ -281,7 +274,3 @@ val store_summary : Procname.t -> summary -> unit (** Return a compact representation of the summary *) val summary_compact : Sil.sharing_env -> summary -> summary - -(** Update the dependency map of [proc_name] with the current - timestamps of the dependents *) -val update_dependency_map : Procname.t -> unit