🐛 Fix reading a latched AIGER file into a combinational network

[marcelwa]

The bug

aiger_reader::on_header only materializes the latch outputs when the network type implements create_ro:

if constexpr ( has_create_ro_v<Ntk> )
{
  /* create latch outputs (ro) */
  for ( auto i = 0u; i < num_latches; ++i )
  {
    signals.push_back( _ntk.create_ro() );
  }
}

For a network type that does not — a plain aig_network, or the mig_network in this reader's own documented example — signals is left short by exactly the latch count, while every AIGER literal above the primary inputs still assumes those slots exist. on_and then does signals[left_lit >> 1] past the end of the vector and hands the result to create_and.

The only thing standing between that and undefined behaviour is one line in on_header:

assert( num_latches == 0 && "network type does not support the creation of latches" );

That condition is data-dependent — it comes from a user-supplied file, not from a programming invariant — so guarding it with assert means it does nothing at all under NDEBUG, i.e. in any release build.

Two failure modes follow:

• Crash. On a design whose logic reaches far enough past the latch outputs, the out-of-bounds read faults. Reading a 4-bit LFSR (0 inputs, 4 latches, 3 ANDs) into an aig_network segfaults.
• Silent corruption. On a design whose literals happen to stay inside the allocation it does not fault, and the file parses with return_code::success into a network quietly missing its registers. A one-latch file came back reporting 0 inputs and 1 output, having dropped the sequential half of the design without a word.

Confirmed with an ASan build against these headers. With assertions live it trips aiger_reader.hpp:139, the on_header guard. Under -DNDEBUG it reports std::vector<aig_network::signal>::operator[] with __n=4 on a size-1 vector, called from on_and( index=5, left_lit=8, right_lit=7 ) at aiger_reader.hpp:193.

The fix

Reading a latched file into a combinational network now flattens one timeframe of the design. Each latch output becomes a primary input, appended behind the file's own primary inputs, and each latch next-state function becomes a primary output, appended behind the file's own primary outputs — the transformation ABC calls comb.

I picked flattening over erroring out for three reasons. It is lossless, where refusing the file or dropping the latches is not. It keeps every literal resolving to the signal the file names, which is what actually fixes the memory error rather than papering over it. And it makes the mig_network example in this class's own documentation work on a sequential file instead of crashing on one — right now that example is only safe for combinational input, which the docs do not say. The sequential<Ntk> path is untouched.

Happy to switch it to a hard error instead if you would rather the reader refuse; I avoided that mainly because there is no throw anywhere in include/mockturtle/io/ today and lorina's callbacks have no way to abort a parse, so it would have been a departure in both style and mechanism.

Two supporting changes: recording and naming latches is no longer conditional on the network type, since the flattened path needs both. And on_header and the destructor disagreed about which trait decides whether a network can hold registers — create_ro in one, create_ri in the other — so both now consult a single has_registers predicate. That drift is what allowed the two halves to get out of step to begin with.

Tests

Three cases added to test/io/aiger_reader.cpp:

• flattening a latched file into an aig_network, checked against the same file read into a sequential<aig_network> — same size, same gate count, same CI and CO counts, only distributed differently
• the zero-primary-input shape that segfaulted, where every literal is reached through a latch output
• the symbol table, which must still put a latch's name on the input standing in for it

The [aiger_reader] suite passes under -fsanitize=address on this branch, and the LFSR and an 8-bit accumulator both round-trip cleanly through the standalone reproducer that used to fault.

Note on behaviour

This does change what a caller sees: reading a sequential design into a combinational network now yields registers as free primary inputs rather than a crash. That is lossless and it is the documented meaning of the operation, but it is not the same circuit, so equivalence checking against the sequential original will not agree. A consumer that wants to refuse rather than flatten can check the latch count itself.

Found while tracking down a segfault in aigverse, which reads AIGER through this reader.

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 94.11765% with 1 line in your changes missing coverage. Please review.
✅ Project coverage is 84.07%. Comparing base (852605f) to head (4d2aa08).
⚠️ Report is 1 commits behind head on master.

Files with missing lines	Patch %	Lines
include/mockturtle/io/aiger_reader.hpp	94.11%	1 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff           @@
##           master     #705   +/-   ##
=======================================
  Coverage   84.07%   84.07%           
=======================================
  Files         190      190           
  Lines       29513    29515    +2     
=======================================
+ Hits        24813    24815    +2     
  Misses       4700     4700           

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.