From b70ba6ed73955d60b9b8556055ee3004b083d444 Mon Sep 17 00:00:00 2001 From: Weng Shiwei Date: Sun, 16 Jun 2024 20:07:49 -0400 Subject: [PATCH 1/9] Update doc for `mk_context`. --- src/api/ml/z3.mli | 32 +++++++++++++++++++++++++++++--- 1 file changed, 29 insertions(+), 3 deletions(-) diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 5320fc38e..0b31874e1 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -42,9 +42,10 @@ type context - timeout (unsigned) default timeout (in milliseconds) used for solvers - well_sorted_check type checker - auto_config use heuristics to automatically select solver and configure it - - model model generation for solvers, this parameter can be overwritten when creating a solver - - model_validate validate models produced by solvers - - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver + - model (Boolean) model generation for solvers, this parameter can be overwritten when creating a solver + - model_validate (Boolean) validate models produced by solvers + - unsat_core (Boolean) unsat-core generation for solvers, this parameter can be overwritten when creating a solver + - encoding the string encoding used internally (must be either "unicode" - 18 bit, "bmp" - 16 bit or "ascii" - 8 bit) *) val mk_context : (string * string) list -> context @@ -3712,6 +3713,31 @@ end For example: (set_global_param "pp.decimal" "true") will set the parameter "decimal" in the module "pp" to true. + + Legal parameters are: + auto_config (bool) (default: true) + debug_ref_count (bool) (default: false) + dot_proof_file (string) (default: proof.dot) + dump_models (bool) (default: false) + encoding (string) (default: unicode) + memory_high_watermark (unsigned int) (default: 0) + memory_high_watermark_mb (unsigned int) (default: 0) + memory_max_alloc_count (unsigned int) (default: 0) + memory_max_size (unsigned int) (default: 0) + model (bool) (default: true) + model_validate (bool) (default: false) + proof (bool) (default: false) + rlimit (unsigned int) (default: 0) + smtlib2_compliant (bool) (default: false) + stats (bool) (default: false) + timeout (unsigned int) (default: 4294967295) + trace (bool) (default: false) + trace_file_name (string) (default: z3.log) + type_check (bool) (default: true) + unsat_core (bool) (default: false) + verbose (unsigned int) (default: 0) + warning (bool) (default: true) + well_sorted_check (bool) (default: false) *) val set_global_param : string -> string -> unit From c998cf2cdbace609a79057a7d20f88e12170ce5e Mon Sep 17 00:00:00 2001 From: Weng Shiwei Date: Sun, 16 Jun 2024 20:07:49 -0400 Subject: [PATCH 2/9] Migrating to cmake. --- README-CMake.md | 3 + cmake/modules/AddOCaml.cmake | 269 +++++++++++++++++++++ cmake/modules/FindOCaml.cmake | 106 +++++++++ src/CMakeLists.txt | 12 + src/api/ml/CMakeLists.txt | 428 ++++++++++++++++++++++++++++++++++ 5 files changed, 818 insertions(+) create mode 100644 cmake/modules/AddOCaml.cmake create mode 100644 cmake/modules/FindOCaml.cmake create mode 100644 src/api/ml/CMakeLists.txt diff --git a/README-CMake.md b/README-CMake.md index 9bfc2d9ef..2c5905df2 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -292,6 +292,9 @@ The following useful options can be passed to CMake whilst configuring. * ``Z3_INSTALL_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_JAVA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Java bindings. * ``Z3_JAVA_JAR_INSTALLDIR`` - STRING. The path to directory to install the Z3 Java ``.jar`` file. This path should be relative to ``CMAKE_INSTALL_PREFIX``. * ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``. +* ``Z3_BUILD_OCAML_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's OCaml bindings will be built. +* ``Z3_BUILD_JULIA_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's Julia bindings will be built. +* ``Z3_INSTALL_JULIA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_JULIA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Julia bindings. * ``Z3_INCLUDE_GIT_DESCRIBE`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the output of ``git describe`` will be included in the build. * ``Z3_INCLUDE_GIT_HASH`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the git hash will be included in the build. * ``Z3_BUILD_DOCUMENTATION`` - BOOL. If set to ``TRUE`` then documentation for the API bindings can be built by invoking the ``api_docs`` target. diff --git a/cmake/modules/AddOCaml.cmake b/cmake/modules/AddOCaml.cmake new file mode 100644 index 000000000..e2993e79a --- /dev/null +++ b/cmake/modules/AddOCaml.cmake @@ -0,0 +1,269 @@ +# Copied from https://github.com/llvm/llvm-project/tree/main/llvm/cmake/modules/AddOCaml.cmake +# Modified by arbipher at 05/2024 +# +# CMake build rules for the OCaml language. +# Assumes FindOCaml is used. +# http://ocaml.org/ +# +# Example usage: +# +# add_ocaml_library(pkg_a OCAML mod_a OCAMLDEP pkg_b C mod_a_stubs PKG ctypes LLVM core) +# +# Unnamed parameters: +# +# * Library name. +# +# Named parameters: +# +# OCAML OCaml module names. Imply presence of a corresponding .ml and .mli files. +# OCAMLDEP Names of libraries this library depends on. +# C C stub sources. Imply presence of a corresponding .c file. +# INCLUDES Path for header files for C sources. +# CFLAGS Additional arguments passed when compiling C stubs. +# PKG Names of ocamlfind packages this library depends on. +# LLVM Names of LLVM libraries this library depends on. +# GEN Generated files. Do not need to copy. +# NOCOPY Do not automatically copy sources (.c, .ml, .mli) from the source directory, +# e.g. if they are generated. +# + +function(add_ocaml_library name) + ## Argument Setting ## + + # CMAKE_PARSE_ARGUMENTS(ARG "NOCOPY" "" "OCAML;OCAMLDEP;C;CFLAGS;PKG;LLVM" ${ARGN}) + CMAKE_PARSE_ARGUMENTS(ARG "NOCOPY" "" "OCAML;OCAMLDEP;C;CFLAGS;PKG;GEN" ${ARGN}) + + set(src ${CMAKE_CURRENT_SOURCE_DIR}) + set(bin ${CMAKE_CURRENT_BINARY_DIR}) + + # TODO: incorrect + set(ocaml_pkgs) + foreach( ocaml_pkg ${ARG_PKG} ) + list(APPEND ocaml_pkgs "-package" "${ocaml_pkg}") + endforeach() + + set(sources) + + set(ocaml_inputs) + + set(ocaml_outputs "${bin}/${name}.cma") + if( ARG_C ) + list(APPEND ocaml_outputs + "${bin}/lib${name}${CMAKE_STATIC_LIBRARY_SUFFIX}") + if ( BUILD_SHARED_LIBS ) + list(APPEND ocaml_outputs + "${bin}/dll${name}${CMAKE_SHARED_LIBRARY_SUFFIX}") + endif() + endif() + if( HAVE_OCAMLOPT ) + list(APPEND ocaml_outputs + "${bin}/${name}.cmxa" + "${bin}/${name}${CMAKE_STATIC_LIBRARY_SUFFIX}") + endif() + + set(ocaml_flags "-lstdc++" "-ldopt" "-L${LLVM_LIBRARY_DIR}" + "-ccopt" "-L\\$CAMLORIGIN/../.." + "-ccopt" "-Wl,-rpath,\\$CAMLORIGIN/../.." + ${ocaml_pkgs}) + + foreach( ocaml_dep ${ARG_OCAMLDEP} ) + get_target_property(dep_ocaml_flags "ocaml_${ocaml_dep}" OCAML_FLAGS) + list(APPEND ocaml_flags ${dep_ocaml_flags}) + endforeach() + + if( NOT BUILD_SHARED_LIBS ) + list(APPEND ocaml_flags "-custom") + endif() + + # if(LLVM_LINK_LLVM_DYLIB) + # list(APPEND ocaml_flags "-lLLVM") + # else() + # explicit_map_components_to_libraries(llvm_libs ${ARG_LLVM}) + # foreach( llvm_lib ${llvm_libs} ) + # list(APPEND ocaml_flags "-l${llvm_lib}" ) + # endforeach() + + # get_property(system_libs TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS) + # foreach(system_lib ${system_libs}) + # if (system_lib MATCHES "^-") + # # If it's an option, pass it without changes. + # list(APPEND ocaml_flags "${system_lib}" ) + # else() + # # Otherwise assume it's a library name we need to link with. + # list(APPEND ocaml_flags "-l${system_lib}" ) + # endif() + # endforeach() + # endif() + + string(REPLACE ";" " " ARG_CFLAGS "${ARG_CFLAGS}") + set(c_flags "${ARG_CFLAGS} ${LLVM_DEFINITIONS}") + foreach( include_dir ${LLVM_INCLUDE_DIR} ${LLVM_MAIN_INCLUDE_DIR} ) + set(c_flags "${c_flags} -I${include_dir}") + endforeach() + # include -D/-UNDEBUG to match dump function visibility + # regex from HandleLLVMOptions.cmake + string(REGEX MATCH "(^| )[/-][UD] *NDEBUG($| )" flag_matches + "${CMAKE_C_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} ${CMAKE_C_FLAGS}") + set(c_flags "${c_flags} ${flag_matches}") + + foreach( ocaml_file ${ARG_OCAML} ) + + if (EXISTS "${bin}/${ocaml_file}.mli") + list(APPEND sources "${ocaml_file}.mli") + else() + add_custom_command( + OUTPUT "${bin}/${ocaml_file}.mli" + COMMAND "${OCAMLFIND}" "ocamlc" "${ocaml_pkgs}" "-i" "-I" "${bin}" "-c" "${bin}/${ocaml_file}.ml" ">" "${bin}/${ocaml_file}.mli" + DEPENDS "${bin}/${ocaml_file}.ml" + COMMENT "Building OCaml mli file if non-exist" + VERBATIM) + endif() + + list(APPEND sources "${ocaml_file}.ml") + + list(APPEND ocaml_inputs "${bin}/${ocaml_file}.mli" "${bin}/${ocaml_file}.ml") + + list(APPEND ocaml_outputs "${bin}/${ocaml_file}.cmi" "${bin}/${ocaml_file}.cmo") + + list(APPEND ocaml_outputs "${bin}/${ocaml_file}.cmti" "${bin}/${ocaml_file}.cmt") + + if( HAVE_OCAMLOPT ) + list(APPEND ocaml_outputs + "${bin}/${ocaml_file}.cmx" + # "${bin}/${ocaml_file}.o" + ) + endif() + + endforeach() + + + ## Compiling ML files ## + + foreach( c_file ${ARG_C} ) + list(APPEND sources "${c_file}.c") + + list(APPEND c_inputs "${bin}/${c_file}.c") + list(APPEND c_outputs "${bin}/${c_file}.o") + endforeach() + + if( NOT ARG_NOCOPY ) + foreach( source ${sources} ) + if (NOT "${bin}/${source}" IN_LIST ARG_GEN) + add_custom_command( + OUTPUT "${bin}/${source}" + COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${src}/${source}" "${bin}" + DEPENDS "${src}/${source}" + COMMENT "Copying ${source} to build area") + endif() + endforeach() + endif() + + ## Compiling C Stub ## + + foreach( c_input ${c_inputs} ) + get_filename_component(basename "${c_input}" NAME_WE) + add_custom_command( + OUTPUT "${bin}/${basename}.o" + COMMAND "${OCAMLFIND}" "ocamlc" "-o" "${bin}/${basename}.o" "-c" "${c_input}" -ccopt ${c_flags} + DEPENDS "${c_input}" + COMMENT "Building OCaml stub object file ${bin}/${basename}.o" + VERBATIM) + endforeach() + + ## Setting linking argument and run mklib ## + + set(ocaml_params) + foreach( ocaml_input ${ocaml_inputs} ${c_outputs}) + get_filename_component(filename "${ocaml_input}" NAME) + list(APPEND ocaml_params "${filename}") + endforeach() + + if( APPLE ) + set(ocaml_rpath "@executable_path/../../../lib${LLVM_LIBDIR_SUFFIX}") + elseif( UNIX ) + set(ocaml_rpath "\\$ORIGIN/../../../lib${LLVM_LIBDIR_SUFFIX}") + endif() + list(APPEND ocaml_flags "-ldopt" "-Wl,-rpath,${ocaml_rpath}") + + add_custom_command( + OUTPUT ${ocaml_outputs} + COMMAND "${OCAMLFIND}" "ocamlmklib" "-ocamlcflags" "-bin-annot" + "-o" "${name}" ${ocaml_flags} ${ocaml_params} + DEPENDS ${ocaml_inputs} ${c_outputs} + COMMENT "Building OCaml library ${name}" + VERBATIM) + + ## Build document + + add_custom_command( + OUTPUT "${bin}/${name}.odoc" + COMMAND "${OCAMLFIND}" "ocamldoc" + "-I" "${bin}" + "-I" "${LLVM_LIBRARY_DIR}/ocaml/llvm/" + "-dump" "${bin}/${name}.odoc" + ${ocaml_pkgs} ${ocaml_inputs} + DEPENDS ${ocaml_inputs} ${ocaml_outputs} + COMMENT "Building OCaml documentation for ${name}" + VERBATIM) + + add_custom_target("ocaml_${name}" ALL DEPENDS ${ocaml_outputs} "${bin}/${name}.odoc") + + set_target_properties("ocaml_${name}" PROPERTIES + OCAML_FLAGS "-I;${bin}") + set_target_properties("ocaml_${name}" PROPERTIES + OCAML_ODOC "${bin}/${name}.odoc") + + ## Setting dependencies + + foreach( ocaml_dep ${ARG_OCAMLDEP} ) + add_dependencies("ocaml_${name}" "ocaml_${ocaml_dep}") + endforeach() + + if( NOT LLVM_OCAML_OUT_OF_TREE ) + foreach( llvm_lib ${llvm_libs} ) + add_dependencies("ocaml_${name}" "${llvm_lib}") + endforeach() + endif() + + ## Configurating installation + + set(install_files) + set(install_shlibs) + foreach( ocaml_output ${ocaml_inputs} ${ocaml_outputs} ) + get_filename_component(ext "${ocaml_output}" EXT) + + if( NOT (ext STREQUAL ".cmo" OR + ext STREQUAL ".ml" OR + ext STREQUAL ".o" OR + ext STREQUAL CMAKE_SHARED_LIBRARY_SUFFIX) ) + list(APPEND install_files "${ocaml_output}") + elseif( ext STREQUAL CMAKE_SHARED_LIBRARY_SUFFIX) + list(APPEND install_shlibs "${ocaml_output}") + endif() + endforeach() + + install(FILES ${install_files} + DESTINATION "${LLVM_OCAML_INSTALL_PATH}/llvm") + install(FILES ${install_shlibs} + PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE + GROUP_READ GROUP_EXECUTE + WORLD_READ WORLD_EXECUTE + DESTINATION "${LLVM_OCAML_INSTALL_PATH}/stublibs") + + foreach( install_file ${install_files} ${install_shlibs} ) + get_filename_component(filename "${install_file}" NAME) + add_custom_command(TARGET "ocaml_${name}" POST_BUILD + COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${install_file}" + "${LLVM_LIBRARY_DIR}/ocaml/llvm/" + COMMENT "Copying OCaml library component ${filename} to intermediate area" + VERBATIM) + add_dependencies("ocaml_${name}" ocaml_make_directory) + endforeach() +endfunction() + +# add_custom_target(ocaml_make_directory +# COMMAND "${CMAKE_COMMAND}" "-E" "make_directory" "${LLVM_LIBRARY_DIR}/ocaml/llvm") +add_custom_target("ocaml_make_directory") +# add_custom_target("ocaml_all") +# set_target_properties(ocaml_all PROPERTIES FOLDER "Misc") +# set_target_properties(ocaml_make_directory PROPERTIES FOLDER "Misc") diff --git a/cmake/modules/FindOCaml.cmake b/cmake/modules/FindOCaml.cmake new file mode 100644 index 000000000..a1bbcd228 --- /dev/null +++ b/cmake/modules/FindOCaml.cmake @@ -0,0 +1,106 @@ +# Copied from https://github.com/llvm/llvm-project/tree/main/llvm/cmake/modules/FindOCaml.cmake +# Modified by arbipher at 05/2024 +# +# CMake find_package() module for the OCaml language. +# Assumes ocamlfind will be used for compilation. +# http://ocaml.org/ +# +# Example usage: +# +# find_package(OCaml) +# +# If successful, the following variables will be defined: +# OCAMLFIND +# OCAML_VERSION +# OCAML_STDLIB_PATH +# HAVE_OCAMLOPT +# +# Also provides find_ocamlfind_package() macro. +# +# Example usage: +# +# find_ocamlfind_package(ctypes) +# +# In any case, the following variables are defined: +# +# HAVE_OCAML_${pkg} +# +# If successful, the following variables will be defined: +# +# OCAML_${pkg}_VERSION + +include( FindPackageHandleStandardArgs ) + +find_program(OCAMLFIND + NAMES ocamlfind) + +if( OCAMLFIND ) + execute_process( + COMMAND ${OCAMLFIND} ocamlc -version + OUTPUT_VARIABLE OCAML_VERSION + OUTPUT_STRIP_TRAILING_WHITESPACE) + + execute_process( + COMMAND ${OCAMLFIND} ocamlc -where + OUTPUT_VARIABLE OCAML_STDLIB_PATH + OUTPUT_STRIP_TRAILING_WHITESPACE) + + execute_process( + COMMAND ${OCAMLFIND} ocamlc -version + OUTPUT_QUIET + RESULT_VARIABLE find_ocaml_result) + if( find_ocaml_result EQUAL 0 ) + set(HAVE_OCAMLOPT TRUE) + else() + set(HAVE_OCAMLOPT FALSE) + endif() +endif() + +find_package_handle_standard_args( OCaml DEFAULT_MSG + OCAMLFIND + OCAML_VERSION + OCAML_STDLIB_PATH) + +mark_as_advanced( + OCAMLFIND) + +function(find_ocamlfind_package pkg) + CMAKE_PARSE_ARGUMENTS(ARG "OPTIONAL" "VERSION" "" ${ARGN}) + + execute_process( + COMMAND "${OCAMLFIND}" "query" "${pkg}" "-format" "%v" + RESULT_VARIABLE result + OUTPUT_VARIABLE version + ERROR_VARIABLE error + OUTPUT_STRIP_TRAILING_WHITESPACE + ERROR_STRIP_TRAILING_WHITESPACE) + + if( NOT result EQUAL 0 AND NOT ARG_OPTIONAL ) + message(FATAL_ERROR ${error}) + endif() + + if( result EQUAL 0 ) + set(found TRUE) + else() + set(found FALSE) + endif() + + if( found AND ARG_VERSION ) + if( version VERSION_LESS ARG_VERSION AND ARG_OPTIONAL ) + # If it's optional and the constraint is not satisfied, pretend + # it wasn't found. + set(found FALSE) + elseif( version VERSION_LESS ARG_VERSION ) + message(FATAL_ERROR + "ocamlfind package ${pkg} should have version ${ARG_VERSION} or newer") + endif() + endif() + + string(TOUPPER ${pkg} pkg) + + set(HAVE_OCAML_${pkg} ${found} + PARENT_SCOPE) + + set(OCAML_${pkg}_VERSION ${version} + PARENT_SCOPE) +endfunction() diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4c09f31aa..c8e66d0d5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -299,6 +299,18 @@ if (Z3_BUILD_JAVA_BINDINGS) add_subdirectory(api/java) endif() +################################################################################ +# OCaml bindings +################################################################################ +option(Z3_BUILD_OCAML_BINDINGS "Build OCaml bindings for Z3" OFF) +if (Z3_BUILD_OCAML_BINDINGS) + if (NOT Z3_BUILD_LIBZ3_SHARED) + message(FATAL_ERROR "The OCaml bindings will not work with a static libz3. " + "You either need to disable Z3_BUILD_OCAML_BINDINGS or enable Z3_BUILD_LIBZ3_SHARED") + endif() + add_subdirectory(api/ml) +endif() + ################################################################################ # Julia bindings ################################################################################ diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt new file mode 100644 index 000000000..0f9636076 --- /dev/null +++ b/src/api/ml/CMakeLists.txt @@ -0,0 +1,428 @@ +# find_program(OCAMLFIND +# NAMES ocamlfind) +# find_library(ocaml) + +find_package(OCaml REQUIRED) +include(FindOCaml) +include(AddOCaml) + +# A file is either copy-ed or gen-ed +# Why do I need to copy + +# Generate ``z3native.ml`` and ``z3native_stubs.c`` +# ${PROJECT_SOURCE_DIR}: /vendor/z3 +# ${PROJECT_BINARY_DIR}: /vendor/z3/build +# ${CMAKE_CURRENT_SOURCE_DIR}: /vendor/z3/src/api/ml +# ${CMAKE_CURRENT_BINARY_DIR}: /vendor/z3/build/src/api/ml + +set(exe_ext ${CMAKE_EXECUTABLE_SUFFIX}) +set(bc_ext ".byte") + +set(z3ml_src ${CMAKE_CURRENT_SOURCE_DIR}) +set(z3ml_bin ${CMAKE_CURRENT_BINARY_DIR}) + +set(z3_api_src "${PROJECT_SOURCE_DIR}/src/api") + +set(Z3ml_native_stubs_c "${z3ml_bin}/z3native_stubs.c") +add_custom_command( + OUTPUT + "${z3ml_bin}/z3native.ml" + "${Z3ml_native_stubs_c}" + COMMAND "${PYTHON_EXECUTABLE}" + "${PROJECT_SOURCE_DIR}/scripts/update_api.py" + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--ml-src-dir" + "${CMAKE_CURRENT_SOURCE_DIR}" + "--ml-output-dir" + "${CMAKE_CURRENT_BINARY_DIR}" + DEPENDS + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "${PROJECT_SOURCE_DIR}/scripts/update_api.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} + COMMENT "Generatinging ${z3ml_bin}/z3native.ml and ${Z3ml_native_stubs_c}" + VERBATIM +) + +set(z3ml_enums_ml "${z3ml_bin}/z3enums.ml") +add_custom_command(OUTPUT "${z3ml_enums_ml}" + COMMAND "${PYTHON_EXECUTABLE}" + "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--ml-output-dir" + "${CMAKE_CURRENT_BINARY_DIR}" + DEPENDS + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} + COMMENT "Generating ${z3ml_enums_ml}" + VERBATIM +) + +# set(z3ml_generated_files +# "${z3ml_bin}/z3native.ml" +# "${Z3ml_native_stubs_c}" +# "${z3ml_enums_ml}" +# ) + +# add_custom_target(ocaml_generated DEPENDS +# ${z3ml_generated_files} +# ) + +# add_dependencies(z3ml ocaml_generated) + +add_custom_command( + OUTPUT "${z3ml_bin}/z3.ml" + "${z3ml_bin}/z3.mli" + COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.ml" "${z3ml_bin}/z3.ml" + COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.mli" "${z3ml_bin}/z3.mli" + DEPENDS "${z3ml_src}/z3.mli" + COMMENT "Copying z3.mli to build area") + +add_custom_command( + OUTPUT "${z3ml_bin}/z3enums.mli" + COMMAND "${OCAMLFIND}" "ocamlc" + "-package" "zarith" + "-i" + "-I" "${z3ml_bin}" + "-c" "${z3ml_bin}/z3enums.ml" + ">" "${z3ml_bin}/z3enums.mli" + DEPENDS "${z3ml_enums_ml}" + COMMENT "Building z3enums.mli" + VERBATIM) + +add_custom_command( + OUTPUT "${z3ml_bin}/z3enums.cmo" + COMMAND "${OCAMLFIND}" "ocamlc" + "-package" "zarith" + "-I" "${z3ml_bin}" + "-c" "${z3ml_bin}/z3enums.ml" + DEPENDS "${z3ml_enums_ml}" + COMMENT "Building z3enums.cmo" + VERBATIM) + +if( HAVE_OCAMLOPT ) + add_custom_command( + OUTPUT "${z3ml_bin}/z3enums.cmx" + COMMAND "${OCAMLFIND}" "ocamlopt" + "-package" "zarith" + "-I" "${z3ml_bin}" + "-c" "${z3ml_bin}/z3enums.ml" + DEPENDS "${z3ml_enums_ml}" + COMMENT "Building z3enums.cmx" + VERBATIM) +endif() + +add_custom_command( + OUTPUT "${z3ml_bin}/z3native_stubs.o" + COMMAND "${OCAMLFIND}" "ocamlc" + "-package" "zarith" + "-o" "${z3ml_bin}/z3native_stubs.o" + "-I" "${z3ml_bin}" + "-I" "${z3ml_src}" + "-I" "${z3_api_src}" + "-I" "$$(ocamlfind ocamlc -where)" + "-c" "${Z3ml_native_stubs_c}" + DEPENDS "${z3ml_bin}/z3enums.cmo" + "${Z3ml_native_stubs_c}" + COMMENT "Building z3native_stubs.o" + USES_TERMINAL + ) + +add_custom_command( + OUTPUT "${z3ml_bin}/z3native.mli" + COMMAND "${OCAMLFIND}" "ocamlc" + "-package" "zarith" + "-i" + "-I" "${z3ml_bin}" + "-c" "${z3ml_bin}/z3native.ml" + ">" "${z3ml_bin}/z3native.mli" + DEPENDS "${z3ml_enums_ml}" + "${z3ml_bin}/z3enums.cmo" + "${z3ml_bin}/z3native.ml" + COMMENT "Building z3native.mli" + VERBATIM) + +add_custom_command( + OUTPUT "${z3ml_bin}/z3native.cmi" + "${z3ml_bin}/z3native.cmo" + COMMAND "${OCAMLFIND}" "ocamlc" + "-package" "zarith" + "-I" "${z3ml_bin}" + "-c" "${z3ml_bin}/z3native.mli" + COMMAND "${OCAMLFIND}" "ocamlc" + "-package" "zarith" + "-I" "${z3ml_bin}" + "-c" "${z3ml_bin}/z3native.ml" + DEPENDS "${z3ml_bin}/z3enums.cmo" + "${z3ml_bin}/z3native.mli" + "${z3ml_bin}/z3native.ml" + COMMENT "Building z3native.cmo" + VERBATIM) + +if( HAVE_OCAMLOPT ) + add_custom_command( + OUTPUT "${z3ml_bin}/z3native.cmx" + COMMAND "${OCAMLFIND}" "ocamlopt" + "-package" "zarith" + "-I" "${z3ml_bin}" + "-c" "${z3ml_bin}/z3native.ml" + DEPENDS "${z3ml_bin}/z3enums.cmo" + "${z3ml_bin}/z3native.mli" + "${z3ml_bin}/z3native.cmi" + "${z3ml_bin}/z3native.ml" + COMMENT "Building z3native.cmx" + VERBATIM) +endif() + +add_custom_command( + OUTPUT "${z3ml_bin}/z3.cmi" + "${z3ml_bin}/z3.cmo" + COMMAND "${OCAMLFIND}" "ocamlc" + "-package" "zarith" + "-I" "${z3ml_bin}" + "-c" "${z3ml_bin}/z3.mli" + COMMAND "${OCAMLFIND}" "ocamlc" + "-package" "zarith" + "-I" "${z3ml_bin}" + "-c" "${z3ml_bin}/z3.ml" + DEPENDS "${z3ml_bin}/z3enums.cmo" + "${z3ml_bin}/z3native.cmo" + "${z3ml_bin}/z3.ml" + "${z3ml_bin}/z3.mli" + COMMENT "Building z3.cmo" + VERBATIM) + +if( HAVE_OCAMLOPT ) + add_custom_command( + OUTPUT "${z3ml_bin}/z3.cmx" + COMMAND "${OCAMLFIND}" "ocamlopt" + "-package" "zarith" + "-I" "${z3ml_bin}" + "-c" "${z3ml_bin}/z3.ml" + DEPENDS "${z3ml_bin}/z3enums.cmo" + "${z3ml_bin}/z3native.cmo" + "${z3ml_bin}/z3.ml" + "${z3ml_bin}/z3.mli" + "${z3ml_bin}/z3.cmi" + COMMENT "Building z3.cmx" + VERBATIM) +endif() + +set(ocamlmklib_flags "-lz3" "-lstdc++" "-ldopt" "-L${PROJECT_BINARY_DIR}" + "-ccopt" "-L\\$CAMLORIGIN/../.." + "-ccopt" "-Wl,-rpath,\\$CAMLORIGIN/../.." + "-package" "zarith") + +add_custom_command( + OUTPUT "${z3ml_bin}/z3ml.cma" + "${z3ml_bin}/dllz3ml.so" + "${z3ml_bin}/libz3ml.a" + COMMAND "${OCAMLFIND}" "ocamlmklib" "-ocamlcflags" "-bin-annot" "-L." + "-o" z3ml + ${ocamlmklib_flags} + "-I" "${z3ml_bin}" + "${z3ml_bin}/z3enums.cmo" + "${z3ml_bin}/z3native.cmo" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmo" + DEPENDS + libz3 + "${z3ml_bin}/z3enums.cmo" + "${z3ml_bin}/z3native.cmo" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmo" + COMMENT "Building OCaml library ${name}" + VERBATIM) + +if( HAVE_OCAMLOPT ) + add_custom_command( + OUTPUT "${z3ml_bin}/z3ml.cmxa" + COMMAND "${OCAMLFIND}" "ocamlmklib" "-ocamlcflags" "-bin-annot" "-L." + "-o" z3ml + ${ocamlmklib_flags} + "-I" "${z3ml_bin}" + "${z3ml_bin}/z3enums.cmx" + "${z3ml_bin}/z3native.cmx" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmx" + DEPENDS + libz3 + "${z3ml_bin}/z3enums.cmx" + "${z3ml_bin}/z3native.cmx" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmx" + COMMENT "Building OCaml library ${name}" + VERBATIM) + + add_custom_command( + OUTPUT "${z3ml_bin}/z3ml.cmxs" + COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared" + "-o" "${z3ml_bin}/z3ml.cmxs" + "-I" "." + "-I" "${z3ml_bin}" + "${z3ml_bin}/z3ml.cmxa" + DEPENDS + "${z3ml_bin}/z3ml.cmxa" + COMMENT "Building OCaml library ${name}" + VERBATIM) +endif() + +# -cclib "-L. -lpthread -lstdc++ -lz3" + +# set (cc_flags "\"-L. -lpthread -lstdc++ -lz3\"") +#"LD_LIBRARY_PATH=${PROJECT_BINARY_DIR}" + +# Example +add_custom_command( + OUTPUT "${z3ml_bin}/ml_example.ml" + COMMAND "${CMAKE_COMMAND}" "-E" + "copy" "${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml" "${z3ml_bin}/ml_example.ml" + DEPENDS "${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml" + COMMENT "Copying ml_example.ml to build area") + +add_custom_command( + OUTPUT "${z3ml_bin}/ml_example${bc_ext}" + "${z3ml_bin}/ml_example.bc.log" + COMMAND "${OCAMLFIND}" "ocamlc" "-custom" + "-o" "${z3ml_bin}/ml_example${bc_ext}" + "-I" "${z3ml_bin}" + "-cclib" "-L${PROJECT_BINARY_DIR}" + "-cclib" [[-L. -lpthread -lstdc++ -lz3]] + "-package" "zarith" + "-linkpkg" + "z3ml.cma" + "\$(ocamlfind query zarith)/zarith.cma" + "${z3ml_bin}/ml_example.ml" + COMMAND + "ocamlrun" + "${z3ml_bin}/ml_example${bc_ext}" + ">" "${z3ml_bin}/ml_example.bc.log" + DEPENDS + "${z3ml_bin}/z3ml.cma" + "${z3ml_bin}/ml_example.ml" + COMMENT "Testing build and run ml_example bytecode" + VERBATIM) + +add_custom_command( + OUTPUT "${z3ml_bin}/ml_example${exe_ext}" + "${z3ml_bin}/ml_example.log" + COMMAND "${OCAMLFIND}" "ocamlopt" + "-o" "${z3ml_bin}/ml_example${exe_ext}" + "-I" "${z3ml_bin}" + "-cclib" "-L${PROJECT_BINARY_DIR}" + "-cclib" [[-L. -lpthread -lstdc++ -lz3]] + "-package" "zarith" + "-linkpkg" + "z3ml.cmxa" + "${z3ml_bin}/ml_example.ml" + COMMAND "LD_LIBRARY_PATH=${PROJECT_BINARY_DIR}" + "${z3ml_bin}/ml_example${exe_ext}" + ">" "${z3ml_bin}/ml_example.log" + DEPENDS + "${z3ml_bin}/z3ml.cmxa" + "${z3ml_bin}/ml_example.ml" + COMMENT "Testing build and run ml_example natively" + VERBATIM) + +# LD_LIBRARY_PATH=build ./build/src/api/ml/ml_example +add_custom_target(build_ocaml_example + ALL + DEPENDS + "${z3ml_bin}/ml_example${bc_ext}" + "${z3ml_bin}/ml_example${exe_ext}" +) + +add_custom_target(build_z3_ocaml_bindings + ALL + DEPENDS + "${z3ml_bin}/z3ml.cma" + "${z3ml_bin}/z3ml.cmxa" + "${z3ml_bin}/z3ml.cmxs" + "${z3ml_bin}/dllz3ml.so" + "${z3ml_bin}/libz3ml.a" + build_ocaml_example +) + +# Link libz3 into the python directory so bindings work out of the box +# add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" +# COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}" +# "${PROJECT_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" +# "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" +# DEPENDS libz3 +# COMMENT "Linking libz3 into python directory" +# ) + +# add_ocaml_library(z3ml +# OCAML z3enums z3native z3 +# # OCAMLDEP llvm +# PKG zarith +# C z3native_stubs +# CFLAGS "-I${Z3_C_API_PATH} -I${CMAKE_CURRENT_SOURCE_DIR} -I\$\(ocamlfind ocamlc -where\)" +# GEN "${OCAML_GENERATED_FILES}" +# # -I${CMAKE_CURRENT_SOURCE_DIR}/../llvm +# # LLVM IRReader) +# ) + + +# set(z3_c_api_path "${PROJECT_SOURCE_DIR}/src/api") +# target_sources(z3ml PRIVATE +# z3native_stubs.h +# ${z3_c_api_path}) + + +# message(heads "--${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}") +# message(extra deps "--${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}") + +# add_custom_target(z3natives_stubs.c DEPENDS "${Z3_OCAML_NATIVE_STUB_PRE_FILE}") +# target_sources(ocaml_z3 +# PRIVATE ${Z3_OCAML_NATIVE_FILE} ${Z3_OCAML_NATIVE_STUB_FILE}) + +# target_include_directories(ocaml_z3 +# PUBLIC ${CMAKE_CURRENT_BINARY_DIR} +# ) + +# add_custom_target (LibCoreBC DEPENDS libcore.bc) + +# target_sources(src/api/ml/z3natives_stubs.c +# PUBLIC Z3_OCAML_NATIVE_STUB_FILE) + +# add_custom_target(${Z3_OCAML_NATIVE_STUB_FILE} DEPENDS +# ${Z3_OCAML_NATIVE_STUB_PRE_FILE}) + +# target_precompile_headers( +# ocaml_z3 PRIVATE +# z3native_stubs.h +# ) + +# target_sources(ocaml_z3 PRIVATE +# "${PROJECT_SOURCE_DIR}/src/api/ml/z3native.ml" +# "${PROJECT_SOURCE_DIR}/src/api/ml/z3native_stubs.c") + +# add_dependencies(ocaml_z3 +# "${PROJECT_SOURCE_DIR}/src/api" +# "${PROJECT_BINARY_DIR}/src/api" +# ) + +# find_package(OCaml) +# message("DDDebug ${OCAMLFIND}") +# message("DDDebug ${pkg}") +# find_ocamlfind_package(ctypes) +# # find_ocamlfind_package("nonexist") +# message(small " ${HAVE_OCAML_ctype}") +# message(caps " ${HAVE_OCAML_CTYPES}") +# message(small " ${OCAML_ctype_VERSION}") +# message(caps " ${OCAML_CTYPES_VERSION}") +# find_package(ocaml REQUIRED) + +# add_custom_target(ocaml_post_z3enums DEPENDS +# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.ml" +# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.mli" +# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.cmo" +# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.cmx" +# ) +# add_custom_target(z3.ml DEPENDS +# ocaml_post_z3enums +# ) +# add_custom_target(z3native.ml DEPENDS +# ocaml_post_z3enums +# ) From e8c1947168eff62a2471b96c5973c0f0fb5ce864 Mon Sep 17 00:00:00 2001 From: Weng Shiwei Date: Sun, 16 Jun 2024 20:07:49 -0400 Subject: [PATCH 3/9] Migrating to cmake. It builds both internal or external libz3. --- cmake/modules/FindOCaml.cmake | 1 + src/api/ml/CMakeLists.txt | 409 +++++++++++----------------------- 2 files changed, 127 insertions(+), 283 deletions(-) diff --git a/cmake/modules/FindOCaml.cmake b/cmake/modules/FindOCaml.cmake index a1bbcd228..32f06790b 100644 --- a/cmake/modules/FindOCaml.cmake +++ b/cmake/modules/FindOCaml.cmake @@ -30,6 +30,7 @@ # OCAML_${pkg}_VERSION include( FindPackageHandleStandardArgs ) +include(AddOCaml) find_program(OCAMLFIND NAMES ocamlfind) diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt index 0f9636076..bd7ccb5aa 100644 --- a/src/api/ml/CMakeLists.txt +++ b/src/api/ml/CMakeLists.txt @@ -1,15 +1,4 @@ -# find_program(OCAMLFIND -# NAMES ocamlfind) -# find_library(ocaml) - find_package(OCaml REQUIRED) -include(FindOCaml) -include(AddOCaml) - -# A file is either copy-ed or gen-ed -# Why do I need to copy - -# Generate ``z3native.ml`` and ``z3native_stubs.c`` # ${PROJECT_SOURCE_DIR}: /vendor/z3 # ${PROJECT_BINARY_DIR}: /vendor/z3/build # ${CMAKE_CURRENT_SOURCE_DIR}: /vendor/z3/src/api/ml @@ -21,13 +10,26 @@ set(bc_ext ".byte") set(z3ml_src ${CMAKE_CURRENT_SOURCE_DIR}) set(z3ml_bin ${CMAKE_CURRENT_BINARY_DIR}) -set(z3_api_src "${PROJECT_SOURCE_DIR}/src/api") +if (Z3_BUILD_OCAML_EXTERNAL_LIBZ3) + add_custom_target(libz3_z3ml + ALL + DEPENDS "${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}/libz3.so" + ) + set(libz3_path ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}) +else() + add_custom_target(libz3_z3ml + ALL + DEPENDS libz3 + ) + set(libz3_path ${PROJECT_BINARY_DIR}) +endif() + +message(libz3_path "${libz3_path}") -set(Z3ml_native_stubs_c "${z3ml_bin}/z3native_stubs.c") add_custom_command( OUTPUT "${z3ml_bin}/z3native.ml" - "${Z3ml_native_stubs_c}" + "${z3ml_bin}/z3native_stubs.c" COMMAND "${PYTHON_EXECUTABLE}" "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} @@ -39,7 +41,7 @@ add_custom_command( ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} - COMMENT "Generatinging ${z3ml_bin}/z3native.ml and ${Z3ml_native_stubs_c}" + COMMENT "Generatinging ${z3ml_bin}/z3native.ml and ${z3ml_bin}/z3native_stubs.c" VERBATIM ) @@ -58,133 +60,87 @@ add_custom_command(OUTPUT "${z3ml_enums_ml}" VERBATIM ) -# set(z3ml_generated_files -# "${z3ml_bin}/z3native.ml" -# "${Z3ml_native_stubs_c}" -# "${z3ml_enums_ml}" -# ) - -# add_custom_target(ocaml_generated DEPENDS -# ${z3ml_generated_files} -# ) - -# add_dependencies(z3ml ocaml_generated) - add_custom_command( OUTPUT "${z3ml_bin}/z3.ml" "${z3ml_bin}/z3.mli" COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.ml" "${z3ml_bin}/z3.ml" COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.mli" "${z3ml_bin}/z3.mli" - DEPENDS "${z3ml_src}/z3.mli" - COMMENT "Copying z3.mli to build area") + DEPENDS "${z3ml_src}/z3.ml" + "${z3ml_src}/z3.mli" + COMMENT "Copying z3.ml and z3.mli to build area") -add_custom_command( - OUTPUT "${z3ml_bin}/z3enums.mli" - COMMAND "${OCAMLFIND}" "ocamlc" - "-package" "zarith" - "-i" - "-I" "${z3ml_bin}" - "-c" "${z3ml_bin}/z3enums.ml" - ">" "${z3ml_bin}/z3enums.mli" - DEPENDS "${z3ml_enums_ml}" - COMMENT "Building z3enums.mli" - VERBATIM) +set(z3ml_common_flags "-package" "zarith" + "-I" "${z3ml_bin}") -add_custom_command( - OUTPUT "${z3ml_bin}/z3enums.cmo" - COMMAND "${OCAMLFIND}" "ocamlc" - "-package" "zarith" - "-I" "${z3ml_bin}" - "-c" "${z3ml_bin}/z3enums.ml" - DEPENDS "${z3ml_enums_ml}" - COMMENT "Building z3enums.cmo" - VERBATIM) - -if( HAVE_OCAMLOPT ) - add_custom_command( - OUTPUT "${z3ml_bin}/z3enums.cmx" - COMMAND "${OCAMLFIND}" "ocamlopt" - "-package" "zarith" - "-I" "${z3ml_bin}" - "-c" "${z3ml_bin}/z3enums.ml" - DEPENDS "${z3ml_enums_ml}" - COMMENT "Building z3enums.cmx" - VERBATIM) -endif() +# z3native_stubs.c depends on nothing add_custom_command( OUTPUT "${z3ml_bin}/z3native_stubs.o" - COMMAND "${OCAMLFIND}" "ocamlc" - "-package" "zarith" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-o" "${z3ml_bin}/z3native_stubs.o" - "-I" "${z3ml_bin}" "-I" "${z3ml_src}" - "-I" "${z3_api_src}" + "-I" "${PROJECT_SOURCE_DIR}/src/api" "-I" "$$(ocamlfind ocamlc -where)" - "-c" "${Z3ml_native_stubs_c}" - DEPENDS "${z3ml_bin}/z3enums.cmo" - "${Z3ml_native_stubs_c}" + "-c" "${z3ml_bin}/z3native_stubs.c" + DEPENDS "${z3ml_bin}/z3native_stubs.c" COMMENT "Building z3native_stubs.o" - USES_TERMINAL - ) + USES_TERMINAL) + +# z3enum.ml depends on nothing + +add_custom_command( + OUTPUT "${z3ml_bin}/z3enums.mli" + "${z3ml_bin}/z3enums.cmi" + "${z3ml_bin}/z3enums.cmo" + "${z3ml_bin}/z3enums.cmx" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-i" + "-c" "${z3ml_bin}/z3enums.ml" + ">" "${z3ml_bin}/z3enums.mli" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3enums.mli" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3enums.ml" + COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3enums.ml" + DEPENDS "${z3ml_enums_ml}" + COMMENT "Building z3enums.{mli,cmi,cmo,cmx}" + VERBATIM) + +# z3native.ml depends on z3enums add_custom_command( OUTPUT "${z3ml_bin}/z3native.mli" - COMMAND "${OCAMLFIND}" "ocamlc" - "-package" "zarith" - "-i" - "-I" "${z3ml_bin}" - "-c" "${z3ml_bin}/z3native.ml" - ">" "${z3ml_bin}/z3native.mli" - DEPENDS "${z3ml_enums_ml}" - "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3native.ml" - COMMENT "Building z3native.mli" - VERBATIM) - -add_custom_command( - OUTPUT "${z3ml_bin}/z3native.cmi" + "${z3ml_bin}/z3native.cmi" "${z3ml_bin}/z3native.cmo" - COMMAND "${OCAMLFIND}" "ocamlc" - "-package" "zarith" - "-I" "${z3ml_bin}" + "${z3ml_bin}/z3native.cmx" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-i" + "-c" "${z3ml_bin}/z3native.ml" + ">" "${z3ml_bin}/z3native.mli" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3native.mli" - COMMAND "${OCAMLFIND}" "ocamlc" - "-package" "zarith" - "-I" "${z3ml_bin}" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3native.ml" + COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3native.ml" DEPENDS "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3native.mli" "${z3ml_bin}/z3native.ml" - COMMENT "Building z3native.cmo" + COMMENT "Building z3native.{mli,cmi,cmo,cmx}" VERBATIM) -if( HAVE_OCAMLOPT ) - add_custom_command( - OUTPUT "${z3ml_bin}/z3native.cmx" - COMMAND "${OCAMLFIND}" "ocamlopt" - "-package" "zarith" - "-I" "${z3ml_bin}" - "-c" "${z3ml_bin}/z3native.ml" - DEPENDS "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3native.mli" - "${z3ml_bin}/z3native.cmi" - "${z3ml_bin}/z3native.ml" - COMMENT "Building z3native.cmx" - VERBATIM) -endif() +# z3.ml depends on z3enums and z3native add_custom_command( OUTPUT "${z3ml_bin}/z3.cmi" "${z3ml_bin}/z3.cmo" - COMMAND "${OCAMLFIND}" "ocamlc" - "-package" "zarith" - "-I" "${z3ml_bin}" + "${z3ml_bin}/z3.cmx" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3.mli" - COMMAND "${OCAMLFIND}" "ocamlc" - "-package" "zarith" - "-I" "${z3ml_bin}" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3.ml" + COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3.ml" DEPENDS "${z3ml_bin}/z3enums.cmo" "${z3ml_bin}/z3native.cmo" "${z3ml_bin}/z3.ml" @@ -192,86 +148,55 @@ add_custom_command( COMMENT "Building z3.cmo" VERBATIM) -if( HAVE_OCAMLOPT ) - add_custom_command( - OUTPUT "${z3ml_bin}/z3.cmx" - COMMAND "${OCAMLFIND}" "ocamlopt" - "-package" "zarith" - "-I" "${z3ml_bin}" - "-c" "${z3ml_bin}/z3.ml" - DEPENDS "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3native.cmo" - "${z3ml_bin}/z3.ml" - "${z3ml_bin}/z3.mli" - "${z3ml_bin}/z3.cmi" - COMMENT "Building z3.cmx" - VERBATIM) -endif() +execute_process( + COMMAND ${OCAMLFIND} printconf destdir + OUTPUT_VARIABLE ocaml_destdir_path + OUTPUT_STRIP_TRAILING_WHITESPACE) -set(ocamlmklib_flags "-lz3" "-lstdc++" "-ldopt" "-L${PROJECT_BINARY_DIR}" - "-ccopt" "-L\\$CAMLORIGIN/../.." - "-ccopt" "-Wl,-rpath,\\$CAMLORIGIN/../.." - "-package" "zarith") +set(ocaml_stublibs_path "${ocaml_destdir_path}/stublibs") + +set(ocamlmklib_flags "-o" "z3ml" + "-ocamlcflags" "-bin-annot" + "-package" "zarith" + "-lz3" "-lstdc++" "-lpthread" + "-L${libz3_path}" + "-dllpath" "${libz3_path}" + "-L${ocaml_stublibs_path}" + "-dllpath" "${ocaml_stublibs_path}" + "-I" "${z3ml_bin}") add_custom_command( - OUTPUT "${z3ml_bin}/z3ml.cma" - "${z3ml_bin}/dllz3ml.so" + OUTPUT "${z3ml_bin}/dllz3ml.so" "${z3ml_bin}/libz3ml.a" - COMMAND "${OCAMLFIND}" "ocamlmklib" "-ocamlcflags" "-bin-annot" "-L." - "-o" z3ml - ${ocamlmklib_flags} + "${z3ml_bin}/z3ml.cma" + "${z3ml_bin}/z3ml.cmxa" + "${z3ml_bin}/z3ml.cmxs" + COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags} + "${z3ml_bin}/z3enums.cmo" + "${z3ml_bin}/z3native.cmo" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmo" + COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags} + "${z3ml_bin}/z3enums.cmx" + "${z3ml_bin}/z3native.cmx" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmx" + COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared" + "-o" "${z3ml_bin}/z3ml.cmxs" "-I" "${z3ml_bin}" + "${z3ml_bin}/z3ml.cmxa" + DEPENDS + libz3_z3ml + "${z3ml_bin}/z3native_stubs.o" "${z3ml_bin}/z3enums.cmo" "${z3ml_bin}/z3native.cmo" - "${z3ml_bin}/z3native_stubs.o" "${z3ml_bin}/z3.cmo" - DEPENDS - libz3 - "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3native.cmo" - "${z3ml_bin}/z3native_stubs.o" - "${z3ml_bin}/z3.cmo" - COMMENT "Building OCaml library ${name}" + "${z3ml_bin}/z3enums.cmx" + "${z3ml_bin}/z3native.cmx" + "${z3ml_bin}/z3.cmx" + COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml.so, and libz3ml.a" VERBATIM) -if( HAVE_OCAMLOPT ) - add_custom_command( - OUTPUT "${z3ml_bin}/z3ml.cmxa" - COMMAND "${OCAMLFIND}" "ocamlmklib" "-ocamlcflags" "-bin-annot" "-L." - "-o" z3ml - ${ocamlmklib_flags} - "-I" "${z3ml_bin}" - "${z3ml_bin}/z3enums.cmx" - "${z3ml_bin}/z3native.cmx" - "${z3ml_bin}/z3native_stubs.o" - "${z3ml_bin}/z3.cmx" - DEPENDS - libz3 - "${z3ml_bin}/z3enums.cmx" - "${z3ml_bin}/z3native.cmx" - "${z3ml_bin}/z3native_stubs.o" - "${z3ml_bin}/z3.cmx" - COMMENT "Building OCaml library ${name}" - VERBATIM) - - add_custom_command( - OUTPUT "${z3ml_bin}/z3ml.cmxs" - COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared" - "-o" "${z3ml_bin}/z3ml.cmxs" - "-I" "." - "-I" "${z3ml_bin}" - "${z3ml_bin}/z3ml.cmxa" - DEPENDS - "${z3ml_bin}/z3ml.cmxa" - COMMENT "Building OCaml library ${name}" - VERBATIM) -endif() - -# -cclib "-L. -lpthread -lstdc++ -lz3" - -# set (cc_flags "\"-L. -lpthread -lstdc++ -lz3\"") -#"LD_LIBRARY_PATH=${PROJECT_BINARY_DIR}" - # Example add_custom_command( OUTPUT "${z3ml_bin}/ml_example.ml" @@ -280,22 +205,27 @@ add_custom_command( DEPENDS "${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml" COMMENT "Copying ml_example.ml to build area") +execute_process( + COMMAND ${OCAMLFIND} query zarith + OUTPUT_VARIABLE ocaml_pkg_zarith_path + OUTPUT_STRIP_TRAILING_WHITESPACE) + add_custom_command( OUTPUT "${z3ml_bin}/ml_example${bc_ext}" - "${z3ml_bin}/ml_example.bc.log" - COMMAND "${OCAMLFIND}" "ocamlc" "-custom" + "${z3ml_bin}/ml_example.bc.log" + COMMAND "${OCAMLFIND}" "ocamlc" "-o" "${z3ml_bin}/ml_example${bc_ext}" - "-I" "${z3ml_bin}" - "-cclib" "-L${PROJECT_BINARY_DIR}" - "-cclib" [[-L. -lpthread -lstdc++ -lz3]] "-package" "zarith" - "-linkpkg" - "z3ml.cma" - "\$(ocamlfind query zarith)/zarith.cma" + "-I" "+threads" + "-I" "${z3ml_bin}" + "-dllpath" "${z3ml_bin}" + "-I" ${ocaml_stublibs_path} + "-dllpath" ${ocaml_stublibs_path} + "${ocaml_pkg_zarith_path}/zarith.cma" + "${z3ml_bin}/z3ml.cma" "${z3ml_bin}/ml_example.ml" COMMAND - "ocamlrun" - "${z3ml_bin}/ml_example${bc_ext}" + "ocamlrun" "${z3ml_bin}/ml_example${bc_ext}" ">" "${z3ml_bin}/ml_example.bc.log" DEPENDS "${z3ml_bin}/z3ml.cma" @@ -308,15 +238,13 @@ add_custom_command( "${z3ml_bin}/ml_example.log" COMMAND "${OCAMLFIND}" "ocamlopt" "-o" "${z3ml_bin}/ml_example${exe_ext}" - "-I" "${z3ml_bin}" - "-cclib" "-L${PROJECT_BINARY_DIR}" - "-cclib" [[-L. -lpthread -lstdc++ -lz3]] + "-I" "+threads" "-package" "zarith" "-linkpkg" - "z3ml.cmxa" + "-I" "${z3ml_bin}" + "${z3ml_bin}/z3ml.cmxa" "${z3ml_bin}/ml_example.ml" - COMMAND "LD_LIBRARY_PATH=${PROJECT_BINARY_DIR}" - "${z3ml_bin}/ml_example${exe_ext}" + COMMAND "${z3ml_bin}/ml_example${exe_ext}" ">" "${z3ml_bin}/ml_example.log" DEPENDS "${z3ml_bin}/z3ml.cmxa" @@ -324,7 +252,6 @@ add_custom_command( COMMENT "Testing build and run ml_example natively" VERBATIM) -# LD_LIBRARY_PATH=build ./build/src/api/ml/ml_example add_custom_target(build_ocaml_example ALL DEPENDS @@ -342,87 +269,3 @@ add_custom_target(build_z3_ocaml_bindings "${z3ml_bin}/libz3ml.a" build_ocaml_example ) - -# Link libz3 into the python directory so bindings work out of the box -# add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" -# COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}" -# "${PROJECT_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" -# "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" -# DEPENDS libz3 -# COMMENT "Linking libz3 into python directory" -# ) - -# add_ocaml_library(z3ml -# OCAML z3enums z3native z3 -# # OCAMLDEP llvm -# PKG zarith -# C z3native_stubs -# CFLAGS "-I${Z3_C_API_PATH} -I${CMAKE_CURRENT_SOURCE_DIR} -I\$\(ocamlfind ocamlc -where\)" -# GEN "${OCAML_GENERATED_FILES}" -# # -I${CMAKE_CURRENT_SOURCE_DIR}/../llvm -# # LLVM IRReader) -# ) - - -# set(z3_c_api_path "${PROJECT_SOURCE_DIR}/src/api") -# target_sources(z3ml PRIVATE -# z3native_stubs.h -# ${z3_c_api_path}) - - -# message(heads "--${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}") -# message(extra deps "--${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}") - -# add_custom_target(z3natives_stubs.c DEPENDS "${Z3_OCAML_NATIVE_STUB_PRE_FILE}") -# target_sources(ocaml_z3 -# PRIVATE ${Z3_OCAML_NATIVE_FILE} ${Z3_OCAML_NATIVE_STUB_FILE}) - -# target_include_directories(ocaml_z3 -# PUBLIC ${CMAKE_CURRENT_BINARY_DIR} -# ) - -# add_custom_target (LibCoreBC DEPENDS libcore.bc) - -# target_sources(src/api/ml/z3natives_stubs.c -# PUBLIC Z3_OCAML_NATIVE_STUB_FILE) - -# add_custom_target(${Z3_OCAML_NATIVE_STUB_FILE} DEPENDS -# ${Z3_OCAML_NATIVE_STUB_PRE_FILE}) - -# target_precompile_headers( -# ocaml_z3 PRIVATE -# z3native_stubs.h -# ) - -# target_sources(ocaml_z3 PRIVATE -# "${PROJECT_SOURCE_DIR}/src/api/ml/z3native.ml" -# "${PROJECT_SOURCE_DIR}/src/api/ml/z3native_stubs.c") - -# add_dependencies(ocaml_z3 -# "${PROJECT_SOURCE_DIR}/src/api" -# "${PROJECT_BINARY_DIR}/src/api" -# ) - -# find_package(OCaml) -# message("DDDebug ${OCAMLFIND}") -# message("DDDebug ${pkg}") -# find_ocamlfind_package(ctypes) -# # find_ocamlfind_package("nonexist") -# message(small " ${HAVE_OCAML_ctype}") -# message(caps " ${HAVE_OCAML_CTYPES}") -# message(small " ${OCAML_ctype_VERSION}") -# message(caps " ${OCAML_CTYPES_VERSION}") -# find_package(ocaml REQUIRED) - -# add_custom_target(ocaml_post_z3enums DEPENDS -# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.ml" -# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.mli" -# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.cmo" -# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.cmx" -# ) -# add_custom_target(z3.ml DEPENDS -# ocaml_post_z3enums -# ) -# add_custom_target(z3native.ml DEPENDS -# ocaml_post_z3enums -# ) From 7844113df19d922e31764f91c3520104e02bc887 Mon Sep 17 00:00:00 2001 From: Weng Shiwei Date: Sun, 16 Jun 2024 20:07:49 -0400 Subject: [PATCH 4/9] Start to work on platform-specific problem. --- src/api/ml/CMakeLists.txt | 58 +++++++++++++++++++++++++++++++-------- 1 file changed, 47 insertions(+), 11 deletions(-) diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt index bd7ccb5aa..a8d74407c 100644 --- a/src/api/ml/CMakeLists.txt +++ b/src/api/ml/CMakeLists.txt @@ -1,10 +1,10 @@ +############################################################################### +# Install +############################################################################### find_package(OCaml REQUIRED) -# ${PROJECT_SOURCE_DIR}: /vendor/z3 -# ${PROJECT_BINARY_DIR}: /vendor/z3/build -# ${CMAKE_CURRENT_SOURCE_DIR}: /vendor/z3/src/api/ml -# ${CMAKE_CURRENT_BINARY_DIR}: /vendor/z3/build/src/api/ml set(exe_ext ${CMAKE_EXECUTABLE_SUFFIX}) +set(so_ext ${CMAKE_SHARED_LIBRARY_SUFFIX}) set(bc_ext ".byte") set(z3ml_src ${CMAKE_CURRENT_SOURCE_DIR}) @@ -13,7 +13,7 @@ set(z3ml_bin ${CMAKE_CURRENT_BINARY_DIR}) if (Z3_BUILD_OCAML_EXTERNAL_LIBZ3) add_custom_target(libz3_z3ml ALL - DEPENDS "${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}/libz3.so" + DEPENDS "${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}/libz3${so_ext}" ) set(libz3_path ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}) else() @@ -73,6 +73,10 @@ set(z3ml_common_flags "-package" "zarith" "-I" "${z3ml_bin}") # z3native_stubs.c depends on nothing +execute_process( + COMMAND ${OCAMLFIND} ocamlc "-where" + OUTPUT_VARIABLE ocaml_stub_lib_path + OUTPUT_STRIP_TRAILING_WHITESPACE) add_custom_command( OUTPUT "${z3ml_bin}/z3native_stubs.o" @@ -80,11 +84,11 @@ add_custom_command( "-o" "${z3ml_bin}/z3native_stubs.o" "-I" "${z3ml_src}" "-I" "${PROJECT_SOURCE_DIR}/src/api" - "-I" "$$(ocamlfind ocamlc -where)" + "-I" "${ocaml_stub_lib_path}" "-c" "${z3ml_bin}/z3native_stubs.c" DEPENDS "${z3ml_bin}/z3native_stubs.c" COMMENT "Building z3native_stubs.o" - USES_TERMINAL) + VERBATIM) # z3enum.ml depends on nothing @@ -159,6 +163,7 @@ set(ocamlmklib_flags "-o" "z3ml" "-ocamlcflags" "-bin-annot" "-package" "zarith" "-lz3" "-lstdc++" "-lpthread" + $<$:-lgmp> "-L${libz3_path}" "-dllpath" "${libz3_path}" "-L${ocaml_stublibs_path}" @@ -166,7 +171,7 @@ set(ocamlmklib_flags "-o" "z3ml" "-I" "${z3ml_bin}") add_custom_command( - OUTPUT "${z3ml_bin}/dllz3ml.so" + OUTPUT "${z3ml_bin}/dllz3ml${so_ext}" "${z3ml_bin}/libz3ml.a" "${z3ml_bin}/z3ml.cma" "${z3ml_bin}/z3ml.cmxa" @@ -180,7 +185,7 @@ add_custom_command( "${z3ml_bin}/z3enums.cmx" "${z3ml_bin}/z3native.cmx" "${z3ml_bin}/z3native_stubs.o" - "${z3ml_bin}/z3.cmx" + "${z3ml_bin}/z3.cmx" COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared" "-o" "${z3ml_bin}/z3ml.cmxs" "-I" "${z3ml_bin}" @@ -194,10 +199,35 @@ add_custom_command( "${z3ml_bin}/z3enums.cmx" "${z3ml_bin}/z3native.cmx" "${z3ml_bin}/z3.cmx" - COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml.so, and libz3ml.a" + COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml${so_ext}, and libz3ml.a" VERBATIM) +# Hacky: When the os is APPLE, a fix command will mutate `libz3.dylib` and `dlllibz3.so` inplace. +# I don't know how to use conditional `COMMAND` nor specify a file dependency for itself +# Renaming it and back seems a simple solution. + +# COMMAND mv "${z3ml_bin}/dllz3ml${so_ext}" "${z3ml_bin}/dllz3ml.pre${so_ext}" +# if (NOT APPLE) +# add_custom_command( +# OUTPUT "${z3ml_bin}/dllz3ml${so_ext}" +# COMMAND mv "${z3ml_bin}/dllz3ml.pre${so_ext}" "${z3ml_bin}/dllz3ml${so_ext}" +# DEPENDS "${z3ml_bin}/dllz3ml.pre${so_ext}" +# ) +# else() +# # if IS_OSX: +# # 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 +# add_custom_command( +# OUTPUT "${z3ml_bin}/dllz3ml${so_ext}" +# COMMAND mv "${z3ml_bin}/dllz3ml.pre${so_ext}" "${z3ml_bin}/dllz3ml${so_ext}" +# DEPENDS "${z3ml_bin}/dllz3ml.pre${so_ext}" +# ) +# endif() + +############################################################################### # Example +############################################################################### + add_custom_command( OUTPUT "${z3ml_bin}/ml_example.ml" COMMAND "${CMAKE_COMMAND}" "-E" @@ -229,6 +259,7 @@ add_custom_command( ">" "${z3ml_bin}/ml_example.bc.log" DEPENDS "${z3ml_bin}/z3ml.cma" + "${z3ml_bin}/dllz3ml${so_ext}" "${z3ml_bin}/ml_example.ml" COMMENT "Testing build and run ml_example bytecode" VERBATIM) @@ -248,6 +279,7 @@ add_custom_command( ">" "${z3ml_bin}/ml_example.log" DEPENDS "${z3ml_bin}/z3ml.cmxa" + "${z3ml_bin}/dllz3ml${so_ext}" "${z3ml_bin}/ml_example.ml" COMMENT "Testing build and run ml_example natively" VERBATIM) @@ -265,7 +297,11 @@ add_custom_target(build_z3_ocaml_bindings "${z3ml_bin}/z3ml.cma" "${z3ml_bin}/z3ml.cmxa" "${z3ml_bin}/z3ml.cmxs" - "${z3ml_bin}/dllz3ml.so" + "${z3ml_bin}/dllz3ml${so_ext}" "${z3ml_bin}/libz3ml.a" build_ocaml_example ) + +############################################################################### +# Install +############################################################################### From 64b7a3aaa85cebe44ffc8bfc5fba451cf571fb3c Mon Sep 17 00:00:00 2001 From: Weng Shiwei Date: Sun, 16 Jun 2024 20:07:49 -0400 Subject: [PATCH 5/9] Messy notes. --- makefile | 390 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 390 insertions(+) create mode 100644 makefile diff --git a/makefile b/makefile new file mode 100644 index 000000000..fae646d8c --- /dev/null +++ b/makefile @@ -0,0 +1,390 @@ +# ${PROJECT_SOURCE_DIR}: /vendor/z3 +# ${PROJECT_BINARY_DIR}: /vendor/z3/build +# ${CMAKE_CURRENT_SOURCE_DIR}: /vendor/z3/src/api/ml +# ${CMAKE_CURRENT_BINARY_DIR}: /vendor/z3/build/src/api/ml + +# TODO: add `-bin-annot` to more `ocamlc` +# Question: who will set `CAMLORIGIN` +# - -dllpath $$CAMLORIGIN/../.. \ +# Q: is `ocamlmklib -ldopt -Lfoo` the same as `ocamlmklib -Lfoo` +# it doesn't looks right (item 4) +# https://www.ocaml.org/manual/5.2/runtime.html#s:ocamlrun-dllpath +# +# if external libz3 is given, no files should be build +# +# find_program(OCAMLFIND +# NAMES ocamlfind) +# find_library(ocaml) +# include(FindOCaml) +# Todo: use DEPFILE in https://cmake.org/cmake/help/latest/command/add_custom_command.html + +# Generate ``z3native.ml`` and ``z3native_stubs.c`` + +# set(z3ml_generated_files +# "${z3ml_bin}/z3native.ml" +# "${z3ml_bin}/z3native_stubs.c" +# "${z3ml_enums_ml}" +# ) + +# add_custom_target(ocaml_generated DEPENDS +# ${z3ml_generated_files} +# ) + +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3enums.mli" +# COMMAND "${OCAMLFIND}" "ocamlc" +# "-package" "zarith" +# "-i" +# "-I" "${z3ml_bin}" +# "-c" "${z3ml_bin}/z3enums.ml" +# ">" "${z3ml_bin}/z3enums.mli" +# DEPENDS "${z3ml_enums_ml}" +# COMMENT "Building z3enums.mli" +# VERBATIM) + +# "-ldopt" +# "-ccopt" "-L\\$CAMLORIGIN/../.." +# "-ccopt" "-Wl,-rpath,\\$CAMLORIGIN/../.." + +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3native.cmx" +# COMMAND "${OCAMLFIND}" "ocamlopt" +# "-package" "zarith" +# "-I" "${z3ml_bin}" +# "-c" "${z3ml_bin}/z3native.ml" +# DEPENDS "${z3ml_bin}/z3enums.cmo" +# "${z3ml_bin}/z3native.mli" +# "${z3ml_bin}/z3native.cmi" +# "${z3ml_bin}/z3native.ml" +# COMMENT "Building z3native.cmx" +# VERBATIM) + +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3enums.cmo" +# COMMAND "${OCAMLFIND}" "ocamlc" +# "-package" "zarith" +# "-I" "${z3ml_bin}" +# "-c" "${z3ml_bin}/z3enums.ml" +# DEPENDS "${z3ml_enums_ml}" +# COMMENT "Building z3enums.cmo" +# VERBATIM) + +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3native.mli" +# COMMAND "${OCAMLFIND}" "ocamlc" +# "-package" "zarith" +# "-i" +# "-I" "${z3ml_bin}" +# "-c" "${z3ml_bin}/z3native.ml" +# ">" "${z3ml_bin}/z3native.mli" +# DEPENDS "${z3ml_enums_ml}" +# "${z3ml_bin}/z3enums.cmo" +# "${z3ml_bin}/z3native.ml" +# COMMENT "Building z3native.mli" +# VERBATIM) + +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3.cmx" +# COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} +# "-c" "${z3ml_bin}/z3.ml" +# DEPENDS "${z3ml_bin}/z3enums.cmo" +# "${z3ml_bin}/z3native.cmo" +# "${z3ml_bin}/z3.ml" +# "${z3ml_bin}/z3.mli" +# "${z3ml_bin}/z3.cmi" +# COMMENT "Building z3.cmx" +# VERBATIM) + +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3ml.cmxa" +# COMMAND "${OCAMLFIND}" "ocamlmklib" +# "-o" z3ml +# ${ocamlmklib_flags} +# "-I" "${z3ml_bin}" +# "${z3ml_bin}/z3enums.cmx" +# "${z3ml_bin}/z3native.cmx" +# "${z3ml_bin}/z3native_stubs.o" +# "${z3ml_bin}/z3.cmx" +# DEPENDS +# libz3 +# "${z3ml_bin}/z3enums.cmx" +# "${z3ml_bin}/z3native.cmx" +# "${z3ml_bin}/z3native_stubs.o" +# "${z3ml_bin}/z3.cmx" +# COMMENT "Building OCaml library ${name}" +# VERBATIM) +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3ml.cmxs" +# COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared" +# "-o" "${z3ml_bin}/z3ml.cmxs" +# "-I" "." +# "-I" "${z3ml_bin}" +# "${z3ml_bin}/z3ml.cmxa" +# DEPENDS +# "${z3ml_bin}/z3ml.cmxa" +# COMMENT "Building OCaml library ${name}" +# VERBATIM) + +# "${z3ml_bin}/z3enums.cmi" + + +ml0: + mkdir -p build + cd build && cmake -G "Ninja" \ + -DZ3_BUILD_LIBZ3_SHARED=TRUE \ + -DZ3_BUILD_OCAML_BINDINGS=TRUE \ + ../ + +# -DGRAPHVIZ_EXECUTABLES=FALSE \ +# -DGRAPHVIZ_INTERFACE_LIBS=FALSE \ +# --graphviz=deps.dot \ + +ml-inner-mk: + mkdir -p build + cd build && cmake \ + -DCMAKE_VERBOSE_MAKEFILE=TRUE \ + -DZ3_BUILD_LIBZ3_SHARED=TRUE \ + -DZ3_BUILD_OCAML_BINDINGS=TRUE \ + -DZ3_BUILD_PYTHON_BINDINGS=TRUE \ + --debug-trycompile \ + ../ + +ml-mk: + mkdir -p build + cd build && cmake \ + -DCMAKE_VERBOSE_MAKEFILE=TRUE \ + -DZ3_BUILD_LIBZ3_SHARED=TRUE \ + -DZ3_BUILD_OCAML_BINDINGS=TRUE \ + -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=/home/ex/my_z3 \ + --debug-trycompile \ + ../ + +ml-inner: + mkdir -p build + cd build && cmake \ + -G "Ninja" \ + -DCMAKE_VERBOSE_MAKEFILE=TRUE \ + -DZ3_BUILD_LIBZ3_SHARED=TRUE \ + -DZ3_BUILD_OCAML_BINDINGS=TRUE \ + --debug-trycompile \ + ../ + +ml: + mkdir -p build + cd build && cmake \ + -G "Ninja" \ + -DCMAKE_VERBOSE_MAKEFILE=TRUE \ + -DZ3_BUILD_LIBZ3_SHARED=TRUE \ + -DZ3_BUILD_OCAML_BINDINGS=TRUE \ + -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=/home/ex/my_z3 \ + -DZ3_USE_LIB_GMP=TRUE \ + --debug-trycompile \ + ../ + +# LD_LIBRARY_PATH=build ./build/src/api/ml/ml_example + +build-all: + cd build && make -j16 + +build-mk: + cd build && make -j16 build_z3_ocaml_bindings +.PHONY:build + +# /bin/sh: 1: ocamlfind ocamlc -where: not found +build: + cd build && ninja build_z3_ocaml_bindings +.PHONY:build-nj + +dot: + cd build && dot -Tpng -o deps.png deps.dot + +clean: + rm -rf build + +MKLIB_FLAGS = \ + ocamlfind ocamlmklib \ + -ocamlcflags -bin-annot \ + -package zarith \ + -lz3 -lstdc++ -lpthread\ + -lgmp \ + -L/home/ex/code/ocaml-build-examples/vendor/z3/build \ + -dllpath /home/ex/code/ocaml-build-examples/vendor/z3/build \ + -L/home/ex/.opam/5.1.1/lib/stublibs \ + -dllpath /home/ex/.opam/5.1.1/lib/stublibs \ + -I build/src/api/ml \ + -o build/src/api/ml/z3ml + +om: + $(MKLIB_FLAGS) \ + build/src/api/ml/z3enums.cmo \ + build/src/api/ml/z3native.cmo \ + build/src/api/ml/z3native_stubs.o \ + build/src/api/ml/z3.cmo + + $(MKLIB_FLAGS) \ + build/src/api/ml/z3enums.cmx \ + build/src/api/ml/z3native.cmx \ + build/src/api/ml/z3native_stubs.o \ + build/src/api/ml/z3.cmx + +# why? +# DEPENDS "${z3ml_bin}/z3enums.cmo" + +or1: + ocamlfind ocamlc -verbose \ + -o ml_example.byte \ + -package zarith \ + -I +threads \ + -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml \ + -dllpath /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml \ + -I /home/ex/.opam/5.1.1/lib/stublibs \ + -dllpath /home/ex/.opam/5.1.1/lib/stublibs \ + /home/ex/.opam/5.1.1/lib/zarith/zarith.cma \ + /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml/z3ml.cma \ + /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml/ml_example.ml \ + +# -linkpkg \ + +or2: + ocamlrun ml_example.byte + +# -I /home/ex/.opam/5.1.1/lib/stublibs \ + # "-cclib" "-L${PROJECT_BINARY_DIR}" + # "-cclib" [[-L. -lpthread -lstdc++ -lz3]] + # "-linkpkg" +# "-cclib" "-L${PROJECT_BINARY_DIR}" +# "-cclib" [[-L. -lpthread -lstdc++ -lz3]] + + +oc1: + ocamlfind ocamlopt \ + -I +threads \ + -o ml_example \ + -package zarith \ + -linkpkg \ + -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml \ + z3ml.cmxa \ + /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml/ml_example.ml + +oc2: + ./ml_example + +# must have +# /home/ex/.opam/5.1.1/lib/zarith/zarith.cma +# -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml + +# can be removed +# -cclib "-lstdc++ -lz3" +# -cclib "-L. -L/home/ex/.opam/5.1.1/lib/stublibs -L/home/ex/.opam/5.1.1/lib/zarith " +# -L/home/ex/code/ocaml-build-examples/vendor/z3/build +# -package zarith +# -linkpkg +# -lpthread +# -package z3 +# -I /home/ex/.opam/5.1.1/lib/zarith + +# must not have +# -custom + +# -o /home/ex/code/ocaml-build-examples/vendor/z3/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 + +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 + +# -I /home/ex/.opam/5.1.1/lib/zarith +# -I /home/ex/.opam/5.1.1/lib/stublibs +# -I /home/ex/code/ocaml-build-examples/vendor/z3/build +# -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml +# -t -b + + +# -cclib "-L. -lpthread -lstdc++ -lz3" + +# set (cc_flags "\"-L. -lpthread -lstdc++ -lz3\"") +#"LD_LIBRARY_PATH=${PROJECT_BINARY_DIR}" + +# Link libz3 into the python directory so bindings work out of the box +# add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" +# COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}" +# "${PROJECT_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" +# "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" +# DEPENDS libz3 +# COMMENT "Linking libz3 into python directory" +# ) + +# add_ocaml_library(z3ml +# OCAML z3enums z3native z3 +# # OCAMLDEP llvm +# PKG zarith +# C z3native_stubs +# CFLAGS "-I${Z3_C_API_PATH} -I${CMAKE_CURRENT_SOURCE_DIR} -I\$\(ocamlfind ocamlc -where\)" +# GEN "${OCAML_GENERATED_FILES}" +# # -I${CMAKE_CURRENT_SOURCE_DIR}/../llvm +# # LLVM IRReader) +# ) + + +# set(z3_c_api_path "${PROJECT_SOURCE_DIR}/src/api") +# target_sources(z3ml PRIVATE +# z3native_stubs.h +# ${z3_c_api_path}) + + +# message(heads "--${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}") +# message(extra deps "--${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}") + +# add_custom_target(z3natives_stubs.c DEPENDS "${Z3_OCAML_NATIVE_STUB_PRE_FILE}") +# target_sources(ocaml_z3 +# PRIVATE ${Z3_OCAML_NATIVE_FILE} ${Z3_OCAML_NATIVE_STUB_FILE}) + +# target_include_directories(ocaml_z3 +# PUBLIC ${CMAKE_CURRENT_BINARY_DIR} +# ) + +# add_custom_target (LibCoreBC DEPENDS libcore.bc) + +# target_sources(src/api/ml/z3natives_stubs.c +# PUBLIC Z3_OCAML_NATIVE_STUB_FILE) + +# add_custom_target(${Z3_OCAML_NATIVE_STUB_FILE} DEPENDS +# ${Z3_OCAML_NATIVE_STUB_PRE_FILE}) + +# target_precompile_headers( +# ocaml_z3 PRIVATE +# z3native_stubs.h +# ) + +# target_sources(ocaml_z3 PRIVATE +# "${PROJECT_SOURCE_DIR}/src/api/ml/z3native.ml" +# "${PROJECT_SOURCE_DIR}/src/api/ml/z3native_stubs.c") + +# add_dependencies(ocaml_z3 +# "${PROJECT_SOURCE_DIR}/src/api" +# "${PROJECT_BINARY_DIR}/src/api" +# ) + +# find_package(OCaml) +# message("DDDebug ${OCAMLFIND}") +# message("DDDebug ${pkg}") +# find_ocamlfind_package(ctypes) +# # find_ocamlfind_package("nonexist") +# message(small " ${HAVE_OCAML_ctype}") +# message(caps " ${HAVE_OCAML_CTYPES}") +# message(small " ${OCAML_ctype_VERSION}") +# message(caps " ${OCAML_CTYPES_VERSION}") +# find_package(ocaml REQUIRED) + +# add_custom_target(ocaml_post_z3enums DEPENDS +# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.ml" +# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.mli" +# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.cmo" +# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.cmx" +# ) +# add_custom_target(z3.ml DEPENDS +# ocaml_post_z3enums +# ) +# add_custom_target(z3native.ml DEPENDS +# ocaml_post_z3enums +# ) From dbc7889d65e0d50b18f9a6709c35b91562e7e4ca Mon Sep 17 00:00:00 2001 From: Weng Shiwei Date: Sun, 16 Jun 2024 20:07:49 -0400 Subject: [PATCH 6/9] debug. --- src/api/ml/CMakeLists.txt | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt index a8d74407c..71902f820 100644 --- a/src/api/ml/CMakeLists.txt +++ b/src/api/ml/CMakeLists.txt @@ -24,12 +24,12 @@ else() set(libz3_path ${PROJECT_BINARY_DIR}) endif() -message(libz3_path "${libz3_path}") +set(Z3ml_native_stubs_c "${z3ml_bin}/z3native_stubs.c") add_custom_command( OUTPUT "${z3ml_bin}/z3native.ml" - "${z3ml_bin}/z3native_stubs.c" + ${Z3ml_native_stubs_c} COMMAND "${PYTHON_EXECUTABLE}" "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} @@ -41,12 +41,14 @@ add_custom_command( ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} - COMMENT "Generatinging ${z3ml_bin}/z3native.ml and ${z3ml_bin}/z3native_stubs.c" + COMMENT "Generatinging ${z3ml_bin}/z3native.ml and ${Z3ml_native_stubs_c}" VERBATIM ) -set(z3ml_enums_ml "${z3ml_bin}/z3enums.ml") -add_custom_command(OUTPUT "${z3ml_enums_ml}" +set(gen_z3enum "${z3ml_bin}/z3enums.ml") +add_custom_command( + OUTPUT + ${gen_z3enum} COMMAND "${PYTHON_EXECUTABLE}" "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} @@ -56,7 +58,7 @@ add_custom_command(OUTPUT "${z3ml_enums_ml}" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} - COMMENT "Generating ${z3ml_enums_ml}" + COMMENT "Generating ${gen_z3enum}" VERBATIM ) @@ -79,14 +81,14 @@ execute_process( OUTPUT_STRIP_TRAILING_WHITESPACE) add_custom_command( - OUTPUT "${z3ml_bin}/z3native_stubs.o" + OUTPUT ${z3ml_bin}/z3native_stubs.o COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-o" "${z3ml_bin}/z3native_stubs.o" "-I" "${z3ml_src}" "-I" "${PROJECT_SOURCE_DIR}/src/api" "-I" "${ocaml_stub_lib_path}" "-c" "${z3ml_bin}/z3native_stubs.c" - DEPENDS "${z3ml_bin}/z3native_stubs.c" + DEPENDS ${Z3ml_native_stubs_c} COMMENT "Building z3native_stubs.o" VERBATIM) @@ -107,7 +109,7 @@ add_custom_command( "-c" "${z3ml_bin}/z3enums.ml" COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3enums.ml" - DEPENDS "${z3ml_enums_ml}" + DEPENDS ${gen_z3enum} COMMENT "Building z3enums.{mli,cmi,cmo,cmx}" VERBATIM) @@ -192,7 +194,7 @@ add_custom_command( "${z3ml_bin}/z3ml.cmxa" DEPENDS libz3_z3ml - "${z3ml_bin}/z3native_stubs.o" + ${z3ml_bin}/z3native_stubs.o "${z3ml_bin}/z3enums.cmo" "${z3ml_bin}/z3native.cmo" "${z3ml_bin}/z3.cmo" @@ -294,6 +296,12 @@ add_custom_target(build_ocaml_example add_custom_target(build_z3_ocaml_bindings ALL DEPENDS + ${gen_z3enum} + "${z3ml_bin}/z3enums.mli" + ${Z3ml_native_stubs_c} + "${z3ml_bin}/z3native.ml" + "${z3ml_bin}/z3native.mli" + "${z3ml_bin}/z3ml.cma" "${z3ml_bin}/z3ml.cmxa" "${z3ml_bin}/z3ml.cmxs" From f0082a78564b68ef69712a378cf5b89969cd8074 Mon Sep 17 00:00:00 2001 From: Weng Shiwei Date: Sun, 16 Jun 2024 20:26:28 -0400 Subject: [PATCH 7/9] Cleanup a bit. --- makefile | 7 +- src/api/ml/CMakeLists.txt | 296 ++++++++++++++++++-------------------- 2 files changed, 146 insertions(+), 157 deletions(-) diff --git a/makefile b/makefile index fae646d8c..5c3360d18 100644 --- a/makefile +++ b/makefile @@ -190,10 +190,13 @@ build-mk: cd build && make -j16 build_z3_ocaml_bindings .PHONY:build -# /bin/sh: 1: ocamlfind ocamlc -where: not found +build-nj: + cd build && ninja +.PHONY:build-nj + build: cd build && ninja build_z3_ocaml_bindings -.PHONY:build-nj +.PHONY:build dot: cd build && dot -Tpng -o deps.png deps.dot diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt index 71902f820..5cd31d444 100644 --- a/src/api/ml/CMakeLists.txt +++ b/src/api/ml/CMakeLists.txt @@ -1,6 +1,3 @@ -############################################################################### -# Install -############################################################################### find_package(OCaml REQUIRED) set(exe_ext ${CMAKE_EXECUTABLE_SUFFIX}) @@ -13,7 +10,7 @@ set(z3ml_bin ${CMAKE_CURRENT_BINARY_DIR}) if (Z3_BUILD_OCAML_EXTERNAL_LIBZ3) add_custom_target(libz3_z3ml ALL - DEPENDS "${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}/libz3${so_ext}" + DEPENDS ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}/libz3${so_ext} ) set(libz3_path ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}) else() @@ -24,13 +21,11 @@ else() set(libz3_path ${PROJECT_BINARY_DIR}) endif() -set(Z3ml_native_stubs_c "${z3ml_bin}/z3native_stubs.c") - add_custom_command( OUTPUT - "${z3ml_bin}/z3native.ml" - ${Z3ml_native_stubs_c} - COMMAND "${PYTHON_EXECUTABLE}" + ${z3ml_bin}/z3native.ml + ${z3ml_bin}/z3native_stubs.c + COMMAND "${Python3_EXECUTABLE}" "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "--ml-src-dir" @@ -38,37 +33,36 @@ add_custom_command( "--ml-output-dir" "${CMAKE_CURRENT_BINARY_DIR}" DEPENDS + ${PROJECT_SOURCE_DIR}/scripts/update_api.py ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} - "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} - COMMENT "Generatinging ${z3ml_bin}/z3native.ml and ${Z3ml_native_stubs_c}" + COMMENT "Generatinging ${z3ml_bin}/z3native.ml and ${z3ml_bin}/z3native_stubs.c" VERBATIM ) -set(gen_z3enum "${z3ml_bin}/z3enums.ml") add_custom_command( OUTPUT - ${gen_z3enum} - COMMAND "${PYTHON_EXECUTABLE}" + ${z3ml_bin}/z3enums.ml + COMMAND "${Python3_EXECUTABLE}" "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "--ml-output-dir" "${CMAKE_CURRENT_BINARY_DIR}" DEPENDS + ${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} - "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} - COMMENT "Generating ${gen_z3enum}" + COMMENT "Generating ${z3ml_bin}/z3enums.ml" VERBATIM ) add_custom_command( - OUTPUT "${z3ml_bin}/z3.ml" - "${z3ml_bin}/z3.mli" + OUTPUT ${z3ml_bin}/z3.ml + ${z3ml_bin}/z3.mli COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.ml" "${z3ml_bin}/z3.ml" COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.mli" "${z3ml_bin}/z3.mli" - DEPENDS "${z3ml_src}/z3.ml" - "${z3ml_src}/z3.mli" + DEPENDS ${z3ml_src}/z3.ml + ${z3ml_src}/z3.mli COMMENT "Copying z3.ml and z3.mli to build area") set(z3ml_common_flags "-package" "zarith" @@ -88,17 +82,16 @@ add_custom_command( "-I" "${PROJECT_SOURCE_DIR}/src/api" "-I" "${ocaml_stub_lib_path}" "-c" "${z3ml_bin}/z3native_stubs.c" - DEPENDS ${Z3ml_native_stubs_c} + DEPENDS ${z3ml_bin}/z3native_stubs.c COMMENT "Building z3native_stubs.o" VERBATIM) # z3enum.ml depends on nothing - add_custom_command( - OUTPUT "${z3ml_bin}/z3enums.mli" - "${z3ml_bin}/z3enums.cmi" - "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3enums.cmx" + OUTPUT ${z3ml_bin}/z3enums.mli + ${z3ml_bin}/z3enums.cmi + ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3enums.cmx COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-i" "-c" "${z3ml_bin}/z3enums.ml" @@ -109,17 +102,16 @@ add_custom_command( "-c" "${z3ml_bin}/z3enums.ml" COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3enums.ml" - DEPENDS ${gen_z3enum} + DEPENDS ${z3ml_bin}/z3enums.ml COMMENT "Building z3enums.{mli,cmi,cmo,cmx}" VERBATIM) # z3native.ml depends on z3enums - add_custom_command( - OUTPUT "${z3ml_bin}/z3native.mli" - "${z3ml_bin}/z3native.cmi" - "${z3ml_bin}/z3native.cmo" - "${z3ml_bin}/z3native.cmx" + OUTPUT ${z3ml_bin}/z3native.mli + ${z3ml_bin}/z3native.cmi + ${z3ml_bin}/z3native.cmo + ${z3ml_bin}/z3native.cmx COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-i" "-c" "${z3ml_bin}/z3native.ml" @@ -130,30 +122,30 @@ add_custom_command( "-c" "${z3ml_bin}/z3native.ml" COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3native.ml" - DEPENDS "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3native.ml" + DEPENDS ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3native.ml COMMENT "Building z3native.{mli,cmi,cmo,cmx}" VERBATIM) # z3.ml depends on z3enums and z3native - add_custom_command( - OUTPUT "${z3ml_bin}/z3.cmi" - "${z3ml_bin}/z3.cmo" - "${z3ml_bin}/z3.cmx" + OUTPUT ${z3ml_bin}/z3.cmi + ${z3ml_bin}/z3.cmo + ${z3ml_bin}/z3.cmx COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3.mli" COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3.ml" COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} "-c" "${z3ml_bin}/z3.ml" - DEPENDS "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3native.cmo" - "${z3ml_bin}/z3.ml" - "${z3ml_bin}/z3.mli" + DEPENDS ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3native.cmo + ${z3ml_bin}/z3.ml + ${z3ml_bin}/z3.mli COMMENT "Building z3.cmo" VERBATIM) +# making ocaml stublibs execute_process( COMMAND ${OCAMLFIND} printconf destdir OUTPUT_VARIABLE ocaml_destdir_path @@ -173,37 +165,119 @@ set(ocamlmklib_flags "-o" "z3ml" "-I" "${z3ml_bin}") add_custom_command( - OUTPUT "${z3ml_bin}/dllz3ml${so_ext}" - "${z3ml_bin}/libz3ml.a" - "${z3ml_bin}/z3ml.cma" - "${z3ml_bin}/z3ml.cmxa" - "${z3ml_bin}/z3ml.cmxs" + OUTPUT ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/libz3ml.a + ${z3ml_bin}/z3ml.cma + ${z3ml_bin}/z3ml.cmxa + ${z3ml_bin}/z3ml.cmxs COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags} - "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3native.cmo" - "${z3ml_bin}/z3native_stubs.o" - "${z3ml_bin}/z3.cmo" + "${z3ml_bin}/z3enums.cmo" + "${z3ml_bin}/z3native.cmo" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmo" COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags} - "${z3ml_bin}/z3enums.cmx" - "${z3ml_bin}/z3native.cmx" - "${z3ml_bin}/z3native_stubs.o" - "${z3ml_bin}/z3.cmx" + "${z3ml_bin}/z3enums.cmx" + "${z3ml_bin}/z3native.cmx" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmx" COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared" - "-o" "${z3ml_bin}/z3ml.cmxs" - "-I" "${z3ml_bin}" - "${z3ml_bin}/z3ml.cmxa" + "-o" "${z3ml_bin}/z3ml.cmxs" + "-I" "${z3ml_bin}" + "${z3ml_bin}/z3ml.cmxa" DEPENDS - libz3_z3ml - ${z3ml_bin}/z3native_stubs.o - "${z3ml_bin}/z3enums.cmo" - "${z3ml_bin}/z3native.cmo" - "${z3ml_bin}/z3.cmo" - "${z3ml_bin}/z3enums.cmx" - "${z3ml_bin}/z3native.cmx" - "${z3ml_bin}/z3.cmx" + libz3_z3ml + ${z3ml_bin}/z3native_stubs.o + ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3native.cmo + ${z3ml_bin}/z3.cmo + ${z3ml_bin}/z3enums.cmx + ${z3ml_bin}/z3native.cmx + ${z3ml_bin}/z3.cmx COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml${so_ext}, and libz3ml.a" VERBATIM) +############################################################################### +# Example +############################################################################### + +add_custom_command( + OUTPUT ${z3ml_bin}/ml_example.ml + COMMAND "${CMAKE_COMMAND}" "-E" + "copy" "${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml" "${z3ml_bin}/ml_example.ml" + DEPENDS ${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml + COMMENT "Copying ml_example.ml to build area") + +execute_process( + COMMAND ${OCAMLFIND} query zarith + OUTPUT_VARIABLE ocaml_pkg_zarith_path + OUTPUT_STRIP_TRAILING_WHITESPACE) + +add_custom_command( + OUTPUT ${z3ml_bin}/ml_example${bc_ext} + ${z3ml_bin}/ml_example.bc.log + COMMAND "${OCAMLFIND}" "ocamlc" + "-o" "${z3ml_bin}/ml_example${bc_ext}" + "-package" "zarith" + "-I" "+threads" + "-I" "${z3ml_bin}" + "-dllpath" "${z3ml_bin}" + "-I" ${ocaml_stublibs_path} + "-dllpath" ${ocaml_stublibs_path} + "${ocaml_pkg_zarith_path}/zarith.cma" + "${z3ml_bin}/z3ml.cma" + "${z3ml_bin}/ml_example.ml" + COMMAND + "ocamlrun" "${z3ml_bin}/ml_example${bc_ext}" + ">" "${z3ml_bin}/ml_example.bc.log" + DEPENDS + ${z3ml_bin}/z3ml.cma + ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/ml_example.ml + COMMENT "Testing build and run ml_example bytecode" + VERBATIM) + +add_custom_command( + OUTPUT ${z3ml_bin}/ml_example${exe_ext} + ${z3ml_bin}/ml_example.log + COMMAND "${OCAMLFIND}" "ocamlopt" + "-o" "${z3ml_bin}/ml_example${exe_ext}" + "-I" "+threads" + "-package" "zarith" + "-linkpkg" + "-I" "${z3ml_bin}" + "${z3ml_bin}/z3ml.cmxa" + "${z3ml_bin}/ml_example.ml" + COMMAND "${z3ml_bin}/ml_example${exe_ext}" + ">" "${z3ml_bin}/ml_example.log" + DEPENDS + ${z3ml_bin}/z3ml.cmxa + ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/ml_example.ml + COMMENT "Testing build and run ml_example natively" + VERBATIM) + +add_custom_target(build_ocaml_example + ALL + DEPENDS + ${z3ml_bin}/ml_example${bc_ext} + ${z3ml_bin}/ml_example${exe_ext} +) + +add_custom_target(build_z3_ocaml_bindings + ALL + DEPENDS + ${z3ml_bin}/z3ml.cma + ${z3ml_bin}/z3ml.cmxa + ${z3ml_bin}/z3ml.cmxs + ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/libz3ml.a + build_ocaml_example +) + +############################################################################### +# Install +############################################################################### + # Hacky: When the os is APPLE, a fix command will mutate `libz3.dylib` and `dlllibz3.so` inplace. # I don't know how to use conditional `COMMAND` nor specify a file dependency for itself # Renaming it and back seems a simple solution. @@ -224,92 +298,4 @@ add_custom_command( # COMMAND mv "${z3ml_bin}/dllz3ml.pre${so_ext}" "${z3ml_bin}/dllz3ml${so_ext}" # DEPENDS "${z3ml_bin}/dllz3ml.pre${so_ext}" # ) -# endif() - -############################################################################### -# Example -############################################################################### - -add_custom_command( - OUTPUT "${z3ml_bin}/ml_example.ml" - COMMAND "${CMAKE_COMMAND}" "-E" - "copy" "${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml" "${z3ml_bin}/ml_example.ml" - DEPENDS "${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml" - COMMENT "Copying ml_example.ml to build area") - -execute_process( - COMMAND ${OCAMLFIND} query zarith - OUTPUT_VARIABLE ocaml_pkg_zarith_path - OUTPUT_STRIP_TRAILING_WHITESPACE) - -add_custom_command( - OUTPUT "${z3ml_bin}/ml_example${bc_ext}" - "${z3ml_bin}/ml_example.bc.log" - COMMAND "${OCAMLFIND}" "ocamlc" - "-o" "${z3ml_bin}/ml_example${bc_ext}" - "-package" "zarith" - "-I" "+threads" - "-I" "${z3ml_bin}" - "-dllpath" "${z3ml_bin}" - "-I" ${ocaml_stublibs_path} - "-dllpath" ${ocaml_stublibs_path} - "${ocaml_pkg_zarith_path}/zarith.cma" - "${z3ml_bin}/z3ml.cma" - "${z3ml_bin}/ml_example.ml" - COMMAND - "ocamlrun" "${z3ml_bin}/ml_example${bc_ext}" - ">" "${z3ml_bin}/ml_example.bc.log" - DEPENDS - "${z3ml_bin}/z3ml.cma" - "${z3ml_bin}/dllz3ml${so_ext}" - "${z3ml_bin}/ml_example.ml" - COMMENT "Testing build and run ml_example bytecode" - VERBATIM) - -add_custom_command( - OUTPUT "${z3ml_bin}/ml_example${exe_ext}" - "${z3ml_bin}/ml_example.log" - COMMAND "${OCAMLFIND}" "ocamlopt" - "-o" "${z3ml_bin}/ml_example${exe_ext}" - "-I" "+threads" - "-package" "zarith" - "-linkpkg" - "-I" "${z3ml_bin}" - "${z3ml_bin}/z3ml.cmxa" - "${z3ml_bin}/ml_example.ml" - COMMAND "${z3ml_bin}/ml_example${exe_ext}" - ">" "${z3ml_bin}/ml_example.log" - DEPENDS - "${z3ml_bin}/z3ml.cmxa" - "${z3ml_bin}/dllz3ml${so_ext}" - "${z3ml_bin}/ml_example.ml" - COMMENT "Testing build and run ml_example natively" - VERBATIM) - -add_custom_target(build_ocaml_example - ALL - DEPENDS - "${z3ml_bin}/ml_example${bc_ext}" - "${z3ml_bin}/ml_example${exe_ext}" -) - -add_custom_target(build_z3_ocaml_bindings - ALL - DEPENDS - ${gen_z3enum} - "${z3ml_bin}/z3enums.mli" - ${Z3ml_native_stubs_c} - "${z3ml_bin}/z3native.ml" - "${z3ml_bin}/z3native.mli" - - "${z3ml_bin}/z3ml.cma" - "${z3ml_bin}/z3ml.cmxa" - "${z3ml_bin}/z3ml.cmxs" - "${z3ml_bin}/dllz3ml${so_ext}" - "${z3ml_bin}/libz3ml.a" - build_ocaml_example -) - -############################################################################### -# Install -############################################################################### +# endif() \ No newline at end of file From f855456e203edde54caf695bd18d24fa339ae427 Mon Sep 17 00:00:00 2001 From: Weng Shiwei Date: Mon, 17 Jun 2024 17:58:56 -0400 Subject: [PATCH 8/9] Fixing shared lib extension. --- makefile | 65 +++++++++++++++++++++------------------ src/api/ml/CMakeLists.txt | 53 +++++++++++++++++++++---------- 2 files changed, 71 insertions(+), 47 deletions(-) diff --git a/makefile b/makefile index 5c3360d18..5b0b58a49 100644 --- a/makefile +++ b/makefile @@ -17,6 +17,7 @@ # find_library(ocaml) # include(FindOCaml) # 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`` @@ -127,6 +128,9 @@ # "${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: mkdir -p build @@ -176,11 +180,12 @@ ml: -DCMAKE_VERBOSE_MAKEFILE=TRUE \ -DZ3_BUILD_LIBZ3_SHARED=TRUE \ -DZ3_BUILD_OCAML_BINDINGS=TRUE \ - -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=/home/ex/my_z3 \ - -DZ3_USE_LIB_GMP=TRUE \ --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 build-all: @@ -210,10 +215,10 @@ MKLIB_FLAGS = \ -package zarith \ -lz3 -lstdc++ -lpthread\ -lgmp \ - -L/home/ex/code/ocaml-build-examples/vendor/z3/build \ - -dllpath /home/ex/code/ocaml-build-examples/vendor/z3/build \ - -L/home/ex/.opam/5.1.1/lib/stublibs \ - -dllpath /home/ex/.opam/5.1.1/lib/stublibs \ + -L$(ROOT)/build \ + -dllpath $(ROOT)/build \ + -L$(ML_LIB)/stublibs \ + -dllpath $(ML_LIB)/stublibs \ -I build/src/api/ml \ -o build/src/api/ml/z3ml @@ -232,74 +237,74 @@ om: # why? # DEPENDS "${z3ml_bin}/z3enums.cmo" +# -I +threads \ or1: ocamlfind ocamlc -verbose \ -o ml_example.byte \ -package zarith \ - -I +threads \ - -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml \ - -dllpath /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml \ - -I /home/ex/.opam/5.1.1/lib/stublibs \ - -dllpath /home/ex/.opam/5.1.1/lib/stublibs \ - /home/ex/.opam/5.1.1/lib/zarith/zarith.cma \ - /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml/z3ml.cma \ - /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml/ml_example.ml \ + -I $(ROOT)/build/src/api/ml \ + -dllpath $(ROOT)/build/src/api/ml \ + -I $(ML_LIB)/stublibs \ + -dllpath $(ML_LIB)/stublibs \ + $(ML_LIB)/zarith/zarith.cma \ + $(ROOT)/build/src/api/ml/z3ml.cma \ + $(ROOT)/build/src/api/ml/ml_example.ml \ # -linkpkg \ or2: ocamlrun ml_example.byte -# -I /home/ex/.opam/5.1.1/lib/stublibs \ +# -I $(ML_LIB)/stublibs \ # "-cclib" "-L${PROJECT_BINARY_DIR}" # "-cclib" [[-L. -lpthread -lstdc++ -lz3]] # "-linkpkg" # "-cclib" "-L${PROJECT_BINARY_DIR}" # "-cclib" [[-L. -lpthread -lstdc++ -lz3]] +# -I +threads \ oc1: ocamlfind ocamlopt \ - -I +threads \ -o ml_example \ -package zarith \ -linkpkg \ - -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml \ + -I $(ROOT)/build/src/api/ml \ 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: ./ml_example # must have -# /home/ex/.opam/5.1.1/lib/zarith/zarith.cma -# -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml +# $(ML_LIB)/zarith/zarith.cma +# -I $(ROOT)/build/src/api/ml # can be removed # -cclib "-lstdc++ -lz3" -# -cclib "-L. -L/home/ex/.opam/5.1.1/lib/stublibs -L/home/ex/.opam/5.1.1/lib/zarith " -# -L/home/ex/code/ocaml-build-examples/vendor/z3/build +# -cclib "-L. -L$(ML_LIB)/stublibs -L$(ML_LIB)/zarith " +# -L$(ROOT)/build # -package zarith # -linkpkg # -lpthread # -package z3 -# -I /home/ex/.opam/5.1.1/lib/zarith +# -I $(ML_LIB)/zarith # must not have # -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: - 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 /home/ex/.opam/5.1.1/lib/stublibs -# -I /home/ex/code/ocaml-build-examples/vendor/z3/build -# -I /home/ex/code/ocaml-build-examples/vendor/z3/build/src/api/ml +# -I $(ML_LIB)/zarith +# -I $(ML_LIB)/stublibs +# -I $(ROOT)/build +# -I $(ROOT)/build/src/api/ml # -t -b diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt index 5cd31d444..18ea6f15d 100644 --- a/src/api/ml/CMakeLists.txt +++ b/src/api/ml/CMakeLists.txt @@ -153,19 +153,36 @@ execute_process( 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" "-ocamlcflags" "-bin-annot" "-package" "zarith" - "-lz3" "-lstdc++" "-lpthread" - $<$:-lgmp> + ${c_lib_deps} "-L${libz3_path}" "-dllpath" "${libz3_path}" "-L${ocaml_stublibs_path}" "-dllpath" "${ocaml_stublibs_path}" + "-dllpath" "@rpath/dllz3ml.so" "-I" "${z3ml_bin}") +# OCaml's dll stublib hava platform-independent name `dll.so` + add_custom_command( - OUTPUT ${z3ml_bin}/dllz3ml${so_ext} + OUTPUT ${z3ml_bin}/dllz3ml.so ${z3ml_bin}/libz3ml.a ${z3ml_bin}/z3ml.cma ${z3ml_bin}/z3ml.cmxa @@ -184,7 +201,7 @@ add_custom_command( "-o" "${z3ml_bin}/z3ml.cmxs" "-I" "${z3ml_bin}" "${z3ml_bin}/z3ml.cmxa" - DEPENDS + DEPENDS libz3_z3ml ${z3ml_bin}/z3native_stubs.o ${z3ml_bin}/z3enums.cmo @@ -193,7 +210,7 @@ add_custom_command( ${z3ml_bin}/z3enums.cmx ${z3ml_bin}/z3native.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) ############################################################################### @@ -212,13 +229,14 @@ execute_process( OUTPUT_VARIABLE ocaml_pkg_zarith_path OUTPUT_STRIP_TRAILING_WHITESPACE) +# "-I" "+threads" + add_custom_command( OUTPUT ${z3ml_bin}/ml_example${bc_ext} ${z3ml_bin}/ml_example.bc.log COMMAND "${OCAMLFIND}" "ocamlc" "-o" "${z3ml_bin}/ml_example${bc_ext}" "-package" "zarith" - "-I" "+threads" "-I" "${z3ml_bin}" "-dllpath" "${z3ml_bin}" "-I" ${ocaml_stublibs_path} @@ -231,17 +249,18 @@ add_custom_command( ">" "${z3ml_bin}/ml_example.bc.log" DEPENDS ${z3ml_bin}/z3ml.cma - ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/dllz3ml.so ${z3ml_bin}/ml_example.ml COMMENT "Testing build and run ml_example bytecode" VERBATIM) +# "-I" "+threads" + add_custom_command( OUTPUT ${z3ml_bin}/ml_example${exe_ext} ${z3ml_bin}/ml_example.log COMMAND "${OCAMLFIND}" "ocamlopt" "-o" "${z3ml_bin}/ml_example${exe_ext}" - "-I" "+threads" "-package" "zarith" "-linkpkg" "-I" "${z3ml_bin}" @@ -251,7 +270,7 @@ add_custom_command( ">" "${z3ml_bin}/ml_example.log" DEPENDS ${z3ml_bin}/z3ml.cmxa - ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/dllz3ml.so ${z3ml_bin}/ml_example.ml COMMENT "Testing build and run ml_example natively" VERBATIM) @@ -269,7 +288,7 @@ add_custom_target(build_z3_ocaml_bindings ${z3ml_bin}/z3ml.cma ${z3ml_bin}/z3ml.cmxa ${z3ml_bin}/z3ml.cmxs - ${z3ml_bin}/dllz3ml${so_ext} + ${z3ml_bin}/dllz3ml.so ${z3ml_bin}/libz3ml.a 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 # 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) # add_custom_command( -# OUTPUT "${z3ml_bin}/dllz3ml${so_ext}" -# COMMAND mv "${z3ml_bin}/dllz3ml.pre${so_ext}" "${z3ml_bin}/dllz3ml${so_ext}" -# DEPENDS "${z3ml_bin}/dllz3ml.pre${so_ext}" +# OUTPUT "${z3ml_bin}/dllz3ml.so" +# COMMAND mv "${z3ml_bin}/dllz3ml.pre.so" "${z3ml_bin}/dllz3ml.so}" +# DEPENDS "${z3ml_bin}/dllz3ml.pre.so" # ) # else() # # if IS_OSX: # # 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 # add_custom_command( -# OUTPUT "${z3ml_bin}/dllz3ml${so_ext}" -# COMMAND mv "${z3ml_bin}/dllz3ml.pre${so_ext}" "${z3ml_bin}/dllz3ml${so_ext}" -# DEPENDS "${z3ml_bin}/dllz3ml.pre${so_ext}" +# OUTPUT "${z3ml_bin}/dllz3ml.so" +# COMMAND mv "${z3ml_bin}/dllz3ml.pre.so" "${z3ml_bin}/dllz3ml.so" +# DEPENDS "${z3ml_bin}/dllz3ml.so" # ) # endif() \ No newline at end of file From 4b3207505b7b7fe2b0c4faf64ca039a0c2f13073 Mon Sep 17 00:00:00 2001 From: Weng Shiwei Date: Wed, 19 Jun 2024 17:06:16 -0400 Subject: [PATCH 9/9] Minor. --- makefile | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/makefile b/makefile index 5b0b58a49..4bce3411d 100644 --- a/makefile +++ b/makefile @@ -131,6 +131,8 @@ ML_LIB=/home/ex/.opam/5.2.0/lib ML_LIB=/Users/ex/.opam/5.2.0/lib ROOT=$$(pwd) +MY_Z3=/home/ex/my_z3 +MY_Z3=/Users/ex/code/tmp/my-z3 ml0: mkdir -p build @@ -159,7 +161,7 @@ ml-mk: -DCMAKE_VERBOSE_MAKEFILE=TRUE \ -DZ3_BUILD_LIBZ3_SHARED=TRUE \ -DZ3_BUILD_OCAML_BINDINGS=TRUE \ - -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=/home/ex/my_z3 \ + -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=$(MY_Z3) \ --debug-trycompile \ ../ @@ -183,7 +185,7 @@ ml: --debug-trycompile \ ../ -# -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=/home/ex/my_z3 \ +# -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=$(MY_Z3) \ # -DZ3_USE_LIB_GMP=TRUE \ # LD_LIBRARY_PATH=build ./build/src/api/ml/ml_example