From: Kirill A. Korinsky Subject: Re: [update] math/z3: update to 4.13.0 To: Klemens Nanni Cc: OpenBSD ports Date: Tue, 03 Sep 2024 18:07:36 +0200 On Sat, 31 Aug 2024 21:08:15 +0200, Klemens Nanni wrote: > > You're right, :Q remained from an earlier iteration. > I dropped it, yielding correct commands now, thanks. > Here an updated diff where I've backported patch from upstream which fixed crash on OpenBSD as side effect. I also drop testing of crash because - '(declare-datatype)' and '(declare-datatype a)' doesn't work on 4.13 and simple complains as: (error "line 1 column 18: unexpected token used as datatype name") (error "line 1 column 20: invalid datatype declaration, '(' expected got a") - '(declare-const p Bool) because this case is covered by example models. So, finally a diff which works without crash on -current/amd64: Index: Makefile =================================================================== RCS file: /cvs/ports/math/z3/Makefile,v retrieving revision 1.33 diff -u -p -r1.33 Makefile --- Makefile 6 May 2024 12:23:45 -0000 1.33 +++ Makefile 3 Sep 2024 16:05:14 -0000 @@ -1,16 +1,9 @@ COMMENT = Z3 theorem prover -VERSION = 4.12.2 -REVISION = 1 +DIST_TUPLE = github Z3Prover z3 z3-4.13.0 . +PKGNAME = ${DISTNAME:S/z3-//} -GH_ACCOUNT = Z3Prover -GH_PROJECT = z3 -GH_TAGNAME = ${GH_PROJECT}-${VERSION} - -DISTNAME = ${GH_TAGNAME} -PKGNAME = ${DISTNAME:L} - -SHARED_LIBS = z3 4.0 # 4.10 +SHARED_LIBS = z3 4.11 CATEGORIES = math @@ -19,25 +12,27 @@ WANTLIB += c m pthread ${COMPILER_LIBCXX # MIT PERMIT_PACKAGE = Yes -# c++11 +# C++17 COMPILER = base-clang ports-gcc MODULES = devel/cmake \ lang/python -CONFIGURE_ARGS += -DZ3_ENABLE_EXAMPLE_TARGETS=ON \ +MODPY_RUNDEP = No + +CONFIGURE_ARGS = -DZ3_BUILD_PYTHON_BINDINGS=ON \ + -DZ3_ENABLE_EXAMPLE_TARGETS=OFF \ -DZ3_INCLUDE_GIT_HASH=OFF \ - -DZ3_INCLUDE_GIT_DESCRIBE=OFF \ - -DZ3_BUILD_PYTHON_BINDINGS=ON \ -DZ3_USE_LIB_GMP=OFF DEBUG_PACKAGES = ${BUILD_PACKAGES} -WRKDIST = ${WRKDIR}/z3-${DISTNAME} - -NO_TEST = Yes - -pre-configure: +post-extract: ${SUBST_CMD} ${WRKSRC}/scripts/mk_util.py + +post-test: + cd ${WRKBUILD} && \ + find ${WRKSRC}/examples/SMT-LIB2/ -type f -name '*.smt2' \ + -exec echo \; -print -exec ./z3 {} \; .include Index: distinfo =================================================================== RCS file: /cvs/ports/math/z3/distinfo,v retrieving revision 1.14 diff -u -p -r1.14 distinfo --- distinfo 12 Aug 2023 13:31:09 -0000 1.14 +++ distinfo 3 Sep 2024 16:05:14 -0000 @@ -1,2 +1,2 @@ -SHA256 (z3-4.12.2.tar.gz) = n1jzcQvSCUCFlRp1eRVQ9UeQPXX+fi/LNzxfA/x2G48= -SIZE (z3-4.12.2.tar.gz) = 5401038 +SHA256 (Z3Prover-z3-z3-4.13.0.tar.gz) = AbzGHINi43u4n9JDD34zheht95FQGb0s5F3p2b2TRQI= +SIZE (Z3Prover-z3-z3-4.13.0.tar.gz) = 5520232 Index: patches/patch-cmake_cxx_compiler_flags_overrides_cmake =================================================================== RCS file: /cvs/ports/math/z3/patches/patch-cmake_cxx_compiler_flags_overrides_cmake,v retrieving revision 1.2 diff -u -p -r1.2 patch-cmake_cxx_compiler_flags_overrides_cmake --- patches/patch-cmake_cxx_compiler_flags_overrides_cmake 11 Mar 2022 19:36:33 -0000 1.2 +++ patches/patch-cmake_cxx_compiler_flags_overrides_cmake 3 Sep 2024 16:05:14 -0000 @@ -1,3 +1,5 @@ +Removed hardcoded optimizations + Index: cmake/cxx_compiler_flags_overrides.cmake --- cmake/cxx_compiler_flags_overrides.cmake.orig +++ cmake/cxx_compiler_flags_overrides.cmake Index: patches/patch-scripts_mk_util_py =================================================================== RCS file: /cvs/ports/math/z3/patches/patch-scripts_mk_util_py,v retrieving revision 1.10 diff -u -p -r1.10 patch-scripts_mk_util_py --- patches/patch-scripts_mk_util_py 9 Feb 2023 06:53:56 -0000 1.10 +++ patches/patch-scripts_mk_util_py 3 Sep 2024 16:05:14 -0000 @@ -1,7 +1,11 @@ +- Remove hardcoded optimizations +- Fix .so versioning +- use -fPIC to build shared libs on all archs + Index: scripts/mk_util.py --- scripts/mk_util.py.orig +++ scripts/mk_util.py -@@ -2607,7 +2607,6 @@ def mk_config(): +@@ -2609,7 +2609,6 @@ def mk_config(): EXAMP_DEBUG_FLAG = '-g' CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS else: @@ -9,7 +13,7 @@ Index: scripts/mk_util.py if GPROF: CXXFLAGS += '-fomit-frame-pointer' CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS -@@ -2632,7 +2631,7 @@ def mk_config(): +@@ -2634,7 +2633,7 @@ def mk_config(): SO_EXT = '.so' SLIBFLAGS = '-shared' elif sysname == 'OpenBSD': @@ -18,15 +22,12 @@ Index: scripts/mk_util.py SLIBFLAGS = '-shared' elif sysname == 'SunOS': SO_EXT = '.so' -@@ -2648,9 +2647,8 @@ def mk_config(): +@@ -2650,7 +2649,7 @@ def mk_config(): LIB_EXT = '.lib' else: raise MKException('Unsupported platform: %s' % sysname) - if is64(): -- if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'): -- CXXFLAGS = '%s -fPIC' % CXXFLAGS -+ if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'): -+ CXXFLAGS = '%s -fPIC' % CXXFLAGS ++ if true: + if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'): + CXXFLAGS = '%s -fPIC' % CXXFLAGS elif not LINUX_X64: - CXXFLAGS = '%s -m32' % CXXFLAGS - LDFLAGS = '%s -m32' % LDFLAGS Index: patches/patch-src_util_memory_manager_cpp =================================================================== RCS file: patches/patch-src_util_memory_manager_cpp diff -N patches/patch-src_util_memory_manager_cpp --- /dev/null 1 Jan 1970 00:00:00 -0000 +++ patches/patch-src_util_memory_manager_cpp 3 Sep 2024 16:05:14 -0000 @@ -0,0 +1,111 @@ +https://github.com/Z3Prover/z3/issues/6902 +Index: src/util/memory_manager.cpp +--- src/util/memory_manager.cpp.orig ++++ src/util/memory_manager.cpp +@@ -29,6 +29,8 @@ Copyright (c) 2015 Microsoft Corporation + # define malloc_usable_size _msize + #endif + ++#define SIZE_T_ALIGN 2 ++ + // The following two function are automatically generated by the mk_make.py script. + // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files. + // For example, rational.h contains +@@ -278,7 +280,7 @@ void memory::deallocate(void * p) { + size_t sz = malloc_usable_size(p); + void * real_p = p; + #else +- size_t * sz_p = reinterpret_cast(p) - 1; ++ size_t * sz_p = reinterpret_cast(p) - SIZE_T_ALIGN; + size_t sz = *sz_p; + void * real_p = reinterpret_cast(sz_p); + #endif +@@ -291,7 +293,7 @@ void memory::deallocate(void * p) { + + void * memory::allocate(size_t s) { + #ifndef HAS_MALLOC_USABLE_SIZE +- s = s + sizeof(size_t); // we allocate an extra field! ++ s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field! + #endif + g_memory_thread_alloc_size += s; + g_memory_thread_alloc_count += 1; +@@ -308,7 +310,7 @@ void * memory::allocate(size_t s) { + return r; + #else + *(static_cast(r)) = s; +- return static_cast(r) + 1; // we return a pointer to the location after the extra field ++ return static_cast(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field + #endif + } + +@@ -320,10 +322,10 @@ void* memory::reallocate(void *p, size_t s) { + if (sz >= s) + return p; + #else +- size_t *sz_p = reinterpret_cast(p)-1; ++ size_t *sz_p = reinterpret_cast(p)-SIZE_T_ALIGN; + size_t sz = *sz_p; + void *real_p = reinterpret_cast(sz_p); +- s = s + sizeof(size_t); // we allocate an extra field! ++ s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field! + #endif + g_memory_thread_alloc_size += s - sz; + g_memory_thread_alloc_count += 1; +@@ -341,7 +343,7 @@ void* memory::reallocate(void *p, size_t s) { + return r; + #else + *(static_cast(r)) = s; +- return static_cast(r) + 1; // we return a pointer to the location after the extra field ++ return static_cast(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field + #endif + } + +@@ -358,7 +360,7 @@ void memory::deallocate(void * p) { + size_t sz = malloc_usable_size(p); + void * real_p = p; + #else +- size_t * sz_p = reinterpret_cast(p) - 1; ++ size_t * sz_p = reinterpret_cast(p) - SIZE_T_ALIGN; + size_t sz = *sz_p; + void * real_p = reinterpret_cast(sz_p); + #endif +@@ -368,7 +370,7 @@ void memory::deallocate(void * p) { + + void * memory::allocate(size_t s) { + #ifndef HAS_MALLOC_USABLE_SIZE +- s = s + sizeof(size_t); // we allocate an extra field! ++ s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field! + #endif + g_memory_alloc_size += s; + g_memory_alloc_count += 1; +@@ -389,7 +391,7 @@ void * memory::allocate(size_t s) { + return r; + #else + *(static_cast(r)) = s; +- return static_cast(r) + 1; // we return a pointer to the location after the extra field ++ return static_cast(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field + #endif + } + +@@ -401,10 +403,10 @@ void* memory::reallocate(void *p, size_t s) { + if (sz >= s) + return p; + #else +- size_t * sz_p = reinterpret_cast(p) - 1; ++ size_t * sz_p = reinterpret_cast(p) - SIZE_T_ALIGN; + size_t sz = *sz_p; + void * real_p = reinterpret_cast(sz_p); +- s = s + sizeof(size_t); // we allocate an extra field! ++ s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field! + #endif + g_memory_alloc_size += s - sz; + g_memory_alloc_count += 1; +@@ -425,7 +427,7 @@ void* memory::reallocate(void *p, size_t s) { + return r; + #else + *(static_cast(r)) = s; +- return static_cast(r) + 1; // we return a pointer to the location after the extra field ++ return static_cast(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field + #endif + } + Index: pkg/PLIST =================================================================== RCS file: /cvs/ports/math/z3/pkg/PLIST,v retrieving revision 1.9 diff -u -p -r1.9 PLIST --- pkg/PLIST 11 Mar 2022 19:36:33 -0000 1.9 +++ pkg/PLIST 3 Sep 2024 16:05:14 -0000 @@ -1,4 +1,4 @@ -@conflict py3-z3-solver-* +@conflict ${MODPY_PY_PREFIX}z3-solver-* @bin bin/z3 include/z3++.h include/z3.h @@ -22,6 +22,8 @@ lib/cmake/z3/Z3Targets${MODCMAKE_BUILD_S lib/cmake/z3/Z3Targets.cmake @lib lib/libz3.so.${LIBz3_VERSION} lib/pkgconfig/z3.pc +lib/python${MODPY_VERSION}/ +lib/python${MODPY_VERSION}/site-packages/ lib/python${MODPY_VERSION}/site-packages/z3/ lib/python${MODPY_VERSION}/site-packages/z3/__init__.py lib/python${MODPY_VERSION}/site-packages/z3/z3.py -- wbr, Kirill