3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

Merge pull request #379 from wintersteiger/new_ocaml_install

New ocaml install
This commit is contained in:
Christoph M. Wintersteiger 2015-12-14 16:45:36 +00:00
commit aa7ce540e8
7 changed files with 148 additions and 149 deletions

View file

@ -1,22 +1,23 @@
Small example using the Z3 ML bindings.
To build the example execute
make examples
in the build directory.
It will create ml_example in the build directory,
which can be run in the build directory via
This will create ml_example and ml_example.byte in the build directory, which
can be run in the build directory by calling
LD_LIBRARY_PATH=. ./ml_example
or
LD_LIBRARY_PATH=. ./ml_example.byte
for the byte-code version.
If Z3 was installed into the ocamlfind package repository (see src/api/ml/README),
then we can compile this example as follows:
If Z3 was installed into the ocamlfind package repository (see
src/api/ml/README), then we can also compile this example as follows:
ocamlfind ocamlc -o ml_example.byte -package Z3 -linkpkg ml_example.ml
or
ocamlfind ocamlopt -o ml_example -package Z3 -linkpkg ml_example.ml
Note that the resulting binaries depend on the shared z3 library, which needs to be
in the PATH (Windows), LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX). If Z3 was
installed into ocamlfind, the path that should be added is
`ocamlfind printconf destdir`/Z3
Note that the resulting binaries depend on the shared z3 library
(libz3.dll/.so/.dylb), which needs to be in the PATH (Windows), LD_LIBRARY_PATH
(Linux), or DYLD_LIBRARY_PATH (OSX).

View file

