[SpecBot] Add formal specifications to Z3 utility data structures

[github-actions[bot]]

✨ Automatic Specification Mining

This discussion proposes formal specifications (class invariants, pre/post-conditions) to improve code correctness and maintainability for core Z3 utility data structures.

📋 Classes Analyzed

• vector(T) in src/util/vector.h
• core_hashtable in src/util/hashtable.h
• lim_svector(T) in src/util/lim_vector.h

🔍 Specifications Proposed

---

1. vector(T) Class (src/util/vector.h)

Class Invariants

Invariant 1: Size-Capacity Relationship

• Assertion: SASSERT(m_data == nullptr || size() <= capacity())
• Rationale: The number of elements must never exceed allocated capacity. This is fundamental to preventing buffer overflows and maintaining memory safety.
• Placement: Add to a check_invariant() method called after state-modifying operations

Invariant 2: Null Pointer Consistency

• Assertion: SASSERT(m_data != nullptr || (size() == 0 && capacity() == 0))
• Rationale: When m_data is null, both size and capacity must be zero (empty vector state). This ensures consistent representation of empty vectors.
• Placement: In check_invariant() method

Invariant 3: Metadata Memory Alignment

• Assertion: SASSERT(m_data == nullptr || reinterpret_cast(uintptr_t)(m_data) % alignof(T) == 0)
• Rationale: Ensures proper alignment of stored elements, critical for correctness on architectures with strict alignment requirements and for performance.
• Placement: In check_invariant() method

Invariant 4: Capacity Growth Validity

• Assertion: SASSERT(m_data == nullptr || capacity() >= 2) (after first expansion)
• Rationale: After initial allocation, capacity should always be at least 2, following the growth strategy in expand_vector().
• Placement: After expand_vector() completes

Pre-conditions

Method: operator[](SZ idx) and get(SZ idx)

• Pre-condition: Index within bounds
• Assertion: SASSERT(idx < size())
• Status: ✅ Already present (lines 364, 369, 374, 379, 384, 389)

Method: back()

• Pre-condition: Vector is non-empty
• Assertion: SASSERT(!empty())
• Status: ✅ Already present (lines 394, 399)

Method: pop_back()

• Pre-condition: Vector is non-empty
• Assertion: SASSERT(!empty())
• Status: ✅ Already present (line 404)

Method: erase(iterator pos)

• Pre-condition: Iterator is valid
• Assertion: SASSERT(pos >= begin() && pos < end())
• Status: ✅ Already present (line 441)

Method: init(SZ s) - NEW

• Pre-condition: Vector must be uninitialized
• Assertion: SASSERT(m_data == nullptr)
• Rationale: Prevents double initialization which would leak memory
• Status: ✅ Already present (line 139)

Post-conditions

Method: push_back(T const & elem)

• Post-condition: Size increases by one
• Assertion: SASSERT(size() == old_size + 1) (requires capturing old_size)
• Rationale: Ensures the element was actually added

Method: expand_vector() - NEW

• Post-condition: Capacity increased
• Assertion: SASSERT(capacity() > old_capacity)
• Rationale: Guarantees forward progress in capacity growth, preventing infinite loops

Method: reset() / clear()

• Post-condition: Size is zero
• Assertion: SASSERT(size() == 0)
• Rationale: Ensures the vector is properly cleared

---

2. core_hashtable Class (src/util/hashtable.h)

Class Invariants

The class already has a comprehensive check_invariant() method (lines 640-669) that validates:

• ✅ Capacity is a power of two
• ✅ m_num_deleted + m_size <= m_capacity
• ✅ m_num_deleted <= m_size
• ✅ Actual count of deleted/used entries matches metadata

Additional Invariants Proposed

Invariant 1: Non-null Table Pointer

• Assertion: SASSERT(m_table != nullptr)
• Rationale: The table pointer should never be null after construction. Current design always allocates at least DEFAULT_HASHTABLE_INITIAL_CAPACITY (8) entries.
• Placement: In check_invariant() method

Invariant 2: Minimum Capacity

• Assertion: SASSERT(m_capacity >= DEFAULT_HASHTABLE_INITIAL_CAPACITY || memory::is_out_of_memory())
• Rationale: Capacity should never fall below the initial capacity unless in OOM state
• Placement: In check_invariant() method

Invariant 3: Load Factor Upper Bound

• Assertion: SASSERT((m_size + m_num_deleted) * 4 <= m_capacity * 3 + 1) (relaxed by 1 for off-by-one)
• Rationale: The hash table maintains a load factor of at most 75% (3/4) to ensure good performance. This is enforced by expand_table() but worth checking as an invariant.
• Placement: After insert() operations complete

Pre-conditions

Method: insert(data && e)

• Pre-condition: Hash function doesn't cause overflow
• Note: This is implicitly assumed but difficult to assert without access to the hash computation
• Current Status: Relies on well-behaved HashProc

Method: expand_table() - NEW

• Pre-condition: Not in out-of-memory state (for reliability)
• Assertion: SASSERT(!memory::is_out_of_memory())
• Rationale: Expanding in OOM state is futile and could cause issues

Post-conditions

Method: insert(data const & e) - NEW

