From c998cf2cdbace609a79057a7d20f88e12170ce5e Mon Sep 17 00:00:00 2001 From: Weng Shiwei Date: Sun, 16 Jun 2024 20:07:49 -0400 Subject: [PATCH] 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 +# )