diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index d2f174f21..889563f12 100644 --- a/infer/src/checkers/accessTree.ml +++ b/infer/src/checkers/accessTree.ml @@ -49,6 +49,8 @@ module type S = sig val trace_fold : ('a -> AccessPath.Abs.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a + val depth : t -> int + val pp_node : F.formatter -> node -> unit end @@ -92,6 +94,19 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct let make_starred_leaf trace = (trace, Star) + (* no need to make it tail-recursive, trees shouldn't be big enough to blow up the call stack *) + let rec node_depth (_, tree) = 1 + tree_depth tree + + and tree_depth = function + | Star + -> 0 + | Subtree node_map + -> AccessMap.fold (fun _ node acc -> max_depth node acc) node_map 0 + + and max_depth node max_depth_acc = Int.max (node_depth node) max_depth_acc + + let depth access_tree = BaseMap.fold (fun _ node acc -> max_depth node acc) access_tree 0 + let make_access_node base_trace access trace = make_node base_trace (AccessMap.singleton access (make_normal_leaf trace)) diff --git a/infer/src/checkers/accessTree.mli b/infer/src/checkers/accessTree.mli index 72b1f34ed..54f260946 100644 --- a/infer/src/checkers/accessTree.mli +++ b/infer/src/checkers/accessTree.mli @@ -75,6 +75,9 @@ module type S = sig val trace_fold : ('a -> AccessPath.Abs.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a + val depth : t -> int + (** number of traces in the tallest branch of the tree *) + val pp_node : Format.formatter -> node -> unit end diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml index 322f6f088..3a37776dc 100644 --- a/infer/src/unit/accessTreeTests.ml +++ b/infer/src/unit/accessTreeTests.ml @@ -398,5 +398,18 @@ let tests = in "fold" >:: fold_test_ in + let depth_test = + let depth_test_ _ = + assert_equal (Domain.depth Domain.empty) 0 ; + assert_equal (Domain.depth x_base_tree) 1 ; + assert_equal (Domain.depth x_y_base_tree) 1 ; + assert_equal (Domain.depth xFG_tree) 3 ; + assert_equal (Domain.depth x_star_tree) 1 ; + assert_equal (Domain.depth yF_star_tree) 2 ; + assert_equal (Domain.depth x_yF_star_tree) 2 ; + () + in + "depth" >:: depth_test_ + in "access_tree_suite" - >::: [get_trace_test; add_trace_test; lteq_test; join_test; widen_test; fold_test] + >::: [get_trace_test; add_trace_test; lteq_test; join_test; widen_test; fold_test; depth_test]