@ -1740,146 +1740,112 @@ class MLComponent(Component):
lib_name = name
self.lib_name = lib_name
self.modules = ["z3enums", "z3native", "z3"] # dependencies in this order!
self.stubs = "z3native_stubs"
self.sub_dir = os.path.join('api', 'ml')
def mk_ml_meta(self, ml_meta_in, ml_meta_out, major, minor, build, revision):
ver_pat = re.compile('version = "VERSION"*')
fin = open(ml_meta_in, 'r')
fout = open(ml_meta_out, 'w')
num_updates = 0
for line in fin:
if ver_pat.match(line):
fout.write('version = "%s.%s.%s.%s"\n' % (major, minor, build, revision))
num_updates = num_updates + 1
else:
fout.write(line)
assert num_updates == 1, "unexpected number of version number updates"
fin.close()
fout.close()
if VERBOSE:
print("Updated '%s'" % ml_meta_out)
def mk_makefile(self, out):
if is_ml_enabled():
CP_CMD = "cp"
if IS_WINDOWS:
CP_CMD = "copy"
src_dir = self.to_src_dir
mk_dir(os.path.join(BUILD_DIR, self.sub_dir))
api_src = get_component(API_COMPONENT).to_src_dir
out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n') # remove /GL; the ocaml tools don't like it.
for f in filter(lambda f: f.endswith('.ml'), os.listdir(self.src_dir)):
out.write('%s: %s\n' % (os.path.join(self.sub_dir,f),os.path.join(src_dir,f)))
str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(self.sub_dir,f))
out.write(str)
for f in filter(lambda f: f.endswith('.mli'), os.listdir(self.src_dir)):
out.write('%s: %s\n' % (os.path.join(self.sub_dir,f),os.path.join(src_dir,f)))
str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(self.sub_dir,f))
out.write(str)
for f in filter(lambda f: f.endswith('.c'), os.listdir(self.src_dir)):
out.write('%s: %s\n' % (os.path.join(self.sub_dir,f),os.path.join(src_dir,f)))
str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(self.sub_dir,f))
out.write(str)
mls = ''
if IS_WINDOWS:
prefix_lib = '-L' + os.path.abspath(BUILD_DIR).replace('\\', '\\\\')
else:
prefix_lib = '-L' + PREFIX + '/lib'
substitutions = { 'LEXTRA': prefix_lib,
'VERSION': "{}.{}.{}.{}".format(VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION) }
configure_file(os.path.join(self.src_dir, 'META.in'),
os.path.join(BUILD_DIR, self.sub_dir, 'META'),
substitutions)
mlis = ''
for m in self.modules:
mlis = os.path.join(src_dir, m) + '.mli ' + mlis
stubsc = os.path.join(src_dir, self.stubs + '.c')
stubso = os.path.join(self.sub_dir, self.stubs) + '$(OBJ_EXT)'
z3dllso = get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT)'
out.write('%s: %s %s\n' % (stubso, stubsc, z3dllso))
out.write('\t%s -ccopt "$(CXXFLAGS_OCAML) -I %s -I %s -I %s $(CXX_OUT_FLAG)%s" -c %s\n' %
(OCAMLC, OCAML_LIB, api_src, src_dir, stubso, stubsc))
cmis = ''
archives = ''
for m in self.modules:
fn = os.path.join(self.src_dir, ('%s.mli' % m))
if not os.path.exists(fn):
out.write('%s.mli: %s.ml%s\n' % (os.path.join(self.sub_dir,m),os.path.join(self.sub_dir,m),mlis))
out.write('\t%s -I %s -i -c %s.ml > %s.mli\n' % (OCAMLC,self.sub_dir,os.path.join(self.sub_dir, m),os.path.join(self.sub_dir, m)))
out.write('%s.cmi: %s.mli%s\n' % (os.path.join(self.sub_dir,m),os.path.join(self.sub_dir,m), cmis))
out.write('\t%s -I %s -c %s.mli\n' % (OCAMLC,self.sub_dir,os.path.join(self.sub_dir,m)))
out.write('%s.cma: %s.ml %s.cmi%s\n' % (os.path.join(self.sub_dir,m),os.path.join(self.sub_dir,m),os.path.join(self.sub_dir,m), archives))
out.write('\t%s -a -o %s.ml -o %s.cma\n' % (OCAMLC,os.path.join(self.sub_dir,m), os.path.join(self.sub_dir,m)))
mlis = mlis + ' ' + os.path.join(self.sub_dir, m) + '.mli'
cmis = cmis + ' ' + os.path.join(self.sub_dir,m) + '.cmi'
archives = archives + ' ' + os.path.join(self.sub_dir,m) + '.cma'
mls = mls + ' ' + os.path.join(self.sub_dir, m) + '.ml'
out.write('%s: %s %s\n' %
(os.path.join(self.sub_dir, 'z3native_stubs$(OBJ_EXT)'),
os.path.join(self.sub_dir, 'z3native_stubs.c'),
get_component(Z3_DLL_COMPONENT).dll_name+'$(SO_EXT)'))
out.write('\t$(CC) $(CXXFLAGS_OCAML) -I %s -I %s %s $(CXX_OUT_FLAG)%s$(OBJ_EXT)\n' %
(OCAML_LIB, api_src, os.path.join(self.sub_dir, 'z3native_stubs.c'), os.path.join(self.sub_dir, 'z3native_stubs')))
out.write('%s: %s %s %s$(SO_EXT)' % (
os.path.join(self.sub_dir, "z3ml.cmxa"),
cmis,
archives,
get_component(Z3_DLL_COMPONENT).dll_name))
out.write(' %s\n' % (os.path.join(self.sub_dir, 'z3native_stubs$(OBJ_EXT)')))
out.write('\tocamlmklib -custom -o %s -I %s -ldopt \"-L. -lz3\" ' % (os.path.join(self.sub_dir, 'z3ml'), self.sub_dir))
# Add ocamlfind destdir to rpath
if OCAMLFIND != '':
if is_verbose():
print ("Finding ocamlfind destdir")
t = TempFile('output')
null = open(os.devnull, 'wb')
try:
subprocess.call([OCAMLFIND, 'printconf', 'destdir'], stdout=t.fname, stderr=null)
t.commit()
except:
raise MKException('Failed to find Ocamlfind destdir')
t = open('output', 'r')
for line in t:
ocamlfind_destdir = line[:-1]
if is_verbose():
print ('ocamlfind destdir=%s' % ocamlfind_destdir)
t.close()
rmf('output')
# ML-specific DLLs are installed into stublibs if it exists, Z3 if not
if os.path.exists(os.path.join(ocamlfind_destdir, 'stublibs')):
dll_path = os.path.join(ocamlfind_destdir, 'stublibs')
else:
dll_path = os.path.join(ocamlfind_destdir, 'Z3')
out.write("-rpath %s " % dll_path)
out.write("-L%s" % dll_path)
#dllfile = '%s$(SO_EXT)' % self.dll_name
#dllInstallPath = os.path.join(INSTALL_LIB_DIR, dllfile)
ff = os.path.join(src_dir, m + '.mli')
ft = os.path.join(self.sub_dir, m + '.cmi')
out.write('%s: %s\n' % (ft, cmis))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLC, self.sub_dir, ft, ff))
cmis = cmis + ' ' + ft
cmos = ''
for m in self.modules:
out.write(' %s' % (os.path.join(self.sub_dir, m+'.ml')))
out.write(' %s\n' % (os.path.join(self.sub_dir, 'z3native_stubs$(OBJ_EXT)')))
out.write('ml: %s\n' % (os.path.join(self.sub_dir, 'z3ml.cmxa')))
self.mk_ml_meta(os.path.join('src/api/ml/META'), os.path.join(BUILD_DIR, self.sub_dir, 'META'), VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION)
ff = os.path.join(src_dir, m + '.ml')
ft = os.path.join(self.sub_dir, m + '.cmo')
fd = os.path.join(self.sub_dir, m + '.cmi')
out.write('%s: %s %s\n' % (ft, ff, fd))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLC, self.sub_dir, ft, ff))
cmos = cmos + ' ' + ft
cmxs = ''
for m in self.modules:
ff = os.path.join(src_dir, m + '.ml')
ft = os.path.join(self.sub_dir, m + '.cmx')
fd = os.path.join(self.sub_dir, m + '.cmi')
out.write('%s: %s %s\n' % (ft, ff, fd))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLOPT, self.sub_dir, ft, ff))
cmxs = cmxs + ' ' + ft
z3mls = os.path.join(self.sub_dir, 'z3ml')
out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3dllso))
out.write('\tocamlmklib -o %s -I %s %s %s -L. -lz3\n' % (z3mls, self.sub_dir, stubso, cmos))
out.write('%s.cmxa: %s %s %s\n' % (z3mls, cmxs, stubso, z3dllso))
out.write('\tocamlmklib -o %s -I %s %s %s -L. -lz3\n' % (z3mls, self.sub_dir, stubso, cmxs))
out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))
out.write('\t%s -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPT, z3mls, self.sub_dir, z3mls))
out.write('\n')
out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls))
out.write('\n')
if IS_WINDOWS:
out.write('ocamlfind_install: ')
self.mk_install_deps(out)
out.write('\n')
self.mk_install(out)
out.write('\n')
out.write('ocamlfind_uninstall:\n')
self.mk_uninstall(out)
out.write('\n')
def mk_install_deps(self, out):
if is_ml_enabled() and OCAMLFIND != '':
out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ')
out.write(os.path.join(self.sub_dir, 'z3ml.cmxa '))
out.write(os.path.join(self.sub_dir, 'META '))
out.write(os.path.join(self.sub_dir, 'z3ml.cma '))
out.write(os.path.join(self.sub_dir, 'z3ml.cmxa '))
out.write(os.path.join(self.sub_dir, 'z3ml.cmxs '))
def mk_install(self, out):
if is_ml_enabled() and OCAMLFIND != '':
out.write('\t@%s remove Z3\n' % (OCAMLFIND))
out.write('\t@%s install Z3 %s' % (OCAMLFIND, (os.path.join(self.sub_dir, 'META'))))
for m in self.modules:
out.write(' %s.cma' % (os.path.join(self.sub_dir, m)))
out.write(' %s.cmx' % (os.path.join(self.sub_dir, m)))
out.write(' %s.cmi' % (os.path.join(self.sub_dir, m)))
out.write(' %s.cmo' % (os.path.join(self.sub_dir, m)))
out.write(' %s.ml' % (os.path.join(self.sub_dir, m)))
out.write(' %s.mli' % (os.path.join(self.sub_dir, m)))
out.write(' %s$(OBJ_EXT)' % (os.path.join(self.sub_dir, m)))
out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli')
out.write(' ' + os.path.join(self.sub_dir, m) + '.cmi')
out.write(' %s' % ((os.path.join(self.sub_dir, 'libz3ml$(LIB_EXT)'))))
out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml$(LIB_EXT)'))))
out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cma'))))
out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxa'))))
out.write(' %s' % ((os.path.join(self.sub_dir, 'libz3ml$(LIB_EXT)'))))
#out.write(' %s' % ((os.path.join(self.sub_dir, 'dllz3ml'))))
#if IS_WINDOWS:
# out.write('.dll')
#else:
# out.write('.so') # .so also on OSX!
#out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT)')
# if IS_WINDOWS:
# out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(LIB_EXT)')
out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxs'))))
out.write(' %s' % ((os.path.join(self.sub_dir, 'dllz3ml'))))
if IS_WINDOWS:
out.write('.dll')
else:
out.write('.so') # .so also on OSX!
out.write('\n')
def mk_uninstall(self, out):
@ -2009,18 +1975,18 @@ class MLExampleComponent(ExampleComponent):
def mk_makefile(self, out):
if ML_ENABLED:
out.write('ml_example.byte: api/ml/z3ml.cmxa ')
out.write('ml_example.byte: api/ml/z3ml.cma')
for mlfile in get_ml_files(self.ex_dir):
out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
out.write('\n')
out.write('\t%s ' % OCAMLC)
if DEBUG_MODE:
out.write('-g ')
out.write('-o ml_example.byte -I api/ml -cclib "-L. -lz3" nums.cma z3ml.cma')
out.write('-custom -o ml_example.byte -I api/ml -cclib "-L. -lz3" nums.cma z3ml.cma')
for mlfile in get_ml_files(self.ex_dir):
out.write(' %s/%s' % (self.to_ex_dir, mlfile))
out.write('\n')
out.write('ml_example$(EXE_EXT): api/ml/z3ml.cmxa ml_example.byte')
out.write('ml_example$(EXE_EXT): api/ml/z3ml.cmxa')
for mlfile in get_ml_files(self.ex_dir):
out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
out.write('\n')
@ -3713,4 +3679,3 @@ if __name__ == '__main__':
import doctest
doctest.testmod()

