pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[access trie] make max depth configurable

Browse Source 
Reviewed By: jberdine

Differential Revision: D5689923

fbshipit-source-id: 471363d
master
Sam Blackshear 7 years ago committed by Facebook Github Bot
parent 04d3142f6b
commit 81fbcf7501
11 changed files with 198 additions and 84 deletions
Show Stats Download Patch File Download Diff File

7
infer/src/checkers/Trace.ml
Unescape View File

@ -34,7 +34,9 @@ module type S = sig
module Sources : sig module Sources : sig
module Known : module type of AbstractDomain.FiniteSet (Source) 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} type astate = {known: Known.astate; footprint: Footprint.astate}
@ -162,7 +164,8 @@ module Make (Spec : Spec) = struct
module Sources = struct module Sources = struct
module Known = AbstractDomain.FiniteSet (Source) 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} type astate = {known: Known.astate; footprint: Footprint.astate}

4
infer/src/checkers/Trace.mli
Unescape View File

@ -37,8 +37,10 @@ module type S = sig
(** Set of sources returned by callees of the current function *) (** Set of sources returned by callees of the current function *)
module Known : module type of AbstractDomain.FiniteSet (Source) 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 *) (** 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} type astate = {known: Known.astate; footprint: Footprint.astate}

94
infer/src/checkers/accessTree.ml
Unescape View File

