From: Klemens Nanni Subject: Re: [update] math/z3: update to 4.13.0 To: OpenBSD ports Date: Tue, 27 Aug 2024 19:59:25 +0000 26.08.2024 21:45, Kirill A. Korinsky пишет: > ports@, > > Here an update version of this diff VERSION is used once and can be inlined. PKGNAME not needed as DISTNAME is already lowercase. One patch had offsets (need 'make update-patches') and could be simplified to make it obviuos what we patch and why. COMPILER comment does not match -std=gnuc++17 usage. Upstream has non-empty src/test/ and a default-ON Z3_BUILD_TEST_EXECUTABLES option, but we still set NO_TEST=Yes -- either don't build or run them. 'make update-plist' changed the @conflict marker (result is the same), I think we want that, or at least not manually revert it everytime. MODPY_RUNDEP=No seems missing unless z3 really needs python at runtime. > On Wed, 21 Aug 2024 00:30:09 +0200, > Kirill A. Korinsky wrote: >> >> ports@, >> >> Here is a clean update of math/z3 to the latest release. >> >> Changelog: >> https://github.com/Z3Prover/z3/releases/tag/z3-4.13.0 >> >> Tested on -current/amd64. >> >> So the crashing problem is still here, see: >> https://github.com/Z3Prover/z3/issues/6902 I see three reproducers there that fit into a post-test! >> >> But it exists on the current version in ports, which means the update >> doesn't break anything new. Which we can use as an argument to not create too much fuzz and leave optimiztions on until a proper fix shows up; at least I cannot judge at all what impact that has. >> > > After spending some time to dig into the issue which lead to crash, I had > discovered that such crash doesn't reproduced if I build z3 wihtout > optimization (-O0). -O1 also crashes. > > During that time I had noticed and fixed a few cases with broken stack... > Unfortently it doesn't help with the crash. > > So, here an updated diff which builds z3 without optimization. It, probably, > works slower but I can't crash it anymore. > > I suggest to keep it that way, until it's fixed. > > An updated diff: New diff including all the feedback above, you can now hack on the port and iterate over 'make retest' until it no longer crashes (or you give up) ;-) Index: Makefile =================================================================== RCS file: /cvs/ports/math/z3/Makefile,v diff -u -p -r1.33 Makefile --- Makefile 6 May 2024 12:23:45 -0000 1.33 +++ Makefile 27 Aug 2024 19:58:52 -0000 @@ -1,16 +1,12 @@ COMMENT = Z3 theorem prover -VERSION = 4.12.2 -REVISION = 1 - GH_ACCOUNT = Z3Prover GH_PROJECT = z3 -GH_TAGNAME = ${GH_PROJECT}-${VERSION} +GH_TAGNAME = ${GH_PROJECT}-4.13.0 DISTNAME = ${GH_TAGNAME} -PKGNAME = ${DISTNAME:L} -SHARED_LIBS = z3 4.0 # 4.10 +SHARED_LIBS = z3 4.1 CATEGORIES = math @@ -19,25 +15,39 @@ 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 \ - -DZ3_INCLUDE_GIT_HASH=OFF \ +MODPY_RUNDEP = No + +CONFIGURE_ARGS = -DZ3_BUILD_PYTHON_BINDINGS=ON \ + -DZ3_ENABLE_EXAMPLE_TARGETS=ON \ -DZ3_INCLUDE_GIT_DESCRIBE=OFF \ - -DZ3_BUILD_PYTHON_BINDINGS=ON \ + -DZ3_INCLUDE_GIT_HASH=OFF \ -DZ3_USE_LIB_GMP=OFF DEBUG_PACKAGES = ${BUILD_PACKAGES} WRKDIST = ${WRKDIR}/z3-${DISTNAME} -NO_TEST = Yes +# https://github.com/Z3Prover/z3/issues/6902 +# effectively -O0 to avoid crashes with -O[12] +MODCMAKE_DEBUG = Yes pre-configure: ${SUBST_CMD} ${WRKSRC}/scripts/mk_util.py + +post-test: + # 4.12.2 segfaults on 1,2,3 + # 4.13.0 segfaults on 2,3 and warns on 1 +.for _repro in \ + '(declare-datatype)' \ + '(declare-datatype a)' \ + '(declare-const p Bool)' + -echo ${_repro:Q} | (cd ${WRKBUILD} && ./z3 -in) +.endfor .include Index: distinfo =================================================================== RCS file: /cvs/ports/math/z3/distinfo,v diff -u -p -r1.14 distinfo --- distinfo 12 Aug 2023 13:31:09 -0000 1.14 +++ distinfo 27 Aug 2024 18:34:26 -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 (z3-4.13.0.tar.gz) = AbzGHINi43u4n9JDD34zheht95FQGb0s5F3p2b2TRQI= +SIZE (z3-4.13.0.tar.gz) = 5520232 \ No newline at end of file Index: patches/patch-cmake_cxx_compiler_flags_overrides_cmake =================================================================== RCS file: /cvs/ports/math/z3/patches/patch-cmake_cxx_compiler_flags_overrides_cmake,v 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 27 Aug 2024 18:38:44 -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 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 27 Aug 2024 18:42:43 -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: pkg/PLIST =================================================================== RCS file: /cvs/ports/math/z3/pkg/PLIST,v diff -u -p -r1.9 PLIST --- pkg/PLIST 11 Mar 2022 19:36:33 -0000 1.9 +++ pkg/PLIST 27 Aug 2024 19:19:02 -0000 @@ -1,4 +1,4 @@ -@conflict py3-z3-solver-* +@conflict ${MODPY_PY_PREFIX}z3-solver-* @bin bin/z3 include/z3++.h include/z3.h