Index | Thread | Search

From:
Kirill A. Korinsky <kirill@korins.ky>
Subject:
math/z3: update to 4.13.3; taken mantainership
To:
OpenBSD ports <ports@openbsd.org>
Cc:
Klemens Nanni <kn@openbsd.org>
Date:
Sat, 12 Oct 2024 17:38:50 +0200

Download raw body.

Thread
  • Kirill A. Korinsky:

    math/z3: update to 4.13.3; taken mantainership

ports@,

Here an update for math/z3 to the last version which includes patch to fix
building under clang.

I've increased SHARE_LIBS version because include files was changes.

And I've also would like to take care of this port.

Changes:
 - https://github.com/Z3Prover/z3/releases/tag/z3-4.13.1
 - https://github.com/Z3Prover/z3/releases/tag/z3-4.13.2
 - https://github.com/Z3Prover/z3/releases/tag/z3-4.13.3

Tested on -current/amd64.

The diff:

Index: Makefile
===================================================================
RCS file: /cvs/ports/math/z3/Makefile,v
retrieving revision 1.34
diff -u -p -r1.34 Makefile
--- Makefile	3 Sep 2024 17:48:45 -0000	1.34
+++ Makefile	12 Oct 2024 15:28:11 -0000
@@ -1,13 +1,15 @@
 COMMENT =	Z3 theorem prover
 
-DIST_TUPLE =	github	Z3Prover	z3	z3-4.13.0	.
+DIST_TUPLE =	github	Z3Prover	z3	z3-4.13.3	.
 PKGNAME =	${DISTNAME:S/z3-//}
 
-SHARED_LIBS =	z3	4.11
+SHARED_LIBS =	z3	4.12
 
 CATEGORIES =	math
 
 WANTLIB +=	c m pthread ${COMPILER_LIBCXX}
+
+MAINTAINER =	Kirill A. Korinsky <kirill@korins.ky>
 
 # MIT
 PERMIT_PACKAGE =	Yes
Index: distinfo
===================================================================
RCS file: /cvs/ports/math/z3/distinfo,v
retrieving revision 1.15
diff -u -p -r1.15 distinfo
--- distinfo	3 Sep 2024 17:48:45 -0000	1.15
+++ distinfo	12 Oct 2024 15:28:11 -0000
@@ -1,2 +1,2 @@
-SHA256 (Z3Prover-z3-z3-4.13.0.tar.gz) = AbzGHINi43u4n9JDD34zheht95FQGb0s5F3p2b2TRQI=
-SIZE (Z3Prover-z3-z3-4.13.0.tar.gz) = 5520232
+SHA256 (Z3Prover-z3-z3-4.13.3.tar.gz) = 9Zyc9gDqV/tk/+/7/9Dy0riWhU8znoRvSPBp0jvBS6A=
+SIZE (Z3Prover-z3-z3-4.13.3.tar.gz) = 5583533
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
--- patches/patch-src_util_memory_manager_cpp	3 Sep 2024 17:48:45 -0000	1.1
+++ /dev/null	1 Jan 1970 00:00:00 -0000
@@ -1,111 +0,0 @@
-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<size_t*>(p) - 1;
-+    size_t * sz_p  = reinterpret_cast<size_t*>(p) - SIZE_T_ALIGN;
-     size_t sz      = *sz_p;
-     void * real_p  = reinterpret_cast<void*>(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<size_t*>(r)) = s;
--    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
-+    return static_cast<size_t*>(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<size_t*>(p)-1;
-+    size_t *sz_p = reinterpret_cast<size_t*>(p)-SIZE_T_ALIGN;
-     size_t sz = *sz_p;
-     void *real_p = reinterpret_cast<void*>(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<size_t*>(r)) = s;
--    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
-+    return static_cast<size_t*>(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<size_t*>(p) - 1;
-+    size_t * sz_p  = reinterpret_cast<size_t*>(p) - SIZE_T_ALIGN;
-     size_t sz      = *sz_p;
-     void * real_p  = reinterpret_cast<void*>(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<size_t*>(r)) = s;
--    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
-+    return static_cast<size_t*>(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<size_t*>(p) - 1;
-+    size_t * sz_p  = reinterpret_cast<size_t*>(p) - SIZE_T_ALIGN;
-     size_t sz      = *sz_p;
-     void * real_p  = reinterpret_cast<void*>(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<size_t*>(r)) = s;
--    return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
-+    return static_cast<size_t*>(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field
- #endif
- }
-  


-- 
wbr, Kirill