View file

@ -1305,7 +1305,8 @@ def mk_ml():
ml_wrapper.write('#ifdef __cplusplus\n')
ml_wrapper.write('}\n')
ml_wrapper.write('#endif\n\n')
ml_wrapper.write('#include <z3.h>\n\n')
ml_wrapper.write('#include <z3.h>\n')
ml_wrapper.write('#include <z3native_stubs.h>\n\n')
ml_wrapper.write('#define CAMLlocal6(X1,X2,X3,X4,X5,X6) \\\n')
ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLlocal1(X6) \n')
@ -1345,11 +1346,11 @@ def mk_ml():
ml_wrapper.write('#ifdef __cplusplus\n')
ml_wrapper.write('extern "C" {\n')
ml_wrapper.write('#endif\n\n')
ml_wrapper.write('CAMLprim value n_is_null(value p) {\n')
ml_wrapper.write('CAMLprim DLL_PUBLIC value n_is_null(value p) {\n')
ml_wrapper.write(' void * t = * (void**) Data_custom_val(p);\n')
ml_wrapper.write(' return Val_bool(t == 0);\n')
ml_wrapper.write('}\n\n')
ml_wrapper.write('CAMLprim value n_mk_null( void ) {\n')
ml_wrapper.write('CAMLprim DLL_PUBLIC value n_mk_null( void ) {\n')
ml_wrapper.write(' CAMLparam0();\n')
ml_wrapper.write(' CAMLlocal1(result);\n')
ml_wrapper.write(' void * z3_result = 0;\n')
@ -1363,7 +1364,7 @@ def mk_ml():
ml_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n')
ml_wrapper.write(' // wrappers below.\n')
ml_wrapper.write('}\n\n')
ml_wrapper.write('void n_set_internal_error_handler(value a0)\n')
ml_wrapper.write('void DLL_PUBLIC n_set_internal_error_handler(value a0)\n')
ml_wrapper.write('{\n')
ml_wrapper.write(' Z3_context _a0 = * (Z3_context*) Data_custom_val(a0);\n')
ml_wrapper.write(' Z3_set_error_handler(_a0, MLErrorHandler);\n')
@ -1377,7 +1378,7 @@ def mk_ml():
ret_size = ret_size + 1
# Setup frame
ml_wrapper.write('CAMLprim value n_%s(' % ml_method_name(name))
ml_wrapper.write('CAMLprim DLL_PUBLIC value n_%s(' % ml_method_name(name))
first = True
i = 0
for p in params:
@ -1519,7 +1520,7 @@ def mk_ml():
ml_wrapper.write(' CAMLreturn(result);\n')
ml_wrapper.write('}\n\n')
if len(ip) > 5:
ml_wrapper.write('CAMLprim value n_%s_bytecode(value * argv, int argn) {\n' % ml_method_name(name))
ml_wrapper.write('CAMLprim DLL_PUBLIC value n_%s_bytecode(value * argv, int argn) {\n' % ml_method_name(name))
ml_wrapper.write(' return n_%s(' % ml_method_name(name))
i = 0
while i < len(ip):

