Fix uninitialised read in lut_map on networks with dangling nodes - #707
Open
marcelwa wants to merge 50 commits into
Open
Fix uninitialised read in lut_map on networks with dangling nodes#707marcelwa wants to merge 50 commits into
marcelwa wants to merge 50 commits into
Conversation
…ly caused issues with _x86, which is used by Windows.
…ly caused issues with _x86, which is used by Windows.
🚨 Fix compilation error for apple clang 15.0.7
🐛 Added missing namespace ``std::chrono``.
… and compiler versions
👷 Modernized the Linux CI system for more extensive testing across OS and compiler versions 👷 Adjust PR triggers 👷 Adjust PR triggers ⏪ Revert triggers ⬆️ Upgrade phmap dependency to the latest version ⏪ Removed sanitizers ✅ Fixed tests
* 👷 Cancel in-progress workflows on newer refs or canceled builds * 👷 Modernize macOS CI workflow * 👷 Modernize Windows CI workflow * 🎨 Formatting * 💚 Try to fix macOS runs * 💚 Attempt to fix CI build * 👷 Re-enable concurrency restrictions for macOS CI * 🎨 Update CMakeLists.txt to add UTF-8 support for MSVC compile options * 💚 Update the Windows CI to use PowerShell for shell execution * 💚 Attempt to fix test execution command in Windows CI
* 🐛 Fix(aag): aag check with invalid index Fixes marcelwa/aigverse#131 Signed-off-by: JingrenWang <wjrforcyber@163.com> * ♻️ Refactor(Var name): Varible name change Signed-off-by: JingrenWang <wjrforcyber@163.com> * ♻️ Refactor(Non-negative Check): Check value of `long` is non-negative before bound check Signed-off-by: JingrenWang <wjrforcyber@163.com> * ♻️ Refactor(Comment): Refactor description. Signed-off-by: JingrenWang <wjrforcyber@163.com> * ♻️ Refactor(Typo): Fix typo according to review Signed-off-by: JingrenWang <wjrforcyber@163.com> * ♻️ Refactor(TypeCast): `uint64_t` to `long` Signed-off-by: JingrenWang <wjrforcyber@163.com> --------- Signed-off-by: JingrenWang <wjrforcyber@163.com> Co-authored-by: Marcel Walter <marcel.walter@tum.de>
Signed-off-by: JingrenWang <wjrforcyber@163.com>
# Conflicts: # .github/workflows/linux.yml # .github/workflows/macos.yml # .github/workflows/windows.yml
The build workflows still passed the pre-rename CMake option names (`MOCKTURTLE_TEST`, `MOCKTURTLE_EXAMPLES`, `MOCKTURTLE_EXPERIMENTS`), which have been no-ops since the options became `MOCKTURTLE_BUILD_*`. `MOCKTURTLE_BUILD_TESTS` defaults to OFF, so `run_tests` was never built and every job failed at the "Run tests" step with "working directory build/test: No such file or directory". The test suite has effectively not run in CI since the rename; `coverage.yml` was migrated at the time, the three build workflows were missed. Windows additionally targeted images that no longer exist: - `windows-2019` was retired as a GitHub-hosted image; its jobs never started. - `windows-2025` ships Visual Studio 2026 since June 2026, so the "Visual Studio 17 2022" generator fails with "could not find any instance of Visual Studio". Visual Studio 2022 is now only on `windows-2022`. The v142 toolset went away with windows-2019, so the matrix is now spelled out explicitly instead of being built from a cross product with exclusions. Also set `fail-fast: false` on all three matrices. A single failing job was cancelling the other 24 and reporting them as failures, which hid what was actually broken. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GbUqcnZayPooFgekEXVSjz
`clone a block network` asserted `ntk3.size() == 7` and `ntk3.num_gates() == 3` for a deep copy of a network that has size 6 and 2 gates. Those numbers encoded the double-initialization bug that "Fixed double initialization of cloned block networks" removed: `clone()` re-ran `_init()` on the copied storage and appended a second constant node. With that fix in place a clone is now an exact snapshot of the source network, so the expectations become 6 and 2. `num_pos()` was already correct. This went unnoticed because the test suite has not actually been built in CI -- see the preceding commit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GbUqcnZayPooFgekEXVSjz
`write_aiger` hardcoded a latch count of 0 and asserted that the network was combinational, so `sequential<aig_network>` could be passed in but silently lost its registers: they degraded into extra PI/PO pairs. Emit registers as AIGER latches when the network type provides `num_registers`, `foreach_ri`, and `foreach_ro`. The combinational path is unchanged and still produces byte-identical output. Reset values are always written explicitly. An omitted reset field means 0 in the AIGER format, so omitting it would silently turn an uninitialized register into a zero-initialized one; an undefined reset is instead encoded by repeating the latch's own current-state literal, as the format prescribes. Latch names are emitted as `l<n>` symbol table entries, mirroring `on_latch_name`. Because the binary format encodes CIs implicitly, PIs must be variables 1..I and register outputs I+1..I+L. That invariant is now checked by a debug assertion rather than being silently assumed. Also add the missing `<cassert>` include; the header used `assert` but only compiled because its includers happened to provide it. Verified against both readers: the output round-trips through `aiger_reader` preserving register count, reset values, and names, and ABC reads it back with the expected `Init0`/`Init1`/`InitDC` counts. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GbUqcnZayPooFgekEXVSjz
A sequential network written by ABC could not be read back correctly. Three separate defects, all in the AIGER latch and output handling. **Omitted latch reset values were read as undefined.** Both the binary and the ASCII reader defaulted to NONDETERMINISTIC when a latch line carried no reset field. The format specifies the opposite: the original AIGER format initialized every latch to zero, and the reset field added in 1.9 is optional, so its absence means 0. ABC relies on this and omits the field for zero-initialized latches, so every zero-initialized register came back undefined. **The ASCII reader compared the wrong token.** The branch recognizing a reset value of 1 tested `tokens[1u]`, the next-state literal, instead of `tokens[2u]`. An explicit reset of 1 was therefore never recognized, and a latch whose next-state literal happened to be 1 was wrongly reported as one-initialized. **Bad state properties were dropped.** A writer emitting the AIGER 1.9 extended header moves the primary outputs into the bad-state section; ABC does this for any design with a non-zero latch initialization. `on_bad_state` was not overridden, so those outputs disappeared and the network came back with none. They are now kept as primary outputs, which is what they were, along with their names from the symbol table. Also fix an adjacent defect in the destructor: the output index only advanced for outputs that carried a name, so with a sparse symbol table every name after the first unnamed output landed on the wrong one. Verified end to end against ABC. A network with three registers initialized to 0, 1, and undefined previously returned with no outputs and a corrupted first register; it now round-trips through `resyn2` with its inputs, outputs, registers, and reset values intact. Note that AIGER constraints are still ignored. They are assumptions rather than outputs, so mapping them onto primary outputs would change the meaning of the network. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GbUqcnZayPooFgekEXVSjz
`register_t::init` carried three different encodings of "undefined" at once.
`register_t` itself defaulted to 3, `blif_reader` used 2 for a nondeterministic
latch and 3 for an unspecified one, and `aiger_reader` produced 255 -- the
result of narrowing an `int8_t` of -1 into a `uint8_t` field rather than a
deliberate choice.
That last one corrupted output. `write_blif` emits the initialization verbatim
and the BLIF `.latch` statement accepts only 0, 1, 2, and 3, so a sequential
AIGER file with an undefined latch reset read back and written as BLIF produced
.latch li0 new_n2 255
which no BLIF consumer accepts, ABC included.
Introduce `register_init` with the four documented values, following the BLIF
`.latch` field since it is the most expressive of the supported formats, and use
it consistently across the readers and writers. AIGER has no counterpart for
`unknown`, so a latch without a defined reset maps to `dont_care`.
`register_init::is_defined` expresses the test that callers actually want,
namely whether a reset value is 0 or 1, so code stays correct if a format ever
introduces further undefined states. `register_init::sanitize` keeps `write_blif`
from emitting a value the format cannot represent.
The only value that changes is the one AIGER produced for a nondeterministic
latch, from 255 to 2. Comparisons of the form `init > 1` are unaffected; only
code testing against 255 would notice, and that value was never intentional.
Verified end to end: the AIGER file above now yields `.latch li0 new_n2 2`,
which ABC reads back as one don't-care-initialized latch.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GbUqcnZayPooFgekEXVSjz
# Conflicts: # .github/workflows/macos.yml # include/mockturtle/io/write_aiger.hpp
`aiger_reader::on_header` only materialized the latch outputs when the network
type implements `create_ro`. For one that does not, the reader's `signals`
vector was left short by exactly the latch count, while every AIGER literal
above the primary inputs still assumed those slots existed. `on_and` then
indexed past the end of the vector and handed the garbage it read to
`create_and`.
The only thing standing between that and undefined behaviour was
assert( num_latches == 0 && "network type does not support the creation of latches" );
which is compiled out under `NDEBUG` -- that is, in every release build. The
result was a segmentation fault on any design whose logic reaches far enough
past the latch outputs, and a silently wrong network on any that does not: a
one-latch file whose literals all stay in bounds parsed "successfully" into a
network missing its registers entirely.
Reading a latched file into a combinational network now flattens one timeframe
of the design instead. 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. That is the
transformation ABC calls `comb`; it loses no logic, keeps every literal
resolving to the signal the file names, and makes the network type in this
reader's own documented example -- `mig_network`, which has no registers -- work
on a sequential file rather than crash on one.
Recording and naming latches is no longer conditional on the network type
either, since the flattened path needs both. The header and the destructor also
disagreed about which trait decides whether a network can hold registers,
`create_ro` in one and `create_ri` in the other; both now consult a single
`has_registers` predicate, which is what let them drift apart to begin with.
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* ✨ Add cycle-accurate simulation of sequential networks
`simulate` evaluates the combinational logic of a network exactly once and has
no notion of a register. Handed a `sequential<Ntk>` it assigns the constants,
the primary inputs and the gates -- but never the register outputs, which are
neither. They keep whatever `node_map` default-constructed them to, so every
value in their fanout cone is meaningless: constant 0 for a `bool` simulation,
a zero-variable truth table otherwise. Nothing warns about it.
`simulate_sequential` runs the network over a number of clock cycles instead.
Every register starts at its reset value, the combinational logic is evaluated
once per cycle, the primary outputs are recorded, and the register inputs are
latched into the register outputs for the next cycle.
The simulator concept is unchanged, with one addition: a simulator that provides
`compute_pi( index, cycle )` is driven per cycle, so the primary inputs can
change from one to the next. `stimulus_simulator` is such a simulator, holding
one assignment vector per cycle and repeating its last one for the rest of the
run. Everything that works with `simulate` keeps working, holding its assignment
for the whole run -- which is what a design with no primary inputs, an LFSR say,
wants anyway.
A register may declare no reset value at all -- `register_init::dont_care` or
`register_init::unknown`, which is what `register_t` defaults to and what an
AIGER latch with a nondeterministic reset reads back as. Simulation needs a
concrete one, so `simulate_sequential_params::undefined_reset_value` says which.
It lives in its own header rather than in `simulation.hpp` because it needs
`networks/sequential.hpp`, which pulls in every network implementation. Putting
it in `simulation.hpp` would put that cost on every translation unit that
simulates anything.
Seven test cases: a 4-bit LFSR walking all 15 of its non-zero states and
returning to its seed on the sixteenth, a second seed producing the same
sequence one step ahead (which only holds if the reset values are honoured), a
shift register driven by a per-cycle stimulus, a stimulus shorter than the run,
an undefined reset following the parameter both ways, truth-table simulation,
and a zero-cycle run.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* 💚 Fix the stimulus construction GCC 12 and older reject
`stimulus_simulator sim( { { true } } )` is ambiguous on GCC 12 and older: a
single-element braced list is as good a match for the copy constructor as for
the one taking the stimulus. Every g++ job up to 12 failed on it while every
clang job and g++ 13 and 14 passed.
Construct it from a named vector, which leaves only one viable candidate on
every compiler. The two-element spelling a few tests up is unambiguous and
stays as it is, since it is the form a reader should copy.
* ♻️ Return a result struct from simulate_sequential
`std::vector<std::vector<SimulationType>>` says nothing about how the data is
laid out -- which index is the cycle and which the output is something a caller
had to learn from the documentation and then remember. Return a
`simulate_sequential_result` that names both axes instead.
It carries the register values as well, which the loop had all along and threw
away. `outputs[cycle][index]` is what primary output `index` emitted in that
cycle, `states[cycle][index]` what register `index` held while that cycle was
evaluated.
The state trace is one entry longer than the output trace, because simulating
`n` cycles crosses `n + 1` state boundaries. `reset_state()` is the one the run
started from and `final_state()` the one it ended in, which also gives a run of
zero cycles something sensible to report: no outputs, and the reset state.
Three new test cases: the fencepost between the two traces, the LFSR walking
fifteen distinct non-zero states and returning to its seed, and a register read
out one cycle after it was written, where the output of each cycle must equal
the state it started in. The truth-table case now checks the register as well as
the output.
Also spell the simulator in the header's example as
`default_simulator<bool>( std::vector<bool>{} )`. `( {} )` is ambiguous on GCC 12
and older, and an example is the last place to put something a reader cannot
compile.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
The six format headers declare their compiled patterns `static` at namespace scope. `static` gives internal linkage, so every translation unit that includes aiger.hpp gets its own private set of nine std::regex objects, each constructed during that TU's static initialization. Linking two such TUs shows 18 distinct objects where the source describes 9; the C++17 spelling for one shared definition is `inline`. `const` matters more than the duplication does. These live in public namespaces under public names, and nothing but convention stops a caller reassigning one. Every use is std::regex_match or an sregex_iterator constructor, both of which take a const reference, so the objects are already read-only in practice -- which is what makes concurrent parsing safe. Spelling them const promotes that from a property of today's call sites, which has to be re-established by reading every one of them, to a guarantee the compiler enforces. aigverse released the GIL around these parsers on exactly that reasoning. 29 patterns across aiger, pla, verilog, bench, blif and dimacs. No call site changes: this is a declaration-only patch.
`cut() = default` leaves `_length`, `_cend` and `_end` indeterminate. A default-constructed cut is reachable: `cut_set` and `lut_cut_set` hold an array of them and `best()` returns `*_pcuts[0]` whether or not any cut has been inserted. `lut_map_impl::compute_share_mapping_init` iterates over every node index and calls `best()`, and a node unreachable from the outputs is never visited by the cut enumerator, so its cut set is empty and the following `for ( auto leaf : cut )` in `compute_cut_data` walks a garbage end pointer and indexes `cuts[leaf]` with whatever it finds. Networks with unreachable nodes are not exotic: ABC's `&dch -f; &put` leaves the choice-class members in as ordinary AND nodes, so every AIG written by the standard `strash; &get; &dch -f; &put; write_aiger` front end has them (cavlc: 1271 ANDs written, 647 reachable). Give the default constructor a defined empty state, and add a lut_mapper test that maps a six-gate AIG whose last four gates drive no output.
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## master #707 +/- ##
==========================================
- Coverage 84.06% 84.03% -0.04%
==========================================
Files 190 191 +1
Lines 29515 29588 +73
==========================================
+ Hits 24812 24864 +52
- Misses 4703 4724 +21 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
# Conflicts: # include/mockturtle/io/aiger_reader.hpp # test/io/aiger_reader.cpp
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
lut_mapreads uninitialised memory, and usually segfaults, on any network that carries nodes unreachable from the outputs.lut_map_impl::compute_share_mapping_initloops over every node index and callscuts[i].best(), but the cut enumerator never visits an unreachable node, so its cut set is still empty andbest()returns*_pcuts[0], which points at a default-constructedcut;cut() = defaultleaves_length,_cendand_endindeterminate, so thefor ( auto leaf : cut )incompute_cut_datawalks a garbage end pointer and then indexescuts[leaf]. This is easy to hit from outside without doing anything unusual: every AIG that ABC writes after&dch -f; &putkeeps the choice-class members as ordinary AND nodes (cavlccomes out with 1271 ANDs of which 647 are reachable), so anyone piping ABC into mockturtle trips it, and because it is undefined behaviour rather than a check it can also just produce plausible-looking numbers instead of crashing. The fix here givescut's default constructor a defined empty state rather than guarding the caller, on the reasoning that a default-constructed cut sitting incut_set::_cutsand reachable throughbest()ought to be readable at all; the regression test added totest/algorithms/lut_mapper.cppmaps a six-gate AIG whose last four gates drive no output, and it exits with signal 11 without the change and passes with it. If you would rather have the guard inlut_mapper.hpp— skipping empty cut sets incompute_share_mapping_init, which is what we carried locally first — or want the initialisation written as default member initialisers instead, say so and we will redo it.