• Post-condition: Element is in the table
• Assertion: SASSERT(contains(e))
• Rationale: Verifies successful insertion (but note: expensive, should be #ifdef DEBUG)
• Note: Current assertion at line 569 checks !contains(e) before insertion in insert_if_not_there_core, which is good

Method: reset() - NEW

• Post-condition: Table is empty
• Assertion: SASSERT(m_size == 0 && m_num_deleted == 0)
• Rationale: Ensures complete reset of table state

---

3. lim_svector(T) Class (src/util/lim_vector.h)

This is a smaller class but with critical scope-management invariants.

Class Invariants

Invariant 1: Monotonic Scope Sizes

• Assertion:

  bool check_scope_invariant() const {
      for (unsigned i = 1; i < m_lim.size(); ++i) {
          SASSERT(m_lim[i-1] <= m_lim[i]);
      }
      return true;
  }

• Rationale: Scope boundaries must be monotonically increasing - each new scope starts at or after the previous scope's boundary. This is fundamental to the backtracking mechanism.
• Placement: Called at the end of push_scope() and pop_scope()

Invariant 2: Last Scope Boundary Validity

• Assertion: SASSERT(m_lim.empty() || m_lim.back() <= this->size())
• Rationale: The last scope boundary must not exceed the current vector size. Elements beyond the last scope boundary would be inaccessible.
• Placement: After any operation that modifies m_lim or the base vector size

Invariant 3: Scope Stack Non-negativity

• Assertion: SASSERT(num_scopes() >= 0) (trivially true for unsigned, but documents intent)
• Rationale: Documents that scope count cannot be negative

Pre-conditions

Method: pop_scope(unsigned num_scopes)

• Pre-condition: Sufficient scopes exist
• Assertion: SASSERT(num_scopes > 0 && num_scopes <= m_lim.size())
• Rationale: Cannot pop more scopes than have been pushed
• Status: Partially present - line 30 checks num_scopes > 0, should also verify num_scopes <= m_lim.size()

Method: old_size(unsigned n) - NEW

• Pre-condition: Valid scope offset
• Assertion: SASSERT(n > 0 && n <= m_lim.size())
• Rationale: The parameter n must reference a valid scope in the stack
• Status: ❌ Missing, should be added

Post-conditions

Method: push_scope()

• Post-condition: Scope count increased
• Assertion: SASSERT(num_scopes() == old_scope_count + 1)
• Rationale: Verifies scope was successfully pushed

Method: pop_scope(unsigned num_scopes) - NEW

• Post-condition: Vector size restored
• Assertion: SASSERT(this->size() == m_lim[m_lim.size()]) (after restoring old size)
• Rationale: Ensures vector was properly truncated to the scope boundary
• Note: This is implicitly guaranteed by shrink() call on line 32

---

🎯 Goals Achieved

• ✅ Improved code documentation: Specifications make implicit contracts explicit
• ✅ Early bug detection: Runtime checks can catch violations before they cause corruption
• ✅ Better understanding: Class invariants clarify the intended behavior and constraints
• ✅ Foundation for verification: Formal specifications enable future verification efforts

⚠️ Review Notes

1. Performance Considerations:

   • Most new invariants suggested are O(1) checks suitable for debug builds
   • The scope monotonicity check in lim_svector is O(n) in scope count - should be #ifdef DEBUG or called selectively

2. Implementation Strategy:

   • Add check_invariant() methods where missing (e.g., in vector(T))
   • Call invariant checks at strategic points: after construction, before/after major operations
   • Use #ifndef NDEBUG guards for expensive checks

3. Existing Coverage:

   • vector(T) already has good pre-condition checking for array access
   • core_hashtable already has a comprehensive check_invariant() method
   • Additional invariants strengthen the existing foundation

4. Manual Review Needed:

   • The alignment invariant for vector(T) may need adjustment based on platform-specific alignment requirements
   • Load factor invariant for core_hashtable should account for edge cases during expansion
   • Scope stack invariants in lim_svector should be verified against usage patterns in the SMT solver

💡 Recommendations

For vector(T):

1. Add a private check_invariant() method (conditionally compiled)
2. Call it in constructors, destructors, and after state-modifying operations
3. Consider caching the alignment check result to avoid repeated computation

For core_hashtable:

1. Extend existing check_invariant() with the additional invariants proposed
2. Make check_invariant() return early if memory::is_out_of_memory() to avoid false failures
3. Consider a lighter-weight check_invariant_fast() for hot paths

For lim_svector:

1. Add the scope monotonicity check as a separate method
2. Strengthen pre-conditions with additional bounds checking
3. Consider adding assertions to catch popping beyond the available scope count

📚 Methodology

Specifications synthesized using LLM-based invariant mining inspired by:

• Paper: "Classinvgen: Class invariant synthesis using large language models" ([arXiv:2502.18917]((redacted)
• Techniques:
  • Static code analysis to identify data member relationships
  • Pattern recognition of common data structure invariants
  • Analysis of existing assertions to infer intended contracts
  • Cross-referencing with method implementations to validate specifications

🔄 Next Steps

1. Human Review: Domain experts should validate these specifications
2. Implementation: Add assertions incrementally, starting with the most critical invariants
3. Testing: Run full test suite with assertions enabled to catch any false positives
4. Refinement: Adjust specifications based on test results and feedback
5. Documentation: Update code comments to reference the formal specifications

---

🤖 Generated by SpecBot - Automatic Specification Mining Agent
Analysis Date: 2026-01-27
Commit: Current HEAD

AI generated by Specbot

• expires on Feb 3, 2026, 9:26 PM UTC