3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Find a file
Ivan Gotovchits 24a9ca3226
fixes numerous issues in OCaml bindings building process (#4468)
It now works both in dynamic and static mode and the compiled
libraries can be used by all linkers in the OCaml system, without
any specificy instructions other than specifying the dependency on
the z3 library.

Using the libraries
===================

Compiling binaries
------------------

The libraries can be linked statically with both ocamlc and ocamlopt
compilers, e.g.,

```
ocamlfind ocamlc -thread -package z3 -linkpkg run.ml -o run
```
or
```
ocamlfind ocamlopt -thread -package z3 -linkpkg run.ml -o run
```

When bindings compiled with the `--staticlib` the produced binary will
not have any dependencies on z3
```
$ ldd ./run
        linux-vdso.so.1 (0x00007fff9c9ed000)
        libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fb56f09c000)
        libgmp.so.10 => /usr/lib/x86_64-linux-gnu/libgmp.so.10 (0x00007fb56ee1b000)
        libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fb56ebfc000)
        libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fb56e85e000)
        libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fb56e65a000)
        libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fb56e442000)
        libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fb56e051000)
        /lib64/ld-linux-x86-64.so.2 (0x00007fb570de9000)
```

The bytecode version will have a depedency on z3 and other external
libraries (packed as dlls and usually installed in opam switch):
```
$ ocamlobjinfo run | grep 'Used DLL' -A5
Used DLLs:
        dllz3ml
        dllzarith
        dllthreads
        dllunix
```

But it is possible to compile a portable self-contained version of the
bytecode executable using the `-custom` switch:

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

The build binary is now quite large but doesn't have any external
dependencies (modulo the system dependencies):
```
$ du -h run
27M     run
$ ocamlobjinfo run | grep 'Used DLL' | wc -l
0
$ ldd run
        linux-vdso.so.1 (0x00007ffee42c2000)
        libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fdbdc415000)
        libgmp.so.10 => /usr/lib/x86_64-linux-gnu/libgmp.so.10 (0x00007fdbdc194000)
        libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fdbdbf75000)
        libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fdbdbbd7000)
        libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fdbdb9d3000)
        libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fdbdb7bb000)
        libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fdbdb3ca000)
        /lib64/ld-linux-x86-64.so.2 (0x00007fdbde026000)
```

Loading in toplevel
-------------------

It is also possible to use the built libraries in toplevel and use
them in ocaml scripts, e.g.,
```
$ ocaml
        OCaml version 4.09.0

 # #use "topfind";;
 - : unit = ()
 Findlib has been successfully loaded. Additional directives:
  #require "package";;      to load a package
  #list;;                   to list the available packages
  #camlp4o;;                to load camlp4 (standard syntax)
  #camlp4r;;                to load camlp4 (revised syntax)
  #predicates "p,q,...";;   to set these predicates
  Topfind.reset();;         to force that packages will be reloaded
  #thread;;                 to enable threads

- : unit = ()
 # #require "z3";;
 /home/ivg/.opam/4.09.0/lib/zarith: added to search path
 /home/ivg/.opam/4.09.0/lib/zarith/zarith.cma: loaded
 /home/ivg/.opam/4.09.0/lib/z3: added to search path
 /home/ivg/.opam/4.09.0/lib/z3/z3ml.cma: loaded
 #
```

To use z3 in a script mode add the following preamble to a file with
OCaml code:
```
  #!/usr/bin/env ocaml
  #use "topfind";;
  #require "z3";;

  (* your OCaml code *)
```

Then it is possible to run it as `./script` (provided that the code is
in a file named `script` and permissions are set with `chmod a+x
script`).

Of course, such scripts will depend on ocaml installation that shall
have z3 dependencies installed.

Using Dynlink
-------------

The built z3ml.cmxs file is a self-contained shared library that
doesn't have any depndencies on z3 (the z3 code is included in it) and
could be loaded with `Dynlink.loadfile` in runtime.

Installation
============

I did not touch the installation part in this PR, as I was using opam
and installed artifacts as simple as:
```
ocamlfind install z3 build/api/ml/* build/libz3-static.a
```

assuming that the following configuration and building process
```
python2.7 scripts/mk_make.py --ml --staticlib
make -C build
```

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

Dynamic Library mode
====================

The dynamic library mode is also supported provided that libz3.so is
installed in a search path of the dynamic loader (or the location is
added via the LD_LIBRARY_PATH) or stored in rpaths of the built
binary.

Build Artifacts
===============

In the static mode (--staticlib), the following files are built and
installed:

- `{z3,z3enums,z3native}.{cmi,cmo,cmx,o,mli}`: the three compilation
units (modules) that comprise Z3 bindings. The `*.mli` files are not
necessary but are installed for the user convenience and documentation
purposes. The *.cmi files enables access to the unit
definitions. Finally, `*.cmo` contain the bytecode and `*.cmx, *.o`
contain the native code. Files with the code are necessary for cross-module
optimization but are not strictly needed as the code is also
duplicated in the libraries.

- libz3-static.a (OR libz3.so if built not in the staticlib mode)
contains the machine code of the Z3 library;

- z3ml.{a,cma,cmxa,cmxs} - the OCaml code for the bindings. File
z3ml.a and z3ml.cmxa are static libraries with OCaml native code,
which will be included in the final binary when ocamlopt is used. The
z3 library code itself is not included in those three artifacts, but
the instructions where to find it are. The same is truce for `z3ml.a`
which includes the bytecode of the bindings as well as instructions
how to link the final product. Finally, `z3ml.cmxs` is a standalone
shared library that could be loaded in runtime use
`Dynlink.loadfile` (which used dlopen on posix machines underneath the
hood).

- libz3ml.a is the archived machine code for `z3native_stubs.c`, which
is made by ocamlmklib: `ar rcs api/ml/libz3ml.a
api/ml/z3native_stubs.o` it is needed to build statically linked
binaries and libraries that use z3 bindings.

- dllz3ml.so is the shared object that contains `z3native_stubs.o` as
well as correct ldd entries for C++ and Z3 libraries to enable proper
static and dynamic linking. The file is built with ocamlmklib on posix
systems as
```
gcc -shared -o api/ml/dllz3ml.so api/ml/z3native_stubs.o -L. -lz3-static -lstdc++
```

It is used by `ocaml`, `ocamlrun`, and `ocamlc` to link z3 and c++
code into the OCaml runtime and enables usage of z3 bindings in
non-custom runtimes (default runtimes).

The `dllz3ml.so` is usually installed in the stubs library in opam
installation (`$(opam config var lib)/stublibs`), it is done
automatically by `ocamlfind` so no special treatment is needed.

Technical Details
=================

The patch itself is rather small. First of all, we have to use
`-l<lib>` instead of `-cclib -l<lib>` in ocamlmklib since the latter
will pass the options only to the ocaml{c,opt} linker and will not
use the passed libraries when shared and non-shared versions of the
bindings are built (libz3ml.a and dllz3ml.so). They were both missing
either z3 code itself and ldd entries for stdc++ (and z3 if built not
in --staticlib mode).

Having stdc++ entry streamlines the compilation process and makes
dynamic loading more resistant to the inclusion order.

Finally, we had to add `-L.` to make sure that the built artifacts are
correctly found by gcc.

I specifically left the cygwin part of the code intact as I have no
idea what the original author meant by this, neither do I use or
tested this patch in the cygwin or mingw environemt. I think that this
code is rather outdated and shouldn't really work. E.g., in the
--staticlib mode adding z3linkdep (which is libz3-static.a) as an
argument to `ocamlmklib` will yield the following broken archive
```
ar rcs api/ml/libz3ml.a libz3-static.a api/ml/z3native_stubs.o
```
and it is not allowed (or supported) to have .a in archives (though it
doesn't really hurt as most of the systems will just ignore it).

But otherwise, cygwin, mingw shall behave as they did (the only change
that affects them is `-L.` which I believe should be benign).
2020-05-27 09:21:14 -07:00
cmake regex pattern per #2986 2020-02-14 17:51:31 -10:00
contrib remove support for decade old ubuntu 14. keep support for 16, 18, 20 LTS 2020-05-23 18:02:34 +01:00
doc align readme-cmake and cmakelists.txt according to current state #2732 2019-11-23 15:59:16 -08:00
examples translate optimize from c++ API #2859 2020-01-15 04:24:51 -08:00
noarch follow instructions from #1879 2018-10-15 11:44:47 -07:00
resources Publishing SNK file private key for reproducible builds 2019-11-18 12:24:39 -08:00
scripts fixes numerous issues in OCaml bindings building process (#4468) 2020-05-27 09:21:14 -07:00
src change to iterative unfolding left build broken for some time 2020-05-26 21:25:53 -07:00
.dockerignore [TravisCI] Implement TravisCI build and testing infrastructure for Linux 2017-07-01 11:51:30 +01:00
.gitattributes set text default to auto to try to avoid crlf disasters 2014-04-01 17:20:37 -07:00
.gitignore ignore my shortcut 2020-05-12 09:10:40 -07:00
.travis.yml remove support for decade old ubuntu 14. keep support for 16, 18, 20 LTS 2020-05-23 18:02:34 +01:00
azure-pipelines.yml remove test-examples from MacOS build, re-add maxsat example 2020-05-19 13:52:44 -07:00
CMakeLists.txt Add pkg-config file (#4368) 2020-05-21 09:10:41 -07:00
configure restore exec bit on configure & scripts/*.sh 2020-05-16 20:07:36 +01:00
LICENSE.txt update license for space/quotes per #982 2017-04-24 13:34:10 -07:00
README-CMake.md updated readme for VS and CMake integration 2019-11-27 09:17:48 -08:00
README.md Update README with infos about Julia bindings (#4298) 2020-05-12 19:34:47 -07:00
RELEASE_NOTES updated release notes 2020-05-05 10:33:25 -07:00
z3.pc.cmake.in Add pkg-config file (#4368) 2020-05-21 09:10:41 -07:00

Z3

Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license.

If you are not familiar with Z3, you can start here.

Pre-built binaries for stable and nightly releases are available from here.

Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for several programming languages.

See the release notes for notes on various stable releases of Z3.

Build status

Azure Pipelines TravisCI
Build Status Build Status

Building Z3 on Windows using Visual Studio Command Prompt

32-bit builds, start with:

python scripts/mk_make.py

or instead, for a 64-bit build:

python scripts/mk_make.py -x

then:

cd build
nmake

Building Z3 using make and GCC/Clang

Execute:

python scripts/mk_make.py
cd build
make
sudo make install

Note by default g++ is used as the C++ compiler if it is available. If you would prefer to use Clang change the mk_make.py invocation to:

CXX=clang++ CC=clang python scripts/mk_make.py

Note that Clang < 3.7 does not support OpenMP.

You can also build Z3 for Windows using Cygwin and the Mingw-w64 cross-compiler. To configure that case correctly, make sure to use Cygwin's own python and not some Windows installation of Python.

For a 64 bit build (from Cygwin64), configure Z3's sources with

CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.py

A 32 bit build should work similarly (but is untested); the same is true for 32/64 bit builds from within Cygwin32.

By default, it will install z3 executable at PREFIX/bin, libraries at PREFIX/lib, and include files at PREFIX/include, where PREFIX installation prefix if inferred by the mk_make.py script. It is usually /usr for most Linux distros, and /usr/local for FreeBSD and macOS. Use the --prefix= command line option to change the install prefix. For example:

python scripts/mk_make.py --prefix=/home/leo
cd build
make
make install

To uninstall Z3, use

sudo make uninstall

To clean Z3 you can delete the build directory and run the mk_make.py script again.

Building Z3 using CMake

Z3 has a build system using CMake. Read the README-CMake.md file for details. It is recommended for most build tasks, except for building OCaml bindings.

Z3 bindings

Z3 has bindings for various programming languages.

.NET

You can install a nuget package for the latest release Z3 from nuget.org.

Use the --dotnet command line flag with mk_make.py to enable building these.

On non-windows platforms mono is required. On these platforms the location of the C# compiler and gac utility need to be known. You can set these as follows if they aren't detected automatically. For example:

CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py --dotnet

Note for very old versions of Mono (e.g. 2.10) you may need to set CSC to /usr/bin/dmcs.

Note that when make install is executed on non-windows platforms the GAC utility is used to install Microsoft.Z3.dll into the GAC as the Microsoft.Z3.Sharp package. During install a pkg-config file (Microsoft.Z3.Sharp.pc) is also installed which allows the MonoDevelop IDE to find the bindings. Running make uninstall will remove the dll from the GAC and the pkg-config file.

See examples/dotnet for examples.

C

These are always enabled.

See examples/c for examples.

C++

These are always enabled.

See examples/c++ for examples.

Java

Use the --java command line flag with mk_make.py to enable building these.

See examples/java for examples.

OCaml

Use the --ml command line flag with mk_make.py to enable building these.

See examples/ml for examples.

Python

You can install the Python wrapper for Z3 for the latest release from pypi using the command

   pip install z3-solver

Use the --python command line flag with mk_make.py to enable building these.

Note that is required on certain platforms that the Python package directory (site-packages on most distributions and dist-packages on Debian based distributions) live under the install prefix. If you use a non standard prefix you can use the --pypkgdir option to change the Python package directory used for installation. For example:

python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages

If you do need to install to a non standard prefix a better approach is to use a Python virtual environment and install Z3 there. Python packages also work for Python3. Under Windows, recall to build inside the Visual C++ native command build environment. Note that the build/python/z3 directory should be accessible from where python is used with Z3 and it depends on libz3.dll to be in the path.

virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# You will find Z3 and the Python bindings installed in the virtual environment
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...

See examples/python for examples.

Julia

The Julia package Z3.jl wraps the C++ API of Z3. Information about updating and building the Julia bindings can be found in src/api/julia.

Web Assembly

WebAssembly bindings are provided by Clément Pit-Claudel.

System Overview

System Diagram

Interfaces