✨Power CNF Encoding Added #11
Conversation
FeldmeierMichael
added
feature
📝 WalkthroughWalkthroughReplaces the exact-power entry with BDD-aware PexaManExactPowerSynthesisBasePower, expands PexaMan_t with P-variable/minterm and SAT state, adds combination-management types/helpers, introduces CNF+BDD P-clause and cardinality encodings, and updates solution-printing signatures to accept a bdd flag. Changes
Sequence Diagram(s)sequenceDiagram
autonumber
participant CLI as init.cpp\n(PexactCommand)
participant PEX as pexact.c\n(PexaMan core)
participant BDD as BDD Builder/Evaluator
participant CNF as CNF Builder / SAT Solver
CLI->>PEX: PexaManExactPowerSynthesisBasePower(pPars)
PEX->>PEX: initialize PexaMan_t (iPVariableStart, iVarMintermBase, comb lists)
alt BDD-aware path
PEX->>BDD: PexaManEvalPVariablesBdd / build BDD-based clauses
BDD-->>PEX: mapped variable indices (iVarP, iVarMinterm)
PEX->>CNF: ExactPowerSynthesisCNF (P-clauses, mux encodings, cardinalities)
else legacy CNF path
PEX->>CNF: build legacy CNF encoding
end
CNF-->>PEX: SAT result (model / UNSAT)
alt model found
PEX->>PEX: PexaManPrintSolution(..., bdd)
PEX-->>CLI: return success
else unsat or iterate
PEX->>PEX: PopComb / iterate combos / rebuild CNF
PEX-->>CLI: return failure
end
Estimated code review effort🎯 4 (Complex) | ⏱️ ~50 minutes Possibly related PRs
Suggested reviewers
🚥 Pre-merge checks | ✅ 3✅ Passed checks (3 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing touches
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 |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 7
🧹 Nitpick comments (4)
init.cpp (1)
84-84: Consider making verbosity configurable.The
verboseparameter is hardcoded to2, which enables detailed output. For production use, consider adding a command-line flag (e.g.,-v) to control verbosity, allowing users to toggle between quiet mode (0), time info (1), and detailed info (2).pexact.h (1)
21-32: Potential ODR violation withconst intin header.In C,
constvariables at file scope have external linkage by default. If this header is included in multiple translation units, you may encounter linker errors for multiple definitions. Consider usingstatic const intor preprocessor#definemacros for these constants.🔎 Proposed fix
-const int CONST_ZERO = 0; -const int CONST_ONE = 1; -const int CONST_TWO = 2; -const int CONST_THREE = 3; -const int CONST_FOUR = 4; -const int CONST_FIVE = 5; -const int CONST_SIX = 6; -const int CONST_SEVEN = 7; -const int CONST_TEN = 10; - -const int CONST_NINETY_SIX = 96; -const int CONST_FIFTY_SIX = 56; +#define CONST_ZERO 0 +#define CONST_ONE 1 +#define CONST_TWO 2 +#define CONST_THREE 3 +#define CONST_FOUR 4 +#define CONST_FIVE 5 +#define CONST_SIX 6 +#define CONST_SEVEN 7 +#define CONST_TEN 10 + +#define CONST_NINETY_SIX 96 +#define CONST_FIFTY_SIX 56pexact.c (2)
1445-1468: Variable shadowing and potential stack overflow with VLA.
- Line 1446: The VLA
xIt[len]wherelen = nObjs * 2^nVarscan be very large. FornVars=10andnObjs=32, this would be ~128KB on the stack.- Lines 1461 and 1465: The inner
indexvariable shadows the outer declaration, causing confusion.Consider using dynamic allocation for
xItand renaming the inner variable.🔎 Proposed fix for variable shadowing
for ( int i = p->nVars; i < p->nVars + p->nNodes - 1; i++ ) { - int index = i * ( pow( 2, p->nVars ) ); - xIt[index] = 0; + int baseIndex = i * ( pow( 2, p->nVars ) ); + xIt[baseIndex] = 0; for ( int t = 1; t < pow( 2, p->nVars ); t++ ) { - int index = ( i * ( pow( 2, p->nVars ) ) ) + t; - xIt[index] = sat_solver_var_value( p->pSat, xiBase + ( CONST_THREE * ( i - p->nVars + 1 ) ) + ( ( t - 1 ) * ( CONST_THREE * p->nNodes ) ) ); + int innerIndex = ( i * ( pow( 2, p->nVars ) ) ) + t; + xIt[innerIndex] = sat_solver_var_value( p->pSat, xiBase + ( CONST_THREE * ( i - p->nVars + 1 ) ) + ( ( t - 1 ) * ( CONST_THREE * p->nNodes ) ) ); } }
1087-1106: Consider checking return values ofsat_solver_addclause.The
AddMuxEncodingfunction callssat_solver_addclausefour times without checking return values. If any clause addition fails, the encoding will be incomplete, leading to incorrect SAT results. Consider returning a boolean status or using assertions.🔎 Proposed fix
-void AddMuxEncoding( PexaMan_t * p, int o, int c, int i1, int i0 ) +bool AddMuxEncoding( PexaMan_t * p, int o, int c, int i1, int i0 ) { int pList[CONST_THREE]; pList[CONST_ZERO] = Abc_Var2Lit( c, 1 ); pList[CONST_ONE] = Abc_Var2Lit( o, 1 ); pList[CONST_TWO] = Abc_Var2Lit( i1, 0 ); - sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ); + if ( !sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ) ) return false; pList[CONST_ZERO] = Abc_Var2Lit( c, 1 ); pList[CONST_ONE] = Abc_Var2Lit( i1, 1 ); pList[CONST_TWO] = Abc_Var2Lit( o, 0 ); - sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ); + if ( !sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ) ) return false; pList[CONST_ZERO] = Abc_Var2Lit( c, 0 ); pList[CONST_ONE] = Abc_Var2Lit( o, 1 ); pList[CONST_TWO] = Abc_Var2Lit( i0, 0 ); - sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ); + if ( !sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ) ) return false; pList[CONST_ZERO] = Abc_Var2Lit( c, 0 ); pList[CONST_ONE] = Abc_Var2Lit( i0, 1 ); pList[CONST_TWO] = Abc_Var2Lit( o, 0 ); - sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ); + if ( !sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ) ) return false; + return true; }
📜 Review details
Configuration used: defaults
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (3)
init.cpppexact.cpexact.h
🧰 Additional context used
🧬 Code graph analysis (2)
pexact.h (1)
pexact.c (2)
PowerExactSynthesisBase(801-869)PexaManExactPowerSynthesisBasePower(1719-1841)
init.cpp (1)
pexact.c (1)
PexaManExactPowerSynthesisBasePower(1719-1841)
🪛 Cppcheck (2.19.0)
pexact.c
[warning] 884-884: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 885-885: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 886-886: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 890-890: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1736-1736: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1737-1737: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
🪛 GitHub Check: 🚨 Clang-Tidy
pexact.c
[warning] 1164-1164: pexact.c:1164:22 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'pVars'
[warning] 1164-1164: pexact.c:1164:20 [clang-analyzer-core.uninitialized.Assign]
Assigned value is uninitialized
[warning] 1149-1149: pexact.c:1149:13 [clang-analyzer-security.ArrayBound]
Out of bound access to memory preceding 'pVars'
[warning] 1114-1114: pexact.c:1114:6 [readability-function-size]
function 'PexaManAddPClausesBdd' exceeds recommended size/complexity thresholds
[warning] 1114-1114: pexact.c:1114:6 [readability-function-cognitive-complexity]
function 'PexaManAddPClausesBdd' has cognitive complexity of 49 (threshold 25)
[warning] 972-972: pexact.c:972:25 [clang-analyzer-deadcode.DeadStores]
Value stored to 'ptrOld' is never read
[warning] 946-946: pexact.c:946:6 [readability-function-size]
function 'RemoveCombis' exceeds recommended size/complexity thresholds
[warning] 946-946: pexact.c:946:6 [readability-function-cognitive-complexity]
function 'RemoveCombis' has cognitive complexity of 29 (threshold 25)
[warning] 892-892: pexact.c:892:5 [clang-analyzer-core.uninitialized.Assign]
Assigned value is uninitialized
[warning] 890-890: pexact.c:890:32 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'res'
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (2)
- GitHub Check: ABC Integration (ubuntu-latest)
- GitHub Check: ABC Integration (macos-latest)
🔇 Additional comments (2)
pexact.h (1)
74-105: New data structures look good.The
Comb_tandCombList_tstructures are well-documented and appropriate for the priority list mechanism. Minor note: ensurestartis always initialized toNULLwhen creating a newCombList_tto prevent undefined behavior when checkinglist->length == 0.pexact.c (1)
1025-1055: LGTM with note on VLA usage.The variable-length array
combiSol[np]is bounded bynVars <= 10, making the maximum size ~513 integers (~2KB), which is acceptable for stack allocation. The logic correctly evaluates P-variable values against the combinational assignment.
There was a problem hiding this comment.
Actionable comments posted: 3
♻️ Duplicate comments (5)
pexact.c (5)
886-923: Missing NULL checks and uninitializednode->nextremain unaddressed.This issue was flagged in a previous review. The malloc calls at lines 889 and 892 lack NULL checks, and
node->nextis never initialized to NULL, which can corrupt the list when appending.
936-942: Missing bounds check before pop operation remains unaddressed.This issue was flagged in a previous review. Calling
PopCombon an empty list will dereference NULL.
1075-1083: Variable shadowing: loop variablepshadows function parameterp.This was flagged in a previous review for the similar
PexaManAddPClausesBddfunction. The loop variablesint pat lines 1076 and 1080 shadow thePexaMan_t * pfunction parameter, causing confusion and triggering static analysis warnings.
1273-1273: Typo:01is octal notation, likely meant1.This was flagged in a previous review. Line 1273 uses
p8 > 01where01is octal (equals decimal 1). Use decimal1for consistency.
1614-1619: Missing NULL check and uninitializedlist->startremain unaddressed.This was flagged in a previous review. The malloc at line 1614 lacks a NULL check, and
list->startshould be initialized to NULL.
🧹 Nitpick comments (2)
pexact.c (2)
1031-1050: Missing return value checks forsat_solver_addclause.Unlike other encoding functions in this file (e.g.,
AddCnfInpUniq,AddCnfTwoInputFunc), this function doesn't check the return values ofsat_solver_addclause. A failed clause addition would silently produce an incorrect CNF encoding.Consider returning a
boolto indicate success/failure, consistent with the rest of the codebase.🔎 Proposed fix
-void AddMuxEncoding( PexaMan_t * p, int o, int c, int i1, int i0 ) +bool AddMuxEncoding( PexaMan_t * p, int o, int c, int i1, int i0 ) { int pList[CONST_THREE]; pList[CONST_ZERO] = Abc_Var2Lit( c, 1 ); pList[CONST_ONE] = Abc_Var2Lit( o, 1 ); pList[CONST_TWO] = Abc_Var2Lit( i1, 0 ); - sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ); + if ( !sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ) ) return 0; pList[CONST_ZERO] = Abc_Var2Lit( c, 1 ); pList[CONST_ONE] = Abc_Var2Lit( i1, 1 ); pList[CONST_TWO] = Abc_Var2Lit( o, 0 ); - sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ); + if ( !sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ) ) return 0; pList[CONST_ZERO] = Abc_Var2Lit( c, 0 ); pList[CONST_ONE] = Abc_Var2Lit( o, 1 ); pList[CONST_TWO] = Abc_Var2Lit( i0, 0 ); - sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ); + if ( !sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ) ) return 0; pList[CONST_ZERO] = Abc_Var2Lit( c, 0 ); pList[CONST_ONE] = Abc_Var2Lit( i0, 1 ); pList[CONST_TWO] = Abc_Var2Lit( o, 0 ); - sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ); + if ( !sat_solver_addclause( p->pSat, pList, pList + CONST_THREE ) ) return 0; + return 1; }
1331-1331: Dead store: assignment tolitis never read.The assignment
lit = 0;at line 1331 is immediately overwritten in the loop. This is also present at line 1540 inPexaManAddCardinalityBdd. While harmless, removing these dead stores would improve clarity.🔎 Proposed fix
sat_solver_addclause( p->pSat, pList, pList + lit ); } } - lit = 0; // more then l j = ni - l + 1;
📜 Review details
Configuration used: defaults
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (1)
pexact.c
🧰 Additional context used
🪛 Cppcheck (2.19.0)
pexact.c
[warning] 890-890: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 891-891: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 892-892: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 896-896: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 952-952: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1615-1615: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1616-1616: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1627-1627: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1627-1627: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
🪛 GitHub Check: 🚨 Clang-Tidy
pexact.c
[warning] 1598-1598: pexact.c:1598:5 [readability-function-cognitive-complexity]
function 'PexaManExactPowerSynthesisBasePower' has cognitive complexity of 27 (threshold 25)
[warning] 1540-1540: pexact.c:1540:5 [clang-analyzer-deadcode.DeadStores]
Value stored to 'lit' is never read
[warning] 1411-1411: pexact.c:1411:30 [clang-analyzer-security.ArrayBound]
Out of bound access to memory preceding 'pListP'
[warning] 1411-1411: pexact.c:1411:28 [clang-analyzer-core.uninitialized.Assign]
Assigned value is uninitialized
[warning] 1331-1331: pexact.c:1331:5 [clang-analyzer-deadcode.DeadStores]
Value stored to 'lit' is never read
[warning] 1270-1270: pexact.c:1270:26 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'res'
[warning] 1269-1269: pexact.c:1269:26 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'res'
[warning] 1082-1082: pexact.c:1082:9 [clang-analyzer-security.ArrayBound]
Out of bound access to memory preceding 'pVars'
[warning] 898-898: pexact.c:898:5 [clang-analyzer-core.uninitialized.Assign]
Assigned value is uninitialized
[warning] 896-896: pexact.c:896:32 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'res'
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (2)
- GitHub Check: ABC Integration (ubuntu-latest)
- GitHub Check: ABC Integration (macos-latest)
🔇 Additional comments (5)
pexact.c (5)
269-292: LGTM!The addition of the
bddparameter and conditionalxiBasecalculation correctly supports the new BDD-based encoding path.
950-958: LGTM!The cleanup logic is correct, properly freeing both the combination array and the node. This will work correctly once
PopCombis fixed to handle empty lists.
1242-1249: Exponential complexity and large VLAs.The
sizevariable at line 1242 ispow(r+1, pow(2, k-1)), which grows exponentially. Fork=4andr=10, this is11^8 = 214,358,881iterations. The VLAs at lines 1244 and 1251 could also cause stack overflow for larger inputs.Consider adding bounds validation or documenting the expected input ranges.
969-999: LGTM!The P-variable evaluation logic correctly aggregates values from the SAT solution and compares against the expected combination.
1185-1203: LGTM!The BDD-based P-clause encoding correctly initializes variables and delegates to helper functions.
There was a problem hiding this comment.
Actionable comments posted: 2
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
pexact.h (1)
21-32: Multiple definition error:const intin header has external linkage in C.Defining
const intvariables in a header file causes multiple definition linker errors when the header is included in multiple translation units. In C (unlike C++),constat file scope has external linkage by default.🔎 Proposed fix: Use macros or extern declarations
Option 1: Use preprocessor macros (preferred for constants)
-const int CONST_ZERO = 0; -const int CONST_ONE = 1; -const int CONST_TWO = 2; -const int CONST_THREE = 3; -const int CONST_FOUR = 4; -const int CONST_FIVE = 5; -const int CONST_SIX = 6; -const int CONST_SEVEN = 7; -const int CONST_TEN = 10; - -const int CONST_NINETY_SIX = 96; -const int CONST_FIFTY_SIX = 56; +#define CONST_ZERO 0 +#define CONST_ONE 1 +#define CONST_TWO 2 +#define CONST_THREE 3 +#define CONST_FOUR 4 +#define CONST_FIVE 5 +#define CONST_SIX 6 +#define CONST_SEVEN 7 +#define CONST_TEN 10 + +#define CONST_NINETY_SIX 96 +#define CONST_FIFTY_SIX 56Option 2: Use
static constfor internal linkage-const int CONST_ZERO = 0; +static const int CONST_ZERO = 0;(Apply to all constants)
♻️ Duplicate comments (6)
pexact.c (6)
894-903: Missing NULL checks for malloc and uninitializednode->next.This issue was flagged in a previous review but remains unaddressed:
- Lines 894 and 897: malloc results are not checked for NULL.
node->nextis never initialized before use (line 903 assignsptrwhich may be garbage when node is appended).
942-948: Missing bounds check before pop operation.This issue was flagged in a previous review but remains unaddressed. If
PopCombis called whenlist->length == 0orlist->start == NULL, undefined behavior occurs.
1100-1108: Variable shadowing: loop variablepshadows function parameterp.This issue was flagged in a previous review but remains unaddressed. The loop variable
int pat lines 1101 and 1105 shadows thePexaMan_t * pparameter, causing confusion and static analysis warnings.
1322-1322: Typo:01is octal notation, likely meant1.This issue was flagged in a previous review but remains unaddressed. While functionally equivalent to decimal 1, using octal
01is inconsistent with surrounding code.
1885-1890: Missing NULL check for malloc and potential infinite loop.These issues were flagged in a previous review but remain unaddressed:
- Line 1885:
mallocresult not checked before use.- Line 1890:
while(1)loop has no termination condition if no solution exists.
1928-1930: Memory leak:listis never freed.This issue was flagged in a previous review but remains unaddressed.
FreeCombList(list)deallocates the nodes but not theCombList_tstructure itself.
🧹 Nitpick comments (2)
pexact.c (2)
1340-1392: Consider performance and stack safety for larger inputs.The function uses exponential iteration (
pow(r+1, pow(2, k-1))combinations) and VLAs inside loops. For the current k=4 use case this is acceptable, but be aware this won't scale to larger input sizes without significant rework.Additionally, the pattern at line 1365-1366 (
j = sizeSingleto break inner loop) is unconventional. Consider usingbreakwith a labeled statement or restructuring for clarity.
1296-1308: Consider documenting the derivation of magic constants.The values
CONST_NINETY_SIX(96) andCONST_FIFTY_SIX(56) for the k=4 special case would benefit from a brief comment explaining their derivation, aiding future maintenance.
📜 Review details
Configuration used: defaults
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (3)
init.cpppexact.cpexact.h
🚧 Files skipped from review as they are similar to previous changes (1)
- init.cpp
🧰 Additional context used
🧬 Code graph analysis (1)
pexact.h (1)
pexact.c (1)
PexaManExactPowerSynthesisBasePower(1870-1931)
🪛 Cppcheck (2.19.0)
pexact.c
[warning] 895-895: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 896-896: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 897-897: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 901-901: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 958-958: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1886-1886: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1887-1887: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1903-1903: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1903-1903: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
🪛 GitHub Check: 🚨 Clang-Tidy
pexact.c
[warning] 1900-1900: pexact.c:1900:17 [clang-analyzer-unix.Malloc]
Potential leak of memory pointed to by 'list'
[warning] 1570-1570: pexact.c:1570:28 [clang-analyzer-core.uninitialized.Assign]
Assigned value is uninitialized
[warning] 1319-1319: pexact.c:1319:14 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'res'
[warning] 1318-1318: pexact.c:1318:14 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'res'
[warning] 1107-1107: pexact.c:1107:9 [clang-analyzer-security.ArrayBound]
Out of bound access to memory preceding 'pVars'
[warning] 903-903: pexact.c:903:5 [clang-analyzer-core.uninitialized.Assign]
Assigned value is uninitialized
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (2)
- GitHub Check: ABC Integration (ubuntu-latest)
- GitHub Check: ABC Integration (macos-latest)
🔇 Additional comments (7)
pexact.h (2)
74-105: LGTM!The
Comb_tandCombList_tdata structures are well-documented and appropriately designed for the combinatorial search framework.
107-108: LGTM!The new public API function prototype is properly declared.
pexact.c (5)
271-292: LGTM!The BDD-aware truth table printing logic correctly adjusts
xiBasebased on the encoding type.
956-964: LGTM!The deallocation logic is correct, assuming
PopCombis fixed to handle edge cases as noted in the previous review.
1831-1856: LGTM!The error handling in
ExactPowerSynthesisCNFhas been improved. The function now properly validates each step and returns early on failure.
1037-1069: LGTM!The MUX encoding correctly implements the CNF clauses for a multiplexer:
o = c ? i1 : i0.
975-1005: LGTM!The P-variable evaluation logic correctly extracts solution information from the SAT solver.
There was a problem hiding this comment.
Actionable comments posted: 0
♻️ Duplicate comments (5)
pexact.c (5)
886-930: Critical issues remain unaddressed from previous reviews.This function still has the following issues previously flagged:
- Missing NULL checks for
mallocon lines 894 and 897node->nextis never initialized to NULL- Memory leak on early return path (lines 889-893) -
nodeis allocated but not freed if length mismatch occurs🔎 Proposed fix
bool AddCombi( int act, int r, const int * combi, int combiLen, CombList_t * list ) { int len = list->len; if ( len != combiLen ) { printf( "Error: combination length mismatch.\n" ); return 0; } Comb_t * node = ( Comb_t * )malloc( sizeof( Comb_t ) ); + if ( node == NULL ) + { + printf( "Error: memory allocation failed in AddCombi.\n" ); + return 0; + } node->act = act; node->r = r; node->combi = ( int * )malloc( len * sizeof( int ) ); + if ( node->combi == NULL ) + { + printf( "Error: memory allocation failed in AddCombi.\n" ); + free( node ); + return 0; + } + node->next = NULL; for ( int i = 0; i < len; i++ ) { *( node->combi + i ) = *( combi + i ); }
1113-1120: Critical: Variable shadowing remains unaddressed.Loop variables
int pat lines 1113 and 1117 shadow the function parameterPexaMan_t * p, which was previously flagged as a critical issue. This causes the wrong variable to be referenced.🔎 Proposed fix
- for ( int p = 0; p < np; p++ ) + for ( int pi = 0; pi < np; pi++ ) { - pVars[p] = pStart + p; + pVars[pi] = pStart + pi; } - for ( int p = np; ( p < ( 2 * np ) - 2 ) && ( p >= 0 ); p++ ) + for ( int pi = np; ( pi < ( 2 * np ) - 2 ) && ( pi >= 0 ); pi++ ) { - pVars[p] = pStart + ( 2 * np ) - 2 - p; + pVars[pi] = pStart + ( 2 * np ) - 2 - pi; }
1334-1334: Typo: Octal literal should be decimal.Line 1334 uses
p8 > 01where01is octal notation. This was previously flagged and should be changed to decimal1for consistency.🔎 Proposed fix
- int exep1 = ( p4 >= 2 ) | ( p8 > 01 ) | ( ( p4 >= 1 ) && ( p8 >= 1 ) ) | ( ( ( p4 >= 1 ) | ( p8 >= 1 ) ) && ( ( p2 >= 1 ) | ( p6 >= 1 ) ) ); + int exep1 = ( p4 >= 2 ) | ( p8 > 1 ) | ( ( p4 >= 1 ) && ( p8 >= 1 ) ) | ( ( ( p4 >= 1 ) | ( p8 >= 1 ) ) && ( ( p2 >= 1 ) | ( p6 >= 1 ) ) );
1565-1571: Critical: Variable shadowing remains unaddressed.Loop variables
int pat lines 1565 and 1569 shadow the function parameterPexaMan_t * p. This was previously flagged as a critical issue causing undefined behavior when accessingp->nVarsandp->nNodes.🔎 Proposed fix
- for ( int p = 0; p < litsize; p++ ) + for ( int pi = 0; pi < litsize; pi++ ) { - pListP[p] = 0; + pListP[pi] = 0; } - for ( int p = 0; p < np; p++ ) + for ( int pi = 0; pi < np; pi++ ) { - pListP[p] = Abc_Var2Lit( pStartvar++, 0 ); + pListP[pi] = Abc_Var2Lit( pStartvar++, 0 ); }
1901-1953: Critical issues remain unaddressed from previous reviews.This function has multiple unresolved issues previously flagged:
- Line 1901:
mallocresult not checked for NULL before accessing list members (lines 1902-1903)- Line 1906:
while(1)infinite loop with no termination condition for unsatisfiable problems- Lines 1915-1916: Error path calls
FreeCombList(list)but doesn'tfree(list)itself, causing memory leak- Line 1951: Same issue -
FreeCombList(list)doesn't free the list structure itself🔎 Proposed fix
CombList_t * list = ( CombList_t * )malloc( sizeof( CombList_t ) ); + if ( list == NULL ) + { + printf( "Error: memory allocation failed.\n" ); + PexaManFree( p ); + return 1; + } + list->start = NULL; list->len = pow( 2, p->nVars - 1 ); list->length = 0; int r = 0; int act = 0; + int maxAct = CalcMaxAct( MAJ_NOBJS - p->nVars, p->nVars ); - while ( 1 ) + while ( act <= maxAct ) { if ( act >= CalcMaxAct( r + 1, p->nVars ) ) { r++; + if ( r >= MAJ_NOBJS - p->nVars ) + { + printf( "No solution found within gate limit.\n" ); + FreeCombList( list ); + free( list ); + PexaManFree( p ); + return 1; + } pPars->nNodes = r + 1; if ( !CalculateCombArray( p->nVars, r, list ) ) { printf( "Error: could not calculate combination array.\n" ); FreeCombList( list ); + free( list ); + PexaManFree( p ); return 0; } } // ... rest of function ... act++; } FreeCombList( list ); + free( list ); return 0;
🧹 Nitpick comments (1)
pexact.c (1)
943-956: Improve bounds check for PopComb.Line 945 checks
list->start == 0which compares a pointer to an integer. While this works, it's better style to useNULL. Additionally, checklist->lengthfor consistency.🔎 Proposed fix
Comb_t * PopComb( CombList_t * list ) { - if ( list->start == 0 ) + if ( list == NULL || list->length == 0 || list->start == NULL ) { return NULL; } list->length--; Comb_t * node = list->start; if ( list->start->next != NULL ) { list->start = list->start->next; } return node; }
📜 Review details
Configuration used: defaults
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (1)
pexact.c
🧰 Additional context used
🪛 Cppcheck (2.19.0)
pexact.c
[warning] 895-895: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 896-896: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 897-897: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 901-901: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 966-966: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1902-1902: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1903-1903: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1919-1919: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1919-1919: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
🪛 GitHub Check: 🚨 Clang-Tidy
pexact.c
[warning] 1919-1919: pexact.c:1919:34 [clang-analyzer-unix.Malloc]
Use of memory after it is freed
[warning] 1916-1916: pexact.c:1916:17 [clang-analyzer-unix.Malloc]
Potential leak of memory pointed to by 'list'
[warning] 1579-1579: pexact.c:1579:13 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'pList'
[warning] 1571-1571: pexact.c:1571:9 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'pListP'
[warning] 1331-1331: pexact.c:1331:14 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'res'
[warning] 1330-1330: pexact.c:1330:14 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'res'
[warning] 951-951: pexact.c:951:28 [clang-analyzer-core.UndefinedBinaryOperatorResult]
The left operand of '!=' is a garbage value
[warning] 951-951: pexact.c:951:10 [clang-analyzer-unix.Malloc]
Use of memory after it is freed
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (2)
- GitHub Check: ABC Integration (ubuntu-latest)
- GitHub Check: ABC Integration (macos-latest)
🔇 Additional comments (17)
pexact.c (17)
269-292: LGTM: BDD parameter properly integrated.The addition of the
bddparameter and conditional logic for adjustingxiBaseis correct and allows the printing function to handle both BDD and non-BDD encoding modes.
345-381: LGTM: BDD parameter correctly threaded through.The
bddparameter is properly passed toPexaManPrintSolutionTruthTable, maintaining consistency with the updated API.
964-976: LGTM: Proper deallocation of list nodes.The function correctly frees both
node->combiandnodefor each element, with proper NULL checking.
1028-1037: LGTM: Base conversion implementation is correct.The function correctly converts an integer to its base representation with proper array indexing.
1049-1081: LGTM: Correct MUX encoding clauses.The four CNF clauses properly encode the multiplexer semantics
o = c ? i1 : i0.
1167-1195: LGTM: Upper bound constraints correctly implemented.The function properly enforces that at most one P-variable is satisfied by adding clauses for all combinations where exactly 2 variables are set.
1207-1237: LGTM: Lower bound constraints correctly implemented.The function properly enforces that at least one P-variable is satisfied by adding clauses for the case where all np-1 variables would be unset.
1272-1297: LGTM: BDD P-variable clauses properly integrated.The function correctly initializes
p->i_p(line 1283) and adds both MUX encoding and sum-to-one constraints for each gate.
1308-1320: LGTM: Maximum activity calculation.The function correctly calculates maximum switching activity with special handling for 4-input cases.
1352-1404: LGTM: Combination array calculation with proper error handling.The function correctly generates all valid switching activity combinations and properly propagates errors from
AddCombi.
1415-1521: LGTM: Cardinality constraints correctly implemented.The three functions properly implement polynomial cardinality constraints for both lower and upper bounds.
1532-1543: LGTM: Bit counting function is correct.The function correctly counts the minimum of ones and zeros in the binary representation.
1603-1698: LGTM: Sum-to-one constraints for naive encoding.The three functions correctly enforce that exactly one P-variable is satisfied for the naive encoding scheme.
1706-1721: LGTM: Naive P-variable encoding entry point.The function properly initializes
p->i_pand adds all necessary constraints for naive encoding.
1731-1845: LGTM: BDD cardinality constraints correctly implemented.The functions properly implement cardinality constraints for the BDD-based P-variable encoding, with appropriate index calculations for the BDD structure.
1847-1872: LGTM: CNF synthesis with proper error handling.The function correctly integrates base CNF encoding, P-variable clauses, and cardinality constraints with proper error checking at each stage.
987-1017: FunctionPexaManEvalPVariablesBddis unused and never called.This function is defined but has no call sites in the codebase. The concern about
i_pinitialization is moot since there are no callers to verify. Consider removing this dead code if it's not intended for future use.Likely an incorrect or invalid review comment.
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (6)
pexact.c (6)
1108-1116: Variable shadowing: loop variablepshadows function parameterp.At lines 1109 and 1113, the loop variable
int pshadows thePexaMan_t * pfunction parameter. While the current loop bodies don't access the struct pointer, this is confusing and error-prone for future modifications.🔎 Proposed fix
- for ( int p = 0; p < np; p++ ) + for ( int pi = 0; pi < np; pi++ ) { - pVars[p] = pStart + p; + pVars[pi] = pStart + pi; } - for ( int p = np; ( p < ( 2 * np ) - 2 ) && ( p >= 0 ); p++ ) + for ( int pi = np; ( pi < ( 2 * np ) - 2 ) && ( pi >= 0 ); pi++ ) { - pVars[p] = pStart + ( 2 * np ) - 2 - p; + pVars[pi] = pStart + ( 2 * np ) - 2 - pi; }
894-901: Missing NULL checks for malloc and uninitializednode->next.This issue was flagged in a previous review and remains unaddressed:
- Memory allocations at lines 894 and 897 lack NULL checks, risking null pointer dereference if allocation fails.
node->nextis never explicitly initialized toNULL. When the node is appended at the end of the list (line 925),node->nextwill contain garbage, corrupting the list.🔎 Proposed fix
bool AddCombi( int act, int r, const int * combi, int combiLen, CombList_t * list ) { int len = list->len; if ( len != combiLen ) { printf( "Error: combination length mismatch.\n" ); return 0; } Comb_t * node = ( Comb_t * )malloc( sizeof( Comb_t ) ); + if ( node == NULL ) + { + printf( "Error: memory allocation failed in AddCombi.\n" ); + return 0; + } node->act = act; node->r = r; node->combi = ( int * )malloc( len * sizeof( int ) ); + if ( node->combi == NULL ) + { + printf( "Error: memory allocation failed in AddCombi.\n" ); + free( node ); + return 0; + } + node->next = NULL; for ( int i = 0; i < len; i++ )
1326-1331: Typo:01is octal notation, likely meant1.Line 1330 uses
p8 > 01where01is octal notation (equals decimal 1). While functionally correct, this appears to be a typo and should use decimal1for consistency with surrounding code.🔎 Proposed fix
- int exep1 = ( p4 >= 2 ) | ( p8 > 01 ) | ( ( p4 >= 1 ) && ( p8 >= 1 ) ) | ( ( ( p4 >= 1 ) | ( p8 >= 1 ) ) && ( ( p2 >= 1 ) | ( p6 >= 1 ) ) ); + int exep1 = ( p4 >= 2 ) | ( p8 > 1 ) | ( ( p4 >= 1 ) && ( p8 >= 1 ) ) | ( ( ( p4 >= 1 ) | ( p8 >= 1 ) ) && ( ( p2 >= 1 ) | ( p6 >= 1 ) ) );
1561-1568: Critical: Variable shadowing causes potential undefined behavior.At lines 1561 and 1565,
int pshadows thePexaMan_t * pfunction parameter. While these specific loop bodies don't dereference the struct pointer, the shadowing confuses static analysis tools and is error-prone. The static analyzer reports potential out-of-bounds access, likely due to this shadowing.🔎 Proposed fix
- for ( int p = 0; p < litsize; p++ ) + for ( int idx = 0; idx < litsize; idx++ ) { - pListP[p] = 0; + pListP[idx] = 0; } - for ( int p = 0; p < np; p++ ) + for ( int idx = 0; idx < np; idx++ ) { - pListP[p] = Abc_Var2Lit( pStartvar++, 0 ); + pListP[idx] = Abc_Var2Lit( pStartvar++, 0 ); }
1941-1942: Memory leak:liststruct not freed.
FreeCombList(list)deallocates the nodes but not theCombList_tstructure itself.🔎 Proposed fix
FreeCombList( list ); + free( list ); return 0; }
1897-1914: Missing NULL checks for malloc, uninitialized fields, and memory leak.Multiple issues in this initialization block:
- Line 1897:
mallocresult is not checked for NULL before use at lines 1898-1899.- Line 1897-1899:
list->startis never initialized toNULL, which is required forPopComb's safety check at line 945.- Lines 1911-1912: When
CalculateCombArrayfails,FreeCombList(list)deallocates the nodes but not theCombList_tstructure itself, causing a memory leak.🔎 Proposed fix
CombList_t * list = ( CombList_t * )malloc( sizeof( CombList_t ) ); + if ( list == NULL ) + { + printf( "Error: memory allocation failed.\n" ); + PexaManFree( p ); + return 1; + } + list->start = NULL; list->len = pow( 2, p->nVars - 1 ); list->length = 0; int r = 0; int act = 0; while ( 1 ) { if ( act >= CalcMaxAct( r + 1, p->nVars ) ) { r++; pPars->nNodes = r + 1; if ( !CalculateCombArray( p->nVars, r, list ) ) { printf( "Error: could not calculate combination array.\n" ); FreeCombList( list ); + free( list ); + PexaManFree( p ); return 0; } }Based on static analysis hints from Cppcheck and Clang-Tidy.
📜 Review details
Configuration used: defaults
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (1)
pexact.c
🧰 Additional context used
🪛 Cppcheck (2.19.0)
pexact.c
[warning] 895-895: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 896-896: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 897-897: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 901-901: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 966-966: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1898-1898: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1899-1899: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1915-1915: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1915-1915: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
🪛 GitHub Check: 🚨 Clang-Tidy
pexact.c
[warning] 1915-1915: pexact.c:1915:34 [clang-analyzer-unix.Malloc]
Use of memory after it is freed
[warning] 1912-1912: pexact.c:1912:17 [clang-analyzer-unix.Malloc]
Potential leak of memory pointed to by 'list'
[warning] 1575-1575: pexact.c:1575:13 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'pList'
[warning] 1567-1567: pexact.c:1567:9 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'pListP'
[warning] 1327-1327: pexact.c:1327:14 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'res'
[warning] 1326-1326: pexact.c:1326:14 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'res'
[warning] 951-951: pexact.c:951:28 [clang-analyzer-core.UndefinedBinaryOperatorResult]
The left operand of '!=' is a garbage value
[warning] 951-951: pexact.c:951:10 [clang-analyzer-unix.Malloc]
Use of memory after it is freed
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (2)
- GitHub Check: ABC Integration (ubuntu-latest)
- GitHub Check: ABC Integration (macos-latest)
🔇 Additional comments (3)
pexact.c (3)
269-292: LGTM!The added
bddparameter and conditionalxiBaserecomputation are consistent with the BDD-aware path documented in the summary. The logic correctly differentiates between BDD and non-BDD modes.
983-1013: LGTM!The
PexaManEvalPVariablesBddfunction correctly evaluates P-variable values from the SAT solver solution and compares against the expected combination. The logic for computingcombiSoland comparing withcombiis sound.
1843-1868: LGTM!The
ExactPowerSynthesisCNFfunction properly propagates errors from all sub-calls (PexaManAddCnfStart,PexaManAddCnf,PexaManAddPClausesBdd, andPexaManAddCardinalityBdd), returning0on any failure. This addresses the previous review concern about incomplete error handling.
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (3)
pexact.c (3)
1331-1348: Typo:01is octal notation, should be1.Line 1341 uses
p8 > 01where01is octal notation (equals decimal 1). While functionally correct, this appears to be a typo and is inconsistent with surrounding code.🔎 Proposed fix
- int exep1 = ( p4 >= 2 ) | ( p8 > 01 ) | ( ( p4 >= 1 ) && ( p8 >= 1 ) ) | ( ( ( p4 >= 1 ) | ( p8 >= 1 ) ) && ( ( p2 >= 1 ) | ( p6 >= 1 ) ) ); + int exep1 = ( p4 >= 2 ) | ( p8 > 1 ) | ( ( p4 >= 1 ) && ( p8 >= 1 ) ) | ( ( ( p4 >= 1 ) | ( p8 >= 1 ) ) && ( ( p2 >= 1 ) | ( p6 >= 1 ) ) );This issue was previously flagged but remains unresolved.
886-931: Missing NULL checks for malloc allocations.The function performs two
malloccalls (lines 894, 897) without checking for NULL before dereferencing. If allocation fails, this will cause undefined behavior.🔎 Proposed fix
bool AddCombi( int act, int r, const int * combi, int combiLen, CombList_t * list ) { int len = list->len; if ( len != combiLen ) { printf( "Error: combination length mismatch.\n" ); return 0; } Comb_t * node = ( Comb_t * )malloc( sizeof( Comb_t ) ); + if ( node == NULL ) + { + printf( "Error: memory allocation failed in AddCombi.\n" ); + return 0; + } node->act = act; node->r = r; node->combi = ( int * )malloc( len * sizeof( int ) ); + if ( node->combi == NULL ) + { + printf( "Error: memory allocation failed in AddCombi.\n" ); + free( node ); + return 0; + } node->next = NULL;Based on static analysis hints from Cppcheck.
1560-1600: Critical bug: Variable shadowing causes invalid pointer dereference.The loop variable
int pat lines 1572 and 1576 shadows the function parameterPexaMan_t * p. Subsequently, line 1583 usesp->nVarsto dereference what it expects to be the struct pointer, but instead dereferences the integer loop variable, causing undefined behavior.🔎 Proposed fix
sat_solver_setnvars( p->pSat, p->iVar ); - for ( int p = 0; p < litsize; p++ ) + for ( int pi = 0; pi < litsize; pi++ ) { - pListP[p] = 0; + pListP[pi] = 0; } - for ( int p = 0; p < np; p++ ) + for ( int pi = 0; pi < np; pi++ ) { - pListP[p] = Abc_Var2Lit( pStartvar++, 0 ); + pListP[pi] = Abc_Var2Lit( pStartvar++, 0 ); }Based on static analysis hints from Clang-Tidy. This issue was flagged in previous reviews but appears to have been reintroduced.
📜 Review details
Configuration used: defaults
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (1)
pexact.c
🧰 Additional context used
🪛 Cppcheck (2.19.0)
pexact.c
[warning] 895-895: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 896-896: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 897-897: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 898-898: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 902-902: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 970-970: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1909-1909: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1910-1910: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1926-1926: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1926-1926: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
🪛 GitHub Check: 🚨 Clang-Tidy
pexact.c
[warning] 1923-1923: pexact.c:1923:17 [clang-analyzer-unix.Malloc]
Potential leak of memory pointed to by 'list'
[warning] 1586-1586: pexact.c:1586:13 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'pList'
[warning] 1578-1578: pexact.c:1578:9 [clang-analyzer-security.ArrayBound]
Out of bound access to memory after the end of 'pListP'
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (2)
- GitHub Check: ABC Integration (macos-latest)
- GitHub Check: ABC Integration (ubuntu-latest)
🔇 Additional comments (3)
pexact.c (3)
269-271: LGTM: Printing API extended correctly.The addition of the
bool bddparameter to both printing functions is implemented consistently across declarations, definitions, and call sites. The conditional logic at lines 288-292 correctly adjustsxiBasebased on the encoding type.Also applies to: 345-347, 381-381, 865-865
944-979: LGTM: Memory management functions are correct.
PopCombproperly handles both the case wherenext != NULLand when removing the last element by settinglist->start = NULL.FreeCombListincludes appropriate NULL checks before dereferencing the popped node.
1854-1879: LGTM: Error handling is complete.All CNF encoding function calls properly check return values and return early on failure, preventing subsequent operations from running with incomplete encoding state.
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (4)
pexact.c (4)
1095-1158: Variable shadowing: loop variablepshadows function parameter.At lines 1116 and 1120, the loop variable
int pshadows the function parameterPexaMan_t * p. While the code is technically correct due to C's scoping rules, this creates confusion and makes the code error-prone for future modifications. This issue was flagged in previous reviews.🔎 Proposed fix
int pVars[( 2 * np ) - 2]; - for ( int p = 0; p < np; p++ ) + for ( int pi = 0; pi < np; pi++ ) { - pVars[p] = pStart + p; + pVars[pi] = pStart + pi; } - for ( int p = np; ( p < ( 2 * np ) - 2 ) && ( p >= 0 ); p++ ) + for ( int pi = np; ( pi < ( 2 * np ) - 2 ) && ( pi >= 0 ); pi++ ) { - pVars[p] = pStart + ( 2 * np ) - 2 - p; + pVars[pi] = pStart + ( 2 * np ) - 2 - pi; }Based on past review comments.
1341-1341: Typo:01is octal notation, likely meant1.Line 1341 uses
p8 > 01where01is octal notation (equals decimal 1). While functionally correct, this appears to be a typo and should use decimal1for consistency. This was flagged in a previous review but not yet addressed.🔎 Proposed fix
- int exep1 = ( p4 >= 2 ) | ( p8 > 01 ) | ( ( p4 >= 1 ) && ( p8 >= 1 ) ) | ( ( ( p4 >= 1 ) | ( p8 >= 1 ) ) && ( ( p2 >= 1 ) | ( p6 >= 1 ) ) ); + int exep1 = ( p4 >= 2 ) | ( p8 > 1 ) | ( ( p4 >= 1 ) && ( p8 >= 1 ) ) | ( ( ( p4 >= 1 ) | ( p8 >= 1 ) ) && ( ( p2 >= 1 ) | ( p6 >= 1 ) ) );
1893-1954: Missing NULL check for malloc and memory leak of list structure.Two critical issues remain unfixed from previous reviews:
Line 1908:
mallocforCombList_tlacks a NULL check before dereferencing at lines 1909-1910. If allocation fails, this will cause a null pointer dereference.Lines 1922 and 1952:
FreeCombList(list)frees the nodes but not theCombList_tstructure itself, causing a memory leak on both the error path (line 1922) and normal exit path (line 1952).🔎 Proposed fix
CombList_t * list = ( CombList_t * )malloc( sizeof( CombList_t ) ); + if ( list == NULL ) + { + printf( "Error: memory allocation failed.\n" ); + PexaManFree( p ); + return 1; + } list->len = pow( 2, p->nVars - 1 ); list->length = 0;if ( !CalculateCombArray( p->nVars, r, list ) ) { printf( "Error: could not calculate combination array.\n" ); FreeCombList( list ); + free( list ); + PexaManFree( p ); return 0; }FreeCombList( list ); + free( list ); return 0;Based on static analysis hints from Cppcheck and Clang-Tidy, and previous review comments.
886-931: Missing NULL checks for malloc allocations.The function allocates memory at lines 894 and 897 but doesn't check if
mallocreturnsNULL. If allocation fails, dereferencingnode(lines 895-898) ornode->combi(line 902) will cause a null pointer dereference.🔎 Proposed fix
bool AddCombi( int act, int r, const int * combi, int combiLen, CombList_t * list ) { int len = list->len; if ( len != combiLen ) { printf( "Error: combination length mismatch.\n" ); return 0; } Comb_t * node = ( Comb_t * )malloc( sizeof( Comb_t ) ); + if ( node == NULL ) + { + printf( "Error: memory allocation failed in AddCombi.\n" ); + return 0; + } node->act = act; node->r = r; node->combi = ( int * )malloc( len * sizeof( int ) ); + if ( node->combi == NULL ) + { + printf( "Error: memory allocation failed in AddCombi.\n" ); + free( node ); + return 0; + } node->next = NULL;Based on static analysis hints from Cppcheck.
🧹 Nitpick comments (1)
pexact.c (1)
1913-1951: Infinite loop without termination bound.The
while(1)loop at line 1913 lacks an explicit upper bound on gate count or activity. If no solution exists for the truth table (or there's a bug in the encoding), the loop will run indefinitely. Consider adding a maximum iteration count or gate count limit for safety.🔎 Proposed enhancement
int r = 0; int act = 0; - while ( 1 ) + int maxGateCount = MAJ_NOBJS - p->nVars; + while ( r < maxGateCount ) { if ( act >= CalcMaxAct( r + 1, p->nVars ) ) { r++; + if ( r >= maxGateCount ) + { + printf( "No solution found within %d gates.\n", maxGateCount ); + break; + }This was noted in a previous review.
📜 Review details
Configuration used: defaults
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (1)
pexact.c
🧰 Additional context used
🪛 Cppcheck (2.19.0)
pexact.c
[warning] 895-895: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 896-896: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 897-897: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 898-898: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 902-902: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 970-970: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1909-1909: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1910-1910: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1926-1926: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
[warning] 1926-1926: If memory allocation fails, then there is a possible null pointer dereference
(nullPointerOutOfMemory)
🪛 GitHub Check: 🚨 Clang-Tidy
pexact.c
[warning] 1923-1923: pexact.c:1923:17 [clang-analyzer-unix.Malloc]
Potential leak of memory pointed to by 'list'
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (2)
- GitHub Check: ABC Integration (ubuntu-latest)
- GitHub Check: ABC Integration (macos-latest)
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (3)
pexact.c (3)
1567-1607: Variable shadowing: loop variablepshadows function parameter.At lines 1579 and 1583, the loop variable
int pshadows the function parameterPexaMan_t * p. This creates confusion and is error-prone. This issue was flagged in previous reviews but remains unaddressed.🔎 Proposed fix
- for ( int p = 0; p < litsize; p++ ) + for ( int pi = 0; pi < litsize; pi++ ) { - pListP[p] = 0; + pListP[pi] = 0; } - for ( int p = 0; p < np && p < litsize; p++ ) + for ( int pi = 0; pi < np && pi < litsize; pi++ ) { - pListP[p] = Abc_Var2Lit( pStartvar++, 0 ); + pListP[pi] = Abc_Var2Lit( pStartvar++, 0 ); }Based on past review comments.
1900-1973: Memory leak:liststructure not freed on success and normal exit paths.Two issues:
- Success path (line 1963): When a solution is found, the function breaks without freeing
list.- Normal exit (line 1971):
FreeCombList(list)frees the nodes but not theCombList_tstructure itself.The error path at lines 1938-1942 correctly frees both the nodes and the structure.
🔎 Proposed fix
if ( status == 1 ) { free( node->combi ); free( node ); PexaManPrintSolution( p, fCompl, true ); PexaManFree( p ); + FreeCombList( list ); + free( list ); Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); break; }FreeCombList( list ); + free( list ); return 1; }Based on static analysis hints from Clang-Tidy and past review comments.
🧰 Tools
🪛 GitHub Check: 🚨 Clang-Tidy
[warning] 1972-1972: pexact.c:1972:5 [clang-analyzer-unix.Malloc]
Potential leak of memory pointed to by 'list'
1915-1919: Memory leak:pnot freed whenlistallocation fails.If
mallocforlistfails at line 1915, the function returns at line 1918 without freeingp(allocated at line 1909), causing a memory leak.🔎 Proposed fix
CombList_t * list = ( CombList_t * )malloc( sizeof( CombList_t ) ); if ( list == NULL ) { + PexaManFree( p ); return 1; }Based on static analysis hints from Clang-Tidy.
🧰 Tools
🪛 GitHub Check: 🚨 Clang-Tidy
[warning] 1918-1918: pexact.c:1918:16 [clang-analyzer-unix.Malloc]
Potential leak of memory pointed to by 'p'
🧹 Nitpick comments (2)
pexact.c (2)
1366-1418: Consider dynamic allocation for larger array sizes.The function uses VLAs (variable-length arrays) at lines 1374 and 1381. For
k >= 8,sizeSingle = pow(2, k-1)could create large stack allocations. While this is fine for the current use case (k=4), consider using dynamic allocation withmalloc/freefor robustness if larger values are anticipated.
1429-1467: VLA usage in cardinality functions.Similar to
CalculateCombArray, these functions use VLAs forpList[ni]andres[ni]. The exponential loopfor (int i = 0; i < pow(2, ni); i++)combined with VLAs could be problematic for largenivalues. For the current use case this appears acceptable, but consider adding a bounds check onnior using dynamic allocation for future-proofing.Also applies to: 1478-1514, 1745-1788, 1798-1838
📜 Review details
Configuration used: defaults
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (1)
pexact.c
🧰 Additional context used
🪛 Cppcheck (2.19.0)
pexact.c
[error] 904-904: Memory leak
(memleak)
🪛 GitHub Check: 🚨 Clang-Tidy
pexact.c
[warning] 1972-1972: pexact.c:1972:5 [clang-analyzer-unix.Malloc]
Potential leak of memory pointed to by 'list'
[warning] 1918-1918: pexact.c:1918:16 [clang-analyzer-unix.Malloc]
Potential leak of memory pointed to by 'p'
[warning] 904-904: pexact.c:904:16 [clang-analyzer-unix.Malloc]
Potential leak of memory pointed to by 'node'
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (2)
- GitHub Check: ABC Integration (ubuntu-latest)
- GitHub Check: ABC Integration (macos-latest)
🔇 Additional comments (4)
pexact.c (4)
269-292: LGTM: BDD-aware printing parameter added.The addition of the
bddparameter to the printing functions is clean and allows toggling between BDD-enabled and legacy printing modes.Also applies to: 347-382, 865-865
1102-1165: Good: Variable shadowing avoided.The loop variables at lines 1123 and 1127 correctly use
piinstead ofp, avoiding shadowing of the function parameterPexaMan_t * p.
1861-1886: LGTM: Complete error handling.All function calls are properly checked for failures, and errors are correctly propagated by returning 0.
1038-1047: LGTM: Utility functions.The utility functions
ConvertBaseInt,CalcMaxAct, andCountOneare straightforward and appear correct.Also applies to: 1318-1330, 1546-1557
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (1)
pexact.c (1)
1568-1608: Critical: Variable shadowing causes undefined behavior.The loop variables
int pat lines 1580 and 1584 shadow the function parameterPexaMan_t * p. This is critical because line 1591 usesp->nVars, which will attempt to dereference the integer loop variable as a pointer, causing undefined behavior and likely a crash.This issue was previously flagged and marked as addressed in commit 79930f6, but it remains in the current code.
🔎 Required fix
sat_solver_setnvars( p->pSat, p->iVar ); - for ( int p = 0; p < litsize; p++ ) + for ( int pi = 0; pi < litsize; pi++ ) { - pListP[p] = 0; + pListP[pi] = 0; } - for ( int p = 0; p < np && p < litsize; p++ ) + for ( int pi = 0; pi < np && pi < litsize; pi++ ) { - pListP[p] = Abc_Var2Lit( pStartvar++, 0 ); + pListP[pi] = Abc_Var2Lit( pStartvar++, 0 ); }
🧹 Nitpick comments (2)
pexact.c (2)
952-968: Consider clearing the returned node'snextpointer.While the current implementation correctly updates
list->start, the returned node'snextpointer still points into the list. This could lead to accidental list corruption if callers are not careful. Consider settingnode->next = NULLbefore returning to make the detached node fully independent.🔎 Proposed enhancement
list->length--; Comb_t * node = list->start; if ( list->start->next != NULL ) { list->start = list->start->next; } else { list->start = NULL; } + node->next = NULL; return node;
998-1028: Consider explicit casts forpow()results used as array sizes.Lines 1000, 1008 use
pow()(which returnsdouble) directly for VLA sizes and loop bounds. While implicit conversion works, explicit(int)casts would improve code clarity and make the intent obvious. Additionally, for largenVars(e.g., 10),npcould be 513, which is acceptable but approaching typical stack limits for VLAs.🔎 Example improvement
- int np = pow( 2, p->nVars - 1 ) + 1; + int np = (int)pow( 2, p->nVars - 1 ) + 1; int combiSol[np];
📜 Review details
Configuration used: defaults
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (1)
pexact.c
🔇 Additional comments (5)
pexact.c (5)
269-292: LGTM: BDD parameter additions are well-structured.The addition of the
bddparameter to the printing functions cleanly supports both BDD-aware and legacy modes. The conditional adjustment ofxiBaseat lines 288-292 correctly distinguishes between encoding types.Also applies to: 345-381
976-987: LGTM: NULL check properly guards against PopComb failure.The function correctly handles the case where
PopCombreturns NULL, preventing potential crashes.
1103-1166: LGTM: Variable shadowing resolved in this function.The loop variables at lines 1124 and 1128 correctly use
piinstead ofp, avoiding shadowing of the function parameter. The MUX encoding logic is properly structured with appropriate error checking.
1862-1887: LGTM: CNF construction with proper error propagation.The function correctly chains CNF construction steps and propagates errors appropriately. Each helper function's return value is checked before proceeding.
1339-1356: TheresLenparameter is correctly passed and checked.At line 1341, the function correctly enforces
resLen > CONST_SEVEN(i.e.,resLen > 7), which is necessary since the function accessesres[7]at line 1348 and earlier indices at line 1350. The caller at line 1403 passessizeSingle, which equals2^(k-1)= 8 when k=4, satisfying this requirement. All array accesses remain within bounds.
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (1)
pexact.c (1)
1572-1612: Critical: Variable shadowing not fully resolved.Lines 1584 and 1588 declare loop variables
int pthat shadow the function parameterPexaMan_t * p. This causes line 1595 to dereference the integer loop variable as a pointer, leading to undefined behavior.While past comments indicate this was addressed in commit 79930f6, the issue remains in this code.
🔎 Proposed fix
sat_solver_setnvars( p->pSat, p->iVar ); - for ( int p = 0; p < litsize; p++ ) + for ( int pi = 0; pi < litsize; pi++ ) { - pListP[p] = 0; + pListP[pi] = 0; } - for ( int p = 0; p < np && p < litsize; p++ ) + for ( int pi = 0; pi < np && pi < litsize; pi++ ) { - pListP[p] = Abc_Var2Lit( pStartvar++, 0 ); + pListP[pi] = Abc_Var2Lit( pStartvar++, 0 ); }
🧹 Nitpick comments (2)
pexact.c (2)
886-943: Minor: Sorted insertion logic could be clearer.The insertion logic handles three cases: empty list, insert at head, and insert in middle/tail. While the NULL check at line 927-930 prevents dereferencing a NULL
ptr->next, the loop conditionl < list->length - 1combined with the break makes the logic somewhat fragile.Consider refactoring to use a
while (ptr->next != NULL)loop instead of a counted loop for clarity:🔎 Suggested refactoring for clarity
} else { - for ( int l = 0; l < list->length - 1; l++ ) + while ( ptr->next != NULL ) { - if ( ptr->next == NULL ) - { - break; - } if ( ( ( ptr->act <= act ) && ( ptr->next->act > act ) ) || ( ( ptr->act == act ) && ( ptr->next->act == act ) && ( r >= ptr->r ) && ( r <= ptr->next->r ) ) ) { node->next = ptr->next; + ptr->next = node; - break; + list->length++; + return 1; } ptr = ptr->next; } + // Append at end ptr->next = node; }
1371-1423: Performance concern: Exponential iteration inCalculateCombArray.Line 1377 computes
size = pow(r+1, pow(2, k-1)). Fork=4andr=10, this yields11^8 ≈ 214 millioniterations. While the inner loop has early exits (line 1394-1397), this function could become a performance bottleneck for larger gate counts.Consider adding a progress indicator for large
ror documenting the expected runtime complexity.
📜 Review details
Configuration used: defaults
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (1)
pexact.c
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (2)
- GitHub Check: ABC Integration (ubuntu-latest)
- GitHub Check: ABC Integration (macos-latest)
🔇 Additional comments (10)
pexact.c (10)
269-292: LGTM: BDD parameter integration looks clean.The addition of the
bddparameter to the printing functions is straightforward and correctly propagated. The conditionalxiBasecalculation for BDD mode is properly isolated.Also applies to: 347-381
956-972: LGTM: PopComb correctly handles the last element case.The function now properly sets
list->start = NULLwhen removing the last element (line 969), addressing the previously identified use-after-free issue.
980-991: LGTM: FreeCombList properly handles NULL returns.The NULL check at line 985 ensures the function handles unexpected NULL returns from
PopCombgracefully.
1064-1096: LGTM: MUX encoding is standard and correct.The four clauses correctly encode the MUX semantics
o = c ? i1 : i0, and eachsat_solver_addclausecall is properly checked for failure.
1182-1252: LGTM: Sum-one constraints correctly enforce exactly-one semantics.The upper and lower bound functions together ensure that exactly one
pvariable is satisfied per gate. The logic is correct for implementing at-most-one (upper) and at-least-one (lower) constraints.Also applies to: 1263-1278
1323-1335: Note: Domain-specific formula for maximum switching activity.The special case for
k==4with constantsCONST_NINETY_SIXandCONST_FIFTY_SIXappears to be an empirically derived formula for 4-input networks. Ensure this formula is validated by tests or documented with references.
1866-1891: LGTM: Error handling is comprehensive.All CNF encoding functions are properly checked for failure, and the function returns early on any error. This addresses the previously identified incomplete error handling.
1920-1928: LGTM: Proper initialization and memory allocation.The function now includes NULL checks for malloc (lines 1921-1925) and explicitly initializes
list->start = NULL(line 1928), addressing previously identified issues. The bounded loop at line 1932 prevents infinite loops.
1002-1032: This function is never invoked anywhere in the codebase, making the initialization concern aboutp->i_pmoot. Remove the review comment or flag this function as unused dead code.Likely an incorrect or invalid review comment.
1137-1170: Array bounds forpVarsare safe; no issue found.The
pVarsarray has size2^nVars, and the loop structure guarantees thatynever exceeds2^nVars - 2, making the maximum accesspVars[2^nVars - 1]always within valid bounds. ThemSizeequals2^nVars - 1(sum of 1 to 2^nVars - 1), and the triangular iteration pattern (whereyincrements once perxEnddecrement) ensures bounds safety across all configurations.Likely an incorrect or invalid review comment.
There was a problem hiding this comment.
Actionable comments posted: 1
🧹 Nitpick comments (4)
pexact.c (4)
886-942: Previous issues resolved - logic is now sound.The malloc NULL checks,
node->nextinitialization, and sorted insertion logic correctly address all previously flagged issues.Optional: improve readability of complex condition
Line 927's condition is dense. Consider extracting to helper variables:
+ bool insertBetween = (ptr->act <= act) && (ptr->next->act > act); + bool insertAtSameAct = (ptr->act == act) && (ptr->next->act == act) && (r >= ptr->r) && (r <= ptr->next->r); - if ( ( ( ptr->act <= act ) && ( ptr->next->act > act ) ) || ( ( ptr->act == act ) && ( ptr->next->act == act ) && ( r >= ptr->r ) && ( r <= ptr->next->r ) ) ) + if ( insertBetween || insertAtSameAct )
1001-1031: Consider heap allocation for large VLAs.Several functions use Variable Length Arrays (VLAs) that could grow large:
- Line 1004:
int combiSol[np]wherenp = pow(2, p->nVars - 1) + 1(up to 513 for nVars=10)- Line 1378:
int arraySingle[sizeSingle]- Lines 1385, 1445:
int res[...]in loopsWhile current limits (nVars ≤ 10) keep these manageable, VLAs on the stack can cause issues in deeply nested calls or if limits are increased. Consider using heap allocation (malloc/free) for arrays larger than ~100 elements.
Also applies to: 1370-1422
1904-1988: All previously flagged issues resolved.The function now correctly:
- Checks malloc results
- Uses bounded loop with proper termination
- Initializes
list->start = NULL- Frees memory on all paths (success, error, and normal exit)
- Logs warnings when CNF encoding fails
Optional: production-safe error handling
Line 1912 uses
assert(pPars->nVars <= CONST_TEN)which is compiled out in release builds. Consider explicit validation:Abc_TtReadHex( pTruth, pPars->pTtStr ); - assert( pPars->nVars <= CONST_TEN ); + if ( pPars->nVars > CONST_TEN ) + { + printf( "Error: nVars out of valid range (supported: 2..%d).\n", CONST_TEN ); + return 1; + } p = PexaManAlloc( pPars, pTruth );
1003-1004: Inefficient: use bit shifts for powers of 2.Throughout the file,
pow(2, n)is used for integer exponentiation. Sincepow()operates on doubles, this is slower than necessary and can introduce floating-point precision issues.Consider replacing
pow(2, n)with(1 << n)for better performance:
pow(2, p->nVars)→(1 << p->nVars)pow(2, p->nVars - 1)→(1 << (p->nVars - 1))Also applies to: 1288-1289, 1370-1376
📜 Review details
Configuration used: defaults
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (1)
pexact.c
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (2)
- GitHub Check: ABC Integration (ubuntu-latest)
- GitHub Check: ABC Integration (macos-latest)
🔇 Additional comments (2)
pexact.c (2)
269-292: LGTM - clean BDD mode addition.The
bddparameter addition and conditionalxiBaserecomputation are implemented correctly and consistently across call sites.Also applies to: 347-381
955-971: LGTM - proper NULL handling and edge cases covered.Both
PopCombandFreeCombListcorrectly address previously flagged issues with NULL pointer handling.Also applies to: 979-990
FeldmeierMichael
added
major
* 🔧Fixed Typo * 💄Added basic exact Encoding * 💄Added basic exact Encoding * 🔧fixed Clang-Tidy Warnings #1 * 🔧Fixed Clang-Tidy Warnings #2 * 🔧Fixed Clang-Tidy Warnings #3 * 🔧Fixed Clang-Tidy Warnings #4 * 🔧Fixed Clang-Tidy Warnings #5 * 🔧Fixed Clang-Tidy Warnings #6 * 🔧Fixed Clang-Tidy Warnings #7 * 🔧Fixed Clang-Tidy Warnings #8 * 🔧Fixed Clang-Tidy Warnings #9 * 🔧Fixed Clang-Tidy Warnings #10 * 🔧Fixed Clang-Tidy Warnings #11 * 🔧Fixed Clang-Tidy Warnings #12 * 🔧Fixed Clang-Tidy Warnings #13 * 🔧Fixed Clang-Tidy Warnings #14 * 🔧Fixed Clang-Tidy Warnings #15 * 🔧Fixed Clang-Tidy Warnings #15 * 🔧Fixed Clang-Tidy Warnings #17 * 🔧Fixed Clang-Tidy Warnings #18 * 🔧Fixed Clang-Tidy Warnings #19 * @FeldmeierMichael 🔧Fixed Clang-Tidy Warnings #20 * 🔧Fixed Clang-Tidy Warnings #20 * 🔧Fixed Clang-Tidy Warnings #21 * 🔧Fixed Clang-Tidy Warnings #22 * 🔧Fixed Clang-Tidy Warnings #23 * 🔧Fixed Clang-Tidy Warnings #24 * 💬Added Comments * 🎨Incooperating AI Feedback * 🔧Fixed Clang-Tidy Warnings #25 * 🎨Incooperating AI Feedback #2 * 🔧Fixed Clang-Tidy Warnings #26 * 🔨Added CodeRabbit Feedback * 🔧Fixed Clang-Tidy Warnings #27 * 🔧Fixed Clang-Tidy Warnings #27 * 🔧Fixed Clang-Tidy Warnings #28 * 🔧Fixed Clang-Tidy Warnings #29 * 🔧Fixed Clang-Tidy Warnings #30 * 🔧Fixed Clang-Tidy Warnings #31 * 🔧Fixed Clang-Tidy Warnings [#32] * 🔧Fixed Clang-Tidy Warnings #32 * 🔧Fixed Clang-Tidy Warnings #32 * 🔧Fixed Clang-Tidy Warnings #32 * 🔧Fixed Clang-Tidy Warnings #33 * 🔧Fixed Clang-Tidy Warnings #33 * 🔧Fixed Clang-Tidy Warnings #34 * 🔧Fixed Clang-Tidy Warnings #35 * 🎨Incooperating AI Feedback #3 * 🔧Fixed Clang-Tidy Warnings #36 * 🎨Incooperating AI Feedback #4 * 🔧Fixed Clang-Tidy Warnings #37 * 🔧Fixed Clang-Tidy Warnings #38 * 🎨Incooperating AI Feedback #4 * 🚑 Integrating reviewer feedback * 🔧Fixed Clang-Tidy Warnings #39 * 🎨Incooperating AI Feedback #5 * 🔧Fixed Clang-Tidy Warnings #40 * 🔧Fixed Clang-Tidy Warnings #41 * 🎨Incooperating AI Feedback #6 * 🎨Incooperating AI Feedback #7 * 🔧Fixed Clang-Tidy Warnings #42 * 🎨Incooperating AI Feedback #8 * 🔧Fixed Clang-Tidy Warnings #43 * 🔧Fixed Clang-Tidy Warnings #44 * 🔧Fixed Clang-Tidy Warnings #45 * ✏️ Fix typo --------- Co-authored-by: Marcel Walter <marcel.walter@tum.de>
There was a problem hiding this comment.
Actionable comments posted: 0
🧹 Nitpick comments (1)
pexact.c (1)
1973-2071: Termination logic is correct; consider early exit for efficiency.The main synthesis loop correctly terminates through the
r < maxGateCountguard:
- When
actexceedsCalcMaxAct(r+1, nVars),rincrements (line 2008)- Eventually
r >= maxGateCounttriggers cleanup and return (lines 2009-2016)- This prevents the infinite loop concern from previous reviews
However, if the combination list becomes empty before finding a solution,
actwill increment uselessly until reaching the nextCalcMaxActthreshold. While bounded and correct, you could add an early exit check after line 2065:act++; if (list->length == 0 && act < CalcMaxAct(r + 1, p->nVars)) { // No more combinations for this r, skip to next r act = CalcMaxAct(r + 1, p->nVars); }This is an optional optimization, not a correctness issue.
📜 Review details
Configuration used: defaults
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (1)
pexact.c
🧰 Additional context used
🧠 Learnings (2)
📓 Common learnings
Learnt from: FeldmeierMichael
Repo: cda-tum/ext-pexact PR: 11
File: pexact.c:1181-1277
Timestamp: 2025-12-30T08:48:02.423Z
Learning: The power synthesis variant `PexaManExactPowerSynthesisBasePower` in pexact.c restricts nVars to the range 2..5 (CONST_FIVE), while the base exact synthesis function `PowerExactSynthesisBase` allows nVars up to 10 (CONST_TEN).
📚 Learning: 2025-12-30T08:48:02.423Z
Learnt from: FeldmeierMichael
Repo: cda-tum/ext-pexact PR: 11
File: pexact.c:1181-1277
Timestamp: 2025-12-30T08:48:02.423Z
Learning: The power synthesis variant `PexaManExactPowerSynthesisBasePower` in pexact.c restricts nVars to the range 2..5 (CONST_FIVE), while the base exact synthesis function `PowerExactSynthesisBase` allows nVars up to 10 (CONST_TEN).
Applied to files:
pexact.c
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (2)
- GitHub Check: ABC Integration (ubuntu-latest)
- GitHub Check: ABC Integration (macos-latest)
🔇 Additional comments (3)
pexact.c (3)
883-939: LGTM: Sorted insertion logic is correct.The function correctly handles all insertion cases (empty list, head, middle, tail) with proper memory allocation checks and list maintenance. The control flow uses a mix of early returns and fall-through, but each path correctly increments
list->lengthexactly once.
269-289: API change reserves parameter for future BDD/naive differentiation.The
bddparameter is currently unused (line 289 void cast) but reserved for future differentiation between BDD and naive encoding output formats. This is a reasonable forward-looking API design.The change of
xiBasefromconstto non-const (line 288) is likely in preparation for future modifications when thebddflag is actually used.
1596-1607: Documentation correctly describes implementation.The function documentation now accurately states it returns
min(one-bits, zero-bits + 1)rather than just count of ones, matching the implementation'sret0 = 1initialization. This was corrected based on previous review feedback.
marcelwa
left a comment
marcelwa
left a comment
There was a problem hiding this comment.
Great to see the work here is progressing so swiftly! 🙌 The code looks great. My comments are mostly related to consistency and can be addressed quickly.
Please double-check that you addressed all of CodeRabbit's suggestions and marked the ones as resolved that no longer apply.
| /** | ||
| * @brief Combination element. | ||
| * | ||
| * @details Combination element storing combinations with their internal data. | ||
| * | ||
| * @param act Switching activity. | ||
| * @param r Number of nodes. | ||
| * @param combi Combination array. | ||
| * @param next Pointer to next combination element. | ||
| */ | ||
| typedef struct Comb_t_ Comb_t; | ||
| struct Comb_t_ { | ||
| int act; | ||
| int r; | ||
| int * combi; | ||
| Comb_t * next; | ||
| }; |
There was a problem hiding this comment.
Two things here: 1) Doxygen docstrings always apply to the symbol directly below, in this case, the typedef. However, you want to document the struct. You would hence have to move the typedef above the docstring. 2) @param is used for function parameters, not attributes. Since there is no @attribute tag, I would resort to using single-line docstring syntax in place, i.e.,
| /** | |
| * @brief Combination element. | |
| * | |
| * @details Combination element storing combinations with their internal data. | |
| * | |
| * @param act Switching activity. | |
| * @param r Number of nodes. | |
| * @param combi Combination array. | |
| * @param next Pointer to next combination element. | |
| */ | |
| typedef struct Comb_t_ Comb_t; | |
| struct Comb_t_ { | |
| int act; | |
| int r; | |
| int * combi; | |
| Comb_t * next; | |
| }; | |
| typedef struct Comb_t_ Comb_t; | |
| /** | |
| * @brief Combination element. | |
| * | |
| * @details Combination element storing combinations with their internal data. | |
| */ | |
| struct Comb_t_ { | |
| /// Switching activity. | |
| int act; | |
| /// Number of nodes. | |
| int r; | |
| /// Combination array. | |
| int * combi; | |
| /// Pointer to next combination element. | |
| Comb_t * next; | |
| }; |
Sorry that I missed this on the initial PR introducing most of these structs. It of course applies throughout the file.
| #define MAJ_NOBJS 32 // Const0 + Const1 + nVars + nNodes | ||
|
|
||
| const long long PEXACT_LLONG_MAX = 9223372036854775807; | ||
|
|
||
| const int CONST_ZERO = 0; | ||
| const int CONST_ONE = 1; | ||
| const int CONST_TWO = 2; | ||
| const int CONST_THREE = 3; | ||
| const int CONST_FOUR = 4; | ||
| const int CONST_FIVE = 5; | ||
| const int CONST_SIX = 6; | ||
| const int CONST_SEVEN = 7; | ||
| const int CONST_TEN = 10; | ||
|
|
||
| const int CONST_NINETY_SIX = 96; | ||
| const int CONST_FIFTY_SIX = 56; |
There was a problem hiding this comment.
We have #defines and const variables. Why make the distinction? Aren't const variables to be preferred for proper typing support since macros are just text replacement done by the preprocessor?
There was a problem hiding this comment.
when changing #define MAJ_NOBJS 32 to const int MAJ_NOBJS=32 Failure in Ubuntu Integration Test appears duo to int VarMarks[MAJ_NOBJS][2][MAJ_NOBJS]; in struct PexaMan_t_
There was a problem hiding this comment.
Ah, that must be because the array size requires a compile-time expression. Since constexpr doesn't exist in plain C, let's leave it as is, i.e., the macro definition.
pexact.c
Outdated
| @@ -284,7 +285,8 @@ static void PexaManPrintSolutionTruthTable( PexaMan_t * p, int fCompl ) | |||
| printf( "Error: memory allocation failed.\n" ); | |||
| return; | |||
| } | |||
| const int xiBase = p->iVarMintermBase; | |||
| int xiBase = p->iVarMintermBase; | |||
| ( void )bdd; // Currently unused, reserved for future differentiation | |||
There was a problem hiding this comment.
C23 supports the [[ maybe_unused ]] attribute for this case. I'm not sure which version of C you're targeting. If C11 only, keep as is; otherwise, consider:
static void PexaManPrintSolutionTruthTable( PexaMan_t * p, int fCompl, [[ maybe_unused ]] bool bdd )
pexact.c
Outdated
| /** | ||
| * @brief Adding and sorting combination to priority list. | ||
| * | ||
| * @details adding combination to priority list sorted by activity and number of gates. | ||
| * | ||
| * @param act Switching activity. | ||
| * @param r Gate count. | ||
| * @param combi Combinational array. | ||
| * @param list Combination list. | ||
| */ | ||
| bool AddCombi( int act, int r, const int * combi, int combiLen, CombList_t * list ) |
There was a problem hiding this comment.
Please document the return value via @return (and optionally @retval, see: https://www.doxygen.nl/manual/commands.html#cmdretval).
pexact.c
Outdated
| // printf("%d,",l+1); | ||
| pList[lit++] = Abc_Var2Lit( p->iPVariableStart + mLen + ( l * ( mLen + np ) ) + pi + 1, 1 ); | ||
| } | ||
| } | ||
| // printf("\n"); | ||
| if ( !sat_solver_addclause( p->pSat, pList, pList + lit ) ) | ||
| { | ||
| return 0; | ||
| } |
pexact.c
Outdated
| /** | ||
| * @brief Adds carinality constraints. | ||
| * | ||
| * @details Introduces cardinality constraints for bdd type encoding for p variables to SAT CNF encoding. |
There was a problem hiding this comment.
| * @details Introduces cardinality constraints for bdd type encoding for p variables to SAT CNF encoding. | |
| * @details Introduces cardinality constraints for BDD type encoding for p variables to SAT CNF encoding. |
| * @param p Pexact struct. | ||
| * @param combi combinational array. | ||
| * @param xp iteration variable of p variables. | ||
| * |
There was a problem hiding this comment.
| * @param p Pexact struct. | |
| * @param combi combinational array. | |
| * @param xp iteration variable of p variables. | |
| * | |
| * @param p Pexact struct. | |
| * @param combi Combinational array. | |
| * @param xp Iteration variable of p variables. | |
| * |
pexact.c
Outdated
| * @param pPars Input information from executed abc command. | ||
| * @param verbose Verbosity level (0: none, 1: time info, 2: detailed info). |
There was a problem hiding this comment.
The verbose parameter doesn't seem to exist.
pexact.c
Outdated
| * @details Running exact synthesis. Calculating logic network with least amount of gates. | ||
| * Iterating over gate count r. For each r checking if a solution exists. First solution | ||
| * corresponds to minimum sized logic network. Adds p variable constraints and cardinality constraints to identyfy | ||
| * switching activity optimal solution. |
There was a problem hiding this comment.
| * @details Running exact synthesis. Calculating logic network with least amount of gates. | |
| * Iterating over gate count r. For each r checking if a solution exists. First solution | |
| * corresponds to minimum sized logic network. Adds p variable constraints and cardinality constraints to identyfy | |
| * switching activity optimal solution. | |
| * @details Running exact synthesis. Calculating a logic network with the least amount of gates. | |
| * Iterating over gate count r. For each r, check if a solution exists. First solution | |
| * corresponds to a minimum-sized logic network. Adds p variable constraints and cardinality constraints to identify | |
| * switching activity optimal solution. |
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Fix all issues with AI agents
In `@pexact.c`:
- Around line 269-272: Define a portable MAYBE_UNUSED macro that detects support
for the C23 maybe_unused attribute (using __has_c_attribute when available) and
falls back to empty otherwise, then replace the C23-only attribute on the
PexaManPrintSolutionTruthTable parameter by changing the signature to use
MAYBE_UNUSED on the bdd parameter; specifically add the macro definition near
other portability macros and update the function declaration for
PexaManPrintSolutionTruthTable to use MAYBE_UNUSED instead of [[maybe_unused]]
to keep C11/C17 compatibility.
In `@pexact.h`:
- Around line 99-106: Typo in the documentation comment inside struct
CombList_t_: change the comment text that reads " aximum capacity of the list."
to "Maximum capacity of the list." so the comment for the field int len is
correct and spelled properly.
🧹 Nitpick comments (2)
pexact.c (2)
1016-1057: Consider removing or documenting the unused function.The documentation states this function is "Currently not in use" and is "Similar to PexaManEval". Consider either:
- Removing it if not needed
- Adding a TODO comment about when it will be integrated
This helps avoid code rot and clarifies intent for future maintainers.
1178-1241: LGTM with minor suggestion - Debug comments could be removed.The BDD inner encoding is correctly implemented. Lines 1207, 1213, 1222 contain commented-out debug statements that could be cleaned up for production code.
📜 Review details
Configuration used: defaults
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (2)
pexact.cpexact.h
🧰 Additional context used
🧠 Learnings (2)
📓 Common learnings
Learnt from: FeldmeierMichael
Repo: cda-tum/ext-pexact PR: 11
File: pexact.c:1181-1277
Timestamp: 2025-12-30T08:48:02.423Z
Learning: The power synthesis variant `PexaManExactPowerSynthesisBasePower` in pexact.c restricts nVars to the range 2..5 (CONST_FIVE), while the base exact synthesis function `PowerExactSynthesisBase` allows nVars up to 10 (CONST_TEN).
📚 Learning: 2025-12-30T08:48:02.423Z
Learnt from: FeldmeierMichael
Repo: cda-tum/ext-pexact PR: 11
File: pexact.c:1181-1277
Timestamp: 2025-12-30T08:48:02.423Z
Learning: The power synthesis variant `PexaManExactPowerSynthesisBasePower` in pexact.c restricts nVars to the range 2..5 (CONST_FIVE), while the base exact synthesis function `PowerExactSynthesisBase` allows nVars up to 10 (CONST_TEN).
Applied to files:
pexact.cpexact.h
🧬 Code graph analysis (1)
pexact.h (1)
pexact.c (2)
PowerExactSynthesisBase(827-895)PexaManExactPowerSynthesisBasePower(2050-2148)
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (3)
- GitHub Check: Agent
- GitHub Check: ABC Integration (macos-latest)
- GitHub Check: ABC Integration (ubuntu-latest)
🔇 Additional comments (14)
pexact.h (3)
20-35: LGTM - Constants look good.The
PEXACT_LLONG_MAXconstant properly addresses the previousINT_MAXcollision issue with the standard library. The new numeric constants are well-organized.
38-74: LGTM - PexaMan_t structure updates are well documented.The new fields
iPVariableStartandiVarMintermBaseare appropriately added to support the BDD-based P-variable encoding. The inline documentation style is consistent throughout.
108-109: LGTM - Function prototypes are correctly declared.Both entry points are properly declared, with
PexaManExactPowerSynthesisBasePowersupporting the new power-aware synthesis flow.pexact.c (11)
910-966: LGTM - Memory handling and sorted insertion are correctly implemented.The function properly:
- Validates combination length before allocation
- Checks malloc return values
- Initializes
node->nextto NULL- Handles sorted insertion with proper list manipulation
979-995: LGTM - Use-after-free issue addressed.The function correctly sets
list->start = NULLwhen popping the last element, preventing the previously identified use-after-free vulnerability.
1003-1015: LGTM - NULL check added as requested.The defensive NULL check after
PopCombprevents potential crashes if list state becomes inconsistent.
1082-1115: LGTM - Well-documented utility functions.The
@exampleblock inConvertBaseIntprovides excellent documentation showing the function's behavior for enumeration purposes.
1131-1163: LGTM - Standard MUX encoding implementation.The four clauses correctly encode the multiplexer constraint with proper polarity handling.
1346-1361: LGTM - Loop bounds are feasible for restricted nVars.With nVars restricted to ≤5 for
PexaManExactPowerSynthesisBasePower, thepow(2, np-1)loop bound (max ~65K iterations) is practical. Based on learnings, this constraint is enforced at the entry point.
1462-1474: LGTM - Overflow check properly implemented.The bounds check using
PEXACT_LLONG_MAXaddresses the previously identified integer overflow concern for combination enumeration.
1683-1719: LGTM - Previously identified issues addressed.The function correctly:
- Updates
p->iVar += litsizeto reserve SAT variables- Uses
piinstead ofpto avoid variable shadowing- Has proper bounds checking for
pTarget
2012-2037: LGTM - Error handling properly implemented.The function correctly propagates errors from all encoding steps, addressing the previously identified incomplete error handling concern.
2050-2102: LGTM - Memory handling and input validation are correct.The function properly:
- Validates nVars range (2..5)
- Checks malloc return for list
- Initializes
list->start = NULL- Handles cleanup on all error paths
2104-2148: LGTM - Main synthesis loop is well-structured.The loop correctly handles:
- Gate count progression via
actandr- Combination popping and processing
- Memory cleanup for both success and failure paths
- SAT solver invocation and result handling
The loop termination is guaranteed by the
r >= maxGateCountcheck, and the boundednVarsconstraint keeps the search space practical.
✏️ Tip: You can disable this entire section by setting review_details to false in your review settings.
pexact.c
Outdated
| * @param bdd Parameter indicating if BDD p variable encoding is used. | ||
| */ | ||
| static void PexaManPrintSolutionTruthTable( PexaMan_t * p, int fCompl ) | ||
| static void PexaManPrintSolutionTruthTable( PexaMan_t * p, int fCompl, [[maybe_unused]] bool bdd ) | ||
| { |
There was a problem hiding this comment.
🧩 Analysis chain
🌐 Web query:
[[maybe_unused]] C standard C11 C17 C23 compatibility
💡 Result:
Short answer
- [[maybe_unused]] is part of the C-style attribute specifiers newly standardized in C23 — it is not in C11 or C17. [1][2][3]
Compatibility notes and practical guidance
- Before C23 use compiler-specific forms: GCC/Clang/ICC support attribute((unused)) (and many accept [[maybe_unused]] as an extension). [2]
- To write portable headers, detect support with __has_c_attribute(maybe_unused) or feature-test macros and fall back to an empty definition:
#if!defined(__has_c_attribute)define __has_c_attribute(x) 0
#endif
#if__has_c_attribute(maybe_unused)define MAYBE_UNUSED [[maybe_unused]]
#elsedefine MAYBE_UNUSED /empty/
#endif
Use MAYBE_UNUSED on parameters/variables. [1][4]
References
- C23 / attributes (cppreference). [1]
- GCC/Clang notes about unused attributes and behavior. [2]
- C23 overview / attribute additions (Wikipedia). [3]
- Practical portability example / blog (scivision). [4]
🏁 Script executed:
# Check the pexact.c file around the flagged lines and for compiler flags
head -n 280 pexact.c | tail -n 20Repository: cda-tum/ext-pexact
Length of output: 703
🏁 Script executed:
# Look for any macro definitions or compiler flag handling in the project
find . -type f \( -name "*.h" -o -name "*.c" \) -print0 | xargs -0 grep -l "maybe_unused\|__attribute__\|pragma" | head -20Repository: cda-tum/ext-pexact
Length of output: 72
🏁 Script executed:
# Find build configuration files
find . -type f \( -name "CMakeLists.txt" -o -name "Makefile*" -o -name "*.mk" -o -name "configure*" \) | head -20Repository: cda-tum/ext-pexact
Length of output: 44
🏁 Script executed:
# Check for any header files that might define macros or handle attributes
find . -type f -name "*.h" | head -20Repository: cda-tum/ext-pexact
Length of output: 72
🏁 Script executed:
# Look for any C standard settings or flags
git ls-files | xargs grep -l "std=c\|C11\|C17\|C23" | head -20Repository: cda-tum/ext-pexact
Length of output: 97
🏁 Script executed:
# Check pexact.h for macro definitions and how it handles compatibility
[ -f pexact.h ] && cat pexact.h | head -100Repository: cda-tum/ext-pexact
Length of output: 2346
🏁 Script executed:
# Check full pexact.h file
wc -l pexact.h && cat pexact.hRepository: cda-tum/ext-pexact
Length of output: 2610
🏁 Script executed:
# Search for build config files recursively (may be in subdirectories)
find . -type f \( -name "CMakeLists.txt" -o -name "configure.ac" -o -name "setup.py" \) 2>/dev/nullRepository: cda-tum/ext-pexact
Length of output: 44
🏁 Script executed:
# Check if there's a parent directory or git info that indicates C standard
git log --oneline -1 2>/dev/null || echo "Not a git repo or no commits"Repository: cda-tum/ext-pexact
Length of output: 160
🏁 Script executed:
# Look at the actual location and structure
ls -la | head -20Repository: cda-tum/ext-pexact
Length of output: 1050
🏁 Script executed:
# Check README for any build or integration information
cat README.mdRepository: cda-tum/ext-pexact
Length of output: 3625
🏁 Script executed:
# Look for any parent project or CI/build information
cat .github/workflows/*.yml 2>/dev/null || echo "No workflows found"Repository: cda-tum/ext-pexact
Length of output: 3251
🏁 Script executed:
# Check if there are any compiler flags in the git history or comments
grep -r "std=c\|CFLAGS\|CXXFLAGS" . --include="*.mk" --include="*.c" --include="*.h" 2>/dev/null | head -10Repository: cda-tum/ext-pexact
Length of output: 44
Replace [[maybe_unused]] with a portable compatibility macro.
The [[maybe_unused]] attribute is C23-only and not available in C11/C17. The project's clang-tidy configuration explicitly targets C11 best practices. While GCC and Clang may accept this as an extension, it is not portable. Define a macro to support both C23 and earlier standards:
`#if` !defined(__has_c_attribute)
# define __has_c_attribute(x) 0
`#endif`
`#if` __has_c_attribute(maybe_unused)
# define MAYBE_UNUSED [[maybe_unused]]
`#else`
# define MAYBE_UNUSED
`#endif`Then use MAYBE_UNUSED instead of [[maybe_unused]] on the bdd parameter at line 269.
🤖 Prompt for AI Agents
In `@pexact.c` around lines 269 - 272, Define a portable MAYBE_UNUSED macro that
detects support for the C23 maybe_unused attribute (using __has_c_attribute when
available) and falls back to empty otherwise, then replace the C23-only
attribute on the PexaManPrintSolutionTruthTable parameter by changing the
signature to use MAYBE_UNUSED on the bdd parameter; specifically add the macro
definition near other portability macros and update the function declaration for
PexaManPrintSolutionTruthTable to use MAYBE_UNUSED instead of [[maybe_unused]]
to keep C11/C17 compatibility.
There was a problem hiding this comment.
changed back
There was a problem hiding this comment.
@FeldmeierMichael, understood! I've noted that you're keeping the [[maybe_unused]] attribute as is. If you encounter any compatibility issues with older C standards in the future, feel free to revisit this approach.
🧠 Learnings used
Learnt from: FeldmeierMichael
Repo: cda-tum/ext-pexact PR: 11
File: pexact.c:1181-1277
Timestamp: 2025-12-30T08:48:02.423Z
Learning: The power synthesis variant `PexaManExactPowerSynthesisBasePower` in pexact.c restricts nVars to the range 2..5 (CONST_FIVE), while the base exact synthesis function `PowerExactSynthesisBase` allows nVars up to 10 (CONST_TEN).
| struct CombList_t_ { | ||
| /// Pointer to the first combination element in the list. | ||
| Comb_t * start; | ||
| /// aximum capacity of the list. | ||
| int len; | ||
| /// Current length of the list. | ||
| int length; | ||
| }; |
There was a problem hiding this comment.
Minor typo in documentation.
Line 102: " aximum" should be "Maximum".
🔧 Suggested fix
struct CombList_t_ {
/// Pointer to the first combination element in the list.
Comb_t * start;
- /// aximum capacity of the list.
+ /// Maximum capacity of the list.
int len;
/// Current length of the list.
int length;
};📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| struct CombList_t_ { | |
| /// Pointer to the first combination element in the list. | |
| Comb_t * start; | |
| /// aximum capacity of the list. | |
| int len; | |
| /// Current length of the list. | |
| int length; | |
| }; | |
| struct CombList_t_ { | |
| /// Pointer to the first combination element in the list. | |
| Comb_t * start; | |
| /// Maximum capacity of the list. | |
| int len; | |
| /// Current length of the list. | |
| int length; | |
| }; |
🤖 Prompt for AI Agents
In `@pexact.h` around lines 99 - 106, Typo in the documentation comment inside
struct CombList_t_: change the comment text that reads " aximum capacity of the
list." to "Maximum capacity of the list." so the comment for the field int len
is correct and spelled properly.
|
@FeldmeierMichael, please mark addressed AI feedback as resolved. Often, CodeRabbit will automatically detect resolved issues and close them automatically. GitHub Copilot doesn't do that yet. Either way, if they are not addressed and left open, please resolve them before requesting another review. Thanks! |
marcelwa
left a comment
marcelwa
left a comment
There was a problem hiding this comment.
Thank you for addressing the feedback so promptly. Here are a few more minor comments. Also, please review the const-correctness of your function parameters. If a value isn't altered by a function, that parameter should be const. This gives the compiler more optimization potential and avoids unintentional mistakes.
pexact.c
Outdated
| * @param results Result array. | ||
| * @param results Pointer to result Combination array. | ||
| * | ||
| * @return Returns value as integer pointer to result Combination array. |
There was a problem hiding this comment.
This function doesn't return anything (void). It should not have a @return docstring. Instead, document how results is altered by this function.
pexact.c
Outdated
| * | ||
| * @return Returns value as integer pointer to result Combination array. | ||
| */ | ||
| void ConvertBaseInt( int base, int value, int size, int * results ) |
There was a problem hiding this comment.
Couldnt baseandsizebeconst`?
pexact.c
Outdated
| * @return Returns value as integer pointer to result Combination array. | ||
| */ | ||
| void ConvertBaseIntLong( int base, long long value, int size, int * results ) |
pexact.c
Outdated
| if ( !ExactPowerSynthesisCNF( pPars, p, node, list ) ) | ||
| { | ||
| printf( "Warning: CNF encoding failed for combination act=%d r=%d.\n", node->act, node->r ); | ||
| printf( "Warning: CNF encoding failed for Combination act=%d r=%d.\n", node->act, node->r ); |
There was a problem hiding this comment.
Maybe changing the capitalization of "combination" here was a search-and-replace mistake?
pexact.c
Outdated
| * | ||
| * @details Determines, based on a solution from SAT solver, if the resulting truth-table matches with the specified one. Needed for CEGAR optimization approach. | ||
| * Returns first mismatching minterm. | ||
| * Returns first mismatching minterm. Currently not in Use. |
There was a problem hiding this comment.
The "Currently not in use." comment should rather go with the @param bdd docstring, no?
There was a problem hiding this comment.
I don't understand this comment. Function PexaManEval has not bdd parameter.
There was a problem hiding this comment.
Sorry, I was confusing it with the function below. Here, I don't understand what is currently not in use. The entire function or just the return value?
There was a problem hiding this comment.
The entire function
pexact.c
Outdated
| * | ||
| * @details Evaluating P variable values. Iteres over solution from solver and evaluates which p-variables are matching to cardinallity constraining. | ||
| * Might be used for CEGAR approach. Currently not in use. Similar to PexaManEval. | ||
| * Might be used for CEGAR approach. Currently not in use. Similar to PexaManEval. Currently not in Use. |
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Fix all issues with AI agents
In `@pexact.c`:
- Around line 2056-2061: The allocation return from PexaManAlloc stored in p
must be NULL-checked before dereferencing p->nWords or calling Abc_TtNot; update
the code after PexaManAlloc(pPars, pTruth) to test if (p == NULL) and handle the
error/early return consistent with the existing reallocation check later (see
the check around PexaManRealloc), then only proceed to set fCompl and call
Abc_TtNot(pTruth, p->nWords) when p is non-NULL.
🧹 Nitpick comments (2)
pexact.c (2)
1536-1557: Consider renaming loop variable to avoid shadowing.The loop variable
lat line 1551 shadows the cardinality variableldeclared at line 1536. While the outerlis only used up to line 1538, having the same name is confusing.The same shadowing pattern appears in
PexaManAddCardinalityUpper(lines 1587/1602) and the BDD cardinality variants.♻️ Suggested fix
- int l = *( combi + pi ); + int cardBound = *( combi + pi ); // less then l - int j = l + 1; + int j = cardBound + 1; for ( int i = 0; i < pow( 2, ni ); i++ ) { ... }
2074-2096: Loop termination is guaranteed, but prior feedback on activity bound optimization remains open.The loop correctly terminates:
rincrements from 0 toward the finitemaxGateCount, andactincrements by 1 each iteration until it reachesCalcMaxAct(r+1, nVars). The CalcMaxAct formula for k=4 is(r-2)*30 + 152, which grows linearly withr, requiring many iterations to trigger eachrincrement. Prior feedback suggested adding a maximum activity bound to enable early exit when exhausting all possibilities—this optimization remains unimplemented and should be evaluated if performance is a concern.
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Fix all issues with AI agents
In `@pexact.c`:
- Around line 834-837: The range check on pPars->nVars currently limits
variables to 2..CONST_FOUR (2..4) which tightens earlier behavior; verify
whether the new limit is intentional and, if not, restore the original upper
bounds by adjusting the guard(s): either expand the check to the previously
supported maxima (e.g., 10 for PowerExactSynthesisBase and 5 for
PexaManExactPowerSynthesisBasePower) or implement separate range checks per
entry point (use distinct conditions around PowerExactSynthesisBase and
PexaManExactPowerSynthesisBasePower instead of a single 2..CONST_FOUR check),
keeping the printf error message in sync with the chosen limits and referencing
pPars->nVars and CONST_FOUR (or new constants) so the code enforces the correct
allowed ranges.
🧹 Nitpick comments (1)
pexact.c (1)
2043-2141: Consider extracting the main loop into helpers to reduce complexity.This function is starting to carry multiple responsibilities (list management, allocation, CNF build, solve). Pulling these into small helpers would improve readability and testability.
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Fix all issues with AI agents
In `@pexact.c`:
- Around line 2112-2149: The trailing "act++" is unreachable because every path
in the combination-processing block starting at PopComb(list) ends with either
continue or return; remove the dead statement to clean up the function. Locate
the block that calls PopComb(list) and handles PexaManAlloc/PexaManFree,
ExactPowerSynthesisCNF, sat_solver_solve, PexaManPrintSolution and then delete
the standalone "act++" after that block so control flow relies on the existing
increment at the earlier location (referenced as act and the combination loop
surrounding PopComb).
🧹 Nitpick comments (1)
pexact.c (1)
12-19: Use angle brackets for standard library headers.Standard library headers should be included with angle brackets instead of quotes.
🔧 Suggested fix
-#include "math.h" +#include <math.h> `#include` "misc/extra/extra.h" `#include` "misc/util/utilTruth.h" `#include` "sat/bmc/bmc.h" `#include` "sat/bsat/satStore.h" `#include` "sat/cnf/cnf.h" -#include "stdbool.h" -#include "stdio.h" +#include <stdbool.h> +#include <stdio.h>
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Fix all issues with AI agents
In `@pexact.c`:
- Around line 1679-1713: AddPClausesInner incorrectly reserves litsize variables
per gate causing a stride mismatch with the sum-one constraints which stride by
np; change the allocation so p->iVar is incremented by np (not litsize) and call
sat_solver_setnvars( p->pSat, p->iVar ) after that reservation, and ensure
pListP filling and any indexing that assumes the per-gate block size (in
AddPClausesInner and referenced AddPClausesSumOne* code paths) use np
consistently instead of litsize so subsequent gates reference the correct
variable block.
| bool AddPClausesInner( PexaMan_t * p, const int i ) | ||
| { | ||
| int pStartvar = p->iVar; | ||
| int xiBase = ( p->nNodes * ( ( 2 * p->nVars ) + p->nNodes - 1 ) ) - p->nNodes + ( CONST_THREE * p->nNodes ); | ||
| int litsize = pow( 2, p->nVars ); | ||
| int nCombs = pow( 2, pow( 2, p->nVars ) - 1 ); | ||
| int pList[litsize]; | ||
| int pListP[litsize]; | ||
| int xIt = 0; | ||
| int pTarget = 0; | ||
| p->iVar += litsize; // Reserve SAT variables for this gate | ||
| sat_solver_setnvars( p->pSat, p->iVar ); | ||
| for ( int pi = 0; pi < litsize; pi++ ) | ||
| { | ||
| pListP[pi] = Abc_Var2Lit( pStartvar++, 0 ); | ||
| } | ||
|
|
||
| for ( int m = 1; m < nCombs; m++ ) | ||
| { | ||
| for ( int t = 1; t < pow( 2, p->nVars ) && t <= litsize; t++ ) | ||
| { | ||
| xIt = xiBase + ( CONST_THREE * ( i - p->nVars ) ) + ( ( t - 1 ) * ( CONST_THREE * p->nNodes ) ); | ||
| pList[t - 1] = Abc_Var2Lit( xIt, ValueNthBit( m, t - 1 ) ); | ||
| } | ||
| pTarget = CountOne( m, litsize - 1 ) - 1; | ||
| if ( pTarget < 0 || pTarget > ( litsize - 1 ) ) | ||
| { | ||
| return 0; | ||
| } | ||
| pList[litsize - 1] = pListP[pTarget]; | ||
| if ( !sat_solver_addclause( p->pSat, pList, pList + litsize ) ) | ||
| { | ||
| return 0; | ||
| } | ||
| } |
There was a problem hiding this comment.
Fix stride mismatch between naive P-variable allocation and sum-one constraints.
AddPClausesInner reserves litsize variables per gate (Line 1689), but AddPClausesSumOne* strides by np, so gates beyond the first can reference the wrong variable block. Align the allocation/stride to np (since only 0..np-1 indices are used via CountOne), or update the sum-one offsets to litsize.
🔧 Proposed fix (align allocation to np)
bool AddPClausesInner( PexaMan_t * p, const int i )
{
int pStartvar = p->iVar;
int xiBase = ( p->nNodes * ( ( 2 * p->nVars ) + p->nNodes - 1 ) ) - p->nNodes + ( CONST_THREE * p->nNodes );
int litsize = pow( 2, p->nVars );
+ int np = pow( 2, p->nVars - 1 );
int nCombs = pow( 2, pow( 2, p->nVars ) - 1 );
int pList[litsize];
- int pListP[litsize];
+ int pListP[np];
int xIt = 0;
int pTarget = 0;
- p->iVar += litsize; // Reserve SAT variables for this gate
+ p->iVar += np; // Reserve SAT variables for this gate
sat_solver_setnvars( p->pSat, p->iVar );
- for ( int pi = 0; pi < litsize; pi++ )
+ for ( int pi = 0; pi < np; pi++ )
{
pListP[pi] = Abc_Var2Lit( pStartvar++, 0 );
}
@@
pTarget = CountOne( m, litsize - 1 ) - 1;
- if ( pTarget < 0 || pTarget > ( litsize - 1 ) )
+ if ( pTarget < 0 || pTarget >= np )
{
return 0;
}
pList[litsize - 1] = pListP[pTarget];Also applies to: 1729-1804
🤖 Prompt for AI Agents
In `@pexact.c` around lines 1679 - 1713, AddPClausesInner incorrectly reserves
litsize variables per gate causing a stride mismatch with the sum-one
constraints which stride by np; change the allocation so p->iVar is incremented
by np (not litsize) and call sat_solver_setnvars( p->pSat, p->iVar ) after that
reservation, and ensure pListP filling and any indexing that assumes the
per-gate block size (in AddPClausesInner and referenced AddPClausesSumOne* code
paths) use np consistently instead of litsize so subsequent gates reference the
correct variable block.
Added Power Exact Synthesis.
P-Variable Constraints naive and BDD Encoding.
Polynomial Cardinality Constraints.
Summary by CodeRabbit
New Features
Refactor
Other
✏️ Tip: You can customize this high-level summary in your review settings.