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 * * *" 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 diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp index ec6d8d8ba..14991c9ac 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 "util/dlist.h" @@ -157,10 +174,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; } 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() { 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) { 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; 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; }