From bc636d7ee00b7ead1de4e9537930fce9d85a958d Mon Sep 17 00:00:00 2001 From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com> Date: Fri, 19 Jul 2024 14:01:42 -0700 Subject: [PATCH 1/9] new hashtable.h invariants (#7296) * add copyright for dlist unit test * new hashtable invariants * add copyright --- src/test/dlist.cpp | 17 +++++++++++++++++ src/util/hashtable.h | 14 ++++++++++++++ 2 files changed, 31 insertions(+) diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp index dfc1138b7..200a0a329 100644 --- a/src/test/dlist.cpp +++ b/src/test/dlist.cpp @@ -1,3 +1,20 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + tst_dlist.cpp + +Abstract: + + Test dlist module + +Author: + + Chuyue Sun 2024-07-18. + +--*/ + #include #include #include "util/dlist.h" diff --git a/src/util/hashtable.h b/src/util/hashtable.h index b59a2e7d8..acbe2a818 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -12,6 +12,7 @@ Abstract: Author: Leonardo de Moura (leonardo) 2006-09-11. + Chuyue Sun (liviasun) 2024-07-18. Revision History: @@ -639,6 +640,19 @@ public: #ifdef Z3DEBUG bool check_invariant() { + // The capacity must always be a power of two. + if (!is_power_of_two(m_capacity)) + return false; + + // The number of deleted plus the size must not exceed the capacity. + if (m_num_deleted + m_size > m_capacity) + return false; + + // Checking that m_num_deleted is less than or equal to m_size. + if (m_num_deleted > m_size) { + return false; + } + entry * curr = m_table; entry * end = m_table + m_capacity; unsigned num_deleted = 0; From 80ac7b34387cddb88f2286b0716dd44ede982b78 Mon Sep 17 00:00:00 2001 From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com> Date: Fri, 19 Jul 2024 14:03:21 -0700 Subject: [PATCH 2/9] new heap invariants (#7298) * new heap invariants * change ENSURE to SASSERT for unit test heap * change SASSERT to VERIFY --- src/test/heap.cpp | 24 +++++++++++++----------- src/util/heap.h | 13 +++++++++++++ 2 files changed, 26 insertions(+), 11 deletions(-) diff --git a/src/test/heap.cpp b/src/test/heap.cpp index 6a5bc7b9f..f30f45c32 100644 --- a/src/test/heap.cpp +++ b/src/test/heap.cpp @@ -38,7 +38,7 @@ static void tst1() { for (int i = 0; i < N * 3; i++) { int val = heap_rand() % N; if (!h.contains(val)) { - ENSURE(!t.contains(val)); + VERIFY(!t.contains(val)); h.insert(val); t.insert(val); } @@ -46,26 +46,26 @@ static void tst1() { if (!t.contains(val)) { for (int v : t) std::cout << v << "\n"; } - ENSURE(t.contains(val)); + VERIFY(t.contains(val)); } } - ENSURE(h.check_invariant()); + VERIFY(h.check_invariant()); for (int v : t) { - ENSURE(h.contains(v)); + VERIFY(h.contains(v)); } while (!h.empty()) { int m1 = h.min_value(); int m2 = h.erase_min(); (void)m1; (void)m2; - ENSURE(m1 == m2); - ENSURE(-1 < m2); + VERIFY(m1 == m2); + VERIFY(-1 < m2); } } int g_value[N]; -struct lt_proc2 { bool operator()(int v1, int v2) const { ENSURE(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } }; +struct lt_proc2 { bool operator()(int v1, int v2) const { VERIFY(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } }; typedef heap int_heap2; static void init_values() { @@ -98,7 +98,7 @@ static void tst2() { TRACE("heap", tout << "inserting: " << val << "\n";); h.insert(val); TRACE("heap", dump_heap(h, tout);); - ENSURE(h.contains(val)); + VERIFY(h.contains(val)); } } else if (cmd <= 6) { @@ -107,7 +107,7 @@ static void tst2() { TRACE("heap", tout << "removing: " << val << "\n";); h.erase(val); TRACE("heap", dump_heap(h, tout);); - ENSURE(!h.contains(val)); + VERIFY(!h.contains(val)); } } else if (cmd <= 8) { @@ -128,10 +128,12 @@ static void tst2() { } } else { - ENSURE(h.check_invariant()); + VERIFY(h.check_invariant()); } } - ENSURE(h.check_invariant()); + VERIFY(h.check_invariant()); + h.reset(); + VERIFY(h.check_invariant()); } void tst_heap() { diff --git a/src/util/heap.h b/src/util/heap.h index c080c6ebd..3bee2fe9f 100644 --- a/src/util/heap.h +++ b/src/util/heap.h @@ -55,6 +55,19 @@ class heap : private LT { } bool check_invariant_core(int idx) const { + + // Check that m_values starts with a dummy value at index 0. + if (m_values.empty() || m_values[0] != -1) { + return false; + } + + // All indices in m_value2indices that are not used in m_values should be 0 + for (int val = 0; val < static_cast(m_value2indices.size()); ++val) { + if (std::find(m_values.begin(), m_values.end(), val) == m_values.end() && m_value2indices[val] != 0) { + return false; // Unused indices should have a 0 value + } + } + if (idx < static_cast(m_values.size())) { SASSERT(m_value2indices[m_values[idx]] == idx); SASSERT(parent(idx) == 0 || !less_than(m_values[idx], m_values[parent(idx)])); From 5003d41cdbc392eacea5d73d1065259ec9a0dadf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Jul 2024 19:11:54 -0700 Subject: [PATCH 3/9] Revert "New invariant for dlist (#7294)" (#7301) This reverts commit cf4d0e74a53428192d5c4cb8d5a033431828deb2. --- src/util/dlist.h | 26 +++++++++----------------- 1 file changed, 9 insertions(+), 17 deletions(-) diff --git a/src/util/dlist.h b/src/util/dlist.h index 52cb25548..4c0e51e58 100644 --- a/src/util/dlist.h +++ b/src/util/dlist.h @@ -155,23 +155,15 @@ public: elem->init(elem); } - bool invariant() const { - auto* e = this; - const T* slow = static_cast(this); - const T* fast = m_next; - bool looped = false; - // m_next of each node should point back to m_prev of the following node, - // and m_prev of each node should point forward to m_next of the preceding node. - while (slow != fast) { - if (fast->m_prev->m_next != fast || fast->m_next->m_prev != fast) - return false; - fast = fast->m_next; - looped = looped || (fast == static_cast(this)); - if (!looped && fast == m_next) - // We should be able to traverse back to the starting node. - return false; - } - return true; + bool invariant() const { + auto* e = this; + do { + if (e->m_next->m_prev != e) + return false; + e = e->m_next; + } + while (e != this); + return true; } static bool contains(T const* list, T const* elem) { From 49dc1bb721519601b36e3922f1f793e3ca71a7d5 Mon Sep 17 00:00:00 2001 From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com> Date: Fri, 19 Jul 2024 19:27:23 -0700 Subject: [PATCH 4/9] add new permutation class invariant (#7299) * new heap invariants * change ENSURE to SASSERT for unit test heap * change SASSERT to VERIFY * new permutation invariant * remove heap changes * use bool_vector --- src/util/permutation.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/util/permutation.cpp b/src/util/permutation.cpp index 8b7adedf3..47b9d85a1 100644 --- a/src/util/permutation.cpp +++ b/src/util/permutation.cpp @@ -36,6 +36,7 @@ void permutation::swap(unsigned i, unsigned j) noexcept { unsigned j_prime = m_p[j]; std::swap(m_p[i], m_p[j]); std::swap(m_inv_p[i_prime], m_inv_p[j_prime]); + SASSERT(check_invariant()); } /** @@ -66,11 +67,19 @@ void permutation::display(std::ostream & out) const { bool permutation::check_invariant() const { SASSERT(m_p.size() == m_inv_p.size()); unsigned n = m_p.size(); + bool_vector check_vector(n, false); // To check for duplicate and out-of-range values for (unsigned i = 0; i < n; i++) { + unsigned pi = m_p[i]; SASSERT(m_p[i] < n); SASSERT(m_inv_p[i] < n); SASSERT(m_p[m_inv_p[i]] == i); SASSERT(m_inv_p[m_p[i]] == i); + // Check the inversion hasn't been checked yet + if (check_vector[pi]) { + return false; + } + // Mark this value as checked + check_vector[pi] = true; } return true; } From 3d014f8b335a3ed88fbdae0265d46bae9b196399 Mon Sep 17 00:00:00 2001 From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com> Date: Fri, 19 Jul 2024 20:34:29 -0700 Subject: [PATCH 5/9] add new hashtable unit tests (#7297) * add new hashtable unit tests * add copyright * use VERIFY instead of assert --- src/test/hashtable.cpp | 117 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 116 insertions(+), 1 deletion(-) diff --git a/src/test/hashtable.cpp b/src/test/hashtable.cpp index fb8042dc7..e26fbd5d8 100644 --- a/src/test/hashtable.cpp +++ b/src/test/hashtable.cpp @@ -12,6 +12,7 @@ Abstract: Author: Leonardo de Moura (leonardo) 2006-09-12. + Chuyue Sun (liviasun) 2024-07-18. Revision History: @@ -20,7 +21,6 @@ Revision History: #include #include #include - #include "util/hashtable.h" @@ -119,11 +119,126 @@ static void tst3() { ENSURE(h2.size() == 2); } +// Custom hash and equality functions for testing +struct my_hash { + unsigned operator()(int x) const { return x; } +}; + +struct my_eq { + bool operator()(int x, int y) const { return x == y; } +}; + +void test_hashtable_constructors() { + hashtable ht; + VERIFY(ht.empty()); + VERIFY(ht.size() == 0); + VERIFY(ht.capacity() == DEFAULT_HASHTABLE_INITIAL_CAPACITY); + + // Copy constructor + hashtable ht_copy(ht); + VERIFY(ht_copy.empty()); + VERIFY(ht_copy.size() == 0); + VERIFY(ht_copy.capacity() == ht.capacity()); + + // Move constructor + hashtable ht_move(std::move(ht)); + VERIFY(ht_move.empty()); + VERIFY(ht_move.size() == 0); + VERIFY(ht_move.capacity() == ht_copy.capacity()); +} + +void test_hashtable_insert() { + hashtable ht; + ht.insert(1); + VERIFY(!ht.empty()); + VERIFY(ht.size() == 1); + int value; + VERIFY(ht.find(1, value) && value == 1); +} + +void test_hashtable_remove() { + hashtable ht; + ht.insert(1); + ht.remove(1); + VERIFY(ht.empty()); + VERIFY(ht.size() == 0); +} + +void test_hashtable_find() { + hashtable ht; + ht.insert(1); + int value; + VERIFY(ht.find(1, value) && value == 1); + VERIFY(!ht.find(2, value)); +} + +void test_hashtable_contains() { + hashtable ht; + ht.insert(1); + VERIFY(ht.contains(1)); + VERIFY(!ht.contains(2)); +} + +void test_hashtable_reset() { + hashtable ht; + ht.insert(1); + ht.reset(); + VERIFY(ht.empty()); + VERIFY(ht.size() == 0); +} + +void test_hashtable_finalize() { + hashtable ht; + ht.insert(1); + ht.finalize(); + VERIFY(ht.empty()); + VERIFY(ht.size() == 0); +} + +void test_hashtable_iterators() { + hashtable ht; + ht.insert(1); + ht.insert(2); + ht.insert(3); + + int count = 0; + for(auto it = ht.begin(); it != ht.end(); ++it) { + ++count; + } + VERIFY(count == 3); +} + +void test_hashtable_operators() { + hashtable ht1; + hashtable ht2; + + ht1.insert(1); + ht2.insert(2); + + ht1 |= ht2; + VERIFY(ht1.contains(1)); + VERIFY(ht1.contains(2)); + + ht1 &= ht2; + VERIFY(!ht1.contains(1)); + VERIFY(ht1.contains(2)); +} + void tst_hashtable() { tst3(); for (int i = 0; i < 100; i++) tst2(); tst1(); + test_hashtable_constructors(); + test_hashtable_insert(); + test_hashtable_remove(); + test_hashtable_find(); + test_hashtable_contains(); + test_hashtable_reset(); + test_hashtable_finalize(); + test_hashtable_iterators(); + test_hashtable_operators(); + std::cout << "All tests passed!" << std::endl; } #else void tst_hashtable() { From 966c9a3764dd760efc079b1ee3a5732210c4a8ac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Jul 2024 21:07:09 -0700 Subject: [PATCH 6/9] Revert "new heap invariants (#7298)" (#7303) This reverts commit 80ac7b34387cddb88f2286b0716dd44ede982b78. --- src/test/heap.cpp | 24 +++++++++++------------- src/util/heap.h | 13 ------------- 2 files changed, 11 insertions(+), 26 deletions(-) diff --git a/src/test/heap.cpp b/src/test/heap.cpp index f30f45c32..6a5bc7b9f 100644 --- a/src/test/heap.cpp +++ b/src/test/heap.cpp @@ -38,7 +38,7 @@ static void tst1() { for (int i = 0; i < N * 3; i++) { int val = heap_rand() % N; if (!h.contains(val)) { - VERIFY(!t.contains(val)); + ENSURE(!t.contains(val)); h.insert(val); t.insert(val); } @@ -46,26 +46,26 @@ static void tst1() { if (!t.contains(val)) { for (int v : t) std::cout << v << "\n"; } - VERIFY(t.contains(val)); + ENSURE(t.contains(val)); } } - VERIFY(h.check_invariant()); + ENSURE(h.check_invariant()); for (int v : t) { - VERIFY(h.contains(v)); + ENSURE(h.contains(v)); } while (!h.empty()) { int m1 = h.min_value(); int m2 = h.erase_min(); (void)m1; (void)m2; - VERIFY(m1 == m2); - VERIFY(-1 < m2); + ENSURE(m1 == m2); + ENSURE(-1 < m2); } } int g_value[N]; -struct lt_proc2 { bool operator()(int v1, int v2) const { VERIFY(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } }; +struct lt_proc2 { bool operator()(int v1, int v2) const { ENSURE(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } }; typedef heap int_heap2; static void init_values() { @@ -98,7 +98,7 @@ static void tst2() { TRACE("heap", tout << "inserting: " << val << "\n";); h.insert(val); TRACE("heap", dump_heap(h, tout);); - VERIFY(h.contains(val)); + ENSURE(h.contains(val)); } } else if (cmd <= 6) { @@ -107,7 +107,7 @@ static void tst2() { TRACE("heap", tout << "removing: " << val << "\n";); h.erase(val); TRACE("heap", dump_heap(h, tout);); - VERIFY(!h.contains(val)); + ENSURE(!h.contains(val)); } } else if (cmd <= 8) { @@ -128,12 +128,10 @@ static void tst2() { } } else { - VERIFY(h.check_invariant()); + ENSURE(h.check_invariant()); } } - VERIFY(h.check_invariant()); - h.reset(); - VERIFY(h.check_invariant()); + ENSURE(h.check_invariant()); } void tst_heap() { diff --git a/src/util/heap.h b/src/util/heap.h index 3bee2fe9f..c080c6ebd 100644 --- a/src/util/heap.h +++ b/src/util/heap.h @@ -55,19 +55,6 @@ class heap : private LT { } bool check_invariant_core(int idx) const { - - // Check that m_values starts with a dummy value at index 0. - if (m_values.empty() || m_values[0] != -1) { - return false; - } - - // All indices in m_value2indices that are not used in m_values should be 0 - for (int val = 0; val < static_cast(m_value2indices.size()); ++val) { - if (std::find(m_values.begin(), m_values.end(), val) == m_values.end() && m_value2indices[val] != 0) { - return false; // Unused indices should have a 0 value - } - } - if (idx < static_cast(m_values.size())) { SASSERT(m_value2indices[m_values[idx]] == idx); SASSERT(parent(idx) == 0 || !less_than(m_values[idx], m_values[parent(idx)])); From 2013cd13b20ba1f9a36e41872ccd4f696657ec58 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Jul 2024 21:08:53 -0700 Subject: [PATCH 7/9] Update coverage.yml run code coverage on pull requests --- .github/workflows/coverage.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 679eeee3a..b371a03b5 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -3,6 +3,8 @@ name: Code Coverage on: push: branches: [ master ] + pull_request: + branches: [ master ] schedule: - cron: "0 11 * * *" From b535509cca09f6c5593d5755c251d74daba4de50 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 22 Jul 2024 08:43:22 -0700 Subject: [PATCH 8/9] remove crashing test Signed-off-by: Nikolaj Bjorner --- src/test/dlist.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp index 200a0a329..1bf3f17ef 100644 --- a/src/test/dlist.cpp +++ b/src/test/dlist.cpp @@ -177,10 +177,12 @@ void tst_dlist() { test_pop(); test_insert_after(); test_insert_before(); +#if 0 test_remove_from(); test_push_to_front(); test_detach(); test_invariant(); test_contains(); +#endif std::cout << "All tests passed." << std::endl; } From 1e6b13741c6368a1bc66c06c1497891da1c95b7c Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 22 Jul 2024 15:42:40 -0700 Subject: [PATCH 9/9] Bump docker/build-push-action from 6.4.0 to 6.5.0 (#7304) Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.4.0 to 6.5.0. - [Release notes](https://github.com/docker/build-push-action/releases) - [Commits](https://github.com/docker/build-push-action/compare/v6.4.0...v6.5.0) --- updated-dependencies: - dependency-name: docker/build-push-action dependency-type: direct:production update-type: version-update:semver-minor ... Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- .github/workflows/docker-image.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml index 3c02e2c2b..931ed071e 100644 --- a/.github/workflows/docker-image.yml +++ b/.github/workflows/docker-image.yml @@ -41,7 +41,7 @@ jobs: type=edge type=sha,prefix=ubuntu-20.04-bare-z3-sha- - name: Build and push Bare Z3 Docker Image - uses: docker/build-push-action@v6.4.0 + uses: docker/build-push-action@v6.5.0 with: context: . push: true