mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 18:36:41 +00:00
Code Activity

Fixing shared lib extension.

Browse source
This commit is contained in:
Weng Shiwei 2024-06-17 17:58:56 -04:00
parent f0082a7856
commit f855456e20
2 changed files with 71 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

65
makefile
View file

@ -17,6 +17,7 @@
# find_library(ocaml) # find_library(ocaml)
# include(FindOCaml) # include(FindOCaml)
# Todo: use DEPFILE in https://cmake.org/cmake/help/latest/command/add_custom_command.html # Todo: use DEPFILE in https://cmake.org/cmake/help/latest/command/add_custom_command.html
# for rpath, see https://discourse.cmake.org/t/how-to-get-an-lc-rpath-and-rpath-prefix-on-a-dylib-on-macos/5540
# Generate ``z3native.ml`` and ``z3native_stubs.c`` # Generate ``z3native.ml`` and ``z3native_stubs.c``
@ -127,6 +128,9 @@
# "${z3ml_bin}/z3enums.cmi" # "${z3ml_bin}/z3enums.cmi"
ML_LIB=/home/ex/.opam/5.2.0/lib
ML_LIB=/Users/ex/.opam/5.2.0/lib
ROOT=$$(pwd)
ml0: ml0:
mkdir -p build mkdir -p build
@ -176,11 +180,12 @@ ml:
-DCMAKE_VERBOSE_MAKEFILE=TRUE \ -DCMAKE_VERBOSE_MAKEFILE=TRUE \
-DZ3_BUILD_LIBZ3_SHARED=TRUE \ -DZ3_BUILD_LIBZ3_SHARED=TRUE \
-DZ3_BUILD_OCAML_BINDINGS=TRUE \ -DZ3_BUILD_OCAML_BINDINGS=TRUE \
-DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=/home/ex/my_z3 \
-DZ3_USE_LIB_GMP=TRUE \
--debug-trycompile \ --debug-trycompile \
../ ../
# -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=/home/ex/my_z3 \
# -DZ3_USE_LIB_GMP=TRUE \
# LD_LIBRARY_PATH=build ./build/src/api/ml/ml_example # LD_LIBRARY_PATH=build ./build/src/api/ml/ml_example
build-all: build-all:
@ -210,10 +215,10 @@ MKLIB_FLAGS = \
-package zarith \ -package zarith \
-lz3 -lstdc++ -lpthread\ -lz3 -lstdc++ -lpthread\
-lgmp \ -lgmp \
-L/home/ex/code/ocaml-build-examples/vendor/z3/build \ -L$(ROOT)/build \
-dllpath /home/ex/code/ocaml-build-examples/vendor/z3/build \ -dllpath $(ROOT)/build \
-L/home/ex/.opam/5.1.1/lib/stublibs \ -L$(ML_LIB)/stublibs \
-dllpath /home/ex/.opam/5.1.1/lib/stublibs \ -dllpath $(ML_LIB)/stublibs \
-I build/src/api/ml \ -I build/src/api/ml \
-o build/src/api/ml/z3ml -o build/src/api/ml/z3ml
@ -232,74 +237,74 @@ om:
# why? # why?
# DEPENDS "${z3ml_bin}/z3enums.cmo" # DEPENDS "${z3ml_bin}/z3enums.cmo"
# -I +threads \
or1: or1:
ocamlfind ocamlc -verbose \ ocamlfind ocamlc -verbose \
-o ml_example.byte \ -o ml_example.byte \
-package zarith \ -package zarith \
-I +threads \ -I $(ROOT)/build/src/api/ml \
-I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml \ -dllpath $(ROOT)/build/src/api/ml \
-dllpath /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml \ -I $(ML_LIB)/stublibs \
-I /home/ex/.opam/5.1.1/lib/stublibs \ -dllpath $(ML_LIB)/stublibs \
-dllpath /home/ex/.opam/5.1.1/lib/stublibs \ $(ML_LIB)/zarith/zarith.cma \
/home/ex/.opam/5.1.1/lib/zarith/zarith.cma \ $(ROOT)/build/src/api/ml/z3ml.cma \
/home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml/z3ml.cma \ $(ROOT)/build/src/api/ml/ml_example.ml \
/home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml/ml_example.ml \
# -linkpkg \ # -linkpkg \
or2: or2:
ocamlrun ml_example.byte ocamlrun ml_example.byte
# -I /home/ex/.opam/5.1.1/lib/stublibs \ # -I $(ML_LIB)/stublibs \
# "-cclib" "-L${PROJECT_BINARY_DIR}" # "-cclib" "-L${PROJECT_BINARY_DIR}"
# "-cclib" [[-L. -lpthread -lstdc++ -lz3]] # "-cclib" [[-L. -lpthread -lstdc++ -lz3]]
# "-linkpkg" # "-linkpkg"
# "-cclib" "-L${PROJECT_BINARY_DIR}" # "-cclib" "-L${PROJECT_BINARY_DIR}"
# "-cclib" [[-L. -lpthread -lstdc++ -lz3]] # "-cclib" [[-L. -lpthread -lstdc++ -lz3]]
# -I +threads \
oc1: oc1:
ocamlfind ocamlopt \ ocamlfind ocamlopt \
-I +threads \
-o ml_example \ -o ml_example \
-package zarith \ -package zarith \
-linkpkg \ -linkpkg \
-I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml \ -I $(ROOT)/build/src/api/ml \
z3ml.cmxa \ z3ml.cmxa \
/home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml/ml_example.ml $(ROOT)/build/src/api/ml/ml_example.ml
oc2: oc2:
./ml_example ./ml_example
# must have # must have
# /home/ex/.opam/5.1.1/lib/zarith/zarith.cma # $(ML_LIB)/zarith/zarith.cma
# -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml # -I $(ROOT)/build/src/api/ml
# can be removed # can be removed
# -cclib "-lstdc++ -lz3" # -cclib "-lstdc++ -lz3"
# -cclib "-L. -L/home/ex/.opam/5.1.1/lib/stublibs -L/home/ex/.opam/5.1.1/lib/zarith " # -cclib "-L. -L$(ML_LIB)/stublibs -L$(ML_LIB)/zarith "
# -L/home/ex/code/ocaml-build-examples/vendor/z3/build # -L$(ROOT)/build
# -package zarith # -package zarith
# -linkpkg # -linkpkg
# -lpthread # -lpthread
# -package z3 # -package z3
# -I /home/ex/.opam/5.1.1/lib/zarith # -I $(ML_LIB)/zarith
# must not have # must not have
# -custom # -custom
# -o /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml/ml_example.byte # -o $(ROOT)/build/src/api/ml/ml_example.byte
# CAML_LD_LIBRARY_PATH=/home/ex/.opam/5.1.1/lib/stublibs:/home/ex/code/ocaml-build-examples/vendor/z3/build:/home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml:/home/ex/.opam/5.1.1/lib/zarith # CAML_LD_LIBRARY_PATH=$(ML_LIB)/stublibs:$(ROOT)/build:$(ROOT)/build/src/api/ml:$(ML_LIB)/zarith
or3: or3:
ocamlrun -I /home/ex/.opam/5.1.1/lib/zarith -I /home/ex/.opam/5.1.1/lib/stublibs -I /home/ex/.opam/5.1.1/lib/zarith ml_example.byte ocamlrun -I $(ML_LIB)/zarith -I $(ML_LIB)/stublibs -I $(ML_LIB)/zarith ml_example.byte
# -I /home/ex/.opam/5.1.1/lib/zarith # -I $(ML_LIB)/zarith
# -I /home/ex/.opam/5.1.1/lib/stublibs # -I $(ML_LIB)/stublibs
# -I /home/ex/code/ocaml-build-examples/vendor/z3/build # -I $(ROOT)/build
# -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml # -I $(ROOT)/build/src/api/ml
# -t -b # -t -b

