From 81fbcf750102b6d2a6de47bdfda32871fc0457cd Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 28 Aug 2017 11:16:56 -0700 Subject: [PATCH] [access trie] make max depth configurable Reviewed By: jberdine Differential Revision: D5689923 fbshipit-source-id: 471363d --- infer/src/checkers/Trace.ml | 7 +- infer/src/checkers/Trace.mli | 4 +- infer/src/checkers/accessTree.ml | 94 ++++++++++---- infer/src/checkers/accessTree.mli | 9 +- infer/src/quandary/ClangTaintAnalysis.ml | 2 +- infer/src/quandary/JavaTaintAnalysis.ml | 2 +- infer/src/quandary/QuandarySummary.ml | 4 +- infer/src/quandary/QuandarySummary.mli | 4 +- infer/src/quandary/TaintSpec.ml | 2 +- infer/src/unit/TaintTests.ml | 2 +- infer/src/unit/accessTreeTests.ml | 152 ++++++++++++++++------- 11 files changed, 198 insertions(+), 84 deletions(-) diff --git a/infer/src/checkers/Trace.ml b/infer/src/checkers/Trace.ml index 9d76d7bef..6cd300e94 100644 --- a/infer/src/checkers/Trace.ml +++ b/infer/src/checkers/Trace.ml @@ -34,7 +34,9 @@ module type S = sig module Sources : sig module Known : module type of AbstractDomain.FiniteSet (Source) - module Footprint = AccessTree.PathSet + module FootprintConfig : AccessTree.Config + + module Footprint : module type of AccessTree.PathSet (FootprintConfig) type astate = {known: Known.astate; footprint: Footprint.astate} @@ -162,7 +164,8 @@ module Make (Spec : Spec) = struct module Sources = struct module Known = AbstractDomain.FiniteSet (Source) - module Footprint = AccessTree.PathSet + module FootprintConfig = AccessTree.DefaultConfig + module Footprint = AccessTree.PathSet (FootprintConfig) type astate = {known: Known.astate; footprint: Footprint.astate} diff --git a/infer/src/checkers/Trace.mli b/infer/src/checkers/Trace.mli index 99d75e59f..a2290875d 100644 --- a/infer/src/checkers/Trace.mli +++ b/infer/src/checkers/Trace.mli @@ -37,8 +37,10 @@ module type S = sig (** Set of sources returned by callees of the current function *) module Known : module type of AbstractDomain.FiniteSet (Source) + module FootprintConfig : AccessTree.Config + (** Set of access paths representing the sources that may flow in from the caller *) - module Footprint = AccessTree.PathSet + module Footprint : module type of AccessTree.PathSet (FootprintConfig) type astate = {known: Known.astate; footprint: Footprint.astate} diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index 889563f12..9a251e00b 100644 --- a/infer/src/checkers/accessTree.ml +++ b/infer/src/checkers/accessTree.ml @@ -54,7 +54,16 @@ module type S = sig val pp_node : F.formatter -> node -> unit end -module Make (TraceDomain : AbstractDomain.WithBottom) = struct +module type Config = sig + val max_depth : int +end + +module DefaultConfig = struct + (* arbitrarily chosen large value *) + let max_depth = Int.max_value / 2 +end + +module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) = struct module TraceDomain = TraceDomain module AccessMap = PrettyPrintable.MakePPMap (struct @@ -94,6 +103,10 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct let make_starred_leaf trace = (trace, Star) + let empty_normal_leaf = make_normal_leaf TraceDomain.empty + + let empty_starred_leaf = make_starred_leaf TraceDomain.empty + (* 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 @@ -213,18 +226,39 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct | None, node_opt | node_opt, None -> node_opt + (* truncate [node] to a tree of depth <= [depth]. [depth] must be positive *) + let node_depth_truncate (_, tree as node) depth = + let rec node_depth_truncate_ depth (trace, tree as node) = + match tree with + | Star + -> node + | Subtree subtree + -> if Int.( <= ) depth 0 then + let trace' = join_all_traces trace tree in + make_starred_leaf trace' + else + let subtree' = AccessMap.map (node_depth_truncate_ (depth - 1)) subtree in + (trace, Subtree subtree') + in + if tree_depth tree > depth then node_depth_truncate_ depth node + else (* already short enough; don't bother truncating *) + node + (* helper for [add_access]. [last_trace] is the trace associated with [tree] in the parent. *) let access_tree_add_trace ~node_to_add ~seen_array_access ~is_exact accesses node = - let rec access_tree_add_trace_ ~seen_array_access accesses node = + let rec access_tree_add_trace_ ~seen_array_access accesses node depth = match (accesses, node) with | [], (trace, tree) -> ( match (is_exact, seen_array_access) with | true, false -> (* adding x.f, do strong update on both subtree and its traces *) - node_to_add + node_depth_truncate node_to_add (Config.max_depth - depth) | true, true - -> (* adding x[_], do weak update on subtree and on its immediate trace *) - node_join node_to_add node + -> (* adding x[_], do weak update on subtree and on its immediate trace. note : [node] + already satisfies the depth invariant because it's already in the tree; no need to + truncate it. *) + let truncated_node = node_depth_truncate node_to_add (Config.max_depth - depth) in + node_join truncated_node node | _ -> (* adding x.f* or x[_]*, join with traces of subtree and replace it with * *) let node_trace, node_tree = node_to_add in @@ -233,34 +267,42 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct | _, (_, Star) -> node_join node_to_add node | access :: accesses, (trace, Subtree subtree) - -> let access_node = - try AccessMap.find access subtree - with Not_found -> make_normal_leaf TraceDomain.empty - in - (* once we encounter a subtree rooted in an array access, we have to do weak updates in - the entire subtree. the reason: if I do x[i].f.g = , then - x[j].f.g = , I don't want to overwrite . instead, I - should get |_| *) - let seen_array_access = - seen_array_access - || - match access with - | AccessPath.ArrayAccess _ - -> true - | AccessPath.FieldAccess _ - -> false + -> let depth' = depth + 1 in + let access_node' = + if depth' >= Config.max_depth then + access_tree_add_trace_ ~seen_array_access accesses empty_starred_leaf depth' + else + let access_node = + try AccessMap.find access subtree + with Not_found -> empty_normal_leaf + in + (* once we encounter a subtree rooted in an array access, we have to do weak updates in + the entire subtree. the reason: if I do x[i].f.g = , then + x[j].f.g = , I don't want to overwrite . instead, I + should get |_| *) + let seen_array_access = + seen_array_access + || + match access with + | AccessPath.ArrayAccess _ + -> true + | AccessPath.FieldAccess _ + -> false + in + access_tree_add_trace_ ~seen_array_access accesses access_node depth' in - let access_node' = access_tree_add_trace_ ~seen_array_access accesses access_node in (trace, Subtree (AccessMap.add access access_node' subtree)) in - access_tree_add_trace_ ~seen_array_access accesses node + access_tree_add_trace_ ~seen_array_access accesses node 1 let add_node ap node_to_add tree = let base, accesses = AccessPath.Abs.extract ap in let is_exact = AccessPath.Abs.is_exact ap in let base_node = try BaseMap.find base tree - with Not_found -> make_normal_leaf TraceDomain.empty + with Not_found -> + (* note: we interpret max_depth <= 0 as max_depth = 1 *) + if Config.max_depth > 1 then empty_normal_leaf else empty_starred_leaf in let base_node' = access_tree_add_trace ~node_to_add ~seen_array_access:false ~is_exact accesses base_node @@ -344,8 +386,8 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct let pp fmt base_tree = BaseMap.pp ~pp_value:pp_node fmt base_tree end -module PathSet = struct - include Make (AbstractDomain.BooleanOr) +module PathSet (Config : Config) = struct + include Make (AbstractDomain.BooleanOr) (Config) (* print as a set of paths rather than a map of paths to bools *) let pp fmt tree = diff --git a/infer/src/checkers/accessTree.mli b/infer/src/checkers/accessTree.mli index 54f260946..2a4590f7d 100644 --- a/infer/src/checkers/accessTree.mli +++ b/infer/src/checkers/accessTree.mli @@ -81,7 +81,14 @@ module type S = sig val pp_node : Format.formatter -> node -> unit end -module Make (TraceDomain : AbstractDomain.WithBottom) : S with module TraceDomain = TraceDomain +module type Config = sig + val max_depth : int +end + +module DefaultConfig : Config + +module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) : + S with module TraceDomain = TraceDomain (** Concise representation of a set of access paths *) module PathSet : module type of Make (AbstractDomain.BooleanOr) diff --git a/infer/src/quandary/ClangTaintAnalysis.ml b/infer/src/quandary/ClangTaintAnalysis.ml index ef189161d..5bce3062b 100644 --- a/infer/src/quandary/ClangTaintAnalysis.ml +++ b/infer/src/quandary/ClangTaintAnalysis.ml @@ -13,7 +13,7 @@ module L = Logging include TaintAnalysis.Make (struct module Trace = ClangTrace - module AccessTree = AccessTree.Make (Trace) + module AccessTree = AccessTree.Make (Trace) (AccessTree.DefaultConfig) let to_summary_access_tree tree = QuandarySummary.AccessTree.Clang tree diff --git a/infer/src/quandary/JavaTaintAnalysis.ml b/infer/src/quandary/JavaTaintAnalysis.ml index 7ec8a5d9e..e0a80a4f2 100644 --- a/infer/src/quandary/JavaTaintAnalysis.ml +++ b/infer/src/quandary/JavaTaintAnalysis.ml @@ -13,7 +13,7 @@ module L = Logging include TaintAnalysis.Make (struct module Trace = JavaTrace - module AccessTree = AccessTree.Make (Trace) + module AccessTree = AccessTree.Make (Trace) (AccessTree.DefaultConfig) let to_summary_access_tree access_tree = QuandarySummary.AccessTree.Java access_tree diff --git a/infer/src/quandary/QuandarySummary.ml b/infer/src/quandary/QuandarySummary.ml index c4d625a31..da916892a 100644 --- a/infer/src/quandary/QuandarySummary.ml +++ b/infer/src/quandary/QuandarySummary.ml @@ -12,8 +12,8 @@ open! IStd module F = Format module L = Logging -module Java = AccessTree.Make (JavaTrace) -module Clang = AccessTree.Make (ClangTrace) +module Java = AccessTree.Make (JavaTrace) (AccessTree.DefaultConfig) +module Clang = AccessTree.Make (ClangTrace) (AccessTree.DefaultConfig) module AccessTree = struct type t = Java of Java.t | Clang of Clang.t diff --git a/infer/src/quandary/QuandarySummary.mli b/infer/src/quandary/QuandarySummary.mli index d299db34b..08eed38c9 100644 --- a/infer/src/quandary/QuandarySummary.mli +++ b/infer/src/quandary/QuandarySummary.mli @@ -13,9 +13,9 @@ open! IStd module F = Format -module Java : module type of AccessTree.Make (JavaTrace) +module Java : module type of AccessTree.Make (JavaTrace) (AccessTree.DefaultConfig) -module Clang : module type of AccessTree.Make (ClangTrace) +module Clang : module type of AccessTree.Make (ClangTrace) (AccessTree.DefaultConfig) module AccessTree : sig type t = Java of Java.t | Clang of Clang.t diff --git a/infer/src/quandary/TaintSpec.ml b/infer/src/quandary/TaintSpec.ml index 958d6ad05..00a6e8884 100644 --- a/infer/src/quandary/TaintSpec.ml +++ b/infer/src/quandary/TaintSpec.ml @@ -24,7 +24,7 @@ type sanitizer = Return (** a sanitizer that removes taint from its return valu module type S = sig module Trace : Trace.S - module AccessTree : module type of AccessTree.Make (Trace) + module AccessTree : module type of AccessTree.Make (Trace) (AccessTree.DefaultConfig) val handle_unknown_call : Typ.Procname.t -> Typ.t option -> HilExp.t list -> Tenv.t -> action list diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 3a814009a..2c439ea19 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -40,7 +40,7 @@ end) module MockTaintAnalysis = TaintAnalysis.Make (struct module Trace = MockTrace - module AccessTree = AccessTree.Make (Trace) + module AccessTree = AccessTree.Make (Trace) (AccessTree.DefaultConfig) let of_summary_access_tree _ = assert false diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml index 3a37776dc..d36b5380c 100644 --- a/infer/src/unit/accessTreeTests.ml +++ b/infer/src/unit/accessTreeTests.ml @@ -36,25 +36,29 @@ module MockTraceDomain = struct let pp fmt s = if phys_equal s top then F.fprintf fmt "T" else pp fmt s end -module Domain = AccessTree.Make (MockTraceDomain) +module MakeTree (Config : AccessTree.Config) = struct + include AccessTree.Make (MockTraceDomain) (Config) -let assert_trees_equal tree1 tree2 = - let rec access_tree_equal (trace1, subtree1) (trace2, subtree2) = - MockTraceDomain.equal trace1 trace2 - && - match (subtree1, subtree2) with - | Domain.Star, Domain.Star - -> true - | Domain.Subtree t1, Domain.Subtree t2 - -> Domain.AccessMap.equal access_tree_equal t1 t2 - | _ - -> false - in - let base_tree_equal tree1 tree2 = Domain.BaseMap.equal access_tree_equal tree1 tree2 in - let pp_diff fmt (actual, expected) = - F.fprintf fmt "Expected to get tree %a but got %a" Domain.pp expected Domain.pp actual - in - OUnit2.assert_equal ~cmp:base_tree_equal ~pp_diff tree1 tree2 + let assert_trees_equal tree1 tree2 = + let rec access_tree_equal (trace1, subtree1) (trace2, subtree2) = + MockTraceDomain.equal trace1 trace2 + && + match (subtree1, subtree2) with + | Star, Star + -> true + | Subtree t1, Subtree t2 + -> AccessMap.equal access_tree_equal t1 t2 + | _ + -> false + in + let base_tree_equal tree1 tree2 = BaseMap.equal access_tree_equal tree1 tree2 in + let pp_diff fmt (actual, expected) = + F.fprintf fmt "Expected to get tree %a but got %a" pp expected pp actual + in + OUnit2.assert_equal ~cmp:base_tree_equal ~pp_diff tree1 tree2 +end + +module Domain = MakeTree (AccessTree.DefaultConfig) let tests = let open AccessPathTestUtils in @@ -200,49 +204,52 @@ let tests = (* normal tests *) (* add base when absent *) let x_y_base_tree_with_added_trace = mk_x_y_base_tree added_trace in - assert_trees_equal (Domain.add_trace x added_trace y_base_tree) + Domain.assert_trees_equal (Domain.add_trace x added_trace y_base_tree) x_y_base_tree_with_added_trace ; (* add base when present *) - assert_trees_equal (Domain.add_trace x added_trace x_y_base_tree) + Domain.assert_trees_equal (Domain.add_trace x added_trace x_y_base_tree) x_y_base_tree_with_added_trace ; let x_y_base_tree_with_y_trace = mk_x_y_base_tree y_trace in - assert_trees_equal (Domain.add_trace x added_trace x_y_base_tree_with_y_trace) + Domain.assert_trees_equal (Domain.add_trace x added_trace x_y_base_tree_with_y_trace) x_y_base_tree_with_added_trace ; (* add path when absent *) let xFG_tree_added_trace = mk_xFG_tree added_trace in - assert_trees_equal (Domain.add_trace xFG added_trace x_base_tree) xFG_tree_added_trace ; + Domain.assert_trees_equal (Domain.add_trace xFG added_trace x_base_tree) xFG_tree_added_trace ; (* add path when present *) let xFG_tree_y_trace = mk_xFG_tree y_trace in - assert_trees_equal (Domain.add_trace xFG added_trace xFG_tree_y_trace) xFG_tree_added_trace ; + Domain.assert_trees_equal (Domain.add_trace xFG added_trace xFG_tree_y_trace) + xFG_tree_added_trace ; (* add starred path when base absent *) let xF_star_tree_added_trace = Domain.make_starred_leaf added_trace |> Domain.AccessMap.singleton f |> Domain.make_node MockTraceDomain.empty |> Domain.BaseMap.singleton x_base in - assert_trees_equal (Domain.add_trace xF_star added_trace Domain.empty) + Domain.assert_trees_equal (Domain.add_trace xF_star added_trace Domain.empty) xF_star_tree_added_trace ; (* add starred path when base present *) - assert_trees_equal (Domain.add_trace xF_star added_trace x_base_tree) + Domain.assert_trees_equal (Domain.add_trace xF_star added_trace x_base_tree) xF_star_tree_added_trace ; (* adding array path should do weak updates *) let aArrF_tree = mk_xArrF_tree array_f_trace in let aArrF_tree_joined_trace = mk_xArrF_tree (MockTraceDomain.join added_trace array_f_trace) in - assert_trees_equal (Domain.add_trace xArrF added_trace aArrF_tree) aArrF_tree_joined_trace ; + Domain.assert_trees_equal (Domain.add_trace xArrF added_trace aArrF_tree) + aArrF_tree_joined_trace ; (* starred tests *) (* we should do a strong update when updating x.f* with x.f *) let yF_tree_added_trace = Domain.make_normal_leaf added_trace |> Domain.AccessMap.singleton f |> Domain.make_node y_trace |> Domain.BaseMap.singleton y_base in - assert_trees_equal (Domain.add_trace yF added_trace yF_star_tree) yF_tree_added_trace ; + Domain.assert_trees_equal (Domain.add_trace yF added_trace yF_star_tree) yF_tree_added_trace ; (* but not when updating x* with x.f *) let x_star_tree_added_trace = let joined_trace = MockTraceDomain.join x_trace added_trace in Domain.BaseMap.singleton x_base (Domain.make_starred_leaf joined_trace) in - assert_trees_equal (Domain.add_trace xF added_trace x_star_tree) x_star_tree_added_trace ; + Domain.assert_trees_equal (Domain.add_trace xF added_trace x_star_tree) + x_star_tree_added_trace ; (* when updating x.f.g with x.f*, we should remember traces associated with f and g even as we replace that subtree with a * *) let xF_star_tree_joined_traces = @@ -252,13 +259,14 @@ let tests = Domain.make_starred_leaf joined_trace |> Domain.AccessMap.singleton f |> Domain.make_node x_trace |> Domain.BaseMap.singleton x_base in - assert_trees_equal (Domain.add_trace xF_star added_trace xFG_tree) xF_star_tree_joined_traces ; + Domain.assert_trees_equal (Domain.add_trace xF_star added_trace xFG_tree) + xF_star_tree_joined_traces ; (* [add_node] tests are sparse, since [add_trace] is just [add_node] . main things to test are (1) adding a non-empty node works, (2) adding a non-empty node does the proper joins in the weak update case *) (* case (1): adding XFG to y base tree works *) let y_xFG_tree = Domain.BaseMap.add y_base Domain.empty_node (mk_xFG_tree xFG_trace) in - assert_trees_equal (Domain.add_node x (mk_xFG_node xFG_trace) y_base_tree) y_xFG_tree ; + Domain.assert_trees_equal (Domain.add_node x (mk_xFG_node xFG_trace) y_base_tree) y_xFG_tree ; (* case (2): adding a non-empty node does weak updates when required *) let arr_tree = let arr_subtree = @@ -268,7 +276,7 @@ let tests = Domain.AccessMap.singleton array (Domain.make_node xF_trace arr_subtree) |> Domain.make_node MockTraceDomain.empty |> Domain.BaseMap.singleton x_base in - assert_trees_equal (Domain.add_node xArr g_subtree aArrF_tree) arr_tree + Domain.assert_trees_equal (Domain.add_node xArr g_subtree aArrF_tree) arr_tree in "add_trace" >:: add_trace_test_ in @@ -317,18 +325,18 @@ let tests = let join_test = let join_test_ _ = (* normal |_| normal *) - assert_trees_equal (Domain.join x_base_tree y_base_tree) x_y_base_tree ; - assert_trees_equal (Domain.join y_base_tree x_base_tree) x_y_base_tree ; - assert_trees_equal (Domain.join x_y_base_tree x_base_tree) x_y_base_tree ; - assert_trees_equal (Domain.join x_base_tree xFG_tree) xFG_tree ; + Domain.assert_trees_equal (Domain.join x_base_tree y_base_tree) x_y_base_tree ; + Domain.assert_trees_equal (Domain.join y_base_tree x_base_tree) x_y_base_tree ; + Domain.assert_trees_equal (Domain.join x_y_base_tree x_base_tree) x_y_base_tree ; + Domain.assert_trees_equal (Domain.join x_base_tree xFG_tree) xFG_tree ; (* starred |_| starred *) - assert_trees_equal (Domain.join x_star_tree yF_star_tree) x_yF_star_tree ; + Domain.assert_trees_equal (Domain.join x_star_tree yF_star_tree) x_yF_star_tree ; (* normal |_| starred *) - assert_trees_equal (Domain.join tree xFG_tree) tree ; + Domain.assert_trees_equal (Domain.join tree xFG_tree) tree ; (* [x_star_tree] and [x_base_tree] both have trace "{ x }" associated with x... *) - assert_trees_equal (Domain.join x_star_tree x_base_tree) x_star_tree ; + Domain.assert_trees_equal (Domain.join x_star_tree x_base_tree) x_star_tree ; (* ...but [xFG_tree] has some nested traces that should get joined with "{ x }" *) - assert_trees_equal (Domain.join x_star_tree xFG_tree) x_star_tree_xFG_trace + Domain.assert_trees_equal (Domain.join x_star_tree xFG_tree) x_star_tree_xFG_trace in "join" >:: join_test_ in @@ -346,7 +354,7 @@ let tests = let x_tree_x_trace = make_x_base_tree x_trace in let x_tree_y_trace = make_x_base_tree y_trace in let x_tree_top_trace = make_x_base_tree MockTraceDomain.top in - assert_trees_equal (widen x_tree_x_trace x_tree_y_trace) x_tree_top_trace ; + Domain.assert_trees_equal (widen x_tree_x_trace x_tree_y_trace) x_tree_top_trace ; (* adding stars to a base works: x |-> ({}, empty) \/ y |-> ({}, empty) = (x |-> ({}, empty), y |-> ({}, Star) ) @@ -354,7 +362,7 @@ let tests = let x_y_star_base_tree = Domain.BaseMap.add y_base (Domain.make_starred_leaf MockTraceDomain.empty) x_base_tree in - assert_trees_equal (widen x_base_tree y_base_tree) x_y_star_base_tree ; + Domain.assert_trees_equal (widen x_base_tree y_base_tree) x_y_star_base_tree ; (* adding stars to a subtree works: x |-> ("y", empty) \/ x |-> ("x" , f |-> ("f", g |-> ("g", empty))) = @@ -364,7 +372,7 @@ let tests = Domain.AccessMap.singleton f (Domain.make_starred_leaf MockTraceDomain.top) |> Domain.make_node MockTraceDomain.top |> Domain.BaseMap.singleton x_base in - assert_trees_equal (widen x_tree_y_trace xFG_tree) xF_star_tree ; + Domain.assert_trees_equal (widen x_tree_y_trace xFG_tree) xF_star_tree ; (* widening is not commutative, and is it not join: x |-> ("x" , f |-> ("f", g |-> ("g", empty))) \/ x |-> ("y", empty) = @@ -374,7 +382,7 @@ let tests = let _, xFG_node = x_subtree in Domain.BaseMap.singleton x_base (MockTraceDomain.top, xFG_node) in - assert_trees_equal (widen xFG_tree x_tree_y_trace) xFG_tree_widened_trace + Domain.assert_trees_equal (widen xFG_tree x_tree_y_trace) xFG_tree_widened_trace in "widen" >:: widen_test_ in @@ -406,10 +414,62 @@ let tests = 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 ; - () + assert_equal (Domain.depth x_yF_star_tree) 2 in "depth" >:: depth_test_ in + let max_depth_test = + let max_depth_test_ _ = + let module Max1 = MakeTree (struct + let max_depth = 1 + end) in + let f_node = + Max1.AccessMap.singleton f (Max1.make_normal_leaf x_trace) + |> Max1.make_node MockTraceDomain.empty + in + let x_tree = Max1.BaseMap.singleton x_base (Max1.make_normal_leaf x_trace) in + let x_star_tree = Max1.BaseMap.singleton x_base (Max1.make_starred_leaf x_trace) in + (* adding (x.f, "x") to a tree with max height 1 should yield x |-> ("x", * ) *) + Max1.assert_trees_equal (Max1.add_trace xF x_trace Max1.empty) x_star_tree ; + (* same, but with (x.f.g, "x") *) + Max1.assert_trees_equal (Max1.add_trace xFG x_trace Max1.empty) x_star_tree ; + (* adding node (f, "x") via access path x should also yield the same tree *) + Max1.assert_trees_equal (Max1.add_node x f_node Max1.empty) x_star_tree ; + (* adding (x, "x") shouldn't add stars *) + Max1.assert_trees_equal (Max1.add_trace x x_trace Max1.empty) x_tree ; + let module Max2 = MakeTree (struct + let max_depth = 2 + end) in + let f_node = + Max2.AccessMap.singleton f (Max2.make_normal_leaf x_trace) + |> Max2.make_node MockTraceDomain.empty + in + let fG_node = + Max2.make_access_node MockTraceDomain.empty g x_trace |> Max2.AccessMap.singleton f + |> Max2.make_node MockTraceDomain.empty + in + let f_star_node = + Max2.AccessMap.singleton f (Max2.make_starred_leaf x_trace) + |> Max2.make_node MockTraceDomain.empty + in + let x_tree = Max2.BaseMap.singleton x_base Max2.empty_node in + let xF_tree = Max2.BaseMap.singleton x_base f_node in + let xF_star_tree = Max2.BaseMap.singleton x_base f_star_node in + (* adding x.f to an empty tree should't add stars... *) + Max2.assert_trees_equal (Max2.add_trace xF x_trace Max2.empty) xF_tree ; + (* ... but adding x.f.g should *) + Max2.assert_trees_equal (Max2.add_trace xFG x_trace Max2.empty) xF_star_tree ; + (* adding the node (f.g, "x") to a tree with x should produce the same result *) + Max2.assert_trees_equal (Max2.add_node x fG_node x_tree) xF_star_tree + in + "max_depth" >:: max_depth_test_ + in "access_tree_suite" - >::: [get_trace_test; add_trace_test; lteq_test; join_test; widen_test; fold_test; depth_test] + >::: [ get_trace_test + ; add_trace_test + ; lteq_test + ; join_test + ; widen_test + ; fold_test + ; depth_test + ; max_depth_test ]