From 92c129dc4e84846baee24b2a6d410cf87146548e Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 17 May 2018 03:47:06 -0700 Subject: [PATCH] [cfg] rename `Cfg.is_proc_cfg_connected` to `Procdesc.is_connected` Summary: Moving this function since it's about a single procdesc. Slight rewrite too. Reviewed By: da319 Differential Revision: D8030494 fbshipit-source-id: f7cc58e --- infer/src/IR/Cfg.ml | 65 ------------------------------- infer/src/IR/Cfg.mli | 3 -- infer/src/IR/Procdesc.ml | 65 +++++++++++++++++++++++++++++++ infer/src/IR/Procdesc.mli | 6 ++- infer/src/clang/cFrontend_decl.ml | 6 +-- 5 files changed, 72 insertions(+), 73 deletions(-) diff --git a/infer/src/IR/Cfg.ml b/infer/src/IR/Cfg.ml index eb5021fc5..7e08d94de 100644 --- a/infer/src/IR/Cfg.ml +++ b/infer/src/IR/Cfg.ml @@ -53,71 +53,6 @@ let iter_all_nodes ?(sorted= false) cfg ~f = |> List.iter ~f:(fun (_, d, n) -> f d n) -let proc_cfg_broken_for_node proc_desc = - let is_exit_node n = - match Procdesc.Node.get_kind n with Procdesc.Node.Exit_node _ -> true | _ -> false - in - let is_between_join_and_exit_node n = - match Procdesc.Node.get_kind n with - | Procdesc.Node.Stmt_node "between_join_and_exit" | Procdesc.Node.Stmt_node "Destruction" -> ( - match Procdesc.Node.get_succs n with [n'] when is_exit_node n' -> true | _ -> false ) - | _ -> - false - in - let rec is_consecutive_join_nodes n visited = - match Procdesc.Node.get_kind n with - | Procdesc.Node.Join_node - -> ( - if Procdesc.NodeSet.mem n visited then false - else - let succs = Procdesc.Node.get_succs n in - match succs with - | [n'] -> - is_consecutive_join_nodes n' (Procdesc.NodeSet.add n visited) - | _ -> - false ) - | _ -> - is_between_join_and_exit_node n - in - let find_broken_node n = - let succs = Procdesc.Node.get_succs n in - let preds = Procdesc.Node.get_preds n in - match Procdesc.Node.get_kind n with - | Procdesc.Node.Start_node _ -> - if List.is_empty succs || not (List.is_empty preds) then Some `Other else None - | Procdesc.Node.Exit_node _ -> - if not (List.is_empty succs) || List.is_empty preds then Some `Other else None - | Procdesc.Node.Stmt_node _ | Procdesc.Node.Prune_node _ | Procdesc.Node.Skip_node _ -> - if List.is_empty succs || List.is_empty preds then Some `Other else None - | Procdesc.Node.Join_node -> - (* Join node has the exception that it may be without predecessors - and pointing to between_join_and_exit which points to an exit node. - This happens when the if branches end with a return. - Nested if statements, where all branches have return statements, - introduce a sequence of join nodes *) - if - (List.is_empty preds && not (is_consecutive_join_nodes n Procdesc.NodeSet.empty)) - || (not (List.is_empty preds) && List.is_empty succs) - then Some `Join - else None - in - let rec find_first_broken nodes res_broken_node = - match nodes with - | [] -> - res_broken_node - | n :: nodes' -> - let broken_node = find_broken_node n in - match broken_node with - | None -> - find_first_broken nodes' res_broken_node - | Some `Join -> - find_first_broken nodes' broken_node - | Some `Other -> - broken_node - in - find_first_broken (Procdesc.get_nodes proc_desc) None - - let load_statement = ResultsDatabase.register_statement "SELECT cfgs FROM source_files WHERE source_file = :k" diff --git a/infer/src/IR/Cfg.mli b/infer/src/IR/Cfg.mli index 4d1781676..c4d0d3a98 100644 --- a/infer/src/IR/Cfg.mli +++ b/infer/src/IR/Cfg.mli @@ -32,9 +32,6 @@ val create_proc_desc : t -> ProcAttributes.t -> Procdesc.t val iter_all_nodes : ?sorted:bool -> t -> f:(Procdesc.t -> Procdesc.Node.t -> unit) -> unit (** Iterate over all the nodes in the cfg *) -val proc_cfg_broken_for_node : Procdesc.t -> [`Join | `Other] option -(** checks whether a cfg for the given procdesc is connected or not *) - val save_attributes : SourceFile.t -> t -> unit (** Save the .attr files for the procedures in the cfg. *) diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 641a528b8..d3d577116 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -815,3 +815,68 @@ let specialize_with_block_args callee_pdesc pname_with_block_args block_args = "signature of specialized method %a@." pp_signature resolved_pdesc ; convert_cfg ~callee_pdesc ~resolved_pdesc ~f_instr_list:(specialize_with_block_args_instrs resolved_pdesc substitutions) + + +let is_connected proc_desc = + let is_exit_node n = match Node.get_kind n with Node.Exit_node _ -> true | _ -> false in + let is_between_join_and_exit_node n = + match Node.get_kind n with + | Node.Stmt_node "between_join_and_exit" | Node.Stmt_node "Destruction" -> ( + match Node.get_succs n with [n'] when is_exit_node n' -> true | _ -> false ) + | _ -> + false + in + let rec is_consecutive_join_nodes n visited = + match Node.get_kind n with + | Node.Join_node + -> ( + if NodeSet.mem n visited then false + else + let succs = Node.get_succs n in + match succs with + | [n'] -> + is_consecutive_join_nodes n' (NodeSet.add n visited) + | _ -> + false ) + | _ -> + is_between_join_and_exit_node n + in + let find_broken_node n = + let succs = Node.get_succs n in + let preds = Node.get_preds n in + match Node.get_kind n with + | Node.Start_node _ -> + if List.is_empty succs || not (List.is_empty preds) then Error `Other else Ok () + | Node.Exit_node _ -> + if not (List.is_empty succs) || List.is_empty preds then Error `Other else Ok () + | Node.Stmt_node _ | Node.Prune_node _ | Node.Skip_node _ -> + if List.is_empty succs || List.is_empty preds then Error `Other else Ok () + | Node.Join_node -> + (* Join node has the exception that it may be without predecessors + and pointing to between_join_and_exit which points to an exit node. + This happens when the if branches end with a return. + Nested if statements, where all branches have return statements, + introduce a sequence of join nodes *) + if + (List.is_empty preds && not (is_consecutive_join_nodes n NodeSet.empty)) + || (not (List.is_empty preds) && List.is_empty succs) + then Error `Join + else Ok () + in + (* unconnected nodes generated by Join nodes are expected *) + let skip_join_errors current_status node = + match find_broken_node node with + | Ok () -> + Ok current_status + | Error `Join -> + Ok (Some `Join) + | Error _ as other_error -> + other_error + in + match List.fold_result (get_nodes proc_desc) ~init:None ~f:skip_join_errors with + | Ok (Some `Join) -> + Error `Join + | Ok None -> + Ok () + | Error _ as error -> + error diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index b89b1dd0d..adefb9965 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -211,9 +211,8 @@ val pp_local : Format.formatter -> ProcAttributes.var_data -> unit val is_specialized : t -> bool -(* true if pvar is a captred variable of a cpp lambda or obcj block *) - val is_captured_var : t -> Pvar.t -> bool +(** true if pvar is a captured variable of a cpp lambda or obcj block *) val has_modify_in_block_attr : t -> Pvar.t -> bool @@ -229,3 +228,6 @@ val specialize_with_block_args : t -> Typ.Procname.t -> Exp.closure option list a) the block parameters are replaces with the closures b) the parameters of the method are extended with parameters for the captured variables in the closures *) + +val is_connected : t -> (unit, [`Join | `Other]) Result.t +(** checks whether a cfg for the given procdesc is connected or not *) diff --git a/infer/src/clang/cFrontend_decl.ml b/infer/src/clang/cFrontend_decl.ml index 2832f04f0..8c5228eeb 100644 --- a/infer/src/clang/cFrontend_decl.ml +++ b/infer/src/clang/cFrontend_decl.ml @@ -81,10 +81,10 @@ module CFrontend_decl_funct (T : CModule_type.CTranslation) : CModule_type.CFron Procdesc.Node.add_locals_ret_declaration start_node proc_attributes (Procdesc.get_locals procdesc) ; Procdesc.node_set_succs_exn procdesc start_node meth_body_nodes [] ; - match Cfg.proc_cfg_broken_for_node procdesc with - | None -> + match Procdesc.is_connected procdesc with + | Ok () -> () - | Some broken_node -> + | Error broken_node -> let lang = CFrontend_config.string_of_clang_lang trans_unit_ctx.CFrontend_config.lang in