From f17f54939b622651806ac1466e381ecc9e89140f Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Mon, 19 Oct 2015 08:25:43 -0700 Subject: [PATCH] checkers can now analyze a restricted subset of the procedures defined in a file Reviewed By: jvillard Differential Revision: D2554136 fb-gh-sync-id: c972f0e --- infer/src/backend/callbacks.ml | 19 +++-- infer/src/backend/cg.ml | 63 ++++++++++++---- infer/src/backend/cg.mli | 116 ++++++++++++++++++++++-------- infer/src/backend/inferanalyze.ml | 4 +- infer/src/backend/interproc.ml | 2 +- infer/src/backend/ondemand.ml | 2 +- infer/src/backend/type_prop.ml | 2 +- infer/src/clang/cMethod_decl.ml | 2 +- infer/src/harness/inhabit.ml | 2 +- infer/src/java/jFrontend.ml | 4 +- infer/src/llvm/lTrans.ml | 2 +- 11 files changed, 158 insertions(+), 60 deletions(-) diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 5c430cc83..175b22711 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -196,7 +196,12 @@ let iterate_cluster_callbacks all_procs exe_env proc_names = (** Invoke all procedure and cluster callbacks on a given environment. *) let iterate_callbacks store_summary call_graph exe_env = - let proc_names = Cg.get_defined_nodes call_graph in + let procs_to_analyze = + (* analyze all the currently defined procedures *) + Cg.get_defined_nodes call_graph in + let originally_defined_procs = + (* all the defined procedures, even if we are analyzing a restricted subset *) + Cg.get_originally_defined_nodes call_graph in let saved_language = !Config.curr_language in let cluster_id proc_name = @@ -225,18 +230,18 @@ let iterate_callbacks store_summary call_graph exe_env = (* Make sure summaries exists. *) - list_iter reset_summary proc_names; + list_iter reset_summary procs_to_analyze; (* Invoke callbacks. *) list_iter - (iterate_procedure_callbacks proc_names exe_env) - proc_names; + (iterate_procedure_callbacks originally_defined_procs exe_env) + procs_to_analyze; list_iter - (iterate_cluster_callbacks proc_names exe_env) - (cluster proc_names); + (iterate_cluster_callbacks originally_defined_procs exe_env) + (cluster procs_to_analyze); - list_iter store_summary proc_names; + list_iter store_summary procs_to_analyze; Config.curr_language := saved_language diff --git a/infer/src/backend/cg.ml b/infer/src/backend/cg.ml index 95b1e9f02..b6066eae7 100644 --- a/infer/src/backend/cg.ml +++ b/infer/src/backend/cg.ml @@ -26,7 +26,8 @@ type in_out_calls = } type node_info = - { mutable defined : bool; + { mutable defined : bool; (** defined procedure as opposed to just declared *) + mutable disabled : bool; (** originally defined procedures disabled by restrict_defined *) mutable parents: Procname.Set.t; mutable children: Procname.Set.t; mutable ancestors : Procname.Set.t option ; (** ancestors are computed lazily *) @@ -48,13 +49,17 @@ let create () = nLOC = !Config.nLOC; node_map = Procname.Hash.create 3 } -let _add_node g n defined = +let _add_node g n defined disabled = try let info = Procname.Hash.find g.node_map n in - if defined then info.defined <- true + (* defined and disabled only go from false to true + to avoid accidental overwrite to false by calling add_edge *) + if defined then info.defined <- true; + if disabled then info.disabled <- true; with Not_found -> let info = { defined = defined; + disabled = disabled; parents = Procname.Set.empty; children = Procname.Set.empty; ancestors = None; @@ -63,8 +68,11 @@ let _add_node g n defined = in_out_calls = None } in Procname.Hash.add g.node_map n info -let add_node g n = - _add_node g n true +let add_defined_node g n = + _add_node g n true false + +let add_disabled_node g n = + _add_node g n false true (** Compute the ancestors of the node, if not already computed *) let compute_ancestors g node = @@ -147,8 +155,8 @@ let node_set_defined (g: t) n defined = with Not_found -> () let add_edge g nfrom nto = - _add_node g nfrom false; - _add_node g nto false; + _add_node g nfrom false false; + _add_node g nto false false; let info_from = Procname.Hash.find g.node_map nfrom in let info_to = Procname.Hash.find g.node_map nto in info_from.children <- Procname.Set.add nto info_from.children; @@ -161,13 +169,18 @@ let node_map_iter f g = let cmp ((n1: Procname.t), _) ((n2: Procname.t), _) = Procname.compare n1 n2 in list_iter (fun (n, info) -> f n info) (list_sort cmp !table) -(** if not None, restrict defined nodes to the given set *) +(** If not None, restrict defined nodes to the given set, + and mark them as disabled. *) let restrict_defined (g: t) (nodeset_opt: Procname.Set.t option) = match nodeset_opt with | None -> () | Some nodeset -> let f node info = - if not (Procname.Set.mem node nodeset) then info.defined <- false in + if info.defined && not (Procname.Set.mem node nodeset) then + begin + info.defined <- false; + info.disabled <- true + end in node_map_iter f g let get_nodes (g: t) = @@ -269,16 +282,18 @@ let get_nodes_and_defined_children (g: t) = let nodes_list = Procname.Set.elements !nodes in list_map (fun n -> (n, get_defined_children g n)) nodes_list -type nodes_and_edges = (node * bool) list * (node * node) list +type nodes_and_edges = + (node * bool * bool) list * (* nodes with defined and disabled flag *) + (node * node) list (* edges *) -(** Return the list of nodes, with defined flag, and the list of edges *) +(** Return the list of nodes, with defined+disabled flags, and the list of edges *) let get_nodes_and_edges (g: t) : nodes_and_edges = let nodes = ref [] in let edges = ref [] in let do_children node info nto = edges := (node, nto) :: !edges in let f node info = - nodes := (node, info.defined) :: !nodes; + nodes := (node, info.defined, info.disabled) :: !nodes; Procname.Set.iter (do_children node info) info.children in node_map_iter f g; (!nodes, !edges) @@ -286,7 +301,21 @@ let get_nodes_and_edges (g: t) : nodes_and_edges = (** Return the list of nodes which are defined *) let get_defined_nodes (g: t) = let (nodes, _) = get_nodes_and_edges g in - list_map fst (list_filter (fun pair -> snd pair) nodes) + let get_node (node, _, _) = node in + list_map get_node + (list_filter (fun (_, defined, _) -> defined) + nodes) + + +(** Return the list of nodes which were originally defined, + i.e. the nodes that were defined before calling restrict_defined. *) +let get_originally_defined_nodes (g: t) = + let (nodes, _) = get_nodes_and_edges g in + let get_node (node, _, _) = node in + list_map get_node + (list_filter + (fun (_, defined, disabled) -> defined || disabled) + nodes) (** Return the path of the source file *) let get_source (g: t) = @@ -299,7 +328,7 @@ let get_nLOC (g: t) = (** [extend cg1 gc2] extends [cg1] in place with nodes and edges from [gc2]; undefined nodes become defined if at least one side is. *) let extend cg_old cg_new = let nodes, edges = get_nodes_and_edges cg_new in - list_iter (fun (node, defined) -> _add_node cg_old node defined) nodes; + list_iter (fun (node, defined, disabled) -> _add_node cg_old node defined disabled) nodes; list_iter (fun (nfrom, nto) -> add_edge cg_old nfrom nto) edges (** Begin support for serialization *) @@ -312,7 +341,11 @@ let load_from_file (filename : DB.filename) : t option = match Serialization.from_file callgraph_serializer filename with | None -> None | Some (source, nLOC, (nodes, edges)) -> - list_iter (fun (node, defined) -> if defined then add_node g node) nodes; + list_iter + (fun (node, defined, disabled) -> + if defined then add_defined_node g node; + if disabled then add_disabled_node g node) + nodes; list_iter (fun (nfrom, nto) -> add_edge g nfrom nto) edges; g.source <- source; g.nLOC <- nLOC; diff --git a/infer/src/backend/cg.mli b/infer/src/backend/cg.mli index 34837e495..b99e1baa3 100644 --- a/infer/src/backend/cg.mli +++ b/infer/src/backend/cg.mli @@ -21,34 +21,94 @@ type t (** the type of a call graph *) (** A call graph consists of a set of nodes (Procname.t), and edges between them. A node can be defined or undefined (to represent whether we have code for it). - In an edge from [n1] to [n2], indicating that [n1] calls [n2], [n1] is the parent and [n2] is the child. - Node [n1] is dependent on [n2] if there is a path from [n1] to [n2] using the child relationship. *) + In an edge from [n1] to [n2], indicating that [n1] calls [n2], + [n1] is the parent and [n2] is the child. + Node [n1] is dependent on [n2] if there is a path from [n1] to [n2] + using the child relationship. *) -(** [add_edge cg f t] adds an edge from [f] to [t] in the call graph [cg]. The nodes are also added as undefined, unless already present. *) +(** [add_edge cg f t] adds an edge from [f] to [t] in the call graph [cg]. + The nodes are also added as undefined, unless already present. *) val add_edge : t -> Procname.t -> Procname.t -> unit -val add_node : t -> Procname.t -> unit (** Add a node to the call graph as defined *) -val calls_recursively: t -> Procname.t -> Procname.t -> bool (** [calls_recursively g source dest] returns [true] if function [source] recursively calls function [dest] *) -val create : unit -> t (** Create an empty call graph *) -val extend : t -> t -> unit (** [extend cg1 gc2] extends [cg1] in place with nodes and edges from [gc2]; undefined nodes become defined if at least one side is. *) -val get_all_children : t -> Procname.t -> Procname.Set.t (** Return all the children of [n], whether defined or not *) -val get_ancestors : t -> Procname.t -> Procname.Set.t (** Compute the ancestors of the node, if not pre-computed already *) -val get_heirs : t -> Procname.t -> Procname.Set.t (** Compute the heirs of the node, if not pre-computed already *) -val get_calls : t -> Procname.t -> in_out_calls (** Return the in/out calls of the node *) -val get_defined_nodes : t -> Procname.t list (** Return the list of nodes which are defined *) -val get_defined_children: t -> Procname.t -> Procname.Set.t (** Return the children of [n] which are defined *) -val get_dependents: t -> Procname.t -> Procname.Set.t (** Return the nodes dependent on [n] *) -val get_nLOC: t -> int (** Return the number of LOC of the source file *) -val get_nodes_and_calls : t -> (Procname.t * in_out_calls) list (** Return the list of nodes with calls *) -val get_nodes_and_defined_children : t -> (Procname.t * Procname.Set.t) list (** Return all the nodes with their defined children *) -val get_nodes_and_edges : t -> (Procname.t * bool) list * (Procname.t * Procname.t) list (** Return the list of nodes, with defined flag, and the list of edges *) -val get_nonrecursive_dependents : t -> Procname.t -> Procname.Set.t (** Return the children of [n] which are not heirs of [n] and are defined *) -val get_parents : t -> Procname.t -> Procname.Set.t (** Return the parents of [n] *) -val get_recursive_dependents: t -> Procname.t -> Procname.Set.t (** Return the ancestors of [n] which are also heirs of [n] *) -val get_source : t -> DB.source_file (** Return the path of the source file *) -val load_from_file : DB.filename -> t option (** Load a call graph from a file *) -val node_defined : t -> Procname.t -> bool (** Returns true if the node is defined *) -val restrict_defined : t -> Procname.Set.t option -> unit (** if not None, restrict defined nodes to the given set *) -val save_call_graph_dotty : DB.filename option -> (Procname.t -> 'a list) -> t -> unit (** Print the current call graph as a dotty file. If the filename is [None], use the current file dir inside the DB dir. *) -val store_to_file : DB.filename -> t -> unit (** Save a call graph into a file *) -val node_set_defined : t -> Procname.t -> bool -> unit (** Change the defined flag of a node *) +(** Add a node to the call graph as defined *) +val add_defined_node : t -> Procname.t -> unit + +(** [calls_recursively g source dest] returns [true] if function [source] + recursively calls function [dest] *) +val calls_recursively: t -> Procname.t -> Procname.t -> bool + +(** Create an empty call graph *) +val create : unit -> t + +(** [extend cg1 gc2] extends [cg1] in place with nodes and edges from [gc2]; + undefined nodes become defined if at least one side is. *) +val extend : t -> t -> unit + +(** Return all the children of [n], whether defined or not *) +val get_all_children : t -> Procname.t -> Procname.Set.t + +(** Compute the ancestors of the node, if not pre-computed already *) +val get_ancestors : t -> Procname.t -> Procname.Set.t + +(** Compute the heirs of the node, if not pre-computed already *) +val get_heirs : t -> Procname.t -> Procname.Set.t + +(** Return the in/out calls of the node *) +val get_calls : t -> Procname.t -> in_out_calls + +(** Return the list of nodes which are defined *) +val get_defined_nodes : t -> Procname.t list + +(** Return the list of nodes which were originally defined, + i.e. the nodes that were defined before calling restrict_defined. *) +val get_originally_defined_nodes : t -> Procname.t list + +(** Return the children of [n] which are defined *) +val get_defined_children: t -> Procname.t -> Procname.Set.t + +(** Return the nodes dependent on [n] *) +val get_dependents: t -> Procname.t -> Procname.Set.t + +(** Return the number of LOC of the source file *) +val get_nLOC: t -> int + +(** Return the list of nodes with calls *) +val get_nodes_and_calls : t -> (Procname.t * in_out_calls) list + +(** Return all the nodes with their defined children *) +val get_nodes_and_defined_children : t -> (Procname.t * Procname.Set.t) list + +(** Return the list of nodes, with defined+disabled flag, and the list of edges *) +val get_nodes_and_edges : t -> (Procname.t * bool * bool) list * (Procname.t * Procname.t) list + +(** Return the children of [n] which are not heirs of [n] and are defined *) +val get_nonrecursive_dependents : t -> Procname.t -> Procname.Set.t + +(** Return the parents of [n] *) +val get_parents : t -> Procname.t -> Procname.Set.t + +(** Return the ancestors of [n] which are also heirs of [n] *) +val get_recursive_dependents: t -> Procname.t -> Procname.Set.t + +(** Return the path of the source file *) +val get_source : t -> DB.source_file + +(** Load a call graph from a file *) +val load_from_file : DB.filename -> t option + +(** Returns true if the node is defined *) +val node_defined : t -> Procname.t -> bool + +(** If not None, restrict defined nodes to the given set, + and mark them as disabled. *) +val restrict_defined : t -> Procname.Set.t option -> unit + +(** Print the current call graph as a dotty file. If the filename is [None], + use the current file dir inside the DB dir. *) +val save_call_graph_dotty : DB.filename option -> (Procname.t -> 'a list) -> t -> unit + +(** Save a call graph into a file *) +val store_to_file : DB.filename -> t -> unit + +(** Change the defined flag of a node *) +val node_set_defined : t -> Procname.t -> bool -> unit diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index 32343846d..b4070eb69 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -477,9 +477,9 @@ let compute_clusters exe_env files_changed : Cluster.t list = let global_cg = Exe_env.get_cg exe_env in let nodes, edges = Cg.get_nodes_and_edges global_cg in let defined_procs = Cg.get_defined_nodes global_cg in - let do_node (n, defined) = + let do_node (n, defined, restricted) = if defined then - Cg.add_node file_cg + Cg.add_defined_node file_cg (ClusterMakefile.source_file_to_pname (Exe_env.get_source exe_env n)) in let do_edge (n1, n2) = if Cg.node_defined global_cg n1 && Cg.node_defined global_cg n2 then diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 5d32a0da7..a1ea724ff 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1266,7 +1266,7 @@ let do_analysis exe_env = let summaryfp = analyze_proc exe_env proc_name in Specs.add_summary proc_name summaryfp; let cg = Cg.create () in - Cg.add_node cg proc_name; + Cg.add_defined_node cg proc_name; perform_transition exe_env cg proc_name; let summaryre = analyze_proc exe_env proc_name in Specs.add_summary proc_name summaryre; diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 7bd7c9e3a..7c0227c1d 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -87,7 +87,7 @@ let do_analysis curr_pdesc proc_name = Some (Cfg.Procdesc.get_attributes proc_desc) in let call_graph = let cg = Cg.create () in - Cg.add_node cg proc_name; + Cg.add_defined_node cg proc_name; cg in Specs.reset_summary call_graph proc_name attributes_opt; Specs.set_status proc_name Specs.ACTIVE in diff --git a/infer/src/backend/type_prop.ml b/infer/src/backend/type_prop.ml index bbdbc3fab..7cc3f7320 100644 --- a/infer/src/backend/type_prop.ml +++ b/infer/src/backend/type_prop.ml @@ -739,7 +739,7 @@ let initialize_map exe_env methods = let collect_methods exe_env = let global_cg = Exe_env.get_cg exe_env in let nodes, edges = Cg.get_nodes_and_edges global_cg in - let do_node (n, defined) defined_methods = + let do_node (n, defined, restricted) defined_methods = if defined then Procname.Set.add n defined_methods else defined_methods in diff --git a/infer/src/clang/cMethod_decl.ml b/infer/src/clang/cMethod_decl.ml index bd7d89334..6c03be0df 100644 --- a/infer/src/clang/cMethod_decl.ml +++ b/infer/src/clang/cMethod_decl.ml @@ -58,7 +58,7 @@ struct let meth_body_nodes = T.instructions_trans context instrs extra_instrs exit_node in Cfg.Node.add_locals_ret_declaration start_node (Cfg.Procdesc.get_locals procdesc); Cfg.Node.set_succs_exn start_node meth_body_nodes []; - Cg.add_node (CContext.get_cg context) (Cfg.Procdesc.get_proc_name procdesc)) + Cg.add_defined_node (CContext.get_cg context) (Cfg.Procdesc.get_proc_name procdesc)) | None -> ()) with | Not_found -> () diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index 34f3731ef..d147574a5 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -252,7 +252,7 @@ let write_harness_to_file harness_instrs harness_file = (** add the harness proc to the cg and make sure its callees can be looked up by sym execution *) let add_harness_to_cg harness_name harness_cfg harness_node loc cg tenv = - Cg.add_node cg harness_name; + Cg.add_defined_node cg harness_name; let create_dummy_procdesc proc_name = (* convert a java type string to a type *) let rec lookup_typ typ_str = match typ_str with diff --git a/infer/src/java/jFrontend.ml b/infer/src/java/jFrontend.ml index 5b53ae7f7..9b3fdb5dd 100644 --- a/infer/src/java/jFrontend.ml +++ b/infer/src/java/jFrontend.ml @@ -100,7 +100,7 @@ let add_cmethod never_null_matcher program icfg node cm is_static = let method_body_nodes = Array.mapi (JTrans.instruction context) instrs in let procname = Cfg.Procdesc.get_proc_name procdesc in add_edges context start_node exn_node [exit_node] method_body_nodes impl false; - Cg.add_node icfg.JContext.cg procname; + Cg.add_defined_node icfg.JContext.cg procname; if Procname.is_constructor procname then Cfg.set_procname_priority cfg procname | JTrans.Called _ -> () @@ -115,7 +115,7 @@ let add_amethod program icfg node am is_static = (* do not capture the method if there is a model for it *) JUtils.log "Skipping method with a model: %s@." (Procname.to_string (Cfg.Procdesc.get_proc_name procdesc)); | JTrans.Defined procdesc -> - Cg.add_node icfg.JContext.cg (Cfg.Procdesc.get_proc_name procdesc) + Cg.add_defined_node icfg.JContext.cg (Cfg.Procdesc.get_proc_name procdesc) | JTrans.Called _ -> () diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index b3c23a160..04d536221 100644 --- a/infer/src/llvm/lTrans.ml +++ b/infer/src/llvm/lTrans.ml @@ -156,7 +156,7 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map) Cfg.Procdesc.set_exit_node procdesc exit_node; link_nodes start_node nodes; Cfg.Node.add_locals_ret_declaration start_node locals; - Cg.add_node cg proc_name; + Cg.add_defined_node cg proc_name; list_iter (Cg.add_edge cg proc_name) (callees_of_function_def func_def) let trans_program : LAst.program -> Cfg.cfg * Cg.t * Sil.tenv = function