From d65cee30179d1c673ebe6544765e802a0f3ddbf9 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Fri, 1 Jun 2018 08:52:13 -0700 Subject: [PATCH] Paths.Path.iter_all_nodes_no_calls -> fold Summary: Keep removing refs... Reviewed By: jvillard Differential Revision: D8235834 fbshipit-source-id: 3713b37 --- infer/src/biabduction/Buckets.ml | 10 +++++----- infer/src/biabduction/Paths.ml | 23 ++++++++++++++--------- infer/src/biabduction/Paths.mli | 4 ++-- infer/src/biabduction/interproc.ml | 20 +++++++++----------- 4 files changed, 30 insertions(+), 27 deletions(-) diff --git a/infer/src/biabduction/Buckets.ml b/infer/src/biabduction/Buckets.ml index 37b0e4e58..e7294a22d 100644 --- a/infer/src/biabduction/Buckets.ml +++ b/infer/src/biabduction/Buckets.ml @@ -112,16 +112,16 @@ let check_access access_opt de_opt = in Instrs.exists ~f:filter (Procdesc.Node.get_instrs node) in - let local_access_found = ref false in - let do_node node = + let do_node local_access_found node = if Int.equal (Procdesc.Node.get_loc node).Location.line line_number && has_call_or_sets_null node - then local_access_found := true + then true + else local_access_found in let path, pos_opt = State.get_path () in - Paths.Path.iter_all_nodes_nocalls do_node path ; - if !local_access_found then + let local_access_found = Paths.Path.fold_all_nodes_nocalls path ~init:false ~f:do_node in + if local_access_found then let bucket = if null_case_flag then Localise.BucketLevel.b5 else if check_nested_loop path pos_opt then Localise.BucketLevel.b3 diff --git a/infer/src/biabduction/Paths.ml b/infer/src/biabduction/Paths.ml index 4f3fe0133..db4d681b2 100644 --- a/infer/src/biabduction/Paths.ml +++ b/infer/src/biabduction/Paths.ml @@ -48,8 +48,8 @@ module Path : sig val add_description : t -> string -> t (** extend a path with a new node reached from the given session, with an optional string for exceptions *) - val iter_all_nodes_nocalls : (Procdesc.Node.t -> unit) -> t -> unit - (** iterate over each node in the path, excluding calls, once *) + val fold_all_nodes_nocalls : (t, Procdesc.Node.t, 'accum) Container.fold + (** fold over each node in the path, excluding calls, once *) val iter_shortest_sequence : (int -> t -> int -> Typ.Name.t option -> unit) -> PredSymb.path_pos option -> t -> unit @@ -251,10 +251,16 @@ end = struct end (* End of module Invariant *) - (** iterate over each node in the path, excluding calls, once *) - let iter_all_nodes_nocalls f path = - Invariant.compute_stats false (fun node -> f node ; true) path ; - Invariant.reset_stats path + (** fold over each node in the path, excluding calls, once *) + let fold_all_nodes_nocalls path ~init ~f = + let acc = ref init in + Invariant.compute_stats false + (fun node -> + acc := f !acc node ; + true ) + path ; + Invariant.reset_stats path ; + !acc let get_path_pos node = @@ -647,9 +653,8 @@ end = struct (** check if the nodes in path p1 are a subset of those in p2 (not trace subset) *) let path_nodes_subset p1 p2 = let get_nodes p = - let s = ref Procdesc.NodeSet.empty in - Path.iter_all_nodes_nocalls (fun n -> s := Procdesc.NodeSet.add n !s) p ; - !s + Path.fold_all_nodes_nocalls p ~init:Procdesc.NodeSet.empty ~f:(fun s n -> + Procdesc.NodeSet.add n s ) in Procdesc.NodeSet.subset (get_nodes p1) (get_nodes p2) diff --git a/infer/src/biabduction/Paths.mli b/infer/src/biabduction/Paths.mli index 3b19b2b6a..58d0e3ae5 100644 --- a/infer/src/biabduction/Paths.mli +++ b/infer/src/biabduction/Paths.mli @@ -42,8 +42,8 @@ module Path : sig val add_description : t -> string -> t - val iter_all_nodes_nocalls : (Procdesc.Node.t -> unit) -> t -> unit - (** iterate over each node in the path, excluding calls, once *) + val fold_all_nodes_nocalls : (t, Procdesc.Node.t, 'accum) Container.fold + (** fold over each node in the path, excluding calls, once *) val iter_shortest_sequence : (int -> t -> int -> Typ.Name.t option -> unit) -> PredSymb.path_pos option -> t -> unit diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index bc2ec5fd7..3777d543d 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -542,12 +542,12 @@ module Pmap = Caml.Map.Make (struct let compare = Prop.compare_prop end) -let vset_ref_add_path vset_ref path = - Paths.Path.iter_all_nodes_nocalls (fun n -> vset_ref := Procdesc.NodeSet.add n !vset_ref) path +let vset_add_path vset path = + Paths.Path.fold_all_nodes_nocalls path ~init:vset ~f:(fun vset n -> Procdesc.NodeSet.add n vset) -let vset_ref_add_pathset vset_ref pathset = - Paths.PathSet.iter (fun _ path -> vset_ref_add_path vset_ref path) pathset +let vset_add_pathset vset pathset = + Paths.PathSet.fold (fun _ path vset -> vset_add_path vset path) pathset vset let compute_visited vset = @@ -594,9 +594,8 @@ let extract_specs tenv pdesc pathset : Prop.normal BiabductionSummary.spec list else Some (Prop.normalize tenv (Prop.prop_sub (`Exp sub) post), path) in let visited = - let vset_ref = ref Procdesc.NodeSet.empty in - vset_ref_add_path vset_ref path ; - compute_visited !vset_ref + let vset = vset_add_path Procdesc.NodeSet.empty path in + compute_visited vset in (pre', post', visited) in @@ -659,11 +658,10 @@ let collect_postconditions wl tenv proc_cfg : Paths.PathSet.t * BiabductionSumma let pathset = collect_do_abstract_post pname tenv pathset in let pathset_diverging = State.get_diverging_states_proc () in let visited = - let vset_ref = ref Procdesc.NodeSet.empty in - vset_ref_add_pathset vset_ref pathset ; + let vset = vset_add_pathset Procdesc.NodeSet.empty pathset in (* nodes from diverging states were also visited *) - vset_ref_add_pathset vset_ref pathset_diverging ; - compute_visited !vset_ref + let vset = vset_add_pathset vset pathset_diverging in + compute_visited vset in (do_join_post pname tenv pathset, visited) with Exceptions.Leak _ ->