facebook / SPARTA

SPARTA is a library of software components specially designed for building high-performance static analyzers based on the theory of Abstract Interpretation.
MIT License
635 stars 49 forks source link

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

Open kaidaniel opened 1 month ago

kaidaniel commented 1 month ago

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 https://github.com/facebook/SPARTA/blob/bd758a81954dc2c8fe75c8b32ab42d327fc4d895/rust-proc-macros/src/lib.rs#L87-L99 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(), 
        }
    }
yuxuanchen1997 commented 1 month ago

Hey @kaidaniel, thank you for finding the bug. Since you have the solution, do you want to create a PR to fix this? You can also add your example to a test.

If you intend to do that, a small suggestion is to incorporate the two if statements into the pattern matching here.

kaidaniel commented 1 month ago

Hi @yuxuanchen1997 - yes I'll go ahead and raise the PR :)