From cf4d0e74a53428192d5c4cb8d5a033431828deb2 Mon Sep 17 00:00:00 2001 From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com> Date: Thu, 18 Jul 2024 10:06:58 -0700 Subject: [PATCH] New invariant for dlist (#7294) * unit tests for dlist.h * new invariant for dlist: should be circular. avoid infinite loop * remove dlist test commit * format * format * Update dlist.h --------- Co-authored-by: Nikolaj Bjorner --- src/util/dlist.h | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/src/util/dlist.h b/src/util/dlist.h index 4c0e51e5898..52cb25548d4 100644 --- a/src/util/dlist.h +++ b/src/util/dlist.h @@ -155,15 +155,23 @@ class dll_base { elem->init(elem); } - 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; + 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; } static bool contains(T const* list, T const* elem) {