math/z3: Update to 4.8.17

(cherry picked from commit 1bbe14a63386e61b53e8c7e1eb082b9b6fe6365e)

4 files changed, 92 insertions, 6 deletions

diff --git a/math/z3/Makefile b/math/z3/Makefile
index 529069510a96..ef4734375840 100644
--- a/math/z3/Makefile
+++ b/math/z3/Makefile
@@ -1,6 +1,6 @@
 PORTNAME=	z3
 DISTVERSIONPREFIX=	z3-
-DISTVERSION=	4.8.16
+DISTVERSION=	4.8.17
 CATEGORIES=	math
 
 MAINTAINER=	arrowd@FreeBSD.org
diff --git a/math/z3/distinfo b/math/z3/distinfo
index f5d61a2521c8..d1a05ca2b821 100644
--- a/math/z3/distinfo
+++ b/math/z3/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1651515677
-SHA256 (Z3Prover-z3-z3-4.8.16_GH0.tar.gz) = 75f95e09f3f35fef746e571d5ec88a4efba27f1bc8f1a0ef1117167486ec3dc6
-SIZE (Z3Prover-z3-z3-4.8.16_GH0.tar.gz) = 5223980
+TIMESTAMP = 1653058564
+SHA256 (Z3Prover-z3-z3-4.8.17_GH0.tar.gz) = 1e57637ce8d5212fd38453df28e2730a18e0a633f723682267be87f5b858a126
+SIZE (Z3Prover-z3-z3-4.8.17_GH0.tar.gz) = 5232392
diff --git a/math/z3/files/patch-scripts_mk__util.py b/math/z3/files/patch-scripts_mk__util.py
index 43e8bd1f6537..0d3cfd52b146 100644
--- a/math/z3/files/patch-scripts_mk__util.py
+++ b/math/z3/files/patch-scripts_mk__util.py
@@ -1,6 +1,6 @@
---- scripts/mk_util.py.orig	2019-09-19 23:43:06 UTC
+--- scripts/mk_util.py.orig	2022-05-05 00:16:30 UTC
 +++ scripts/mk_util.py
-@@ -2508,8 +2508,8 @@ def mk_config():
+@@ -2543,8 +2543,8 @@ def mk_config():
          check_ar()
          CXX = find_cxx_compiler()
          CC  = find_c_compiler()
@@ -11,3 +11,12 @@
          EXE_EXT = ''
          LIB_EXT = '.a'
          if GPROF:
+@@ -2632,7 +2632,7 @@ def mk_config():
+         if is64():
+             if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
+                 CXXFLAGS     = '%s -fPIC' % CXXFLAGS
+-            if sysname == 'Linux':
++            if sysname == 'Linux' or sysname == 'FreeBSD':
+                 CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS
+         elif not LINUX_X64:
+             CXXFLAGS     = '%s -m32' % CXXFLAGS
diff --git a/math/z3/files/patch-src_util_memory__manager.cpp b/math/z3/files/patch-src_util_memory__manager.cpp
new file mode 100644
index 000000000000..8616f05b8f5a
--- /dev/null
+++ b/math/z3/files/patch-src_util_memory__manager.cpp
@@ -0,0 +1,77 @@
+Z3 memory manager stores actual data along with its size, which causes the
+memory to be 8-byte aligned. Use malloc non-portable functions to obtain
+memory region size instead.
+
+https://github.com/Z3Prover/z3/issues/6015
+
+--- src/util/memory_manager.cpp.orig	2022-05-05 00:16:30 UTC
++++ src/util/memory_manager.cpp
+@@ -13,6 +13,7 @@ --*/
+ #include "util/error_codes.h"
+ #include "util/debug.h"
+ #include "util/scoped_timer.h"
++#include <malloc_np.h>
+ // 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
+@@ -258,52 +259,43 @@ void memory::deallocate(void * p) {
+ }
+ 
+ void memory::deallocate(void * p) {
+-    size_t * sz_p  = reinterpret_cast<size_t*>(p) - 1;
+-    size_t sz      = *sz_p;
+-    void * real_p  = reinterpret_cast<void*>(sz_p);
+-    g_memory_thread_alloc_size -= sz;
+-    free(real_p);
++    g_memory_thread_alloc_size -= malloc_usable_size(p);
++    if (g_memory_thread_alloc_size < 0) g_memory_thread_alloc_size = 0;
++    free(p);
+     if (g_memory_thread_alloc_size < -SYNCH_THRESHOLD) {
+         synchronize_counters(false);
+     }
+ }
+ 
+ void * memory::allocate(size_t s) {
+-    s = s + sizeof(size_t); // we allocate an extra field!
+     void * r = malloc(s);
+     if (r == 0) {
+         throw_out_of_memory();
+         return nullptr;
+     }
+-    *(static_cast<size_t*>(r)) = s;
+     g_memory_thread_alloc_size += s;
+     g_memory_thread_alloc_count += 1;
+     if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
+         synchronize_counters(true);
+     }
+ 
+-    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
++    return r; // we return a pointer to the location after the extra field
+ }
+ 
+ void* memory::reallocate(void *p, size_t s) {
+-    size_t *sz_p = reinterpret_cast<size_t*>(p)-1;
+-    size_t sz = *sz_p;
+-    void *real_p = reinterpret_cast<void*>(sz_p);
+-    s = s + sizeof(size_t); // we allocate an extra field!
+-
+-    g_memory_thread_alloc_size += s - sz;
++    g_memory_thread_alloc_size += s - malloc_usable_size(p);
++    if (g_memory_thread_alloc_size < 0) g_memory_thread_alloc_size = 0;
+     g_memory_thread_alloc_count += 1;
+     if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
+         synchronize_counters(true);
+     }
+ 
+-    void *r = realloc(real_p, s);
++    void *r = realloc(p, s);
+     if (r == 0) {
+         throw_out_of_memory();
+         return nullptr;
+     }
+-    *(static_cast<size_t*>(r)) = s;
+-    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
++    return r;
+ }
+ 
+ #else