Skip to content

rust's #[derive(DisjointUnion)] derives incorrect bottom and top. #25

@kaidaniel

Description

@kaidaniel

The "bottom" element of a Lattice is the identity element of the "join" operation.
The "top" element of a Lattice is the identity element of the "meet" operation.

But when using the #[derive(DisjointUnion)] macro, I can create elements for which x.clone().join(bottom) != x and x.clone().meet(top) != x.

Reproducible Example

These tests should pass:

use sparta::datatype::PatriciaTreeSetAbstractDomain;
use sparta::datatype::DisjointUnion;

#[derive(Debug, Clone, PartialEq, Eq, DisjointUnion)]
enum X {
    A(PatriciaTreeSetAbstractDomain<u32>),
    B(PatriciaTreeSetAbstractDomain<u32>),
}
#[test]
fn test_bottom_is_identity_element_of_join_operation() {
    let mut b = X::B(PatriciaTreeSetAbstractDomain::Value(Default::default()));
    let b2 = b.clone();
    b.join_with(X::bottom());
    assert_eq!(b, b2);
}

#[test]
fn test_top_is_identity_element_of_meet_operation() {
    let mut b = X::B(PatriciaTreeSetAbstractDomain::Value(Default::default()));
    let b2 = b.clone();
    b.meet_with(X::top());
    assert_eq!(b, b2);
}

but they fail with the following error message:

---- value::tests::test_bottom_is_identity_element_of_join_operation stdout ----
thread 'value::tests::test_bottom_is_identity_element_of_join_operation' panicked at src/value.rs:237:9:
assertion `left == right` failed
  left: A(Top)
 right: B(Value(PatriciaTreeSet { storage: PatriciaTree { root: None }, _key_type_phantom: PhantomData<u32> }))
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

---- value::tests::test_top_is_identity_element_of_meet_operation stdout ----
thread 'value::tests::test_top_is_identity_element_of_meet_operation' panicked at src/value.rs:245:9:
assertion `left == right` failed
  left: A(Bottom)
 right: B(Value(PatriciaTreeSet { storage: PatriciaTree { root: None }, _key_type_phantom: PhantomData<u32> }))

Solution

replace

fn join_with(&mut self, rhs: Self) {
match (self, rhs) {
#( (#enum_name::#variant_idents(ref mut ldom), #enum_name::#variant_idents(rdom)) => ldom.join_with(rdom), )*
(s, _) => *s = Self::top(),
}
}
fn meet_with(&mut self, rhs: Self) {
match (self, rhs) {
#( (#enum_name::#variant_idents(ref mut ldom), #enum_name::#variant_idents(rdom)) => ldom.meet_with(rdom), )*
(s, _) => *s = Self::bottom(),
}
}
with

    fn join_with(&mut self, rhs: Self) {
        if self.is_bottom() {
            *self = rhs;
            return;
        }
        if rhs.is_bottom() {
            return;
        }
        match (self, rhs) {
           #( (#enum_name::#variant_idents(ref mut ldom), #enum_name::#variant_idents(rdom)) => ldom.join_with(rdom), )* 
           (s, _) => *s = Self::top(), 
        }
    }

    fn meet_with(&mut self, rhs: Self) {
        if self.is_top() {
            *self = rhs;
            return;
        }
        if rhs.is_top() {
            return;
        }
        match (self, rhs) {
          #( (#enum_name::#variant_idents(ref mut ldom), #enum_name::#variant_idents(rdom)) => ldom.meet_with(rdom), )* 
          (s, _) => *s = Self::bottom(), 
        }
    }

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions