Fix leq for PatriciaTreeMap when branches have uneven depths

rust/src/datatype/patricia_tree_impl.rs

@@ -585,20 +585,23 @@ impl<D: AbstractDomain> Node<D> {
                     Self::is_tree_leq_impl(s_left, t_left, implicit_value)
                         && Self::is_tree_leq_impl(s_right, t_right, implicit_value)
                 } else if s_prefix.begins_with(t_prefix) {
-                    // The tree t only contains bindings present in a subtree of s, and s has bindings not present in t.
+                    // The tree s only contains bindings present in a subtree of t, and t has
+                    // bindings not present in s.
                     let branching_bit = s_prefix.get(t_prefix.len());
-                    implicit_value.is_top()
+                    implicit_value.is_bottom()
                         && Self::is_tree_leq_impl(
-                            if !branching_bit { s_left } else { s_right },
-                            t,
+                            s,
+                            if !branching_bit { t_left } else { t_right },
                             implicit_value,
                         )
                 } else if t_prefix.begins_with(s_prefix) {
+                    // The tree t only contains bindings present in a subtree of s, and s has
+                    // bindings not present in t.
                     let branching_bit = t_prefix.get(s_prefix.len());
-                    implicit_value.is_bottom()
+                    implicit_value.is_top()
                         && Self::is_tree_leq_impl(
-                            s,
-                            if !branching_bit { t_left } else { t_right },
+                            if !branching_bit { s_left } else { s_right },
+                            t,
                             implicit_value,
                         )
                 } else {

rust/tests/abstract_environment_test.rs

@@ -150,4 +150,29 @@ mod abstract_environment_test {
         assert!(e1.clone().meet(Environment::bottom()).is_bottom());
         assert!(e1.clone().meet(Environment::top()) == e1);
     }
+
+    #[test]
+    fn test_ptmae_leq_uneven_branch_depths() {
+        type Environment = PatriciaTreeMapAbstractEnvironment<u32, Domain>;
+
+        // `s` maps a strict superset of the keys mapped by `t`. Their Patricia
+        // trees have branch nodes at different depths, so the branch-vs-branch
+        // `leq` path compares a prefix against one of its proper prefixes.
+        let mut s = Environment::top();
+        s.set(0, build_domain(["a"]));
+        s.set(1, build_domain(["c"]));
+        s.set(2, build_domain(["b"]));
+        s.set(3, build_domain(["d"]));
+
+        let mut t = Environment::top();
+        t.set(0, build_domain(["a"]));
+        t.set(2, build_domain(["b"]));
+
+        // The bindings missing from `t` are implicitly Top. `s`'s extra
+        // bindings are <= Top, so s <= t holds.
+        assert!(s.leq(&t));
+        // The bindings missing from `s` are Top, which is not <= the explicit
+        // values in `t`, so t <= s does not hold.
+        assert!(!t.leq(&s));
+    }
 }

rust/tests/abstract_partition_test.rs

@@ -168,4 +168,28 @@ mod abstract_partition_test {
         assert!(p1.clone().meet(Partition::bottom()).is_bottom());
         assert!(p1.clone().meet(Partition::top()) == p1);
     }
+
+    #[test]
+    fn test_ptmap_leq_uneven_branch_depths() {
+        type Partition = PatriciaTreeMapAbstractPartition<u32, Domain>;
+
+        // `s` maps a strict subset of the keys mapped by `t`. Their Patricia
+        // trees have branch nodes at different depths, so the branch-vs-branch
+        // `leq` path compares a prefix against one of its proper prefixes.
+        let mut s = Partition::bottom();
+        s.set(0, build_domain(["a"]));
+        s.set(2, build_domain(["b"]));
+
+        let mut t = Partition::bottom();
+        t.set(0, build_domain(["a"]));
+        t.set(1, build_domain(["c"]));
+        t.set(2, build_domain(["b"]));
+        t.set(3, build_domain(["d"]));
+
+        // The bindings missing from `s` are implicitly Bottom, which is <= any
+        // value, so s <= t holds even though t has extra bindings.
+        assert!(s.leq(&t));
+        // The extra bindings in `t` are not <= Bottom, so t <= s does not hold.
+        assert!(!t.leq(&s));
+    }
 }