commit f7ef783c7170c4930d2461edf78a63de83a7b0f7 · anil.recoil.org/opam-repository

+267

packages/z3/z3.4.8.5-1/files/4468.patch

···

       1
       +
       From 8179ae62817d46c7a3df82aded1ff105fa2c3646 Mon Sep 17 00:00:00 2001

     

       2
       +
       From: ivg <ivg@ieee.org>

     

       3
       +
       Date: Wed, 27 May 2020 07:52:52 -0400

     

       4
       +
       Subject: [PATCH] fixes numerous issues in OCaml bindings building process

     

       5
       +
       

     

       6
       +
       It now works both in dynamic and static mode and the compiled

     

       7
       +
       libraries can be used by all linkers in the OCaml system, without

     

       8
       +
       any specificy instructions other than specifying the dependency on

     

       9
       +
       the z3 library.

     

       10
       +
       

     

       11
       +
       Using the libraries

     

       12
       +
       ===================

     

       13
       +
       

     

       14
       +
       Compiling binaries

     

       15
       +
       ------------------

     

       16
       +
       

     

       17
       +
       The libraries can be linked statically with both ocamlc and ocamlopt

     

       18
       +
       compilers, e.g.,

     

       19
       +
       

     

       20
       +
       ```

     

       21
       +
       ocamlfind ocamlc -thread -package z3 -linkpkg run.ml -o run

     

       22
       +
       ```

     

       23
       +
       or

     

       24
       +
       ```

     

       25
       +
       ocamlfind ocamlopt -thread -package z3 -linkpkg run.ml -o run

     

       26
       +
       ```

     

       27
       +
       

     

       28
       +
       When bindings compiled with the `--staticlib` the produced binary will

     

       29
       +
       not have any dependencies on z3

     

       30
       +
       ```

     

       31
       +
       $ ldd ./run

     

       32
       +
               linux-vdso.so.1 (0x00007fff9c9ed000)

     

       33
       +
               libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fb56f09c000)

     

       34
       +
               libgmp.so.10 => /usr/lib/x86_64-linux-gnu/libgmp.so.10 (0x00007fb56ee1b000)

     

       35
       +
               libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fb56ebfc000)

     

       36
       +
               libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fb56e85e000)

     

       37
       +
               libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fb56e65a000)

     

       38
       +
               libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fb56e442000)

     

       39
       +
               libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fb56e051000)

     

       40
       +
               /lib64/ld-linux-x86-64.so.2 (0x00007fb570de9000)

     

       41
       +
       ```

     

       42
       +
       

     

       43
       +
       The bytecode version will have a depedency on z3 and other external

     

       44
       +
       libraries (packed as dlls and usually installed in opam switch):

     

       45
       +
       ```

     

       46
       +
       $ ocamlobjinfo run | grep 'Used DLL' -A5

     

       47
       +
       Used DLLs:

     

       48
       +
               dllz3ml

     

       49
       +
               dllzarith

     

       50
       +
               dllthreads

     

       51
       +
               dllunix

     

       52
       +
       ```

     

       53
       +
       

     

       54
       +
       But it is possible to compile a portable self-contained version of the

     

       55
       +
       bytecode executable using the `-custom` switch:

     

       56
       +
       

     

       57
       +
       ```

     

       58
       +
       ocamlfind ocamlc -custom -thread -package z3 -linkpkg run.ml -o run

     

       59
       +
       ```

     

       60
       +
       

     

       61
       +
       The build binary is now quite large but doesn't have any external

     

       62
       +
       dependencies (modulo the system dependencies):

     

       63
       +
       ```

     

       64
       +
       $ du -h run

     

       65
       +
       27M     run

     

       66
       +
       $ ocamlobjinfo run | grep 'Used DLL' | wc -l

     

       67
       +
       0

     

       68
       +
       $ ldd run

     

       69
       +
               linux-vdso.so.1 (0x00007ffee42c2000)

     

       70
       +
               libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fdbdc415000)

     

       71
       +
               libgmp.so.10 => /usr/lib/x86_64-linux-gnu/libgmp.so.10 (0x00007fdbdc194000)

     

       72
       +
               libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fdbdbf75000)

     

       73
       +
               libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fdbdbbd7000)

     

       74
       +
               libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fdbdb9d3000)

     

       75
       +
               libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fdbdb7bb000)

     

       76
       +
               libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fdbdb3ca000)

     

       77
       +
               /lib64/ld-linux-x86-64.so.2 (0x00007fdbde026000)

     

       78
       +
       ```

     

       79
       +
       

     

       80
       +
       Loading in toplevel

     

       81
       +
       -------------------

     

       82
       +
       

     

       83
       +
       It is also possible to use the built libraries in toplevel and use

     

       84
       +
       them in ocaml scripts, e.g.,

     

       85
       +
       ```

     

       86
       +
       $ ocaml

     

       87
       +
               OCaml version 4.09.0

     

       88
       +
       

     

       89
       +
        # #use "topfind";;

     

       90
       +
        - : unit = ()

     

       91
       +
        Findlib has been successfully loaded. Additional directives:

     

       92
       +
         #require "package";;      to load a package

     

       93
       +
         #list;;                   to list the available packages

     

       94
       +
         #camlp4o;;                to load camlp4 (standard syntax)

     

       95
       +
         #camlp4r;;                to load camlp4 (revised syntax)

     

       96
       +
         #predicates "p,q,...";;   to set these predicates

     

       97
       +
         Topfind.reset();;         to force that packages will be reloaded

     

       98
       +
         #thread;;                 to enable threads

     

       99
       +
       

     

       100
       +
       - : unit = ()

     

       101
       +
        # #require "z3";;

     

       102
       +
        /home/ivg/.opam/4.09.0/lib/zarith: added to search path

     

       103
       +
        /home/ivg/.opam/4.09.0/lib/zarith/zarith.cma: loaded

     

       104
       +
        /home/ivg/.opam/4.09.0/lib/z3: added to search path

     

       105
       +
        /home/ivg/.opam/4.09.0/lib/z3/z3ml.cma: loaded

     

       106
       +
        #

     

       107
       +
       ```

     

       108
       +
       

     

       109
       +
       To use z3 in a script mode add the following preamble to a file with

     

       110
       +
       OCaml code:

     

       111
       +
       ```

     

       112
       +
         #!/usr/bin/env ocaml

     

       113
       +
         #use "topfind";;

     

       114
       +
         #require "z3";;

     

       115
       +
       

     

       116
       +
         (* your OCaml code *)

     

       117
       +
       ```

     

       118
       +
       

     

       119
       +
       Then it is possible to run it as `./script` (provided that the code is

     

       120
       +
       in a file named `script` and permissions are set with `chmod a+x

     

       121
       +
       script`).

     

       122
       +
       

     

       123
       +
       Of course, such scripts will depend on ocaml installation that shall

     

       124
       +
       have z3 dependencies installed.

     

       125
       +
       

     

       126
       +
       Using Dynlink

     

       127
       +
       -------------

     

       128
       +
       

     

       129
       +
       The built z3ml.cmxs file is a self-contained shared library that

     

       130
       +
       doesn't have any depndencies on z3 (the z3 code is included in it) and

     

       131
       +
       could be loaded with `Dynlink.loadfile` in runtime.

     

       132
       +
       

     

       133
       +
       Installation

     

       134
       +
       ============

     

       135
       +
       

     

       136
       +
       I did not touch the installation part in this PR, as I was using opam

     

       137
       +
       and installed artifacts as simple as:

     

       138
       +
       ```

     

       139
       +
       ocamlfind install z3 build/api/ml/* build/libz3-static.a

     

       140
       +
       ```

     

       141
       +
       

     

       142
       +
       assuming that the following configuration and building process

     

       143
       +
       ```

     

       144
       +
       python2.7 scripts/mk_make.py --ml --staticlib

     

       145
       +
       make -C build

     

       146
       +
       ```

     

       147
       +
       

     

       148
       +
       Though the default installation script in the make file shall work.

     

       149
       +
       

     

       150
       +
       Dynamic Library mode

     

       151
       +
       ====================

     

       152
       +
       

     

       153
       +
       The dynamic library mode is also supported provided that libz3.so is

     

       154
       +
       installed in a search path of the dynamic loader (or the location is

     

       155
       +
       added via the LD_LIBRARY_PATH) or stored in rpaths of the built

     

       156
       +
       binary.

     

       157
       +
       

     

       158
       +
       Build Artifacts

     

       159
       +
       ===============

     

       160
       +
       

     

       161
       +
       In the static mode (--staticlib), the following files are built and

     

       162
       +
       installed:

     

       163
       +
       

     

       164
       +
       - `{z3,z3enums,z3native}.{cmi,cmo,cmx,o,mli}`: the three compilation

     

       165
       +
       units (modules) that comprise Z3 bindings. The `*.mli` files are not

     

       166
       +
       necessary but are installed for the user convenience and documentation

     

       167
       +
       purposes. The *.cmi files enables access to the unit

     

       168
       +
       definitions. Finally, `*.cmo` contain the bytecode and `*.cmx, *.o`

     

       169
       +
       contain the native code. Files with the code are necessary for cross-module

     

       170
       +
       optimization but are not strictly needed as the code is also

     

       171
       +
       duplicated in the libraries.

     

       172
       +
       

     

       173
       +
       - libz3-static.a (OR libz3.so if built not in the staticlib mode)

     

       174
       +
       contains the machine code of the Z3 library;

     

       175
       +
       

     

       176
       +
       - z3ml.{a,cma,cmxa,cmxs} - the OCaml code for the bindings. File

     

       177
       +
       z3ml.a and z3ml.cmxa are static libraries with OCaml native code,

     

       178
       +
       which will be included in the final binary when ocamlopt is used. The

     

       179
       +
       z3 library code itself is not included in those three artifacts, but

     

       180
       +
       the instructions where to find it are. The same is truce for `z3ml.a`

     

       181
       +
       which includes the bytecode of the bindings as well as instructions

     

       182
       +
       how to link the final product. Finally, `z3ml.cmxs` is a standalone

     

       183
       +
       shared library that could be loaded in runtime use

     

       184
       +
       `Dynlink.loadfile` (which used dlopen on posix machines underneath the

     

       185
       +
       hood).

     

       186
       +
       

     

       187
       +
       - libz3ml.a is the archived machine code for `z3native_stubs.c`, which

     

       188
       +
       is made by ocamlmklib: `ar rcs api/ml/libz3ml.a

     

       189
       +
       api/ml/z3native_stubs.o` it is needed to build statically linked

     

       190
       +
       binaries and libraries that use z3 bindings.

     

       191
       +
       

     

       192
       +
       - dllz3ml.so is the shared object that contains `z3native_stubs.o` as

     

       193
       +
       well as correct ldd entries for C++ and Z3 libraries to enable proper

     

       194
       +
       static and dynamic linking. The file is built with ocamlmklib on posix

     

       195
       +
       systems as

     

       196
       +
       ```

     

       197
       +
       gcc -shared -o api/ml/dllz3ml.so api/ml/z3native_stubs.o -L. -lz3-static -lstdc++

     

       198
       +
       ```

     

       199
       +
       

     

       200
       +
       It is used by `ocaml`, `ocamlrun`, and `ocamlc` to link z3 and c++

     

       201
       +
       code into the OCaml runtime and enables usage of z3 bindings in

     

       202
       +
       non-custom runtimes (default runtimes).

     

       203
       +
       

     

       204
       +
       The `dllz3ml.so` is usually installed in the stubs library in opam

     

       205
       +
       installation (`$(opam config var lib)/stublibs`), it is done

     

       206
       +
       automatically by `ocamlfind` so no special treatment is needed.

     

       207
       +
       

     

       208
       +
       Technical Details

     

       209
       +
       =================

     

       210
       +
       

     

       211
       +
       The patch itself is rather small. First of all, we have to use

     

       212
       +
       `-l<lib>` instead of `-cclib -l<lib>` in ocamlmklib since the latter

     

       213
       +
       will pass the options only to the ocaml{c,opt} linker and will not

     

       214
       +
       use the passed libraries when shared and non-shared versions of the

     

       215
       +
       bindings are built (libz3ml.a and dllz3ml.so). They were both missing

     

       216
       +
       either z3 code itself and ldd entries for stdc++ (and z3 if built not

     

       217
       +
       in --staticlib mode).

     

       218
       +
       

     

       219
       +
       Having stdc++ entry streamlines the compilation process and makes

     

       220
       +
       dynamic loading more resistant to the inclusion order.

     

       221
       +
       

     

       222
       +
       Finally, we had to add `-L.` to make sure that the built artifacts are

     

       223
       +
       correctly found by gcc.

     

       224
       +
       

     

       225
       +
       I specifically left the cygwin part of the code intact as I have no

     

       226
       +
       idea what the original author meant by this, neither do I use or

     

       227
       +
       tested this patch in the cygwin or mingw environemt. I think that this

     

       228
       +
       code is rather outdated and shouldn't really work. E.g., in the

     

       229
       +
       --staticlib mode adding z3linkdep (which is libz3-static.a) as an

     

       230
       +
       argument to `ocamlmklib` will yield the following broken archive

     

       231
       +
       ```

     

       232
       +
       ar rcs api/ml/libz3ml.a libz3-static.a api/ml/z3native_stubs.o

     

       233
       +
       ```

     

       234
       +
       and it is not allowed (or supported) to have .a in archives (though it

     

       235
       +
       doesn't really hurt as most of the systems will just ignore it).

     

       236
       +
       

     

       237
       +
       But otherwise, cygwin, mingw shall behave as they did (the only change

     

       238
       +
       that affects them is `-L.` which I believe should be benign).

     

       239
       +
       ---

     

       240
       +
        scripts/mk_util.py | 6 +++---

     

       241
       +
        1 file changed, 3 insertions(+), 3 deletions(-)

     

       242
       +
       

     

       243
       +
       diff --git a/scripts/mk_util.py b/scripts/mk_util.py

     

       244
       +
       index 1a95ee20c3..156be9ca2f 100644

     

       245
       +
       --- a/scripts/mk_util.py

     

       246
       +
       +++ b/scripts/mk_util.py

     

       247
       +
       @@ -1957,7 +1957,7 @@ def mk_makefile(self, out):

     

       248
       +
        

     

       249
       +
                    OCAMLMKLIB = 'ocamlmklib'

     

       250
       +
        

     

       251
       +
       -            LIBZ3 = '-cclib -l' + z3link

     

       252
       +
       +            LIBZ3 = '-l' + z3link + ' -lstdc++'

     

       253
       +
                    if is_cygwin() and not(is_cygwin_mingw()):

     

       254
       +
                        LIBZ3 = z3linkdep

     

       255
       +
        

     

       256
       +
       @@ -1970,9 +1970,9 @@ def mk_makefile(self, out):

     

       257
       +
                    z3mls = os.path.join(self.sub_dir, 'z3ml')

     

       258
       +
        

     

       259
       +
                    out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3linkdep))

     

       260
       +
       -            out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos, LIBZ3))

     

       261
       +
       +            out.write('\t%s -o %s -I %s -L. %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos, LIBZ3))

     

       262
       +
                    out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3linkdep, z3mls))

     

       263
       +
       -            out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3))

     

       264
       +
       +            out.write('\t%s -o %s -I %s -L. %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3))

     

       265
       +
                    out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))

     

       266
       +
                    out.write('\t%s -linkall -shared -o %s.cmxs -I . -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))

     

       267
       +

+37

packages/z3/z3.4.8.5-1/opam

···

       1
       +
       opam-version: "2.0"

     

       2
       +
       maintainer: "simon@aestheticintegration.com"

     

       3
       +
       authors: "MSR"

     

       4
       +
       homepage: "https://github.com/Z3prover/z3"

     

       5
       +
       bug-reports: "https://github.com/Z3prover/z3/issues"

     

       6
       +
       license: "MIT"

     

       7
       +
       dev-repo: "git+https://github.com/Z3prover/z3.git"

     

       8
       +
       patches: ["4468.patch"]

     

       9
       +
       depexts: [

     

       10
       +
         ["python3-distutils"] {os-family = "debian"}

     

       11
       +
       ]

     

       12
       +
       build: [

     

       13
       +
         [ "python3" "scripts/mk_make.py" "--ml" "--staticlib" ]

     

       14
       +
         [ make "-C" "build" "-j" jobs ]

     

       15
       +
       ]

     

       16
       +
       install: [

     

       17
       +
         [ "sh" "-c" "ocamlfind install z3 build/api/ml/* build/libz3-static.a"]

     

       18
       +
         [ "cp" "build/z3" "%{bin}%/z3"]

     

       19
       +
       ]

     

       20
       +
       

     

       21
       +
       depends: [

     

       22
       +
         "ocaml" {< "5.0"}

     

       23
       +
         "ocamlfind" {build}

     

       24
       +
         "num"

     

       25
       +
         "conf-gmp"

     

       26
       +
         "conf-python-3" {build}

     

       27
       +
         "conf-c++" {build}

     

       28
       +
       ]

     

       29
       +
       synopsis: "Z3 solver"

     

       30
       +
       extra-files: [

     

       31
       +
         ["4468.patch" "sha512=5fdf023a793f857d79497ad0c68b2a55b7ec0e14243cfd1874b3dd0ee09538bf46bedf39caf8380deb85a2f6d06472fa982faa1e4cc9ec9c8b88291cbf97ab5e"]

     

       32
       +
       ]

     

       33
       +
       

     

       34
       +
       url {

     

       35
       +
         src: "https://github.com/Z3Prover/z3/archive/Z3-4.8.5.tar.gz"

     

       36
       +
         checksum: "sha512=ca36e1a0332bd473a64f41dfdb31656fb3486178473e4fd4934dccce109a84c9686c08f94998df74bacb588eb12ea5db25dc17a564ee76f82fd2559349697309"

     

       37
       +
       }