diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 6ccf14bc0..7427226c6 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -751,7 +751,10 @@ let checker {Callbacks.tenv; proc_desc; integer_type_widths; summary} : Summary. (* computes reaching defs: node -> (var -> node set) *) let reaching_defs_invariant_map = ReachingDefs.compute_invariant_map proc_desc tenv in (* collect all prune nodes that occur in loop guards, needed for ControlDepAnalyzer *) - let control_maps, loop_head_to_loop_nodes = Loop_control.get_control_maps node_cfg in + let control_maps, loop_head_to_loop_nodes = + let loop_head_to_source_nodes_map = Loop_control.get_loop_head_to_source_nodes node_cfg in + Loop_control.get_control_maps loop_head_to_source_nodes_map + in (* computes the control dependencies: node -> var set *) let control_dep_invariant_map = Control.compute_invariant_map proc_desc tenv control_maps in (* compute loop invariant map for control var analysis *) diff --git a/infer/src/checkers/loop_control.ml b/infer/src/checkers/loop_control.ml index 69b7c16fa..3cc9f335a 100644 --- a/infer/src/checkers/loop_control.ml +++ b/infer/src/checkers/loop_control.ml @@ -72,9 +72,11 @@ let get_exit_nodes_in_loop loop_nodes = Control.GuardNodes.diff succs_of_loop_nodes loop_nodes |> Control.GuardNodes.elements -(* 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 *) +(** + 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 +*) let get_all_nodes_upwards_until target start_nodes = let rec aux found_nodes = function | [] -> @@ -92,9 +94,11 @@ let is_prune node = match Procdesc.Node.get_kind node with Procdesc.Node.Prune_node _ -> true | _ -> false -(* 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 *) +(** + 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 @@ -108,6 +112,10 @@ let remove_prune_node_pairs exit_nodes guard_nodes = |> Control.GuardNodes.union exit_nodes +(** + Since there could be multiple back-edges per loop, collect all source nodes per loop head. + loop_head (target of back-edges) --> source nodes +*) let get_loop_head_to_source_nodes cfg = get_back_edges cfg |> List.fold ~init:Procdesc.NodeMap.empty ~f:(fun loop_head_to_source_list {source; target} -> @@ -116,16 +124,14 @@ let get_loop_head_to_source_nodes cfg = loop_head_to_source_list ) -(* 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. *) -let get_control_maps cfg = - (* Since there could be multiple back-edges per loop, collect all - source nodes per loop head *) - (* loop_head (target of back-edges) --> source nodes *) - let loop_head_to_source_nodes_map = get_loop_head_to_source_nodes cfg in +(** + 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. +*) +let get_control_maps 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) -> @@ -174,7 +180,7 @@ let get_control_maps cfg = ( {exit_map= exit_map'; loop_head_to_guard_nodes= loop_head_to_guard_nodes'} , loop_head_to_loop_nodes' ) ) loop_head_to_source_nodes_map - ( (let open Control in - { exit_map= Control.ExitNodeToLoopHeads.empty - ; loop_head_to_guard_nodes= Control.LoopHeadToGuardNodes.empty }) + ( Control. + { exit_map= Control.ExitNodeToLoopHeads.empty + ; loop_head_to_guard_nodes= Control.LoopHeadToGuardNodes.empty } , LoopInvariant.LoopHeadToLoopNodes.empty ) diff --git a/infer/src/checkers/loop_control.mli b/infer/src/checkers/loop_control.mli new file mode 100644 index 000000000..a1700468f --- /dev/null +++ b/infer/src/checkers/loop_control.mli @@ -0,0 +1,32 @@ +(* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +val get_all_nodes_upwards_until : Procdesc.Node.t -> Procdesc.Node.t list -> Control.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 +*) + +val get_loop_head_to_source_nodes : Procdesc.t -> Procdesc.Node.t list Procdesc.NodeMap.t +(** + 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_control_maps : + Procdesc.Node.t list Procdesc.NodeMap.t + -> Control.loop_control_maps * Control.GuardNodes.t Procdesc.NodeMap.t +(** + 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. +*)