🐛 Refuse a latched AIGER file in the combinational readers - #457
Conversation
`read_aiger_into_aig` and `read_ascii_aiger_into_aig` segfaulted on any AIGER file with latches. The defect is in mockturtle's `aiger_reader`: `on_header` only materializes the latch outputs when the network type implements `create_ro`, so for one that does not, its `signals` vector is left short by exactly the latch count while every literal above the primary inputs still assumes those slots exist. `on_and` then reads past the end of the vector. The only guard was an `assert`, which is compiled out under `NDEBUG` -- that is, in every wheel we ship. Nothing in `aigverse` could produce a latched AIGER file until now, so the crash was only reachable through an externally written one. That changes as soon as `write_aiger` accepts a `SequentialAig`. The reader used by the combinational bindings now refuses such a file in `on_header`, before a single node is created, and the error names the sequential reader to use instead. Refusing rather than reading is deliberate: mockturtle will soon flatten a latched file into extra primary input and output pairs, one per latch, which is lossless but hands back a network whose registers have become free primary inputs -- a different circuit than the file describes, and one that will not equivalence-check against it. Someone who reached for `read_aiger_into_aig` on a sequential design wanted the sequential reader. The upstream fix is marcelwa/mockturtle#12 and lsils/mockturtle#705. This guard does not depend on either landing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
b3ef0c6 to
c011147
Compare
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (1)
🚧 Files skipped from review as they are similar to previous changes (1)
Included review availability: Your plan provides up to 1 included review per hour; 0 remain after this review. 📝 WalkthroughWalkthroughCombinational AIGER readers now reject latch-containing files for unsupported network types. Sequential readers continue to load these files and preserve register metadata. Documentation, changelog entries, and regression tests describe and validate the behavior. ChangesAIGER latch rejection
Estimated code review effort: 3 (Moderate) | ~20 minutes Merge Risk: ⚪ Minimal · up to The change rejects latched files in combinational readers before parsing can corrupt or crash the process, while directing callers to the sequential readers that preserve registers. No actionable merge-blocking risk remains beyond normal checks and review. Sequence Diagram(s)sequenceDiagram
participant Caller
participant AIGERReader
participant LatchGuard
participant MockturtleReader
Caller->>AIGERReader: Read ASCII or binary AIGER
AIGERReader->>LatchGuard: Check header and network register support
alt Unsupported network with latches
LatchGuard-->>Caller: Raise RuntimeError
else Supported network or no latches
LatchGuard->>MockturtleReader: Delegate parsing
MockturtleReader-->>Caller: Populate network
end
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
|
Holding this until marcelwa/mockturtle#12 lands on |
marcelwa/mockturtle#12 landed on `mnt`. The reader no longer walks off the end of its own signal vector on a latched file -- it flattens one timeframe instead -- so the guard in this branch is now the only thing standing between `read_aiger_into_aig` and a silently reshaped network, rather than between it and a segmentation fault.
Two CI failures, both mine. **Stale stubs.** Adding to the readers' `Raises:` section changed the docstrings the `.pyi` files are generated from, and I did not regenerate them. Regenerating exposed a second problem: all four readers share one docstring template, so the sequential ones were also claiming to refuse a latched file -- misleading for the two functions whose whole purpose is reading one. The clause is now chosen per network type, so only the readers that actually refuse a latched file document it, and they name the sequential readers to use instead. nanobind copies docstrings, so building it at runtime is safe. **Non-virtual destructor.** `refuse_latches` overrides a virtual function but inherited a public non-virtual destructor from `lorina::aiger_reader`, which `cppcoreguidelines-virtual-class-destructor` and `-Wnon-virtual-dtor` both flag, once per instantiation. The reader is only ever a stack temporary handed to lorina by const reference and is never deleted through a base pointer, but a polymorphic type should not be left without a virtual destructor. Declare one, and delete the copy and move operations that declaring it otherwise leaves implicitly defined against the rule of five. `clang-tidy` is clean on the file, and 398 tests and `nox -s lint` pass.
Two conflicts, both from main moving underneath the branch. MOCKTURTLE_REV: this branch pinned 84b1b6e for the AIGER latch read fix; main has since moved to b856d3e via #459. b856d3e is a strict descendant (ahead 1, behind 0 -- the extra commit is mockturtle#13, sequential simulation), so it still carries the out-of-bounds fix. Took main's. CHANGELOG: additive on both sides, in the Fixed section and in the PR link block. Kept both entries, newest PR first.
The branch pinned the revision fixing the underlying out-of-bounds read, but main reached b856d3e first via #459, so the entry was crediting this PR with a bump it no longer carries. The guard never depended on that fix landing anyway -- it sits in front of the buggy path.
The bug
read_aiger_into_aigandread_ascii_aiger_into_aigsegfault on any AIGER file that has latches. Not raise — segfault, taking the interpreter with them.The defect is in mockturtle's
aiger_reader.on_headeronly materializes the latch outputs when the network type implementscreate_ro, so for a network type that does not — which is what backs the combinational bindings — itssignalsvector is left short by exactly the latch count, while every AIGER literal above the primary inputs still assumes those slots exist.on_andthen indexes past the end of the vector and hands what it read tocreate_and. The only thing standing between that and undefined behaviour is anassert( num_latches == 0 ), which is compiled out underNDEBUG— that is, in every wheel we ship.There is a quieter failure mode too. If the file's literals happen to stay inside the allocation, nothing faults and the file parses with
return_code::successinto a network silently missing its registers.Nothing in
aigversecould produce a latched AIGER file until now, so the crash was only reachable through an externally written one. That changes the momentwrite_aigeraccepts aSequentialAig(#406), at which point pure-Python code that never touches ABC can crash the interpreter in two calls.The fix
The reader behind the combinational bindings now refuses a latched file in
on_header, before a single node is created, so a refused file leaves the network untouched. The message names the sequential reader to use instead:Refusing rather than reading is deliberate. The upstream fix flattens a latched file into extra primary input and output pairs, one per latch — the transformation ABC calls
comb. That is lossless and well-defined, but it yields a network whose registers have become free primary inputs: a different circuit than the file describes, and one that will not equivalence-check against it. Anyone who reached forread_aiger_into_aigon a sequential design wantedread_aiger_into_sequential_aig, so this says so rather than quietly handing back something else. The sequential bindings are untouched and read the same files as before.Upstream
The mockturtle side is fixed separately, in marcelwa/mockturtle#12 (into
mnt, the branch of our fork we consume). This guard does not depend on it landing — it sits in front of the buggy path rather than relying on it being fixed — and it stays useful afterwards, since flattening is not what these bindings should do.Tests
Two cases in
test/inout/test_read_aiger.py, one per format, each checking that the combinational reader raises and that the sequential reader takes the very same file:seq.aagresource, one latchlfsr.aigresource — a 4-bit LFSR with no primary inputs, four latches, and every literal reached through a latch output. This is the file that segfaulted; without the guard the test process dies rather than fails.nox -s tests-3.12is green (398 passed, 80 skipped — the skips are the ABC suite with no binary on this machine), andnox -s lintis clean.🤖 Generated with Claude Code
Summary by CodeRabbit
Bug Fixes
Documentation
Tests