[access trees] function for computing depth

Summary:
I'm working on parameterizing access trees with a config that will limit max depth + perhaps width if needed.
This is a stepping stone to enforcing max depth.

Reviewed By: jvillard

Differential Revision: D5693453

fbshipit-source-id: c15b0ee

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

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
 

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]