diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index a9aaac762..d09467b30 100644 --- a/infer/src/checkers/accessTree.ml +++ b/infer/src/checkers/accessTree.ml @@ -106,64 +106,6 @@ module Make (TraceDomain : AbstractDomain.S) = struct let get_trace ap tree = Option.map fst (get_node ap tree) - (* helper for [add_access]. [last_trace] is the trace associated with [tree] in the parent. *) - let rec access_tree_add_trace ~last_trace ~seen_array_access ~is_exact trace access_list tree = - match access_list, tree with - | [], subtree -> - begin - match is_exact, seen_array_access with - | true, false -> - (* adding x.f, do strong update on both subtree and its traces *) - make_normal_leaf trace - | true, true -> - (* adding x[_], do weak update on subtree and on its immediate trace *) - let trace' = TraceDomain.join last_trace trace in - trace', subtree - | _ -> - (* adding x.f* or x[_]*, join with traces of subtree and replace it with * *) - let trace' = join_all_traces (TraceDomain.join last_trace trace) subtree in - make_starred_leaf trace' - end - | _, Star -> - let trace' = TraceDomain.join last_trace trace in - make_starred_leaf trace' - | access :: accesses, Subtree subtree -> - let access_trace, access_subtree = - try AccessMap.find access subtree - with Not_found -> make_normal_leaf TraceDomain.initial 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 - let access_node' = - access_tree_add_trace ~last_trace:access_trace - ~seen_array_access - ~is_exact - trace - accesses - access_subtree in - last_trace, Subtree (AccessMap.add access access_node' subtree) - - (** add [ap] to [tree] and associate its leaf node with [trace]. - if [ap] or a suffix of [ap] is not already present in the tree, it will be added with empty - traces associated with each of the inner nodes. - if [ap] is already present in the tree and contains no array accesses, this overwrites the - existing trace. if [ap] does contain array accesses, it joins the existing trace with [trace]. - *) - let add_trace ap trace tree = - let base, accesses = AccessPath.extract ap in - let is_exact = AccessPath.is_exact ap in - let base_trace, base_tree = - try BaseMap.find base tree - with Not_found -> make_normal_leaf TraceDomain.initial in - let base_node' = - access_tree_add_trace - ~last_trace:base_trace ~seen_array_access:false ~is_exact trace accesses base_tree in - BaseMap.add base base_node' tree - let rec access_tree_lteq ((lhs_trace, lhs_tree) as lhs) ((rhs_trace, rhs_tree) as rhs) = if lhs == rhs then true @@ -223,22 +165,78 @@ module Make (TraceDomain : AbstractDomain.S) = struct then node2 else trace'', Star + let rec node_merge node1_opt node2_opt = + match node1_opt, node2_opt with + | Some node1, Some node2 -> + let joined_node = node_join node_merge TraceDomain.join node1 node2 in + if joined_node == node1 + then node1_opt + else if joined_node == node2 + then node2_opt + else Some joined_node + | None, node_opt | node_opt, None -> + node_opt + + (* 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 = + match accesses, node with + | [], (trace, tree) -> + begin + match is_exact, seen_array_access with + | true, false -> + (* adding x.f, do strong update on both subtree and its traces *) + node_to_add + | true, true -> + (* adding x[_], do weak update on subtree and on its immediate trace *) + node_join node_merge TraceDomain.join node_to_add node + | _ -> + (* adding x.f* or x[_]*, join with traces of subtree and replace it with * *) + let node_trace, node_tree = node_to_add in + let trace' = join_all_traces (TraceDomain.join trace node_trace) tree in + make_starred_leaf (join_all_traces trace' node_tree) + end + | _, (_, Star) -> + node_join node_merge TraceDomain.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.initial 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 + 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 + + (** add ([ap], [node]) to [tree]. *) + let add_node ap node_to_add tree = + let base, accesses = AccessPath.extract ap in + let is_exact = AccessPath.is_exact ap in + let base_node = + try BaseMap.find base tree + with Not_found -> make_normal_leaf TraceDomain.initial in + let base_node' = + access_tree_add_trace ~node_to_add ~seen_array_access:false ~is_exact accesses base_node in + BaseMap.add base base_node' tree + + (** add [ap] to [tree] and associate its leaf node with [trace]. + if [ap] or a suffix of [ap] is not already present in the tree, it will be added with empty + traces associated with each of the inner nodes. + if [ap] is already present in the tree and contains no array accesses, this overwrites the + existing trace. if [ap] does contain array accesses, it joins the existing trace with [trace]. + *) + let add_trace ap trace tree = + add_node ap (make_normal_leaf trace) tree + let join tree1 tree2 = if tree1 == tree2 then tree1 - else - let rec node_merge node1_opt node2_opt = - match node1_opt, node2_opt with - | Some node1, Some node2 -> - let joined_node = node_join node_merge TraceDomain.join node1 node2 in - if joined_node == node1 - then node1_opt - else if joined_node == node2 - then node2_opt - else Some joined_node - | None, node_opt | node_opt, None -> - node_opt in - BaseMap.merge (fun _ n1 n2 -> node_merge n1 n2) tree1 tree2 + else BaseMap.merge (fun _ n1 n2 -> node_merge n1 n2) tree1 tree2 (* replace the normal leaves of [node] with starred leaves *) let rec node_add_stars ((trace, tree) as node) = match tree with diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml index 91154c1ca..7b4746433 100644 --- a/infer/src/unit/accessTreeTests.ml +++ b/infer/src/unit/accessTreeTests.ml @@ -83,6 +83,8 @@ let tests = let zF = AccessPath.Exact (make_access_path "z" ["f"]) in let zFG = AccessPath.Exact (make_access_path "z" ["f"; "g"]) in + let xArr = + AccessPath.Exact (make_base "x", [array]) in let xArrF = let accesses = [array; make_field_access "f"] in AccessPath.Exact (make_base "x", accesses) in @@ -208,10 +210,13 @@ let tests = Domain.BaseMap.singleton x_base (Domain.make_normal_leaf trace) |> Domain.BaseMap.add y_base Domain.empty_node in - let mk_xFG_tree leaf_trace = + let mk_xFG_node leaf_trace = Domain.make_access_node MockTraceDomain.empty g leaf_trace |> Domain.AccessMap.singleton f - |> Domain.make_node MockTraceDomain.empty + |> Domain.make_node MockTraceDomain.empty in + + let mk_xFG_tree leaf_trace = + mk_xFG_node leaf_trace |> Domain.BaseMap.singleton x_base in let mk_xArrF_tree leaf_trace = @@ -254,7 +259,6 @@ let tests = (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 = @@ -289,7 +293,27 @@ let tests = |> Domain.BaseMap.singleton x_base in assert_trees_equal (Domain.add_trace xF_star added_trace xFG_tree) - xF_star_tree_joined_traces in + 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; + + (* case (2): adding a non-empty node does weak updates when required *) + let arr_tree = + let arr_subtree = + Domain.AccessMap.singleton f (Domain.make_normal_leaf array_f_trace) + |> Domain.AccessMap.add g (Domain.make_normal_leaf xFG_trace) in + 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 in "add_trace">::add_trace_test_ in