diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml index c0634f6e1..cb3a572e6 100644 --- a/infer/src/checkers/control.ml +++ b/infer/src/checkers/control.ml @@ -49,15 +49,14 @@ module LoopHeadToGuardNodes = Procdesc.NodeMap type loop_control_maps = { exit_map: LoopHeads.t ExitNodeToLoopHeads.t - ; loop_head_to_guard_nodes: GuardNodes.t LoopHeadToGuardNodes.t - ; nodes: Procdesc.Node.t list Lazy.t } + ; loop_head_to_guard_nodes: GuardNodes.t LoopHeadToGuardNodes.t } (* forward transfer function for control dependencies *) module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ControlDepSet - type analysis_data = loop_control_maps + type analysis_data = Procdesc.Node.t list * loop_control_maps let collect_vars_in_exp exp loop_head = Var.get_all_vars_in_exp exp @@ -90,27 +89,26 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct | Some deps -> ControlDepSet.union deps acc | None -> ( - (* the variables in the prone node do not appear in - predecessor nodes. This could happen if the variable - is defined in a dangling node due to a frontend - issue (when reading from a global variable). In that - case, we find that node among all the nodes of the - cfg and pick up the control variables. *) - let all_nodes = force nodes in - match - List.find_map all_nodes ~f:(fun node -> - if Procdesc.Node.is_dangling node then - let instrs = Procdesc.Node.get_instrs node in - Instrs.find_map instrs ~f:(find_vars_in_decl id loop_head prune_node) - else None ) - with - | Some deps -> - ControlDepSet.union deps acc - | None -> - L.internal_error - "Failed to get the definition of the control variable %a in exp %a \n" Ident.pp - id Exp.pp exp ; - acc ) ) + (* the variables in the prune node do not appear in + predecessor nodes. This could happen if the variable + is defined in a dangling node due to a frontend + issue (when reading from a global variable). In that + case, we find that node among all the nodes of the + cfg and pick up the control variables. *) + match + List.find_map nodes ~f:(fun node -> + if Procdesc.Node.is_dangling node then + let instrs = Procdesc.Node.get_instrs node in + Instrs.find_map instrs ~f:(find_vars_in_decl id loop_head prune_node) + else None ) + with + | Some deps -> + ControlDepSet.union deps acc + | None -> + L.internal_error + "Failed to get the definition of the control variable %a in exp %a \n" Ident.pp + id Exp.pp exp ; + acc ) ) (* extract vars from the prune instructions in the node *) @@ -135,7 +133,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct along with the loop header that CV is originating from - a loop exit node, remove control variables of its guard nodes This is correct because the CVs are only going to be temporaries. *) - let exec_instr astate {exit_map; nodes; loop_head_to_guard_nodes} (node : CFG.Node.t) _ = + let exec_instr astate (nodes, {exit_map; loop_head_to_guard_nodes}) (node : CFG.Node.t) _ = let node = CFG.Node.underlying_node node in let astate' = match LoopHeadToGuardNodes.find_opt node loop_head_to_guard_nodes with @@ -179,7 +177,9 @@ type invariant_map = ControlDepAnalyzer.invariant_map let compute_invariant_map proc_desc control_maps : invariant_map = let node_cfg = CFG.from_pdesc proc_desc in - ControlDepAnalyzer.exec_cfg node_cfg control_maps ~initial:ControlDepSet.empty + ControlDepAnalyzer.exec_cfg node_cfg + (Procdesc.get_nodes proc_desc, control_maps) + ~initial:ControlDepSet.empty (* Filter CVs which are invariant in the loop where the CV originated from *) diff --git a/infer/src/checkers/control.mli b/infer/src/checkers/control.mli index 4bb0df3b0..dc7df0fdb 100644 --- a/infer/src/checkers/control.mli +++ b/infer/src/checkers/control.mli @@ -24,8 +24,7 @@ type invariant_map type loop_control_maps = { exit_map: LoopHeads.t ExitNodeToLoopHeads.t - ; loop_head_to_guard_nodes: GuardNodes.t LoopHeadToGuardNodes.t - ; nodes: Procdesc.Node.t list Lazy.t } + ; loop_head_to_guard_nodes: GuardNodes.t LoopHeadToGuardNodes.t } val compute_invariant_map : Procdesc.t -> loop_control_maps -> invariant_map diff --git a/infer/src/checkers/inefficientKeysetIterator.ml b/infer/src/checkers/inefficientKeysetIterator.ml index ea795d7cd..f41307ac6 100644 --- a/infer/src/checkers/inefficientKeysetIterator.ml +++ b/infer/src/checkers/inefficientKeysetIterator.ml @@ -104,7 +104,9 @@ let when_dominating_preds_satisfy idom my_node ~fun_name ~class_name_f ~f = let checker {IntraproceduralAnalysis.proc_desc; tenv; err_log} = let cfg = CFG.from_pdesc proc_desc in - let _, loop_head_to_loop_nodes = Loop_control.get_loop_control_maps cfg in + let loop_head_to_loop_nodes = + Loop_control.(get_loop_head_to_source_nodes cfg |> get_loop_head_to_loop_nodes) + in let idom = Dominators.get_idoms proc_desc in Procdesc.NodeMap.iter (fun loop_head loop_nodes -> diff --git a/infer/src/checkers/loop_control.ml b/infer/src/checkers/loop_control.ml index 3f62650d2..c2bbbdf42 100644 --- a/infer/src/checkers/loop_control.ml +++ b/infer/src/checkers/loop_control.ml @@ -7,8 +7,7 @@ open! IStd module L = Logging - -let nid_int n = (Procdesc.Node.get_id n :> int) +open Control type edge_type = {source: Procdesc.Node.t; target: Procdesc.Node.t} [@@deriving compare] @@ -48,7 +47,7 @@ let get_back_edges pdesc = Visually: - target + target (loop head) /| / . / | @@ -64,12 +63,13 @@ let get_back_edges pdesc = Often, exit_node is a prune node. *) let get_exit_nodes_in_loop loop_nodes = let succs_of_loop_nodes = - Control.GuardNodes.fold + GuardNodes.fold (fun n acc -> - Procdesc.Node.get_succs n |> Control.GuardNodes.of_list |> Control.GuardNodes.union acc ) - loop_nodes Control.GuardNodes.empty + Procdesc.Node.get_succs n + |> List.fold ~init:acc ~f:(fun acc succ -> GuardNodes.add succ acc) ) + loop_nodes GuardNodes.empty in - Control.GuardNodes.diff succs_of_loop_nodes loop_nodes |> Control.GuardNodes.elements + GuardNodes.diff succs_of_loop_nodes loop_nodes (** Starting from the start_nodes, find all the nodes upwards until the target is reached, i.e @@ -79,12 +79,12 @@ let get_all_nodes_upwards_until target start_nodes = | [] -> found_nodes | node :: wl' -> - if Control.GuardNodes.mem node found_nodes then aux found_nodes wl' + if GuardNodes.mem node found_nodes then aux found_nodes wl' else let preds = Procdesc.Node.get_preds node in - aux (Control.GuardNodes.add node found_nodes) (List.append preds wl') + aux (GuardNodes.add node found_nodes) (List.append preds wl') in - aux (Control.GuardNodes.singleton target) start_nodes + aux (GuardNodes.singleton target) start_nodes let is_prune node = @@ -94,16 +94,14 @@ let is_prune node = (** Remove pairs of prune nodes that are for the same condition, i.e. sibling of the same parent. This is necessary to prevent picking unnecessary control variables in do-while like loops *) let remove_prune_node_pairs exit_nodes guard_nodes = - let exit_nodes = Control.GuardNodes.of_list exit_nodes in - let except_exit_nodes = Control.GuardNodes.diff guard_nodes exit_nodes in - L.(debug Analysis Medium) "Except exit nodes: [%a]\n" Control.GuardNodes.pp except_exit_nodes ; + let except_exit_nodes = GuardNodes.diff guard_nodes exit_nodes in + L.(debug Analysis Medium) "Except exit nodes: [%a]\n" GuardNodes.pp except_exit_nodes ; except_exit_nodes - |> Control.GuardNodes.filter (fun node -> + |> GuardNodes.filter (fun node -> is_prune node && Procdesc.Node.get_siblings node |> Sequence.hd - |> Option.value_map ~default:false ~f:(fun sibling -> - not (Control.GuardNodes.mem sibling except_exit_nodes) ) ) - |> Control.GuardNodes.union exit_nodes + |> Option.exists ~f:(fun sibling -> not (GuardNodes.mem sibling except_exit_nodes)) ) + |> GuardNodes.union exit_nodes (** Since there could be multiple back-edges per loop, collect all source nodes per loop head. @@ -120,63 +118,60 @@ let get_loop_head_to_source_nodes cfg = set (i.e. target of the back edges) loop_head_to_guard_map : loop_head -> guard_nodes and guard_nodes contains the nodes that may affect the looping behavior, i.e. occur in the guard of the loop conditional. *) -let get_control_maps pdesc loop_head_to_source_nodes_map = - let nodes = lazy (Procdesc.get_nodes pdesc) in +let get_control_maps loop_head_to_loop_nodes = + let acc = (ExitNodeToLoopHeads.empty, LoopHeadToGuardNodes.empty) in + let exit_map, loop_head_to_guard_nodes = + Procdesc.NodeMap.fold + (fun loop_head loop_nodes (exit_map, loop_head_to_guard_nodes) -> + let exit_nodes = get_exit_nodes_in_loop loop_nodes in + L.(debug Analysis Medium) "Exit nodes: [%a]\n" GuardNodes.pp exit_nodes ; + (* find all the prune nodes in the loop guard *) + let guard_prune_nodes = + get_all_nodes_upwards_until loop_head (GuardNodes.elements exit_nodes) + |> remove_prune_node_pairs exit_nodes + |> GuardNodes.filter is_prune + in + let exit_map' = + GuardNodes.fold + (fun exit_node exit_map_acc -> + ExitNodeToLoopHeads.update exit_node + (function + | Some existing_loop_heads -> + Some (LoopHeads.add loop_head existing_loop_heads) + | None -> + Some (LoopHeads.singleton loop_head) ) + exit_map_acc ) + exit_nodes exit_map + in + let loop_head_to_guard_nodes' = + LoopHeadToGuardNodes.update loop_head + (function + | Some existing_guard_nodes -> + Some (GuardNodes.union existing_guard_nodes guard_prune_nodes) + | None -> + Some guard_prune_nodes ) + loop_head_to_guard_nodes + in + (exit_map', loop_head_to_guard_nodes') ) + loop_head_to_loop_nodes acc + in + {exit_map; loop_head_to_guard_nodes} + + +let get_loop_head_to_loop_nodes loop_head_to_source_nodes_map = Procdesc.NodeMap.fold - (fun loop_head source_list - (Control.{exit_map; loop_head_to_guard_nodes}, loop_head_to_loop_nodes) -> - L.(debug Analysis Medium) - "Back-edge source list : [%a] --> loop_head: %i \n" (Pp.comma_seq Procdesc.Node.pp) - source_list (nid_int loop_head) ; + (fun loop_head source_list acc -> let loop_nodes = get_all_nodes_upwards_until loop_head source_list in - let exit_nodes = get_exit_nodes_in_loop loop_nodes in - L.(debug Analysis Medium) "Exit nodes: [%a]\n" (Pp.comma_seq Procdesc.Node.pp) exit_nodes ; - (* find all the prune nodes in the loop guard *) - let guard_prune_nodes = - get_all_nodes_upwards_until loop_head exit_nodes - |> remove_prune_node_pairs exit_nodes - |> Control.GuardNodes.filter is_prune - in - let exit_map' = - (List.fold_left ~init:exit_map ~f:(fun exit_map_acc exit_node -> - Control.ExitNodeToLoopHeads.update exit_node - (function - | Some existing_loop_heads -> - Some (Control.LoopHeads.add loop_head existing_loop_heads) - | None -> - Some (Control.LoopHeads.singleton loop_head) ) - exit_map_acc )) - exit_nodes - in - let loop_head_to_guard_nodes' = - Control.LoopHeadToGuardNodes.update loop_head - (function - | Some existing_guard_nodes -> - Some (Control.GuardNodes.union existing_guard_nodes guard_prune_nodes) - | None -> - Some guard_prune_nodes ) - loop_head_to_guard_nodes - in - let loop_head_to_loop_nodes' = - LoopInvariant.LoopHeadToLoopNodes.update loop_head - (function - | Some existing_loop_nodes -> - Some (LoopInvariant.LoopNodes.union existing_loop_nodes loop_nodes) - | None -> - Some loop_nodes ) - loop_head_to_loop_nodes - in - let open Control in - ( {exit_map= exit_map'; loop_head_to_guard_nodes= loop_head_to_guard_nodes'; nodes} - , loop_head_to_loop_nodes' ) ) - loop_head_to_source_nodes_map - ( Control. - { exit_map= Control.ExitNodeToLoopHeads.empty - ; loop_head_to_guard_nodes= Control.LoopHeadToGuardNodes.empty - ; nodes } - , LoopInvariant.LoopHeadToLoopNodes.empty ) - - -let get_loop_control_maps cfg = - let loop_head_to_source_nodes_map = get_loop_head_to_source_nodes cfg in - get_control_maps cfg loop_head_to_source_nodes_map + LoopInvariant.LoopHeadToLoopNodes.update loop_head + (function + | Some existing_loop_nodes -> + Some (LoopInvariant.LoopNodes.union existing_loop_nodes loop_nodes) + | None -> + Some loop_nodes ) + acc ) + loop_head_to_source_nodes_map LoopInvariant.LoopHeadToLoopNodes.empty + + +let get_loop_control_maps loop_head_to_source_nodes_map = + let loop_head_to_loop_nodes = get_loop_head_to_loop_nodes loop_head_to_source_nodes_map in + get_control_maps loop_head_to_loop_nodes diff --git a/infer/src/checkers/loop_control.mli b/infer/src/checkers/loop_control.mli index 230c84bcc..11104dce7 100644 --- a/infer/src/checkers/loop_control.mli +++ b/infer/src/checkers/loop_control.mli @@ -6,8 +6,9 @@ *) open! IStd +open Control -val get_all_nodes_upwards_until : Procdesc.Node.t -> Procdesc.Node.t list -> Control.GuardNodes.t +val get_all_nodes_upwards_until : Procdesc.Node.t -> Procdesc.Node.t list -> GuardNodes.t (** Starting from the start_nodes, find all the nodes upwards until the target is reached, i.e picking up predecessors which have not been already added to the found_nodes *) @@ -15,9 +16,12 @@ val get_loop_head_to_source_nodes : Procdesc.t -> Procdesc.Node.t list Procdesc. (** Since there could be multiple back-edges per loop, collect all source nodes per loop head. loop_head (target of back-edges) --> source nodes *) -val get_loop_control_maps : - Procdesc.t -> Control.loop_control_maps * Control.GuardNodes.t Procdesc.NodeMap.t +val get_loop_control_maps : Procdesc.Node.t list Procdesc.NodeMap.t -> loop_control_maps (** Get a pair of maps (exit_map, loop_head_to_guard_map) where exit_map : exit_node -> loop_head set (i.e. target of the back edges) loop_head_to_guard_map : loop_head -> guard_nodes and guard_nodes contains the nodes that may affect the looping behavior, i.e. occur in the guard of the loop conditional. *) + +val get_loop_head_to_loop_nodes : + Procdesc.Node.t list Procdesc.NodeMap.t -> GuardNodes.t LoopHeadToGuardNodes.t +(** Get a map from loop head -> all the nodes included in the corresponding loop *) diff --git a/infer/src/cost/cost.ml b/infer/src/cost/cost.ml index 5e25fb3be..184411f28 100644 --- a/infer/src/cost/cost.ml +++ b/infer/src/cost/cost.ml @@ -337,10 +337,27 @@ type bound_map = BasicCost.t Node.IdMap.t type get_node_nb_exec = Node.t -> BasicCost.t -let compute_bound_map node_cfg inferbo_invariant_map control_dep_invariant_map loop_invmap : - bound_map = +let compute_bound_map tenv proc_desc node_cfg inferbo_invariant_map analyze_dependency : bound_map = + (* computes reaching defs: node -> (var -> node set) *) + let reaching_defs_invariant_map = ReachingDefs.compute_invariant_map proc_desc in + (* collect all prune nodes that occur in loop guards, needed for ControlDepAnalyzer *) + let loop_head_to_source_nodes = Loop_control.get_loop_head_to_source_nodes node_cfg in + let control_maps = Loop_control.get_loop_control_maps loop_head_to_source_nodes in + (* computes the control dependencies: node -> var set *) + let control_dep_invariant_map = Control.compute_invariant_map proc_desc control_maps in + (* compute loop invariant map for control var analysis *) + let loop_head_to_loop_nodes = + Loop_control.get_loop_head_to_loop_nodes loop_head_to_source_nodes + in + let loop_inv_map = + let get_callee_purity callee_pname = + match analyze_dependency callee_pname with Some (_, (_, _, purity)) -> purity | _ -> None + in + LoopInvariant.get_loop_inv_var_map tenv get_callee_purity reaching_defs_invariant_map + loop_head_to_loop_nodes + in BoundMap.compute_upperbound_map node_cfg inferbo_invariant_map control_dep_invariant_map - loop_invmap + loop_inv_map let compute_get_node_nb_exec node_cfg bound_map : get_node_nb_exec = @@ -378,23 +395,9 @@ let checker ({InterproceduralAnalysis.proc_desc; exe_env; analyze_dependency} as (InterproceduralAnalysis.bind_payload ~f:snd3 analysis_data) in let node_cfg = NodeCFG.from_pdesc proc_desc in - (* computes reaching defs: node -> (var -> node set) *) - let reaching_defs_invariant_map = ReachingDefs.compute_invariant_map proc_desc in - (* collect all prune nodes that occur in loop guards, needed for ControlDepAnalyzer *) - let control_maps, loop_head_to_loop_nodes = Loop_control.get_loop_control_maps node_cfg in - (* computes the control dependencies: node -> var set *) - let control_dep_invariant_map = Control.compute_invariant_map proc_desc control_maps in - (* compute loop invariant map for control var analysis *) - let loop_inv_map = - let get_callee_purity callee_pname = - match analyze_dependency callee_pname with Some (_, (_, _, purity)) -> purity | _ -> None - in - LoopInvariant.get_loop_inv_var_map tenv get_callee_purity reaching_defs_invariant_map - loop_head_to_loop_nodes - in (* given the semantics computes the upper bound on the number of times a node could be executed *) let bound_map = - compute_bound_map node_cfg inferbo_invariant_map control_dep_invariant_map loop_inv_map + compute_bound_map tenv proc_desc node_cfg inferbo_invariant_map analyze_dependency in let is_on_ui_thread = (not (Procname.is_objc_method proc_name)) && ConcurrencyModels.runs_on_ui_thread tenv proc_name