fraig_restore: stack overflow when a representative chain has a cycle longer than two

[marcelwa]

We hit a reproducible SIGSEGV in fraig_restore and would like to check our reading of the code before calling it a bug. Abc_NtkHaigResetReprs (src/base/abci/abcHaig.c) normalises the pData representative chain and handles exactly two shapes, a self-loop and a two-node cycle — the comment there calls the second one "the strange situation of double-loop" — but the very next loop in the same function calls Hop_ObjRepr on every object, and Hop_ObjRepr recurses on pObj->pData until it reaches NULL or a self-loop, so a cycle of three or more recurses until the stack is gone and the process dies with no diagnostic; we see 521105 identical Hop_ObjRepr frames entered at abcHaig.c:478, by way of fraig_restore -> Abc_NtkFraigRestore -> Abc_NtkFraigPartitioned -> Abc_NtkPartStitchChoices -> Abc_NtkHopRemoveLoops. Attached is a reproducer that is three AIGER files derived from EPFL mem_ctrl and a four-line script (read_aiger; strash; fraig_store on each, then one fraig_restore): it exits with signal 11 on master at c6e8823 after about three minutes, it completes with this patch, and dropping any one of the three files makes it go away — the ingredient that seems to matter is that one of the stored networks is the re-strashed expansion of a cover that was mapped from an earlier fraig_restore's choice network, which gives a denser equivalence structure than a plain set of synthesis variants. The patch generalises the existing normalisation from cycles of length two to cycles of any length using Floyd's algorithm and breaks a detected cycle the way the two-node case already did, by making the meeting node its own representative; it is constant space, it sits inside a loop that already visits every object, and it is inert where there is no cycle — a single-round fraig_store/fraig_restore pipeline gives byte-identical mapped netlists with and without it (adder 212 LUTs / 84 levels, cavlc 111/6, i2c 258/7). Our question is whether a cycle longer than two is supposed to be impossible at this point: if it is, the real defect is wherever the chain gets built and this patch only hides it, and we would rather know that and close this.

Attachment archive