From 375b8083944d5126a55a4ba5ed2f3a871aebd4ad Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 11 Sep 2017 19:13:57 -0700 Subject: [PATCH] [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 | 17 ++++++++++-- infer/src/checkers/accessTree.mli | 2 ++ infer/src/unit/accessTreeTests.ml | 44 ++++++++++++++++++++++++++++++- 3 files changed, 60 insertions(+), 3 deletions(-) diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index 9a251e00b..aedbf5fc1 100644 --- a/infer/src/checkers/accessTree.ml +++ b/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 diff --git a/infer/src/checkers/accessTree.mli b/infer/src/checkers/accessTree.mli index 2a4590f7d..eb3acd101 100644 --- a/infer/src/checkers/accessTree.mli +++ b/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 diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml index d36b5380c..fc5ae5360 100644 --- a/infer/src/unit/accessTreeTests.ml +++ b/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 ]