mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 20:18:18 +00:00
Enabled .so support
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
0990a2e045
commit
87c2e5bc3c
14
configure.ac
14
configure.ac
|
@ -103,21 +103,24 @@ host_os=`uname -s`
|
||||||
|
|
||||||
AS_IF([test "$host_os" = "Darwin"], [
|
AS_IF([test "$host_os" = "Darwin"], [
|
||||||
PLATFORM=osx
|
PLATFORM=osx
|
||||||
SO_EXT=dylib
|
SO_EXT=.dylib
|
||||||
SLIBFLAGS="-dynamiclib -fopenmp"
|
SLIBFLAGS="-dynamiclib -fopenmp"
|
||||||
|
SLIBEXTRAFLAGS=""
|
||||||
COMP_VERSIONS="-compatibility_version \$(Z3_VERSION) -current_version \$(Z3_VERSION)"
|
COMP_VERSIONS="-compatibility_version \$(Z3_VERSION) -current_version \$(Z3_VERSION)"
|
||||||
STATIC_FLAGS=
|
STATIC_FLAGS=
|
||||||
], [test "$host_os" = "Linux"], [
|
], [test "$host_os" = "Linux"], [
|
||||||
PLATFORM=linux
|
PLATFORM=linux
|
||||||
SO_EXT=so
|
SO_EXT=.so
|
||||||
SLIBFLAGS="-shared -fopenmp"
|
SLIBFLAGS="-shared -fopenmp -Wl,--whole-archive"
|
||||||
|
SLIBEXTRAFLAGS="-Wl,--no-whole-archive"
|
||||||
COMP_VERSIONS=
|
COMP_VERSIONS=
|
||||||
STATIC_FLAGS=-static
|
STATIC_FLAGS=-static
|
||||||
], [test "${host_os:0:6}" = "CYGWIN"], [
|
], [test "${host_os:0:6}" = "CYGWIN"], [
|
||||||
PLATFORM=win
|
PLATFORM=win
|
||||||
SO_EXT=dll
|
SO_EXT=.dll
|
||||||
LDFLAGS=
|
LDFLAGS=
|
||||||
SLIBFLAGS="-shared -fopenmp"
|
SLIBFLAGS="-shared -fopenmp"
|
||||||
|
SLIBEXTRAFLAGS=""
|
||||||
COMP_VERSIONS=
|
COMP_VERSIONS=
|
||||||
STATIC_FLAGS=-static
|
STATIC_FLAGS=-static
|
||||||
CXXFLAGS+=" -D_CYGWIN"
|
CXXFLAGS+=" -D_CYGWIN"
|
||||||
|
@ -125,6 +128,9 @@ AS_IF([test "$host_os" = "Darwin"], [
|
||||||
[
|
[
|
||||||
AC_MSG_ERROR([Unknown host platform: $host_os])
|
AC_MSG_ERROR([Unknown host platform: $host_os])
|
||||||
])
|
])
|
||||||
|
AC_SUBST(SLIBFLAGS)
|
||||||
|
AC_SUBST(SLIBEXTRAFLAGS)
|
||||||
|
AC_SUBST(SO_EXT)
|
||||||
|
|
||||||
###################
|
###################
|
||||||
#
|
#
|
||||||
|
|
|
@ -12,3 +12,8 @@ EXE_EXT=
|
||||||
LINK=@CXX@
|
LINK=@CXX@
|
||||||
LINK_FLAGS=-lpthread -fopenmp
|
LINK_FLAGS=-lpthread -fopenmp
|
||||||
LINK_OUT_FLAG=-o
|
LINK_OUT_FLAG=-o
|
||||||
|
SO_EXT=@SO_EXT@
|
||||||
|
SLINK=@CXX@
|
||||||
|
SLINK_FLAGS=@SLIBFLAGS@
|
||||||
|
SLINK_EXTRA_FLAGS=@SLIBEXTRAFLAGS@
|
||||||
|
SLINK_OUT_FLAG=-o
|
|
@ -12,3 +12,8 @@ EXE_EXT=
|
||||||
LINK=@CXX@
|
LINK=@CXX@
|
||||||
LINK_FLAGS=-lpthread -fopenmp
|
LINK_FLAGS=-lpthread -fopenmp
|
||||||
LINK_OUT_FLAG=-o
|
LINK_OUT_FLAG=-o
|
||||||
|
SO_EXT=@SO_EXT@
|
||||||
|
SLINK=@CXX@
|
||||||
|
SLINK_FLAGS=@SLIBFLAGS@
|
||||||
|
SLINK_EXTRA_FLAGS=@SLIBEXTRAFLAGS@
|
||||||
|
SLINK_OUT_FLAG=-o
|
|
@ -62,5 +62,6 @@ add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe',
|
||||||
add_lib('api', ['portfolio', 'user_plugin'])
|
add_lib('api', ['portfolio', 'user_plugin'])
|
||||||
add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
|
add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
|
||||||
add_exe('test', ['api', 'fuzzing'], exe_name='test-z3')
|
add_exe('test', ['api', 'fuzzing'], exe_name='test-z3')
|
||||||
|
add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', dll_name='libz3')
|
||||||
|
|
||||||
mk_makefile()
|
mk_makefile()
|
||||||
|
|
|
@ -24,9 +24,6 @@ DEBUG_MODE=False
|
||||||
SHOW_CPPS = True
|
SHOW_CPPS = True
|
||||||
VS_X64 = False
|
VS_X64 = False
|
||||||
|
|
||||||
LIB_KIND = 0
|
|
||||||
EXE_KIND = 1
|
|
||||||
|
|
||||||
if os.name == 'nt':
|
if os.name == 'nt':
|
||||||
IS_WINDOW=True
|
IS_WINDOW=True
|
||||||
# Visual Studio already displays the files being compiled
|
# Visual Studio already displays the files being compiled
|
||||||
|
@ -142,13 +139,12 @@ def find_all_deps(name, deps):
|
||||||
return new_deps
|
return new_deps
|
||||||
|
|
||||||
class Component:
|
class Component:
|
||||||
def __init__(self, name, kind, path, deps):
|
def __init__(self, name, path, deps):
|
||||||
global BUILD_DIR, SRC_DIR, REV_BUILD_DIR
|
global BUILD_DIR, SRC_DIR, REV_BUILD_DIR
|
||||||
if name in _ComponentNames:
|
if name in _ComponentNames:
|
||||||
raise MKException("Component '%s' was already defined." % name)
|
raise MKException("Component '%s' was already defined." % name)
|
||||||
if path == None:
|
if path == None:
|
||||||
path = name
|
path = name
|
||||||
self.kind = kind
|
|
||||||
self.name = name
|
self.name = name
|
||||||
self.path = path
|
self.path = path
|
||||||
self.deps = find_all_deps(name, deps)
|
self.deps = find_all_deps(name, deps)
|
||||||
|
@ -232,7 +228,7 @@ class Component:
|
||||||
|
|
||||||
class LibComponent(Component):
|
class LibComponent(Component):
|
||||||
def __init__(self, name, path, deps):
|
def __init__(self, name, path, deps):
|
||||||
Component.__init__(self, name, LIB_KIND, path, deps)
|
Component.__init__(self, name, path, deps)
|
||||||
|
|
||||||
def mk_makefile(self, out):
|
def mk_makefile(self, out):
|
||||||
Component.mk_makefile(self, out)
|
Component.mk_makefile(self, out)
|
||||||
|
@ -267,7 +263,7 @@ def sort_components(cnames):
|
||||||
|
|
||||||
class ExeComponent(Component):
|
class ExeComponent(Component):
|
||||||
def __init__(self, name, exe_name, path, deps):
|
def __init__(self, name, exe_name, path, deps):
|
||||||
Component.__init__(self, name, EXE_KIND, path, deps)
|
Component.__init__(self, name, path, deps)
|
||||||
if exe_name == None:
|
if exe_name == None:
|
||||||
exe_name = name
|
exe_name = name
|
||||||
self.exe_name = exe_name
|
self.exe_name = exe_name
|
||||||
|
@ -305,6 +301,46 @@ class ExeComponent(Component):
|
||||||
def main_component(self):
|
def main_component(self):
|
||||||
return True
|
return True
|
||||||
|
|
||||||
|
class DLLComponent(Component):
|
||||||
|
def __init__(self, name, dll_name, path, deps):
|
||||||
|
Component.__init__(self, name, path, deps)
|
||||||
|
if dll_name == None:
|
||||||
|
dll_name = name
|
||||||
|
self.dll_name = dll_name
|
||||||
|
|
||||||
|
def mk_makefile(self, out):
|
||||||
|
global _Name2Component
|
||||||
|
Component.mk_makefile(self, out)
|
||||||
|
# generate rule for (SO_EXT)
|
||||||
|
|
||||||
|
dllfile = '%s$(SO_EXT)' % self.dll_name
|
||||||
|
out.write('%s:' % dllfile)
|
||||||
|
deps = sort_components(self.deps)
|
||||||
|
objs = []
|
||||||
|
for cppfile in get_cpp_files(self.src_dir):
|
||||||
|
objfile = '%s/%s$(OBJ_EXT)' % (self.build_dir, os.path.splitext(cppfile)[0])
|
||||||
|
objs.append(objfile)
|
||||||
|
for obj in objs:
|
||||||
|
out.write(' ')
|
||||||
|
out.write(obj)
|
||||||
|
for dep in deps:
|
||||||
|
c_dep = _Name2Component[dep]
|
||||||
|
out.write(' %s/%s$(LIB_EXT)' % (c_dep.build_dir, c_dep.name))
|
||||||
|
out.write('\n')
|
||||||
|
out.write('\t$(LINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS)' % dllfile)
|
||||||
|
for obj in objs:
|
||||||
|
out.write(' ')
|
||||||
|
out.write(obj)
|
||||||
|
for dep in deps:
|
||||||
|
c_dep = _Name2Component[dep]
|
||||||
|
out.write(' %s/%s$(LIB_EXT)' % (c_dep.build_dir, c_dep.name))
|
||||||
|
out.write(' $(SLINK_EXTRA_FLAGS)\n')
|
||||||
|
out.write('%s: %s\n\n' % (self.name, dllfile))
|
||||||
|
|
||||||
|
# All DLLs are included in the all: rule
|
||||||
|
def main_component(self):
|
||||||
|
return True
|
||||||
|
|
||||||
def reg_component(name, c):
|
def reg_component(name, c):
|
||||||
global _Id, _Components, _ComponentNames, _Name2Component
|
global _Id, _Components, _ComponentNames, _Name2Component
|
||||||
c.id = _Id
|
c.id = _Id
|
||||||
|
@ -323,6 +359,10 @@ def add_exe(name, deps=[], path=None, exe_name=None):
|
||||||
c = ExeComponent(name, exe_name, path, deps)
|
c = ExeComponent(name, exe_name, path, deps)
|
||||||
reg_component(name, c)
|
reg_component(name, c)
|
||||||
|
|
||||||
|
def add_dll(name, deps=[], path=None, dll_name=None):
|
||||||
|
c = DLLComponent(name, dll_name, path, deps)
|
||||||
|
reg_component(name, c)
|
||||||
|
|
||||||
# Copy configuration correct file to BUILD_DIR
|
# Copy configuration correct file to BUILD_DIR
|
||||||
def cp_config_mk():
|
def cp_config_mk():
|
||||||
if IS_WINDOW:
|
if IS_WINDOW:
|
||||||
|
@ -352,7 +392,7 @@ def mk_makefile():
|
||||||
# Generate :all rule
|
# Generate :all rule
|
||||||
out.write('all:')
|
out.write('all:')
|
||||||
for c in _Components:
|
for c in _Components:
|
||||||
if c.main_component:
|
if c.main_component():
|
||||||
out.write(' %s' % c.name)
|
out.write(' %s' % c.name)
|
||||||
out.write('\n\n')
|
out.write('\n\n')
|
||||||
# Generate components
|
# Generate components
|
||||||
|
|
Loading…
Reference in a new issue