Repository navigation
utils, tests: +feat Assert the universal iterator precondition and add randomized oracle tests - #953
Conversation
e1d2d42 to
863e2ca
Compare
8b898e2 to
b88e1a7
Compare
|
Rebased onto |
 [Low impact] The runtime effect stays within one utility iterator's debug-time caller contract. The PR appears safe to merge, with two non-blocking test improvements. Findings
|
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| while (sync_iterator.advance()) { | ||
| const auto& current{sync_iterator.get_current()}; | ||
| REQUIRE(current.size() == num_inputs); | ||
| const int value{*current[0]}; | ||
| for (const auto& position : current) { REQUIRE(*position == value); } | ||
| synchronizations.push_back(value); |
There was a problem hiding this comment.
The new collection loops have no limit on returned values. If advance() regresses and repeatedly returns the same result, these tests keep growing a vector until the job times out or runs out of memory. Add a REQUIRE inside each loop that limits the collected count to the oracle's size, including the runs after reset().
There was a problem hiding this comment.
Fixed: every collection loop now has REQUIRE(collected.size() <= oracle.size()) right after the push, in the first run and in the run after reset(), for both the universal (intersection) and the existential (merged) iterator. A stalling advance() now fails the REQUIRE instead of growing the vector until timeout.
| INFO("seed " << seed); | ||
| const size_t num_inputs{2 + draw(rng, 4)}; | ||
| const size_t universe{6 + draw(rng, 20)}; | ||
| // All inputs share one buffer, so the outcome cannot depend on where they are allocated. |
There was a problem hiding this comment.
The comment says all inputs share one buffer, but each inner std::vector<int> owns a separate buffer. This matters because the earlier iterator bug depended on where separate buffers were allocated. Remove the shared-buffer claim, or store the inputs as ranges within one buffer as the existing regression test does.
| // All inputs share one buffer, so the outcome cannot depend on where they are allocated. |
Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
There was a problem hiding this comment.
Fixed as suggested: the claim was wrong (each inner vector owns its buffer), so the comment is removed. The buffer placement is irrelevant to the oracle check either way: the test compares only values against std::ranges::set_intersection.
…d randomized oracle tests The two remaining actionable items of #797: item 6 (precondition of the universal iterator) and item 7 (randomized oracle tests for the utility headers). The #769 container fixes these oracles depend on landed in #946. Item 3 (packing a 32-bit `State` pair in `PairHash`) stays blocked on #789 / #939 and is not part of this pull request. ## Item 6: precondition of `SynchronizedUniversalIterator::advance()` Universal synchronization over zero inputs is not meaningful. `advance()` now documents "at least one input pushed since construction or the last `reset()`" as its precondition and asserts it in debug builds (`MATA_ASSERT(!this->positions.empty())`). Release builds keep returning `false`. The library callers (NFT intersection and composition) always push two inputs. The header now also includes the `<cstddef>`, `<vector>` and `assert.hh` it uses. The existing unit tests that called `advance()` on an iterator without inputs now check only the state after `reset()`. The release fallback has its own `#ifdef NDEBUG` test case. ## Item 7: seeded randomized oracle tests Every value is drawn from raw `std::mt19937` output over a fixed seed range, as in `tests/nfa/nfa-differential.cc`, so the tests are deterministic across standard libraries: | Test case | Oracle | Seeds | |---|---|---| | `OrdVector against std::set (randomized)`: construction (vector, `std::set`, iterator range), `set_union` and `insert(OrdVector)`, `intersection`, `difference`, `is_subset_of`, `is_intersection_empty_with`, `are_disjoint`, `==`/`<`, `contains`/`count`/`find`, `min`/`max`, random insert/erase sequences, `erase_if` | `std::set` and `std::ranges` set algorithms | 500 | | `filter() and filter_indexes() against std::erase_if (randomized)`: the free functions and the `OrdVector` wrappers | `std::erase_if`, an index mask | 500 | | `SparseSet against std::set (randomized)`: 60-step traces of `insert`/`erase`/`complement`/`filter`/`rename` (a permutation of `[0, 61)`)/`truncate`/`sort`, then `size`, `empty`, `max`, membership over the whole domain, `are_disjoint`, `intersects_with`, copies | `std::set`. Contents are compared as sorted element lists: `SparseSet::operator==` compares the internal buffers, which is a separate #769 item left untouched here. | 300 | | `SynchronizedUniversalIterator against a brute-force intersection (randomized)`: 2–5 inputs, also after `reset()`, with the collected count required to stay within the oracle's size so a stalling iterator fails instead of timing out | `std::ranges::set_intersection` | 300 | | `SynchronizedExistentialIterator against a brute-force merge (randomized)`: 1–5 inputs, per-value count of synchronized positions, also after `reset()`, with the collected count likewise bounded by the oracle's size | `std::ranges::set_union`, `binary_search` | 300 | ## Verification * `nix fmt` on the touched files: `(0 changed)`. * `just cpp::build debug` + `./build/debug/g++/tests/tests` on the pushed head, rebased onto `devel` `8b4c09b` (GCC, Nix dev shell): `test cases: 374 | 368 passed | 2 skipped | 4 failed as expected`, `assertions: 4754234 | 4754197 passed | 37 failed as expected`. Release build: `test cases: 375 | 369 passed | 2 skipped | 4 failed as expected`, `assertions: 4754239 | 4754202 passed | 37 failed as expected` (the extra case is the release-only zero-input test). The 4 expected failures are the existing `[!shouldfail]` cases in `tests/nft/nft-differential.cc`. * **The assertion fires in debug.** A probe that calls `advance()` on an empty `SynchronizedUniversalIterator`, compiled without `NDEBUG`, prints `include/mata/utils/synchronized-iterator.hh:117: advance: Assertion '!this->positions.empty()' failed.` and exits with 134 (SIGABRT). Compiled with `-DNDEBUG`, it returns `false`. * **The oracles catch real bugs.** I compiled the three test files against a copy of the headers with the following re-introduced: the `devel` `filter`/`filter_indexes` (`reserve(last)`), the `devel` universal restart check, a `SparseSet::complement` that keeps values above the new domain, an `OrdVector::difference` that drops the last element, and an existential iterator that keeps at most two synchronized positions. All five randomized test cases failed (10 of 21 test cases, 2237 assertions); with the real headers all pass. * Performance: these are test and debug-only changes, so release code is unchanged and nothing needs measuring. Part of #797.
b88e1a7 to
37eb8f3
Compare
|
Rebased onto the latest |
1 participant
The two remaining actionable items of #797: item 6 (precondition of the universal iterator) and item 7 (randomized oracle tests for the utility headers). The #769 container fixes these oracles depend on landed in #946. Item 3 (packing a 32-bit
Statepair inPairHash) stays blocked on #789 / #939 and is not part of this pull request.Item 6: precondition of
SynchronizedUniversalIterator::advance()Universal synchronization over zero inputs is not meaningful.
advance()now documents "at least one input pushed since construction or the lastreset()" as its precondition and asserts it in debug builds (MATA_ASSERT(!this->positions.empty())). Release builds keep returningfalse. The library callers (NFT intersection and composition) always push two inputs. The header now also includes the<cstddef>,<vector>andassert.hhit uses.The existing unit tests that called
advance()on an iterator without inputs now check only the state afterreset(). The release fallback has its own#ifdef NDEBUGtest case.Item 7: seeded randomized oracle tests
Every value is drawn from raw
std::mt19937output over a fixed seed range, as intests/nfa/nfa-differential.cc, so the tests are deterministic across standard libraries:OrdVector against std::set (randomized): construction (vector,std::set, iterator range),set_unionandinsert(OrdVector),intersection,difference,is_subset_of,is_intersection_empty_with,are_disjoint,==/<,contains/count/find,min/max, random insert/erase sequences,erase_ifstd::setandstd::rangesset algorithmsfilter() and filter_indexes() against std::erase_if (randomized): the free functions and theOrdVectorwrappersstd::erase_if, an index maskSparseSet against std::set (randomized): 60-step traces ofinsert/erase/complement/filter/rename(a permutation of[0, 61))/truncate/sort, thensize,empty,max, membership over the whole domain,are_disjoint,intersects_with, copiesstd::set. Contents are compared as sorted element lists:SparseSet::operator==compares the internal buffers, which is a separate #769 item left untouched here.SynchronizedUniversalIterator against a brute-force intersection (randomized): 2–5 inputs, also afterreset(), with the collected count required to stay within the oracle's size so a stalling iterator fails instead of timing outstd::ranges::set_intersectionSynchronizedExistentialIterator against a brute-force merge (randomized): 1–5 inputs, per-value count of synchronized positions, also afterreset(), with the collected count likewise bounded by the oracle's sizestd::ranges::set_union,binary_searchVerification
nix fmton the touched files:(0 changed).just cpp::build debug+./build/debug/g++/tests/testson the pushed head, rebased ontodevel8b4c09b(GCC, Nix dev shell):test cases: 374 | 368 passed | 2 skipped | 4 failed as expected,assertions: 4754234 | 4754197 passed | 37 failed as expected. Release build:test cases: 375 | 369 passed | 2 skipped | 4 failed as expected,assertions: 4754239 | 4754202 passed | 37 failed as expected(the extra case is the release-only zero-input test). The 4 expected failures are the existing[!shouldfail]cases intests/nft/nft-differential.cc.advance()on an emptySynchronizedUniversalIterator, compiled withoutNDEBUG, printsinclude/mata/utils/synchronized-iterator.hh:117: advance: Assertion '!this->positions.empty()' failed.and exits with 134 (SIGABRT). Compiled with-DNDEBUG, it returnsfalse.develfilter/filter_indexes(reserve(last)), thedeveluniversal restart check, aSparseSet::complementthat keeps values above the new domain, anOrdVector::differencethat drops the last element, and an existential iterator that keeps at most two synchronized positions. All five randomized test cases failed (10 of 21 test cases, 2237 assertions); with the real headers all pass.Part of #797.