diff --git a/rust-proc-macros/src/lib.rs b/rust-proc-macros/src/lib.rs index d3adddf..407c262 100644 --- a/rust-proc-macros/src/lib.rs +++ b/rust-proc-macros/src/lib.rs @@ -86,6 +86,8 @@ pub fn derive_disjoint_union(input: TokenStream) -> TokenStream { fn join_with(&mut self, rhs: Self) { match (self, rhs) { + (_, r) if r.is_bottom() => {/*do nothing because bottom is the identity element of join*/}, + (s, r) if s.is_bottom() => *s = r, #( (#enum_name::#variant_idents(ref mut ldom), #enum_name::#variant_idents(rdom)) => ldom.join_with(rdom), )* (s, _) => *s = Self::top(), } @@ -93,6 +95,8 @@ pub fn derive_disjoint_union(input: TokenStream) -> TokenStream { fn meet_with(&mut self, rhs: Self) { match (self, rhs) { + (_, r) if r.is_top() => {/*do nothing because top is the identity element of meet*/}, + (s, r) if s.is_top() => *s = r, #( (#enum_name::#variant_idents(ref mut ldom), #enum_name::#variant_idents(rdom)) => ldom.meet_with(rdom), )* (s, _) => *s = Self::bottom(), } diff --git a/rust/tests/datatype/disjoint_union_test.rs b/rust/tests/disjoint_union_test.rs similarity index 81% rename from rust/tests/datatype/disjoint_union_test.rs rename to rust/tests/disjoint_union_test.rs index 02c873e..8b24d8e 100644 --- a/rust/tests/datatype/disjoint_union_test.rs +++ b/rust/tests/disjoint_union_test.rs @@ -11,7 +11,8 @@ use sparta::datatype::AbstractDomain; use sparta::datatype::DisjointUnion; use sparta::datatype::HashSetAbstractDomain; -#[derive(Clone, DisjointUnion, PartialEq, Eq)] +#[allow(dead_code)] +#[derive(Clone, DisjointUnion, PartialEq, Eq, Debug)] enum MyUnionedDomain { FirstCase(HashSetAbstractDomain), SecondCase(HashSetAbstractDomain), @@ -119,6 +120,31 @@ fn test_meet_diff_arm() { assert!(met_mudom.is_bottom()); } +#[test] +fn test_bottom_is_right_identity_of_join() { + let mudom = MyUnionedDomain::SecondCase([1].into_iter().collect()); + assert_eq!(mudom.clone().join(MyUnionedDomain::bottom()), mudom.clone()); +} + +#[test] +fn test_bottom_is_left_identity_of_join() { + let mudom = MyUnionedDomain::SecondCase([1].into_iter().collect()); + assert_eq!(MyUnionedDomain::bottom().join(mudom.clone()), mudom); +} + +#[test] +fn test_top_is_right_identity_of_meet() { + let mudom = MyUnionedDomain::SecondCase([1].into_iter().collect()); + assert_eq!(mudom.clone().meet(MyUnionedDomain::top()), mudom.clone()); +} + +#[test] +fn test_top_is_left_identity_of_meet() { + let mudom = MyUnionedDomain::SecondCase([1].into_iter().collect()); + assert_eq!(MyUnionedDomain::top().meet(mudom.clone()), mudom); +} + +#[allow(dead_code)] #[derive(Clone, DisjointUnion, PartialEq, Eq)] enum TestGenericsDeriveTypechecks where @@ -129,6 +155,7 @@ where SecondCase(HashSetAbstractDomain), } +#[allow(dead_code)] #[derive(Clone, DisjointUnion, PartialEq, Eq)] enum TestGenericsDeriveForWholeDomainTypechecks where