[access tries] max width config

Summary: It's useful to be able to configure both max depth and max width

Reviewed By: jeremydubreil

Differential Revision: D5801567

fbshipit-source-id: 0138cd7

infer/src/checkers/accessTree.ml

@@ -56,11 +56,17 @@ end
 
 module type Config = sig
   val max_depth : int
+
+  (* note : doesn't apply to bases, since we can't represent a starred base *)
+
+  val max_width : int
 end
 
 module DefaultConfig = struct
   (* arbitrarily chosen large value *)
   let max_depth = Int.max_value / 2
+
+  let max_width = Int.max_value / 2
 end
 
 module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) = struct
@@ -202,7 +208,11 @@ module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) = struct
       match (tree1, tree2) with
       | Subtree subtree1, Subtree subtree2
        -> let tree' = AccessMap.merge (fun _ v1 v2 -> f_node_merge v1 v2) subtree1 subtree2 in
-          if phys_equal trace' trace1 && phys_equal tree' subtree1 then node1
+          if AccessMap.cardinal tree' > Config.max_width then
+            (* too big; create a star insted *)
+            let trace'' = join_all_traces trace' (Subtree tree') in
+            (trace'', Star)
+          else if phys_equal trace' trace1 && phys_equal tree' subtree1 then node1
           else if phys_equal trace' trace2 && phys_equal tree' subtree2 then node2
           else (trace', Subtree tree')
       | Star, t
@@ -291,7 +301,10 @@ module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) = struct
               in
               access_tree_add_trace_ ~seen_array_access accesses access_node depth'
           in
-          (trace, Subtree (AccessMap.add access access_node' subtree))
+          let access_map = AccessMap.add access access_node' subtree in
+          if AccessMap.cardinal access_map > Config.max_width then
+            (join_all_traces trace (Subtree access_map), Star)
+          else (trace, Subtree (AccessMap.add access access_node' subtree))
     in
     access_tree_add_trace_ ~seen_array_access accesses node 1
 

infer/src/checkers/accessTree.mli

@@ -83,6 +83,8 @@ end
 
 module type Config = sig
   val max_depth : int
+
+  val max_width : int
 end
 
 module DefaultConfig : Config

infer/src/unit/accessTreeTests.ml

@@ -422,6 +422,8 @@ let tests =
     let max_depth_test_ _ =
       let module Max1 = MakeTree (struct
         let max_depth = 1
+
+        let max_width = Int.max_value / 2
       end) in
       let f_node =
         Max1.AccessMap.singleton f (Max1.make_normal_leaf x_trace)
@@ -439,6 +441,8 @@ let tests =
       Max1.assert_trees_equal (Max1.add_trace x x_trace Max1.empty) x_tree ;
       let module Max2 = MakeTree (struct
         let max_depth = 2
+
+        let max_width = Int.max_value / 2
       end) in
       let f_node =
         Max2.AccessMap.singleton f (Max2.make_normal_leaf x_trace)
@@ -464,6 +468,43 @@ let tests =
     in
     "max_depth" >:: max_depth_test_
   in
+  let max_width_test =
+    let max_width_test_ _ =
+      let module Max1 = MakeTree (struct
+        let max_depth = Int.max_value / 2
+
+        let max_width = 1
+      end) in
+      let x_base_tree = Max1.BaseMap.singleton x_base Max1.empty_node in
+      let y_base_tree = Max1.BaseMap.singleton y_base Max1.empty_node in
+      let x_y_base_tree = Max1.BaseMap.add y_base Max1.empty_node x_base_tree in
+      let f_node =
+        Max1.AccessMap.singleton f (Max1.make_normal_leaf y_trace)
+        |> Max1.make_node MockTraceDomain.empty
+      in
+      let g_node =
+        Max1.AccessMap.singleton g (Max1.make_normal_leaf z_trace)
+        |> Max1.make_node MockTraceDomain.empty
+      in
+      let star_node = Max1.make_starred_leaf (MockTraceDomain.join y_trace z_trace) in
+      let xF_tree = Max1.BaseMap.singleton x_base f_node in
+      let xG_tree = Max1.BaseMap.singleton x_base g_node in
+      let x_star_tree = Max1.BaseMap.singleton x_base star_node in
+      (* adding x.f to a tree containing just x should work *)
+      Max1.assert_trees_equal (Max1.add_trace xF y_trace Max1.empty) xF_tree ;
+      (* but adding x.g to a tree containing x.f should create a star *)
+      Max1.assert_trees_equal (Max1.add_trace xG z_trace xF_tree) x_star_tree ;
+      (* joining the x.f and x.g trees should also create a star *)
+      Max1.assert_trees_equal (Max1.join xF_tree xG_tree) x_star_tree ;
+      (* adding x.f to a tree where it's already present shouldn't create a star *)
+      Max1.assert_trees_equal (Max1.add_trace xF y_trace xF_tree) xF_tree ;
+      (* and joining the same tree with itself shouldn't either *)
+      Max1.assert_trees_equal (Max1.join xF_tree xF_tree) xF_tree ;
+      (* note that the width limit doesn't apply to the base layer *)
+      Max1.assert_trees_equal (Max1.join x_base_tree y_base_tree) x_y_base_tree
+    in
+    "max_width" >:: max_width_test_
+  in
   "access_tree_suite"
   >::: [ get_trace_test
        ; add_trace_test
@@ -472,4 +513,5 @@ let tests =
        ; widen_test
        ; fold_test
        ; depth_test
-       ; max_depth_test ]
+       ; max_depth_test
+       ; max_width_test ]