53
src/api/ml/CMakeLists.txt
View file

@ -153,19 +153,36 @@ execute_process(
set(ocaml_stublibs_path "${ocaml_destdir_path}/stublibs") set(ocaml_stublibs_path "${ocaml_destdir_path}/stublibs")
set(c_lib_deps "-lz3" "-lstdc++" "-lpthread")
if (Z3_USE_LIB_GMP)
list(APPEND c_lib_deps "-lgmp")
endif()
if( APPLE )
set(ocaml_rpath "@executable_path/../libz3${so_ext}")
elseif( UNIX )
set(ocaml_rpath "\\$ORIGIN/../libz3${so_ext}")
endif()
list(APPEND c_lib_deps "-dllpath" ${ocaml_rpath})
# We may not directly use CMake's BUILD_RPATH or INSTALL_RPATH since they don't set
# the ocaml stub libraries as a normal library target.
set(ocamlmklib_flags "-o" "z3ml" set(ocamlmklib_flags "-o" "z3ml"
"-ocamlcflags" "-bin-annot" "-ocamlcflags" "-bin-annot"
"-package" "zarith" "-package" "zarith"
"-lz3" "-lstdc++" "-lpthread" ${c_lib_deps}
$<$<BOOL:${Z3_USE_LIB_GMP}>:-lgmp>
"-L${libz3_path}" "-L${libz3_path}"
"-dllpath" "${libz3_path}" "-dllpath" "${libz3_path}"
"-L${ocaml_stublibs_path}" "-L${ocaml_stublibs_path}"
"-dllpath" "${ocaml_stublibs_path}" "-dllpath" "${ocaml_stublibs_path}"
"-dllpath" "@rpath/dllz3ml.so"
"-I" "${z3ml_bin}") "-I" "${z3ml_bin}")
# OCaml's dll stublib hava platform-independent name `dll<pkg>.so`
add_custom_command( add_custom_command(
OUTPUT ${z3ml_bin}/dllz3ml${so_ext} OUTPUT ${z3ml_bin}/dllz3ml.so
${z3ml_bin}/libz3ml.a ${z3ml_bin}/libz3ml.a
${z3ml_bin}/z3ml.cma ${z3ml_bin}/z3ml.cma
${z3ml_bin}/z3ml.cmxa ${z3ml_bin}/z3ml.cmxa
@ -184,7 +201,7 @@ add_custom_command(
"-o" "${z3ml_bin}/z3ml.cmxs" "-o" "${z3ml_bin}/z3ml.cmxs"
"-I" "${z3ml_bin}" "-I" "${z3ml_bin}"
"${z3ml_bin}/z3ml.cmxa" "${z3ml_bin}/z3ml.cmxa"
DEPENDS DEPENDS
libz3_z3ml libz3_z3ml
${z3ml_bin}/z3native_stubs.o ${z3ml_bin}/z3native_stubs.o
${z3ml_bin}/z3enums.cmo ${z3ml_bin}/z3enums.cmo
@ -193,7 +210,7 @@ add_custom_command(
${z3ml_bin}/z3enums.cmx ${z3ml_bin}/z3enums.cmx
${z3ml_bin}/z3native.cmx ${z3ml_bin}/z3native.cmx
${z3ml_bin}/z3.cmx ${z3ml_bin}/z3.cmx
COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml${so_ext}, and libz3ml.a" COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml.so, and libz3ml.a"
VERBATIM) VERBATIM)
############################################################################### ###############################################################################
@ -212,13 +229,14 @@ execute_process(
OUTPUT_VARIABLE ocaml_pkg_zarith_path OUTPUT_VARIABLE ocaml_pkg_zarith_path
OUTPUT_STRIP_TRAILING_WHITESPACE) OUTPUT_STRIP_TRAILING_WHITESPACE)
# "-I" "+threads"
add_custom_command( add_custom_command(
OUTPUT ${z3ml_bin}/ml_example${bc_ext} OUTPUT ${z3ml_bin}/ml_example${bc_ext}
${z3ml_bin}/ml_example.bc.log ${z3ml_bin}/ml_example.bc.log
COMMAND "${OCAMLFIND}" "ocamlc" COMMAND "${OCAMLFIND}" "ocamlc"
"-o" "${z3ml_bin}/ml_example${bc_ext}" "-o" "${z3ml_bin}/ml_example${bc_ext}"
"-package" "zarith" "-package" "zarith"
"-I" "+threads"
"-I" "${z3ml_bin}" "-I" "${z3ml_bin}"
"-dllpath" "${z3ml_bin}" "-dllpath" "${z3ml_bin}"
"-I" ${ocaml_stublibs_path} "-I" ${ocaml_stublibs_path}
@ -231,17 +249,18 @@ add_custom_command(
">" "${z3ml_bin}/ml_example.bc.log" ">" "${z3ml_bin}/ml_example.bc.log"
DEPENDS DEPENDS
${z3ml_bin}/z3ml.cma ${z3ml_bin}/z3ml.cma
${z3ml_bin}/dllz3ml${so_ext} ${z3ml_bin}/dllz3ml.so
${z3ml_bin}/ml_example.ml ${z3ml_bin}/ml_example.ml
COMMENT "Testing build and run ml_example bytecode" COMMENT "Testing build and run ml_example bytecode"
VERBATIM) VERBATIM)
# "-I" "+threads"
add_custom_command( add_custom_command(
OUTPUT ${z3ml_bin}/ml_example${exe_ext} OUTPUT ${z3ml_bin}/ml_example${exe_ext}
${z3ml_bin}/ml_example.log ${z3ml_bin}/ml_example.log
COMMAND "${OCAMLFIND}" "ocamlopt" COMMAND "${OCAMLFIND}" "ocamlopt"
"-o" "${z3ml_bin}/ml_example${exe_ext}" "-o" "${z3ml_bin}/ml_example${exe_ext}"
"-I" "+threads"
"-package" "zarith" "-package" "zarith"
"-linkpkg" "-linkpkg"
"-I" "${z3ml_bin}" "-I" "${z3ml_bin}"
@ -251,7 +270,7 @@ add_custom_command(
">" "${z3ml_bin}/ml_example.log" ">" "${z3ml_bin}/ml_example.log"
DEPENDS DEPENDS
${z3ml_bin}/z3ml.cmxa ${z3ml_bin}/z3ml.cmxa
${z3ml_bin}/dllz3ml${so_ext} ${z3ml_bin}/dllz3ml.so
${z3ml_bin}/ml_example.ml ${z3ml_bin}/ml_example.ml
COMMENT "Testing build and run ml_example natively" COMMENT "Testing build and run ml_example natively"
VERBATIM) VERBATIM)
@ -269,7 +288,7 @@ add_custom_target(build_z3_ocaml_bindings
${z3ml_bin}/z3ml.cma ${z3ml_bin}/z3ml.cma
${z3ml_bin}/z3ml.cmxa ${z3ml_bin}/z3ml.cmxa
${z3ml_bin}/z3ml.cmxs ${z3ml_bin}/z3ml.cmxs
${z3ml_bin}/dllz3ml${so_ext} ${z3ml_bin}/dllz3ml.so
${z3ml_bin}/libz3ml.a ${z3ml_bin}/libz3ml.a
build_ocaml_example build_ocaml_example
) )
@ -282,20 +301,20 @@ add_custom_target(build_z3_ocaml_bindings
# I don't know how to use conditional `COMMAND` nor specify a file dependency for itself # I don't know how to use conditional `COMMAND` nor specify a file dependency for itself
# Renaming it and back seems a simple solution. # Renaming it and back seems a simple solution.
# COMMAND mv "${z3ml_bin}/dllz3ml${so_ext}" "${z3ml_bin}/dllz3ml.pre${so_ext}" # COMMAND mv "${z3ml_bin}/dllz3ml.so" "${z3ml_bin}/dllz3ml.pre.so"
# if (NOT APPLE) # if (NOT APPLE)
# add_custom_command( # add_custom_command(
# OUTPUT "${z3ml_bin}/dllz3ml${so_ext}" # OUTPUT "${z3ml_bin}/dllz3ml.so"
# COMMAND mv "${z3ml_bin}/dllz3ml.pre${so_ext}" "${z3ml_bin}/dllz3ml${so_ext}" # COMMAND mv "${z3ml_bin}/dllz3ml.pre.so" "${z3ml_bin}/dllz3ml.so}"
# DEPENDS "${z3ml_bin}/dllz3ml.pre${so_ext}" # DEPENDS "${z3ml_bin}/dllz3ml.pre.so"
# ) # )
# else() # else()
# # if IS_OSX: # # if IS_OSX:
# # install_name_tool -id ${stubs_install_path}/libz3.dylib libz3.dylib # # install_name_tool -id ${stubs_install_path}/libz3.dylib libz3.dylib
# # install_name_tool -change libz3.dylib ${stubs_install_path}/libz3.dylib api/ml/dllz3ml.so # # install_name_tool -change libz3.dylib ${stubs_install_path}/libz3.dylib api/ml/dllz3ml.so
# add_custom_command( # add_custom_command(
# OUTPUT "${z3ml_bin}/dllz3ml${so_ext}" # OUTPUT "${z3ml_bin}/dllz3ml.so"
# COMMAND mv "${z3ml_bin}/dllz3ml.pre${so_ext}" "${z3ml_bin}/dllz3ml${so_ext}" # COMMAND mv "${z3ml_bin}/dllz3ml.pre.so" "${z3ml_bin}/dllz3ml.so"
# DEPENDS "${z3ml_bin}/dllz3ml.pre${so_ext}" # DEPENDS "${z3ml_bin}/dllz3ml.so"
# ) # )
# endif() # endif()