@ -54,7 +54,16 @@ module type S = sig
val pp_node : F.formatter -> node -> unit val pp_node : F.formatter -> node -> unit
end 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 TraceDomain = TraceDomain
module AccessMap = PrettyPrintable.MakePPMap (struct module AccessMap = PrettyPrintable.MakePPMap (struct
@ -94,6 +103,10 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct
let make_starred_leaf trace = (trace, Star) 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 *) (* 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 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 | None, node_opt | node_opt, None
-> node_opt -> 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. *) (* 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 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 match (accesses, node) with
| [], (trace, tree) -> ( | [], (trace, tree) -> (
match (is_exact, seen_array_access) with match (is_exact, seen_array_access) with
| true, false | true, false
-> (* adding x.f, do strong update on both subtree and its traces *) -> (* 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 | true, true
-> (* adding x[_], do weak update on subtree and on its immediate trace *) -> (* adding x[_], do weak update on subtree and on its immediate trace. note : [node]
node_join node_to_add 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 * *) -> (* adding x.f* or x[_]*, join with traces of subtree and replace it with * *)
let node_trace, node_tree = node_to_add in let node_trace, node_tree = node_to_add in
@ -233,34 +267,42 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct
| _, (_, Star) | _, (_, Star)
-> node_join node_to_add node -> node_join node_to_add node
| access :: accesses, (trace, Subtree subtree) | access :: accesses, (trace, Subtree subtree)
-> let access_node = -> let depth' = depth + 1 in
try AccessMap.find access subtree let access_node' =
with Not_found -> make_normal_leaf TraceDomain.empty if depth' >= Config.max_depth then
in access_tree_add_trace_ ~seen_array_access accesses empty_starred_leaf depth'
(* once we encounter a subtree rooted in an array access, we have to do weak updates in else
the entire subtree. the reason: if I do x[i].f.g = <interesting trace>, then let access_node =
x[j].f.g = <empty trace>, I don't want to overwrite <interesting trace>. instead, I try AccessMap.find access subtree
should get <interesting trace> |_| <empty trace> *) with Not_found -> empty_normal_leaf
let seen_array_access = in
seen_array_access (* 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 = <interesting trace>, then
match access with x[j].f.g = <empty trace>, I don't want to overwrite <interesting trace>. instead, I
| AccessPath.ArrayAccess _ should get <interesting trace> |_| <empty trace> *)
-> true let seen_array_access =
| AccessPath.FieldAccess _ seen_array_access
-> false ||
match access with
| AccessPath.ArrayAccess _
-> true
| AccessPath.FieldAccess _
-> false
in
access_tree_add_trace_ ~seen_array_access accesses access_node depth'
in in
let access_node' = access_tree_add_trace_ ~seen_array_access accesses access_node in
(trace, Subtree (AccessMap.add access access_node' subtree)) (trace, Subtree (AccessMap.add access access_node' subtree))
in 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 add_node ap node_to_add tree =
let base, accesses = AccessPath.Abs.extract ap in let base, accesses = AccessPath.Abs.extract ap in
let is_exact = AccessPath.Abs.is_exact ap in let is_exact = AccessPath.Abs.is_exact ap in
let base_node = let base_node =
try BaseMap.find base tree 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 in
let base_node' = let base_node' =
access_tree_add_trace ~node_to_add ~seen_array_access:false ~is_exact accesses 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 let pp fmt base_tree = BaseMap.pp ~pp_value:pp_node fmt base_tree
end end
module PathSet = struct module PathSet (Config : Config) = struct
include Make (AbstractDomain.BooleanOr) include Make (AbstractDomain.BooleanOr) (Config)
(* print as a set of paths rather than a map of paths to bools *) (* print as a set of paths rather than a map of paths to bools *)
let pp fmt tree = let pp fmt tree =

9
infer/src/checkers/accessTree.mli
Unescape View File

@ -81,7 +81,14 @@ module type S = sig
val pp_node : Format.formatter -> node -> unit val pp_node : Format.formatter -> node -> unit
end 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 *) (** Concise representation of a set of access paths *)
module PathSet : module type of Make (AbstractDomain.BooleanOr) module PathSet : module type of Make (AbstractDomain.BooleanOr)

2
infer/src/quandary/ClangTaintAnalysis.ml
Unescape View File

@ -13,7 +13,7 @@ module L = Logging
include TaintAnalysis.Make (struct include TaintAnalysis.Make (struct
module Trace = ClangTrace 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 let to_summary_access_tree tree = QuandarySummary.AccessTree.Clang tree

2
infer/src/quandary/JavaTaintAnalysis.ml
Unescape View File

@ -13,7 +13,7 @@ module L = Logging
include TaintAnalysis.Make (struct include TaintAnalysis.Make (struct
module Trace = JavaTrace 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 let to_summary_access_tree access_tree = QuandarySummary.AccessTree.Java access_tree

4
infer/src/quandary/QuandarySummary.ml
Unescape View File

@ -12,8 +12,8 @@
open! IStd open! IStd
module F = Format module F = Format
module L = Logging module L = Logging
module Java = AccessTree.Make (JavaTrace) module Java = AccessTree.Make (JavaTrace) (AccessTree.DefaultConfig)
module Clang = AccessTree.Make (ClangTrace) module Clang = AccessTree.Make (ClangTrace) (AccessTree.DefaultConfig)
module AccessTree = struct module AccessTree = struct
type t = Java of Java.t | Clang of Clang.t type t = Java of Java.t | Clang of Clang.t

4
infer/src/quandary/QuandarySummary.mli
Unescape View File

@ -13,9 +13,9 @@ open! IStd
module F = Format 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 module AccessTree : sig
type t = Java of Java.t | Clang of Clang.t type t = Java of Java.t | Clang of Clang.t

2
infer/src/quandary/TaintSpec.ml
Unescape View File

@ -24,7 +24,7 @@ type sanitizer = Return (** a sanitizer that removes taint from its return valu
module type S = sig module type S = sig
module Trace : Trace.S 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 : val handle_unknown_call :
Typ.Procname.t -> Typ.t option -> HilExp.t list -> Tenv.t -> action list Typ.Procname.t -> Typ.t option -> HilExp.t list -> Tenv.t -> action list

2
infer/src/unit/TaintTests.ml
Unescape View File

@ -40,7 +40,7 @@ end)
module MockTaintAnalysis = TaintAnalysis.Make (struct module MockTaintAnalysis = TaintAnalysis.Make (struct
module Trace = MockTrace module Trace = MockTrace
module AccessTree = AccessTree.Make (Trace) module AccessTree = AccessTree.Make (Trace) (AccessTree.DefaultConfig)
let of_summary_access_tree _ = assert false let of_summary_access_tree _ = assert false

152
infer/src/unit/accessTreeTests.ml
Unescape View File

@ -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 let pp fmt s = if phys_equal s top then F.fprintf fmt "T" else pp fmt s
end end
module Domain = AccessTree.Make (MockTraceDomain) module MakeTree (Config : AccessTree.Config) = struct
include AccessTree.Make (MockTraceDomain) (Config)
let assert_trees_equal tree1 tree2 = let assert_trees_equal tree1 tree2 =
let rec access_tree_equal (trace1, subtree1) (trace2, subtree2) = let rec access_tree_equal (trace1, subtree1) (trace2, subtree2) =
MockTraceDomain.equal trace1 trace2 MockTraceDomain.equal trace1 trace2
&& &&
match (subtree1, subtree2) with match (subtree1, subtree2) with
| Domain.Star, Domain.Star | Star, Star
-> true -> true
| Domain.Subtree t1, Domain.Subtree t2 | Subtree t1, Subtree t2
-> Domain.AccessMap.equal access_tree_equal t1 t2 -> AccessMap.equal access_tree_equal t1 t2
| _ | _
-> false -> false
in in
let base_tree_equal tree1 tree2 = Domain.BaseMap.equal access_tree_equal tree1 tree2 in let base_tree_equal tree1 tree2 = BaseMap.equal access_tree_equal tree1 tree2 in
let pp_diff fmt (actual, expected) = let pp_diff fmt (actual, expected) =
F.fprintf fmt "Expected to get tree %a but got %a" Domain.pp expected Domain.pp actual F.fprintf fmt "Expected to get tree %a but got %a" pp expected pp actual
in in
OUnit2.assert_equal ~cmp:base_tree_equal ~pp_diff tree1 tree2 OUnit2.assert_equal ~cmp:base_tree_equal ~pp_diff tree1 tree2
end
module Domain = MakeTree (AccessTree.DefaultConfig)
let tests = let tests =
let open AccessPathTestUtils in let open AccessPathTestUtils in
@ -200,49 +204,52 @@ let tests =
(* normal tests *) (* normal tests *)
(* add base when absent *) (* add base when absent *)
let x_y_base_tree_with_added_trace = mk_x_y_base_tree added_trace in 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 ; x_y_base_tree_with_added_trace ;
(* add base when present *) (* 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 ; x_y_base_tree_with_added_trace ;
let x_y_base_tree_with_y_trace = mk_x_y_base_tree y_trace in 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 ; x_y_base_tree_with_added_trace ;
(* add path when absent *) (* add path when absent *)
let xFG_tree_added_trace = mk_xFG_tree added_trace in 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 *) (* add path when present *)
let xFG_tree_y_trace = mk_xFG_tree y_trace in 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 *) (* add starred path when base absent *)
let xF_star_tree_added_trace = let xF_star_tree_added_trace =
Domain.make_starred_leaf added_trace |> Domain.AccessMap.singleton f Domain.make_starred_leaf added_trace |> Domain.AccessMap.singleton f
|> Domain.make_node MockTraceDomain.empty |> Domain.BaseMap.singleton x_base |> Domain.make_node MockTraceDomain.empty |> Domain.BaseMap.singleton x_base
in 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 ; xF_star_tree_added_trace ;
(* add starred path when base present *) (* 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 ; xF_star_tree_added_trace ;
(* adding array path should do weak updates *) (* adding array path should do weak updates *)
let aArrF_tree = mk_xArrF_tree array_f_trace in let aArrF_tree = mk_xArrF_tree array_f_trace in
let aArrF_tree_joined_trace = let aArrF_tree_joined_trace =
mk_xArrF_tree (MockTraceDomain.join added_trace array_f_trace) mk_xArrF_tree (MockTraceDomain.join added_trace array_f_trace)
in 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 *) (* starred tests *)
(* we should do a strong update when updating x.f* with x.f *) (* we should do a strong update when updating x.f* with x.f *)
let yF_tree_added_trace = let yF_tree_added_trace =
Domain.make_normal_leaf added_trace |> Domain.AccessMap.singleton f Domain.make_normal_leaf added_trace |> Domain.AccessMap.singleton f
|> Domain.make_node y_trace |> Domain.BaseMap.singleton y_base |> Domain.make_node y_trace |> Domain.BaseMap.singleton y_base
in 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 *) (* but not when updating x* with x.f *)
let x_star_tree_added_trace = let x_star_tree_added_trace =
let joined_trace = MockTraceDomain.join x_trace added_trace in let joined_trace = MockTraceDomain.join x_trace added_trace in
Domain.BaseMap.singleton x_base (Domain.make_starred_leaf joined_trace) Domain.BaseMap.singleton x_base (Domain.make_starred_leaf joined_trace)
in 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 (* 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 * *) we replace that subtree with a * *)
let xF_star_tree_joined_traces = let xF_star_tree_joined_traces =
@ -252,13 +259,14 @@ let tests =
Domain.make_starred_leaf joined_trace |> Domain.AccessMap.singleton f Domain.make_starred_leaf joined_trace |> Domain.AccessMap.singleton f
|> Domain.make_node x_trace |> Domain.BaseMap.singleton x_base |> Domain.make_node x_trace |> Domain.BaseMap.singleton x_base
in 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] <empty node>. main things (* [add_node] tests are sparse, since [add_trace] is just [add_node] <empty node>. main things
to test are (1) adding a non-empty node works, (2) adding a non-empty node does the proper 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 *) joins in the weak update case *)
(* case (1): adding XFG to y base tree works *) (* 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 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 *) (* case (2): adding a non-empty node does weak updates when required *)
let arr_tree = let arr_tree =
let arr_subtree = let arr_subtree =
@ -268,7 +276,7 @@ let tests =
Domain.AccessMap.singleton array (Domain.make_node xF_trace arr_subtree) Domain.AccessMap.singleton array (Domain.make_node xF_trace arr_subtree)
|> Domain.make_node MockTraceDomain.empty |> Domain.BaseMap.singleton x_base |> Domain.make_node MockTraceDomain.empty |> Domain.BaseMap.singleton x_base
in 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 in
"add_trace" >:: add_trace_test_ "add_trace" >:: add_trace_test_
in in
@ -317,18 +325,18 @@ let tests =
let join_test = let join_test =
let join_test_ _ = let join_test_ _ =
(* normal |_| normal *) (* normal |_| normal *)
assert_trees_equal (Domain.join x_base_tree y_base_tree) x_y_base_tree ; Domain.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 ; Domain.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 ; Domain.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 xFG_tree) xFG_tree ;
(* starred |_| starred *) (* 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 *) (* 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... *) (* [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 }" *) (* ...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 in
"join" >:: join_test_ "join" >:: join_test_
in in
@ -346,7 +354,7 @@ let tests =
let x_tree_x_trace = make_x_base_tree x_trace in 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_y_trace = make_x_base_tree y_trace in
let x_tree_top_trace = make_x_base_tree MockTraceDomain.top 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: (* adding stars to a base works:
x |-> ({}, empty) \/ y |-> ({}, empty) = x |-> ({}, empty) \/ y |-> ({}, empty) =
(x |-> ({}, empty), y |-> ({}, Star) ) (x |-> ({}, empty), y |-> ({}, Star) )
@ -354,7 +362,7 @@ let tests =
let x_y_star_base_tree = let x_y_star_base_tree =
Domain.BaseMap.add y_base (Domain.make_starred_leaf MockTraceDomain.empty) x_base_tree Domain.BaseMap.add y_base (Domain.make_starred_leaf MockTraceDomain.empty) x_base_tree
in 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: (* adding stars to a subtree works:
x |-> ("y", empty) \/ x |-> ("y", empty) \/
x |-> ("x" , f |-> ("f", g |-> ("g", 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.AccessMap.singleton f (Domain.make_starred_leaf MockTraceDomain.top)
|> Domain.make_node MockTraceDomain.top |> Domain.BaseMap.singleton x_base |> Domain.make_node MockTraceDomain.top |> Domain.BaseMap.singleton x_base
in 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: (* widening is not commutative, and is it not join:
x |-> ("x" , f |-> ("f", g |-> ("g", empty))) \/ x |-> ("x" , f |-> ("f", g |-> ("g", empty))) \/
x |-> ("y", empty) = x |-> ("y", empty) =
@ -374,7 +382,7 @@ let tests =
let _, xFG_node = x_subtree in let _, xFG_node = x_subtree in
Domain.BaseMap.singleton x_base (MockTraceDomain.top, xFG_node) Domain.BaseMap.singleton x_base (MockTraceDomain.top, xFG_node)
in 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 in
"widen" >:: widen_test_ "widen" >:: widen_test_
in in
@ -406,10 +414,62 @@ let tests =
assert_equal (Domain.depth xFG_tree) 3 ; assert_equal (Domain.depth xFG_tree) 3 ;
assert_equal (Domain.depth x_star_tree) 1 ; assert_equal (Domain.depth x_star_tree) 1 ;
assert_equal (Domain.depth yF_star_tree) 2 ; 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 in
"depth" >:: depth_test_ "depth" >:: depth_test_
in 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" "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 ]

Write Preview
Loading…
Cancel
Save