python: load libz3 with soversion

[sertonix]

The python bindings load libz3 without a soversion which means that it will happily load a version of libz3 which could be ABI incompatible with the generated bindings. Things like this can happen while upgrading or when multiple versions of libz3 are available.

On linux the library can be loaded using libz3.so.<soversion> instead. I don't know how to fix that on other platforms so I can't create a PR to fix this. For linux the patch could look something like this (not properly tested!):

diff --git a/scripts/update_api.py b/scripts/update_api.py
index 153052deb..924df6a29 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1823,9 +1823,10 @@ del _lib
 del _default_dirs
 del _all_dirs
 del _ext
+del _sover
 """)
 
-def write_core_py_preamble(core_py):
+def write_core_py_preamble(core_py, z3py_soversion):
   core_py.write(
 """
 # Automatically generated file
@@ -1842,6 +1843,10 @@ from .z3consts import *
 
 _file_manager = contextlib.ExitStack()
 atexit.register(_file_manager.close)
+"""
+  core_py.write("_sover=\"%s\"\n" % z3py_soversion)
+  core_py.write(
+"""
 _ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so'
 _lib = None
 _z3_lib_resource = importlib_resources.files('z3').joinpath('lib')
@@ -1877,7 +1882,7 @@ for d in _all_dirs:
   try:
     d = os.path.realpath(d)
     if os.path.isdir(d):
-      d = os.path.join(d, 'libz3.%s' % _ext)
+      d = os.path.join(d, 'libz3.%s.%s' % (_ext, _sover))
       if os.path.isfile(d):
         _lib = ctypes.CDLL(d)
         break
@@ -1888,24 +1893,24 @@ for d in _all_dirs:
 if _lib is None:
   # If all else failed, ask the system to find it.
   try:
-    _lib = ctypes.CDLL('libz3.%s' % _ext)
+    _lib = ctypes.CDLL('libz3.%s.%s' % (_ext, _sover))
   except Exception as e:
     _failures += [e]
     pass
 
 if _lib is None:
-  print("Could not find libz3.%s; consider adding the directory containing it to" % _ext)
+  print("Could not find libz3.%s.%s; consider adding the directory containing it to" % (_ext, _sover))
   print("  - your system's PATH environment variable,")
   print("  - the Z3_LIBRARY_PATH environment variable, or ")
   print("  - to the custom Z3_LIB_DIRS Python-builtin before importing the z3 module, e.g. via")
   if sys.version < '3':
     print("    import __builtin__")
-    print("    __builtin__.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s" % _ext)
+    print("    __builtin__.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s.%s" % (_ext, _sover))
   else:
     print("    import builtins")
-    print("    builtins.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s" % _ext)
+    print("    builtins.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s.%s" % (_ext, _sover))
   print(_failures)
-  raise Z3Exception("libz3.%s not found." % _ext)
+  raise Z3Exception("libz3.%s.%s not found." % (_ext, _sover))
 
 
 if sys.version < '3':
@@ -1970,6 +1975,7 @@ core_py = None
 def generate_files(api_files,
                    api_output_dir=None,
                    z3py_output_dir=None,
+                   z3py_soversion=None,
                    dotnet_output_dir=None,
                    java_input_dir=None,
                    java_output_dir=None,
@@ -2026,7 +2032,7 @@ def generate_files(api_files,
           write_log_h_preamble(log_h)
           write_log_c_preamble(log_c)
           write_exe_c_preamble(exe_c)
-          write_core_py_preamble(core_py)
+          write_core_py_preamble(core_py, z3py_soversion)
 
           # FIXME: these functions are awful
           apiTypes.def_Types(api_files)
@@ -2069,6 +2075,10 @@ def main(args):
                       dest="z3py_output_dir",
                       default=None,
                       help="Directory to emit z3py files. If not specified no files are emitted.")
+  parser.add_argument("--z3py-soversion",
+                      dest="z3py_soversion",
+                      default=None,
+                      help="SOVERSION for loading libz3 library.")
   parser.add_argument("--dotnet-output-dir",
                       dest="dotnet_output_dir",
                       default=None,
@@ -2095,6 +2105,11 @@ def main(args):
                       help="Directory to emit OCaml files. If not specified no files are emitted.")
   pargs = parser.parse_args(args)
 
+  if pargs.z3py_output_dir:
+    if pargs.z3py_soversion is None:
+      logging.error('--z3py-soversion must be specified')
+      return 1
+
   if pargs.java_output_dir:
     if pargs.java_package_name == None:
       logging.error('--java-package-name must be specified')
@@ -2116,6 +2131,7 @@ def main(args):
   generate_files(api_files=pargs.api_files,
                  api_output_dir=pargs.api_output_dir,
                  z3py_output_dir=pargs.z3py_output_dir,
+                 z3py_soversion=pargs.z3py_soversion,
                  dotnet_output_dir=pargs.dotnet_output_dir,
                  java_input_dir=pargs.java_input_dir,
                  java_output_dir=pargs.java_output_dir,
diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt
index 5da66dfe4..2947905f4 100644
--- a/src/api/python/CMakeLists.txt
+++ b/src/api/python/CMakeLists.txt
@@ -36,6 +36,8 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3core.py"
   COMMAND "${Python3_EXECUTABLE}"
     "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
     ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "--z3py-soversion"
+    ${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}
     "--z3py-output-dir"
     "${z3py_bindings_build_dest}"
   DEPENDS

[jirislaby]

This works for me, except:

@@ -1842,6 +1843,10 @@ from .z3consts import *
 
 _file_manager = contextlib.ExitStack()
 atexit.register(_file_manager.close)
+"""

You forgot to close the paren here ^^^.

+  core_py.write("_sover=\"%s\"\n" % z3py_soversion)
+  core_py.write(
+"""

[NikolajBjorner]

we could make this conditional on the platform then on Windows etc this is a no-op?