From 5100825c51086fe3a7af76d65e20979677f2374f Mon Sep 17 00:00:00 2001 From: Petter Reinholdtsen Date: Tue, 5 May 2026 13:04:37 +0200 Subject: [PATCH 1/4] Only use __int128 on architectures where it is present. With GCC and Clang, look for the __SIZEOF_INT128__ define only defined when __int128 is present before trying to use it. This fixes build problem on all 32 bit Linux architectures. --- src/misc/util/utilAigSim.c | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/src/misc/util/utilAigSim.c b/src/misc/util/utilAigSim.c index 4d89b615f..a86753aa2 100644 --- a/src/misc/util/utilAigSim.c +++ b/src/misc/util/utilAigSim.c @@ -34,6 +34,11 @@ #include #endif +// defined by gcc and clang when __int128 is available +#if defined(__SIZEOF_INT128__) +# define HAVE_INT_128 +#endif + #ifdef _WIN32 // Windows doesn't have __builtin_ctzll, implement it using portable algorithm static inline int __builtin_ctzll(uint64_t x) { @@ -187,8 +192,9 @@ static inline uint64_t u64_mask_n(int nBits) { return (nBits >= 64) ? ~0ull : ((nBits <= 0) ? 0ull : ((1ull << nBits) - 1ull)); } -#ifdef _WIN32 -// Windows doesn't support __int128, so we limit to 32 variables on Windows +#ifndef HAVE_INT_128 +// Most 32 bit platforms and Windows doesn't support __int128, so we +// limit to 32 variables on those. static void u128_to_dec(uint64_t x, char *buf, size_t cap) { char tmp[64]; int n = 0; if (!x) { snprintf(buf, cap, "0"); return; } @@ -397,10 +403,10 @@ static int SimulateCompareAigAig(const AigMan *p1, const AigMan *p2, const uint64_t inMask = u64_mask_n(p1->nCis); const uint64_t outMask = u64_mask_n(p1->nCos); -#ifdef _WIN32 - // Windows doesn't support __int128, limit to 32 variables +#ifndef HAVE_INT_128 + // No support for __int128, limit to 32 variables if (nVars > 32) { - fprintf(stderr, "Error: Windows build supports nVars<=32 (got nVars=%d)\n", nVars); + fprintf(stderr, "Error: This architecture build supports nVars<=32 (got nVars=%d)\n", nVars); return 0; } const uint64_t combs = ((uint64_t)1) << (unsigned)nVars; @@ -420,7 +426,7 @@ static int SimulateCompareAigAig(const AigMan *p1, const AigMan *p2, uint64_t inVec[BATCH], valid[NW]; unsigned long long rounds = 0; -#ifdef _WIN32 +#ifndef HAVE_INT_128 uint64_t patsDone = 0; #else unsigned __int128 patsDone = 0; @@ -428,7 +434,7 @@ static int SimulateCompareAigAig(const AigMan *p1, const AigMan *p2, clock_t t0 = clock(); -#ifdef _WIN32 +#ifndef HAVE_INT_128 for (uint64_t base = 0; base < combs; base += BATCH) { uint64_t remain = combs - base; #else @@ -535,10 +541,10 @@ static int SimulateCompareAigBin(const AigMan *p1, const char *bin, const uint64_t inMask = u64_mask_n(p1->nCis); const uint64_t outMask = u64_mask_n(p1->nCos); -#ifdef _WIN32 - // Windows doesn't support __int128, limit to 32 variables +#ifndef HAVE_INT_128 + // No support for __int128, limit to 32 variables if (nVars > 32) { - fprintf(stderr, "Error: Windows build supports nVars<=32 (got nVars=%d)\n", nVars); + fprintf(stderr, "Error: This architecture build supports nVars<=32 (got nVars=%d)\n", nVars); return 0; } const uint64_t combs = ((uint64_t)1) << (unsigned)nVars; @@ -565,7 +571,7 @@ static int SimulateCompareAigBin(const AigMan *p1, const char *bin, uint64_t inVec[BATCH], valid[NW]; unsigned long long rounds = 0; -#ifdef _WIN32 +#ifndef HAVE_INT_128 uint64_t patsDone = 0; #else unsigned __int128 patsDone = 0; @@ -573,7 +579,7 @@ static int SimulateCompareAigBin(const AigMan *p1, const char *bin, clock_t t0 = clock(); -#ifdef _WIN32 +#ifndef HAVE_INT_128 for (uint64_t base = 0; base < combs; base += BATCH) { uint64_t remain = combs - base; #else From 0e328193259ad4ed799e4fa6ebc8f537d5552d8f Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 9 Mar 2026 13:02:54 +0100 Subject: [PATCH 2/4] Fix WASI and make prototype valid --- src/base/abci/abc.c | 7 +++---- src/opt/untk/NtkNtk.cpp | 4 ++++ 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 8d95d60b4..3b14c940e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -18,6 +18,7 @@ ***********************************************************************/ +#include #include "base/abc/abc.h" #include "base/main/main.h" #include "base/main/mainInt.h" @@ -61438,7 +61439,7 @@ int Abc_CommandAbc9elSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) { } int Abc_CommandAbc9CatBtor( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Abc_BtorCat( char * pFileName, int fVerbose ); + extern int32_t Abc_BtorCat( char * pFileName, int fVerbose ); int c, fVerbose = 0; char * pFileName; @@ -61461,9 +61462,7 @@ int Abc_CommandAbc9CatBtor( Abc_Frame_t * pAbc, int argc, char ** argv ) { return 0; } - Abc_BtorCat( pFileName, fVerbose ); - - return 0; + return Abc_BtorCat( pFileName, fVerbose ); usage: Abc_Print( -2, "usage: &catbtor [-v] \n" ); diff --git a/src/opt/untk/NtkNtk.cpp b/src/opt/untk/NtkNtk.cpp index 2e6782731..6fc3700b3 100755 --- a/src/opt/untk/NtkNtk.cpp +++ b/src/opt/untk/NtkNtk.cpp @@ -1281,7 +1281,11 @@ static inline int run_external_solver_on_aig( Abc_Ntk_t * pAbcNtk, const string& command = "timeout " + to_string(nRuntimeLimitSec) + " " + command; command += " > log.txt 2>&1"; LOG(1) << "UFAR external solver: launching command instead of PDR: " << command; +#ifdef __wasm + int res = -1; +#else int res = system( command.c_str() ); +#endif std::remove( pAigFile ); return res; } From b89ccd36bce5e5a0f67ed2e345f0a982e3c569fb Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Thu, 25 Jun 2026 13:24:00 +0200 Subject: [PATCH 3/4] Fix for case where ABC_USE_PTHREADS is not used --- src/proof/cec/cecProve.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c index f9a6de09b..94eafa479 100644 --- a/src/proof/cec/cecProve.c +++ b/src/proof/cec/cecProve.c @@ -61,8 +61,10 @@ struct Cec_SproveTrace_t_; static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result ); static Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut ); static Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut ); +#ifdef ABC_USE_PTHREADS static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, const char * pUfarArgs, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, struct Cec_SproveTrace_t_ * pTrace ); static void Cec_GiaStopThreads( Par_ThData_t * ThData, pthread_t * WorkerThread, int nWorkers ); +#endif static int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine ); extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs ); From 9794114a6814424c8eec227e9634d705bdc1972d Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Thu, 25 Jun 2026 14:15:03 +0200 Subject: [PATCH 4/4] Change to ABC_NO_HISTORY so it is possible to change externally --- src/base/cmd/cmdHist.c | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/src/base/cmd/cmdHist.c b/src/base/cmd/cmdHist.c index 0edd8a686..759e7ff36 100644 --- a/src/base/cmd/cmdHist.c +++ b/src/base/cmd/cmdHist.c @@ -26,12 +26,6 @@ ABC_NAMESPACE_IMPL_START -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -#define ABC_USE_HISTORY 1 - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -102,7 +96,7 @@ void Cmd_HistoryAddCommand( Abc_Frame_t * p, const char * command ) ***********************************************************************/ void Cmd_HistoryRead( Abc_Frame_t * p ) { -#if defined(ABC_USE_HISTORY) +#if !defined(ABC_NO_HISTORY) char Buffer[ABC_MAX_STR]; FILE * pFile; assert( Vec_PtrSize(p->aHistory) == 0 ); @@ -134,7 +128,7 @@ void Cmd_HistoryRead( Abc_Frame_t * p ) ***********************************************************************/ void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit ) { -#if defined(ABC_USE_HISTORY) +#if !defined(ABC_NO_HISTORY) FILE * pFile; char * pStr; int i; @@ -186,7 +180,7 @@ void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit ) ***********************************************************************/ void Cmd_HistoryPrint( Abc_Frame_t * p, int Limit ) { -#if defined(ABC_USE_HISTORY) +#if !defined(ABC_NO_HISTORY) char * pStr; int i; Limit = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory)-Limit );