From c5d7762f6092f4d9021f0416a64ba4cda1be8c2d Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 20 Mar 2017 10:03:43 -0700 Subject: [PATCH] [access trees] expose join of nodes and fold over nodes Reviewed By: mbouaziz Differential Revision: D4729701 fbshipit-source-id: 5fe27c9 --- infer/src/checkers/accessTree.ml | 36 +++++++++++++++++++---------- infer/src/checkers/accessTree.mli | 7 +++++- infer/src/quandary/TaintAnalysis.ml | 4 ++-- infer/src/unit/TaintTests.ml | 2 +- infer/src/unit/accessTreeTests.ml | 2 +- 5 files changed, 34 insertions(+), 17 deletions(-) diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index 58f0e5d9a..3207e2e09 100644 --- a/infer/src/checkers/accessTree.ml +++ b/infer/src/checkers/accessTree.ml @@ -44,7 +44,11 @@ module type S = sig val add_trace : AccessPath.t -> TraceDomain.astate -> t -> t - val fold : ('a -> AccessPath.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a + val node_join : node -> node -> node + + val fold : ('a -> AccessPath.t -> node -> 'a) -> t -> 'a -> 'a + + val trace_fold : ('a -> AccessPath.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a val pp_node : F.formatter -> node -> unit end @@ -149,7 +153,7 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct with Not_found -> false) lhs - let node_join f_node_merge f_trace_merge ((trace1, tree1) as node1) ((trace2, tree2) as node2) = + let node_join_ f_node_merge f_trace_merge ((trace1, tree1) as node1) ((trace2, tree2) as node2) = if phys_equal node1 node2 then node1 else @@ -177,10 +181,13 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct then node2 else trace'', Star - let rec node_merge node1_opt node2_opt = + let rec node_join node1 node2 = + node_join_ node_merge TraceDomain.join node1 node2 + + and node_merge node1_opt node2_opt = match node1_opt, node2_opt with | Some node1, Some node2 -> - let joined_node = node_join node_merge TraceDomain.join node1 node2 in + let joined_node = node_join node1 node2 in if phys_equal joined_node node1 then node1_opt else if phys_equal joined_node node2 @@ -201,7 +208,7 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct node_to_add | true, true -> (* adding x[_], do weak update on subtree and on its immediate trace *) - node_join node_merge TraceDomain.join node_to_add node + node_join node_to_add node | _ -> (* adding x.f* or x[_]*, join with traces of subtree and replace it with * *) let node_trace, node_tree = node_to_add in @@ -209,7 +216,7 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct make_starred_leaf (join_all_traces trace' node_tree) end | _, (_, Star) -> - node_join node_merge TraceDomain.join node_to_add node + node_join node_to_add node | access :: accesses, (trace, Subtree subtree) -> let access_node = try AccessMap.find access subtree @@ -245,21 +252,26 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct let rec access_map_fold_ f base accesses m acc = AccessMap.fold (fun access node acc -> node_fold_ f base (accesses @ [access]) node acc) m acc - and node_fold_ f base accesses (trace, tree) acc = + and node_fold_ f base accesses ((_, tree) as node) acc = let cur_ap_raw = base, accesses in match tree with | Subtree access_map -> - let acc' = f acc (AccessPath.Exact cur_ap_raw) trace in + let acc' = f acc (AccessPath.Exact cur_ap_raw) node in access_map_fold_ f base accesses access_map acc' | Star -> - f acc (AccessPath.Abstracted cur_ap_raw) trace + f acc (AccessPath.Abstracted cur_ap_raw) node - let node_fold (f : 'a -> AccessPath.t -> TraceDomain.astate -> 'a) base node acc = + let node_fold (f : 'a -> AccessPath.t -> node -> 'a) base node acc = node_fold_ f base [] node acc - let fold (f : 'a -> AccessPath.t -> TraceDomain.astate -> 'a) tree acc_ = + let fold (f : 'a -> AccessPath.t -> node -> 'a) tree acc_ = BaseMap.fold (fun base node acc -> node_fold f base node acc) tree acc_ + let trace_fold (f : 'a -> AccessPath.t -> TraceDomain.astate -> 'a) = + let f_ acc ap (trace, _) = + f acc ap trace in + fold f_ + (* replace the normal leaves of [node] with starred leaves *) let rec node_add_stars ((trace, tree) as node) = match tree with | Subtree subtree -> @@ -281,7 +293,7 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct let rec node_widen prev_node_opt next_node_opt = match prev_node_opt, next_node_opt with | Some prev_node, Some next_node -> - let widened_node = node_join node_widen trace_widen prev_node next_node in + let widened_node = node_join_ node_widen trace_widen prev_node next_node in if phys_equal widened_node prev_node then prev_node_opt else if phys_equal widened_node next_node diff --git a/infer/src/checkers/accessTree.mli b/infer/src/checkers/accessTree.mli index b62b05b85..236e0ed3f 100644 --- a/infer/src/checkers/accessTree.mli +++ b/infer/src/checkers/accessTree.mli @@ -61,8 +61,13 @@ module type S = sig with with empty traces associated with each of the inner nodes. *) val add_trace : AccessPath.t -> TraceDomain.astate -> t -> t + (** join two nodes *) + val node_join : node -> node -> node + (** apply a function to each (access path, node) pair in the tree. *) - val fold : ('a -> AccessPath.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a + val fold : ('a -> AccessPath.t -> node -> 'a) -> t -> 'a -> 'a + + val trace_fold : ('a -> AccessPath.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a val pp_node : Format.formatter -> node -> unit end diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index d0557c027..e3fc7b592 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -163,7 +163,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct else match Summary.read_summary proc_data.pdesc pname with | Some summary -> - TaintDomain.fold + TaintDomain.trace_fold (fun acc _ trace -> TraceDomain.join trace acc) (TaintSpecification.of_summary_access_tree summary) TraceDomain.empty @@ -296,7 +296,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct TaintDomain.add_node caller_ap (appended_trace, caller_tree) access_tree_acc in let access_tree = - TaintDomain.fold + TaintDomain.trace_fold add_to_caller_tree (TaintSpecification.of_summary_access_tree summary) caller_access_tree in diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 501f8a904..4b2cf4537 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -83,7 +83,7 @@ let tests = F.fprintf fmt "%a => %a" AccessPath.pp ap pp_trace trace in (* flatten access tree into list of access paths with associated traces *) let trace_assocs = - MockTaintAnalysis.TaintDomain.fold + MockTaintAnalysis.TaintDomain.trace_fold (fun acc ap t -> if not (MockTrace.is_empty t) then (ap, t) :: acc diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml index 1231d6349..006782f7c 100644 --- a/infer/src/unit/accessTreeTests.ml +++ b/infer/src/unit/accessTreeTests.ml @@ -439,7 +439,7 @@ let tests = let fold_test_ _ = let collect_ap_traces acc ap trace = (ap, trace) :: acc in - let ap_traces = Domain.fold collect_ap_traces tree [] in + let ap_traces = Domain.trace_fold collect_ap_traces tree [] in let has_ap_trace_pair ap_in trace_in = List.exists ~f:(fun (ap, trace) -> AccessPath.equal ap ap_in && MockTraceDomain.equal trace trace_in)