From a02988ef64f062dce138c33aafc36b7f95542f55 Mon Sep 17 00:00:00 2001 From: Kai Daniel Date: Tue, 22 Oct 2024 21:30:07 +0100 Subject: [PATCH 1/6] move file so cargo can detect it --- rust/tests/{datatype => }/disjoint_union_test.rs | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename rust/tests/{datatype => }/disjoint_union_test.rs (100%) diff --git a/rust/tests/datatype/disjoint_union_test.rs b/rust/tests/disjoint_union_test.rs similarity index 100% rename from rust/tests/datatype/disjoint_union_test.rs rename to rust/tests/disjoint_union_test.rs From 4d7d36fa5fd8a5973cf4efb185f6396b7b78a6aa Mon Sep 17 00:00:00 2001 From: Kai Daniel Date: Tue, 22 Oct 2024 22:02:03 +0100 Subject: [PATCH 2/6] allow dead code in test --- rust/tests/disjoint_union_test.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/rust/tests/disjoint_union_test.rs b/rust/tests/disjoint_union_test.rs index 02c873e..28f757d 100644 --- a/rust/tests/disjoint_union_test.rs +++ b/rust/tests/disjoint_union_test.rs @@ -11,6 +11,7 @@ use sparta::datatype::AbstractDomain; use sparta::datatype::DisjointUnion; use sparta::datatype::HashSetAbstractDomain; +#[allow(dead_code)] #[derive(Clone, DisjointUnion, PartialEq, Eq)] enum MyUnionedDomain { FirstCase(HashSetAbstractDomain), @@ -119,6 +120,7 @@ fn test_meet_diff_arm() { assert!(met_mudom.is_bottom()); } +#[allow(dead_code)] #[derive(Clone, DisjointUnion, PartialEq, Eq)] enum TestGenericsDeriveTypechecks where @@ -129,6 +131,7 @@ where SecondCase(HashSetAbstractDomain), } +#[allow(dead_code)] #[derive(Clone, DisjointUnion, PartialEq, Eq)] enum TestGenericsDeriveForWholeDomainTypechecks where From f3b8fb756f0919f0dcc3250a99d23a8d640534e4 Mon Sep 17 00:00:00 2001 From: Kai Daniel Date: Tue, 22 Oct 2024 22:28:37 +0100 Subject: [PATCH 3/6] add failing test --- rust/tests/disjoint_union_test.rs | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/rust/tests/disjoint_union_test.rs b/rust/tests/disjoint_union_test.rs index 28f757d..d0f6378 100644 --- a/rust/tests/disjoint_union_test.rs +++ b/rust/tests/disjoint_union_test.rs @@ -12,7 +12,7 @@ use sparta::datatype::DisjointUnion; use sparta::datatype::HashSetAbstractDomain; #[allow(dead_code)] -#[derive(Clone, DisjointUnion, PartialEq, Eq)] +#[derive(Clone, DisjointUnion, PartialEq, Eq, Debug)] enum MyUnionedDomain { FirstCase(HashSetAbstractDomain), SecondCase(HashSetAbstractDomain), @@ -120,6 +120,20 @@ fn test_meet_diff_arm() { assert!(met_mudom.is_bottom()); } +#[test] +fn test_bottom_is_identity_element_of_join_operation() { + let hsdom: HashSetAbstractDomain<_> = [1, 2].into_iter().collect(); + let mudom = MyUnionedDomain::SecondCase(hsdom); + assert_eq!(mudom.clone().join(AbstractDomain::bottom()), mudom.clone()); +} + +#[test] +fn test_top_is_identity_element_of_meet_operation() { + let hsdom: HashSetAbstractDomain<_> = [1, 2].into_iter().collect(); + let mudom = MyUnionedDomain::SecondCase(hsdom); + assert_eq!(mudom.clone().meet(AbstractDomain::top()), mudom.clone()); +} + #[allow(dead_code)] #[derive(Clone, DisjointUnion, PartialEq, Eq)] enum TestGenericsDeriveTypechecks From ccd4298a336a68eb8899c85e69ac8d19f370f4a2 Mon Sep 17 00:00:00 2001 From: Kai Daniel Date: Tue, 22 Oct 2024 22:44:53 +0100 Subject: [PATCH 4/6] add left identity tests --- rust/tests/disjoint_union_test.rs | 26 ++++++++++++++++++++++---- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/rust/tests/disjoint_union_test.rs b/rust/tests/disjoint_union_test.rs index d0f6378..39be32b 100644 --- a/rust/tests/disjoint_union_test.rs +++ b/rust/tests/disjoint_union_test.rs @@ -121,17 +121,35 @@ fn test_meet_diff_arm() { } #[test] -fn test_bottom_is_identity_element_of_join_operation() { +fn test_bottom_is_right_identity_of_join() { let hsdom: HashSetAbstractDomain<_> = [1, 2].into_iter().collect(); let mudom = MyUnionedDomain::SecondCase(hsdom); - assert_eq!(mudom.clone().join(AbstractDomain::bottom()), mudom.clone()); + let bottom = MyUnionedDomain::bottom(); + assert_eq!(mudom.clone().join(bottom), mudom.clone()); } #[test] -fn test_top_is_identity_element_of_meet_operation() { +fn test_bottom_is_left_identity_of_join() { let hsdom: HashSetAbstractDomain<_> = [1, 2].into_iter().collect(); let mudom = MyUnionedDomain::SecondCase(hsdom); - assert_eq!(mudom.clone().meet(AbstractDomain::top()), mudom.clone()); + let bottom = MyUnionedDomain::bottom(); + assert_eq!(bottom.clone().join(mudom), bottom.clone()); +} + +#[test] +fn test_top_is_right_identity_of_meet() { + let hsdom: HashSetAbstractDomain<_> = [1, 2].into_iter().collect(); + let mudom = MyUnionedDomain::SecondCase(hsdom); + let top = MyUnionedDomain::top(); + assert_eq!(mudom.clone().meet(top), mudom.clone()); +} + +#[test] +fn test_top_is_left_identity_of_meet() { + let hsdom: HashSetAbstractDomain<_> = [1, 2].into_iter().collect(); + let mudom = MyUnionedDomain::SecondCase(hsdom); + let top = MyUnionedDomain::top(); + assert_eq!(top.clone().meet(mudom), top.clone()); } #[allow(dead_code)] From d8dc266bf976ef8f9ec37f2f34f97c164143bc7d Mon Sep 17 00:00:00 2001 From: Kai Daniel Date: Tue, 22 Oct 2024 22:45:28 +0100 Subject: [PATCH 5/6] add (incorrect) solutoin --- rust-proc-macros/src/lib.rs | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/rust-proc-macros/src/lib.rs b/rust-proc-macros/src/lib.rs index d3adddf..15b0d92 100644 --- a/rust-proc-macros/src/lib.rs +++ b/rust-proc-macros/src/lib.rs @@ -85,6 +85,13 @@ pub fn derive_disjoint_union(input: TokenStream) -> TokenStream { } 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(), @@ -92,6 +99,13 @@ pub fn derive_disjoint_union(input: TokenStream) -> TokenStream { } 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(), From fedd8a89eb44c6cd29f424e1f59cfbcd920e7cf8 Mon Sep 17 00:00:00 2001 From: Kai Daniel Date: Wed, 23 Oct 2024 11:38:43 +0100 Subject: [PATCH 6/6] correct tests and put if into match --- rust-proc-macros/src/lib.rs | 18 ++++-------------- rust/tests/disjoint_union_test.rs | 24 ++++++++---------------- 2 files changed, 12 insertions(+), 30 deletions(-) diff --git a/rust-proc-macros/src/lib.rs b/rust-proc-macros/src/lib.rs index 15b0d92..407c262 100644 --- a/rust-proc-macros/src/lib.rs +++ b/rust-proc-macros/src/lib.rs @@ -85,28 +85,18 @@ pub fn derive_disjoint_union(input: TokenStream) -> TokenStream { } fn join_with(&mut self, rhs: Self) { - if self.is_bottom() { - *self = rhs; - return; - } - if rhs.is_bottom() { - return; - } 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(), } } fn meet_with(&mut self, rhs: Self) { - if self.is_top() { - *self = rhs; - return; - } - if rhs.is_top() { - return; - } 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/disjoint_union_test.rs b/rust/tests/disjoint_union_test.rs index 39be32b..8b24d8e 100644 --- a/rust/tests/disjoint_union_test.rs +++ b/rust/tests/disjoint_union_test.rs @@ -122,34 +122,26 @@ fn test_meet_diff_arm() { #[test] fn test_bottom_is_right_identity_of_join() { - let hsdom: HashSetAbstractDomain<_> = [1, 2].into_iter().collect(); - let mudom = MyUnionedDomain::SecondCase(hsdom); - let bottom = MyUnionedDomain::bottom(); - assert_eq!(mudom.clone().join(bottom), mudom.clone()); + 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 hsdom: HashSetAbstractDomain<_> = [1, 2].into_iter().collect(); - let mudom = MyUnionedDomain::SecondCase(hsdom); - let bottom = MyUnionedDomain::bottom(); - assert_eq!(bottom.clone().join(mudom), bottom.clone()); + 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 hsdom: HashSetAbstractDomain<_> = [1, 2].into_iter().collect(); - let mudom = MyUnionedDomain::SecondCase(hsdom); - let top = MyUnionedDomain::top(); - assert_eq!(mudom.clone().meet(top), mudom.clone()); + 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 hsdom: HashSetAbstractDomain<_> = [1, 2].into_iter().collect(); - let mudom = MyUnionedDomain::SecondCase(hsdom); - let top = MyUnionedDomain::top(); - assert_eq!(top.clone().meet(mudom), top.clone()); + let mudom = MyUnionedDomain::SecondCase([1].into_iter().collect()); + assert_eq!(MyUnionedDomain::top().meet(mudom.clone()), mudom); } #[allow(dead_code)]