Paths.Path.iter_all_nodes_no_calls -> fold

Summary: Keep removing refs...

Reviewed By: jvillard

Differential Revision: D8235834

fbshipit-source-id: 3713b37
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent a5b8093c42
commit d65cee3017

@ -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

@ -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)

@ -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

@ -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 _ ->

Loading…
Cancel
Save