join for access trees and tests

Reviewed By: mbouaziz

Differential Revision: D3555411

fbshipit-source-id: 3dc8276

infer/src/checkers/accessTree.ml

@@ -132,4 +132,63 @@ module Make (TraceDomain : AbstractDomain.S) = struct
              access_tree_lteq lhs_v rhs_v
            with Not_found -> false)
         lhs
+
+  let node_join f_node_merge f_trace_merge ((trace1, tree1) as node1) ((trace2, tree2) as node2) =
+    if node1 == node2
+    then node1
+    else
+      let trace' = f_trace_merge trace1 trace2 in
+      (* note: this is much-uglified by address equality optimization checks. skip to the else cases
+         for the actual semantics *)
+      match tree1, tree2 with
+      | Subtree subtree1, Subtree subtree2 ->
+          let tree' = AccessMap.merge (fun _ v1 v2 -> f_node_merge v1 v2) subtree1 subtree2 in
+          if trace' == trace1 && tree' == subtree1
+          then node1
+          else if trace' == trace2 && tree' == subtree2
+          then node2
+          else trace', Subtree tree'
+      | Star, Star ->
+          if trace' == trace1
+          then node1
+          else if trace' == trace2
+          then node2
+          else trace', Star
+      | Star, Subtree t ->
+          (* vacuum up all the traces associated with the subtree t and join them with trace' *)
+          let trace'' = join_all_traces trace' t in
+          if trace'' == trace1
+          then node1
+          else trace'', Star
+      | Subtree t, Star ->
+          (* same as above, but kind-of duplicated to allow address equality optimization *)
+          let trace'' = join_all_traces trace' t in
+          if trace'' == trace2
+          then node2
+          else trace'', Star
+
+  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
+
+  let pp fmt base_tree =
+    let rec pp_node fmt (trace, subtree) =
+      let pp_subtree fmt = function
+        | Subtree access_map -> AccessMap.pp ~pp_value:pp_node fmt access_map
+        | Star -> F.fprintf fmt "*" in
+      F.fprintf fmt "(%a, %a)" TraceDomain.pp trace pp_subtree subtree in
+    BaseMap.pp ~pp_value:pp_node fmt base_tree
 end

infer/src/unit/accessTreeTests.ml

@@ -66,29 +66,32 @@ let tests =
   let xF_trace = MockTraceDomain.singleton "xF" in
   let yF_trace = MockTraceDomain.singleton "yF" in
   let xFG_trace = MockTraceDomain.singleton "xFG" in
+  let x_star_trace = MockTraceDomain.of_list ["x"; "xF"; "xFG"] in
 
-  let x_tree =
+  let x_subtree =
     let g_subtree = Domain.make_access_node xF_trace g xFG_trace in
     Domain.AccessMap.singleton f g_subtree
     |> Domain.make_node x_trace in
-  let y_tree =
+  let y_subtree =
     let yF_subtree = Domain.make_starred_leaf yF_trace in
     Domain.AccessMap.singleton f yF_subtree
     |> Domain.make_node y_trace in
-  let z_tree = Domain.make_starred_leaf z_trace in
+  let z_subtree = Domain.make_starred_leaf z_trace in
+
   let tree =
-    Domain.BaseMap.singleton x_base x_tree
-    |> Domain.BaseMap.add y_base y_tree
-    |> Domain.BaseMap.add z_base z_tree in
-
-  (* [tree] is:
-     x |-> ("x",
-            f |-> ("Xf",
-                   g |-> ("xFG", {})))
-     y |-> ("y",
-            f |-> ("yF", * ))
-     z |-> ("z", * )
-  *)
+    Domain.BaseMap.singleton x_base x_subtree
+    |> Domain.BaseMap.add y_base y_subtree
+    |> Domain.BaseMap.add z_base z_subtree in
+  let x_base_tree = Domain.BaseMap.singleton x_base Domain.empty_node in
+  let y_base_tree = Domain.BaseMap.singleton y_base Domain.empty_node in
+  let x_y_base_tree = Domain.BaseMap.add y_base Domain.empty_node x_base_tree in
+  let xFG_tree = Domain.BaseMap.singleton x_base x_subtree in
+
+  let x_star_tree = Domain.BaseMap.singleton x_base (Domain.make_starred_leaf x_trace) in
+  let yF_star_tree = Domain.BaseMap.singleton y_base y_subtree in
+  let x_yF_star_tree = Domain.BaseMap.add y_base y_subtree x_star_tree in
+  let x_star_tree_xFG_trace =
+    Domain.BaseMap.singleton x_base (Domain.make_starred_leaf x_star_trace) in
 
   let open OUnit2 in
   let no_trace = "NONE" in
@@ -134,14 +137,6 @@ let tests =
 
   let lteq_test =
     let lteq_test_ _ =
-      let x_base_tree = Domain.BaseMap.singleton x_base Domain.empty_node in
-      let y_base_tree = Domain.BaseMap.singleton y_base Domain.empty_node in
-      let x_y_base_tree = Domain.BaseMap.add y_base Domain.empty_node x_base_tree in
-      let xFG_tree = Domain.BaseMap.singleton x_base x_tree in
-
-      let x_star_tree = Domain.BaseMap.singleton x_base (Domain.make_starred_leaf x_trace) in
-      let yF_star_tree = Domain.BaseMap.singleton y_base y_tree in
-
       (* regular tree tests *)
       assert_bool "<= equal;" (Domain.(<=) ~lhs:tree ~rhs:tree);
       assert_bool "<= bases" (Domain.(<=) ~lhs:x_base_tree ~rhs:x_y_base_tree);
@@ -185,4 +180,35 @@ let tests =
         (not (Domain.(<=) ~lhs:x_star_tree ~rhs:x_star_tree_diff_trace)) in
     "lteq">::lteq_test_ in
 
-  "access_tree_suite">:::[get_trace_test; lteq_test]
+  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
+    assert_equal ~cmp:base_tree_equal ~pp_diff tree1 tree2 in
+
+  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;
+
+      (* starred |_| starred *)
+      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;
+      (* [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;
+      (* ...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 in
+    "join">::join_test_ in
+
+  "access_tree_suite">:::[get_trace_test; lteq_test; join_test]