From b2c422827a5d89907be610f2ae9ec2265c14030d Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Wed, 13 Jul 2016 07:44:16 -0700
Subject: [PATCH] adding <=, tests to access tree domain

Reviewed By: mbouaziz

Differential Revision: D3546470

fbshipit-source-id: a31045f
---
 infer/src/checkers/accessTree.ml  | 31 +++++++++++++++++
 infer/src/unit/accessTreeTests.ml | 56 ++++++++++++++++++++++++++++++-
 2 files changed, 86 insertions(+), 1 deletion(-)

diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml
index 8762c98c8..d9afe6751 100644
--- a/infer/src/checkers/accessTree.ml
+++ b/infer/src/checkers/accessTree.ml
@@ -101,4 +101,35 @@ module Make (TraceDomain : AbstractDomain.S) = struct
           Some (join_all_traces trace subtree)
     | exception Not_found ->
         None
+
+  let rec access_tree_lteq ((lhs_trace, lhs_tree) as lhs) ((rhs_trace, rhs_tree) as rhs) =
+    if lhs == rhs
+    then true
+    else
+      TraceDomain.(<=) ~lhs:lhs_trace ~rhs:rhs_trace &&
+      match lhs_tree, rhs_tree with
+      | Subtree lhs_subtree, Subtree rhs_subtree ->
+          AccessMap.for_all
+            (fun k lhs_v ->
+               try
+                 let rhs_v = AccessMap.find k rhs_subtree in
+                 access_tree_lteq lhs_v rhs_v
+               with Not_found -> false)
+            lhs_subtree
+      | _, Star ->
+          true
+      | Star, Subtree _ ->
+          false
+
+  let (<=) ~lhs ~rhs =
+    if lhs == rhs
+    then true
+    else
+      BaseMap.for_all
+        (fun k lhs_v ->
+           try
+             let rhs_v = BaseMap.find k rhs in
+             access_tree_lteq lhs_v rhs_v
+           with Not_found -> false)
+        lhs
 end
diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml
index 505989a44..49bf17bbb 100644
--- a/infer/src/unit/accessTreeTests.ml
+++ b/infer/src/unit/accessTreeTests.ml
@@ -131,4 +131,58 @@ let tests =
       assert_traces_eq yFG tree "{ yF }";
       assert_trace_not_found yG tree in
     "get_trace">::get_trace_test_ in
-  "access_tree_suite">:::[get_trace_test]
+
+  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);
+      assert_bool "<= regular1" (Domain.(<=) ~lhs:x_base_tree ~rhs:xFG_tree);
+      assert_bool "<= regular2" (Domain.(<=) ~lhs:xFG_tree ~rhs:tree);
+      assert_bool "<= regular3" (Domain.(<=) ~lhs:y_base_tree ~rhs:tree);
+      assert_bool "<= bases negative1" (not (Domain.(<=) ~lhs:x_y_base_tree ~rhs:x_base_tree));
+      assert_bool "<= bases negative2" (not (Domain.(<=) ~lhs:x_base_tree ~rhs:y_base_tree));
+      assert_bool "<= negative1" (not (Domain.(<=) ~lhs:xFG_tree ~rhs:y_base_tree));
+      assert_bool "<= negative2" (not (Domain.(<=) ~lhs:tree ~rhs:xFG_tree));
+
+      (* star tree tests *)
+      assert_bool "<= star lhs equal" (Domain.(<=) ~lhs:x_star_tree ~rhs:x_star_tree);
+      assert_bool "<= star rhs1" (Domain.(<=) ~lhs:x_base_tree ~rhs:x_star_tree);
+      assert_bool "<= star rhs2" (Domain.(<=) ~lhs:xFG_tree ~rhs:x_star_tree);
+      assert_bool "<= star rhs3" (Domain.(<=) ~lhs:y_base_tree ~rhs:yF_star_tree);
+      assert_bool "<= star rhs4" (Domain.(<=) ~lhs:yF_star_tree ~rhs:tree);
+      assert_bool "<= star lhs negative1" (not (Domain.(<=) ~lhs:x_star_tree ~rhs:x_base_tree));
+      assert_bool "<= star lhs negative2" (not (Domain.(<=) ~lhs:x_star_tree ~rhs:xFG_tree));
+      assert_bool "<= star lhs negative3" (not (Domain.(<=) ~lhs:yF_star_tree ~rhs:y_base_tree));
+      assert_bool "<= star lhs negative4" (not (Domain.(<=) ~lhs:tree ~rhs:yF_star_tree));
+
+      (* <= tree but not <= trace tests *)
+      (* same as x_base_tree, but with a trace higher in the traces lattice *)
+      let x_base_tree_higher_trace =
+        Domain.BaseMap.singleton x_base (Domain.make_normal_leaf y_trace) in
+      (* same as x_star_tree, but with a trace incomparable in the traces lattice *)
+      let x_star_tree_diff_trace =
+        Domain.BaseMap.singleton x_base (Domain.make_starred_leaf y_trace) in
+      assert_bool
+        "(x, {}) <= (x, {y})"
+        (Domain.(<=) ~lhs:x_base_tree ~rhs:x_base_tree_higher_trace);
+      assert_bool
+        "(x, {y}) not <= (x, {})"
+        (not (Domain.(<=) ~lhs:x_base_tree_higher_trace ~rhs:x_base_tree));
+      assert_bool
+        "(x*, {y})* not <= (x*, {x})"
+        (not (Domain.(<=) ~lhs:x_star_tree_diff_trace ~rhs:x_star_tree));
+      assert_bool
+        "(x*, {x})* not <= (x*, {y})"
+        (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]