From 5262c16d699e76d4bb9440e6f93cbe85595bcf30 Mon Sep 17 00:00:00 2001 From: Stephen L Arnold Date: Fri, 7 Mar 2025 17:16:57 -0800 Subject: [PATCH] fix: dev: prep msvc cl and github environment for conda on windows * disable pthreads when using msvc compiler * fix build errors on windows, including the following: missing symbols, non-const, designated initializers, and non-standard explicit type conversions * uncork sys/stat.h and add missing win32 define for S_ISDIR * add clang++ flag to get errors on c++20 initializers and set C99 std Signed-off-by: Stephen L Arnold --- .github/workflows/conda-dev.yml | 31 +++++++++++++++++++++++++++++-- CMakeLists.txt | 7 +++++++ Makefile | 1 + src/base/abc/abcHieNew.c | 2 +- src/sat/kissat/bump.c | 2 +- src/sat/kissat/colors.c | 1 + src/sat/kissat/congruence.c | 18 +++++++++--------- src/sat/kissat/dense.c | 2 +- src/sat/kissat/file.c | 7 ++++++- src/sat/kissat/kitten.c | 6 +++--- src/sat/kissat/proplit.h | 2 +- src/sat/kissat/sweep.c | 8 ++++---- src/sat/kissat/walk.c | 2 +- src/sat/kissat/watch.c | 4 ++-- 14 files changed, 67 insertions(+), 26 deletions(-) diff --git a/.github/workflows/conda-dev.yml b/.github/workflows/conda-dev.yml index 92600166fb..f7523a1a59 100644 --- a/.github/workflows/conda-dev.yml +++ b/.github/workflows/conda-dev.yml @@ -34,7 +34,7 @@ jobs: - os: 'windows-2019' generator: 'Ninja' build_type: 'Debug' - extra_args: '-DBUILD_SHARED_LIBS=OFF -DABC_USE_NO_READLINE=ON -DVENDOR_GTEST=ON' + extra_args: '-DBUILD_SHARED_LIBS=OFF -DABC_USE_NO_PTHREADS=ON -DABC_USE_NO_READLINE=ON -DVENDOR_GTEST=ON' env: OS: ${{ matrix.os }} PY_VER: ${{ matrix.python-version }} @@ -42,6 +42,21 @@ jobs: CMAKE_ARGS: ${{ matrix.use_namespace && '-DABC_USE_NAMESPACE=xxx' || '' }} steps: + #- if: matrix.os == 'windows-2019' + #name: Install newer windows compiler + #id: install_cc + #uses: rlalik/setup-cpp-compiler@master + #with: + #compiler: g++-11.2.0 + + #- if: matrix.os == 'windows-2019' + #name: Use compiler + #shell: bash -l {0} + #env: + #CC: ${{ steps.install_cc.outputs.cc }} + #CXX: ${{ steps.install_cc.outputs.cxx }} + #run: | + - uses: actions/checkout@v4 - name: Setup base python @@ -49,12 +64,24 @@ jobs: with: python-version: ${{ matrix.python-version }} + - name: Prepare build environment for windows + if: runner.os == 'Windows' + uses: ilammy/msvc-dev-cmd@v1 + with: + arch: x64 + + - name: Env (Windows) + if: runner.os == 'Windows' + run: | + echo "CXX=cl.exe" >> $GITHUB_ENV + echo "CC=cl.exe" >> $GITHUB_ENV + - name: Cache conda id: cache uses: actions/cache@v4 env: # Increase this value to reset cache if environment.devenv.yml has not changed - CACHE_NUMBER: 1 + CACHE_NUMBER: 2 with: path: ~/conda_pkgs_dir key: ${{ runner.os }}-conda-${{ env.CACHE_NUMBER }}-${{ hashFiles('environment.devenv.yml') }} diff --git a/CMakeLists.txt b/CMakeLists.txt index b5fc49ff21..49d4dd1708 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -28,6 +28,8 @@ set(CMAKE_CXX_STANDARD 17) set(CMAKE_CXX_STANDARD_REQUIRED ON) set(CMAKE_CXX_EXTENSIONS OFF) +set(CMAKE_C_STANDARD 99) + # MSVC has symbols hidden by default. On GCC and Clang we need to explicitly # set the visibility to hidden to achieve the same result and then manually # expose what we need. This results in smaller abc dynamic library and thus @@ -160,6 +162,10 @@ if(CMAKE_CXX_COMPILER_ID STREQUAL "GNU" AND NOT (CMAKE_CXX_COMPILER_VERSION VERS target_compile_options(abc_interface INTERFACE -fno-aggressive-loop-optimizations -Wno-unused-but-set-variable ) +elseif(CMAKE_CXX_COMPILER_ID STREQUAL "Clang" OR CMAKE_CXX_COMPILER_ID STREQUAL "AppleClang") + target_compile_options(abc_interface + INTERFACE -Werror=c99-designator + ) endif() if(CMAKE_CXX_COMPILER_ID STREQUAL "GNU" OR CMAKE_CXX_COMPILER_ID STREQUAL "Clang" OR CMAKE_CXX_COMPILER_ID STREQUAL "AppleClang") @@ -182,6 +188,7 @@ elseif(CMAKE_CXX_COMPILER_ID STREQUAL "MSVC") "_MBCS" "_SCL_SECURE_NO_WARNINGS" "_CRT_SECURE_NO_WARNINGS" + "_CRT_INTERNAL_NONSTDC_NAMES" "_XKEYCHECK_H" "_ALLOW_KEYWORD_MACROS=1" ) diff --git a/Makefile b/Makefile index 51957d7b06..467d555332 100644 --- a/Makefile +++ b/Makefile @@ -71,6 +71,7 @@ ifdef ABC_USE_NAMESPACE DLIBS := -lstdc++ $(info $(MSG_PREFIX)Compiling in namespace $(ABC_NAMESPACE)) else + CFLAGS += -std=gnu99 CXXFLAGS := $(CFLAGS) ABC_USE_LIBSTDCXX := 1 endif diff --git a/src/base/abc/abcHieNew.c b/src/base/abc/abcHieNew.c index 54a61609f8..5906bf476e 100644 --- a/src/base/abc/abcHieNew.c +++ b/src/base/abc/abcHieNew.c @@ -1488,7 +1488,7 @@ Gia_Man_t * Au_ManDeriveTest( Abc_Ntk_t * pRoot ) extern Vec_Ptr_t * Abc_NtkCollectHie( Abc_Ntk_t * pNtk ); // char * pModelName = NULL; - char * pModelName = "path_0_r_x_lhs"; + char pModelName[] = "path_0_r_x_lhs"; Gia_Man_t * pGia = NULL; Vec_Ptr_t * vOrder, * vModels; Abc_Ntk_t * pMod; diff --git a/src/sat/kissat/bump.c b/src/sat/kissat/bump.c index 5dc365f51b..efe3fa46b2 100644 --- a/src/sat/kissat/bump.c +++ b/src/sat/kissat/bump.c @@ -85,7 +85,7 @@ static void move_analyzed_variables_to_front_of_queue (kissat *solver) { const links *const links = solver->links; for (all_stack (unsigned, idx, solver->analyzed)) { // clang-format off - const datarank rank = { .data = idx, .rank = links[idx].stamp }; + const datarank rank = { /*.data = */idx, /*.rank = */links[idx].stamp }; // c++20 only // clang-format on PUSH_STACK (solver->ranks, rank); } diff --git a/src/sat/kissat/colors.c b/src/sat/kissat/colors.c index c6141b7491..7c41fba617 100644 --- a/src/sat/kissat/colors.c +++ b/src/sat/kissat/colors.c @@ -1,6 +1,7 @@ #include "colors.h" #if defined(WIN32) && !defined(__MINGW32__) +#include #define isatty _isatty #else #include diff --git a/src/sat/kissat/congruence.c b/src/sat/kissat/congruence.c index 221f6a13a0..f2a8565f8e 100644 --- a/src/sat/kissat/congruence.c +++ b/src/sat/kissat/congruence.c @@ -846,7 +846,7 @@ static void add_binary_clause (closure *closure, unsigned a, unsigned b) { kissat_new_binary_clause (solver, a, b); else { kissat_new_unwatched_binary_clause (solver, a, b); - litpair litpair = {.lits = {a < b ? a : b, a < b ? b : a}}; + litpair litpair = {/*.lits = */{a < b ? a : b, a < b ? b : a}}; // c++20 only PUSH_STACK (closure->binaries, litpair); } } @@ -2500,7 +2500,7 @@ static bool indexed_binary (closure *closure, unsigned lit, SWAP (unsigned, lit, other); if (lit > other) SWAP (unsigned, lit, other); - binary_clause binary = {.lits = {lit, other}}; + binary_clause binary = {/*.lits = */{lit, other}}; // c++20 only const unsigned hash = hash_binary (closure, &binary); const size_t size = bintab->size; const size_t size2 = bintab->size2; @@ -2986,7 +2986,7 @@ static void index_binary (closure *closure, unsigned lit, unsigned other) { KISSAT_assert (lit < other); binary_hash_table *bintab = &closure->bintab; KISSAT_assert (!binaries_hash_table_is_full (bintab)); - binary_clause binary = {.lits = {lit, other}}; + binary_clause binary = {/*.lits = */{lit, other}}; // c++20 only const unsigned hash = hash_binary (closure, &binary); const size_t size = bintab->size; const size_t size2 = bintab->size2; @@ -3416,10 +3416,10 @@ static void copy_conditional_equivalences (kissat *solver, unsigned lit, KISSAT_assert (second != INVALID_LIT); litpair pair; if (first < second) - pair = (litpair){.lits = {first, second}}; + pair = (struct litpair) { first, second }; // c++20 only else { KISSAT_assert (second < first); - pair = (litpair){.lits = {second, first}}; + pair = (struct litpair) { second, first }; // c++20 only } LOG ("literal %s conditional binary clause %s %s", LOGLIT (lit), LOGLIT (first), LOGLIT (second)); @@ -3491,13 +3491,13 @@ static void search_condeq (closure *closure, unsigned lit, unsigned pos_lit, KISSAT_assert (first < second); check_ternary (closure, lit, first, NOT (second)); check_ternary (closure, lit, NOT (first), second); - litpair equivalence = {.lits = {first, second}}; + litpair equivalence = {/*.lits = */{first, second}}; // c++20 only PUSH_STACK (*condeq, equivalence); if (NEGATED (second)) { - litpair inverse_equivalence = {.lits = {NOT (second), NOT (first)}}; + litpair inverse_equivalence = {/*.lits = */{NOT (second), NOT (first)}}; // c++20 only PUSH_STACK (*condeq, inverse_equivalence); } else { - litpair inverse_equivalence = {.lits = {second, first}}; + litpair inverse_equivalence = {/*.lits = */{second, first}}; // c++20 only PUSH_STACK (*condeq, inverse_equivalence); } } @@ -4549,7 +4549,7 @@ static void forward_subsume_matching_clauses (closure *closure) { } const reference ref = kissat_reference_clause (solver, c); KISSAT_assert (size <= UINT_MAX); - refsize refsize = {.ref = ref, .size = (unsigned)size}; + refsize refsize = {/*.ref = */ref, /*.size = */(unsigned)size}; // c++20 only PUSH_STACK (candidates, refsize); } DEALLOC (matchable, VARS); diff --git a/src/sat/kissat/dense.c b/src/sat/kissat/dense.c index 65c668cbcc..c5273e4807 100644 --- a/src/sat/kissat/dense.c +++ b/src/sat/kissat/dense.c @@ -60,7 +60,7 @@ static void flush_large_watches (kissat *solver, litpairs *irredundant) { if (irredundant) { const unsigned other = watch.binary.lit; if (lit < other) { - const litpair litpair = {.lits = {lit, other}}; + const litpair litpair = {/*.lits = */{lit, other}}; // c++20 only PUSH_STACK (*irredundant, litpair); } } else diff --git a/src/sat/kissat/file.c b/src/sat/kissat/file.c index e4486783d2..d9564e696e 100644 --- a/src/sat/kissat/file.c +++ b/src/sat/kissat/file.c @@ -5,14 +5,19 @@ #include #include #include -#include + #include +#include #ifdef WIN32 +#include #define unlink _unlink #define access _access #define R_OK 4 #define W_OK 2 +#ifndef S_ISDIR +# define S_ISDIR(mode) (((mode) & _S_IFMT) == _S_IFDIR) +#endif #else #include #endif diff --git a/src/sat/kissat/kitten.c b/src/sat/kissat/kitten.c index ea2e7f3607..9c08d73c6d 100644 --- a/src/sat/kissat/kitten.c +++ b/src/sat/kissat/kitten.c @@ -1892,7 +1892,7 @@ unsigned kitten_compute_clausal_core (kitten *kitten, if (reason_ref == INVALID) { LOG ("assumptions mutually inconsistent"); - + // goto DONE; if (learned_ptr) *learned_ptr = learned; @@ -1907,7 +1907,7 @@ unsigned kitten_compute_clausal_core (kitten *kitten, return original; - + } } @@ -2412,7 +2412,7 @@ static inline void print_lit (line *line, int lit) { static void print_witness (kitten *kitten, int max_var) { KISSAT_assert (max_var >= 0); - line line = {.size = 0}; + line line = {/*.size = */0}; // c++20 only const size_t parsed_lits = 2 * (size_t) max_var; for (size_t ulit = 0; ulit < parsed_lits; ulit += 2) { const value sign = kitten_value (kitten, ulit); diff --git a/src/sat/kissat/proplit.h b/src/sat/kissat/proplit.h index be0632d0cb..203c1eb398 100644 --- a/src/sat/kissat/proplit.h +++ b/src/sat/kissat/proplit.h @@ -8,7 +8,7 @@ static inline void kissat_watch_large_delayed (kissat *solver, while (d != end_delayed) { const unsigned lit = *d++; KISSAT_assert (d != end_delayed); - const watch watch = {.raw = *d++}; + const watch watch = {/*.raw =*/ *d++}; // c++20 only KISSAT_assert (!watch.type.binary); KISSAT_assert (lit < LITS); watches *const lit_watches = all_watches + lit; diff --git a/src/sat/kissat/sweep.c b/src/sat/kissat/sweep.c index 42420cc541..0e56669e5f 100644 --- a/src/sat/kissat/sweep.c +++ b/src/sat/kissat/sweep.c @@ -877,8 +877,8 @@ static void substitute_connected_clauses (sweeper *sweeper, unsigned lit, REMOVE_CHECKER_BINARY (lit, other); DELETE_BINARY_FROM_PROOF (lit, other); PUSH_STACK (*delayed, head.raw); - watch src = {.raw = head.raw}; - watch dst = {.raw = head.raw}; + watch src = {/*.raw = */head.raw}; // c++20 only + watch dst = {/*.raw = */head.raw}; // c++20 only src.binary.lit = lit; dst.binary.lit = repr; watches *other_watches = &WATCHES (other); @@ -970,7 +970,7 @@ static void substitute_connected_clauses (sweeper *sweeper, unsigned lit, LOGLIT (second)); KISSAT_assert (first == repr || second == repr); const unsigned other = first ^ second ^ repr; - const watch src = {.raw = head.raw}; + const watch src = {/*.raw = */head.raw}; // c++20 only watch dst = kissat_binary_watch (repr); watches *other_watches = &WATCHES (other); kissat_substitute_large_watch (solver, other_watches, src, dst); @@ -1029,7 +1029,7 @@ static void substitute_connected_clauses (sweeper *sweeper, unsigned lit, const unsigned *const begin_delayed = BEGIN_STACK (*delayed); const unsigned *const end_delayed = END_STACK (*delayed); for (const unsigned *p = begin_delayed; p != end_delayed; p++) { - const watch head = {.raw = *p}; + const watch head = {/*.raw = */*p}; // c++20 only watches *repr_watches = &WATCHES (repr); PUSH_WATCHES (*repr_watches, head); } diff --git a/src/sat/kissat/walk.c b/src/sat/kissat/walk.c index 72ce38a6c3..18ebdd6792 100644 --- a/src/sat/kissat/walk.c +++ b/src/sat/kissat/walk.c @@ -28,7 +28,7 @@ struct tagged { static inline tagged make_tagged (bool binary, unsigned ref) { KISSAT_assert (ref <= MAX_WALK_REF); - tagged res = {.ref = ref, .binary = binary}; + tagged res = {/*.ref = */ref, /*.binary = */binary}; // c++20 only return res; } diff --git a/src/sat/kissat/watch.c b/src/sat/kissat/watch.c index 78f9a69ce7..d444f18c26 100644 --- a/src/sat/kissat/watch.c +++ b/src/sat/kissat/watch.c @@ -36,7 +36,7 @@ void kissat_remove_binary_watch (kissat *solver, watches *watches, KISSAT_assert (begin + 1 <= end); watches->end -= 1; #endif - const watch empty = {.raw = INVALID_VECTOR_ELEMENT}; + const watch empty = {/*.raw = */INVALID_VECTOR_ELEMENT}; // c++20 only end[-1] = empty; KISSAT_assert (solver->vectors.usable < MAX_SECTOR - 1); solver->vectors.usable += 1; @@ -73,7 +73,7 @@ void kissat_remove_blocking_watch (kissat *solver, watches *watches, KISSAT_assert (begin + 2 <= end); watches->end -= 2; #endif - const watch empty = {.raw = INVALID_VECTOR_ELEMENT}; + const watch empty = {/*.raw = */INVALID_VECTOR_ELEMENT}; // c++20 only end[-2] = end[-1] = empty; KISSAT_assert (solver->vectors.usable < MAX_SECTOR - 2); solver->vectors.usable += 2;