View file

@ -1,11 +1,11 @@
# META file for the "z3" package:
version = "VERSION"
version = "@VERSION@"
description = "Z3 Theorem Prover (OCaml API)"
requires = "num"
archive(byte) = "z3ml.cma"
archive(native) = "z3ml.cmxa"
archive(byte,plugin) = "z3ml.cma"
archive(native,plugin) = "z3ml.cmxa"
archive(native,plugin) = "z3ml.cmxs"
archive(byte,toploop) = "z3ml.cma"
archive(native,toploop) = "z3ml.cmxa"
linkopts = "-cclib -lz3"
linkopts = "-cclib @LEXTRA@"

View file

@ -1,10 +0,0 @@
# This is a temporary support file for emacs annotations.
# It does not compile the Z3 ML API; this will be built
# in the top-level build directory.
all:
ocamlbuild -cflag -annot z3.cmxa
doc: *.ml
mkdir -p doc
ocamldoc -html -d doc -I _build -sort *.mli -hide Z3

View file

@ -4,8 +4,10 @@ refer to previous releases of Z3.
On Windows, there are no less than four different ports of OCaml. The Z3 build
system assumes that either the win32 or the win64 port is installed. This means
that OCaml will use `cl' as the underlying C compiler and not the cygwin or
mingw compilers.
mingw compilers.
By default, a make target called `ocamlfind_install' is added. This installs Z3
into the ocamlfind package repository such that programs can be compiled via
ocamlfind.
OCamlfind: When ocamlfind is found, the `install' target will install the Z3
OCaml bindings into the ocamlfind site-lib directory. The installed package is
linked against the (dynamic) libz3 and it adds $(PREFIX)/lib to the library
include paths. On Windows, there is no $(PREFIX), so the build directory is
used instead (see META.in).

View file

@ -0,0 +1,40 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
z3native_stubs.h
Abstract:
DLL/SO/DYLIB export macros.
Author:
Christoph (cwinter) 2015-12-12
Notes:
--*/
#ifndef Z3NATIVE_STUBS_H_
#define Z3NATIVE_STUBS_H_
#if defined _WIN32 || defined __CYGWIN__
#ifdef __GNUC__
#define DLL_PUBLIC __attribute__ ((dllexport))
#else
#define DLL_PUBLIC __declspec(dllexport)
#endif
#define DLL_LOCAL
#else
#if __GNUC__ >= 4
#define DLL_PUBLIC __attribute__ ((visibility ("default")))
#define DLL_LOCAL __attribute__ ((visibility ("hidden")))
#else
#define DLL_PUBLIC
#define DLL_LOCAL
#endif
#endif
#endif