mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

Cleanup a bit.

Browse source
This commit is contained in:
Weng Shiwei 2024-06-16 20:26:28 -04:00
parent dbc7889d65
commit f0082a7856
No known key found for this signature in database
GPG key ID: CFB31B6A2D733ADB
2 changed files with 146 additions and 157 deletions
Download patch file Download diff file Expand all files Collapse all files

7
makefile
View file

@ -190,10 +190,13 @@ build-mk:
cd build && make -j16 build_z3_ocaml_bindings cd build && make -j16 build_z3_ocaml_bindings
.PHONY:build .PHONY:build
# /bin/sh: 1: ocamlfind ocamlc -where: not found build-nj:
cd build && ninja
.PHONY:build-nj
build: build:
cd build && ninja build_z3_ocaml_bindings cd build && ninja build_z3_ocaml_bindings
.PHONY:build-nj .PHONY:build
dot: dot:
cd build && dot -Tpng -o deps.png deps.dot cd build && dot -Tpng -o deps.png deps.dot

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

@ -1,6 +1,3 @@
###############################################################################
# Install
###############################################################################
find_package(OCaml REQUIRED) find_package(OCaml REQUIRED)
set(exe_ext ${CMAKE_EXECUTABLE_SUFFIX}) set(exe_ext ${CMAKE_EXECUTABLE_SUFFIX})
@ -13,7 +10,7 @@ set(z3ml_bin ${CMAKE_CURRENT_BINARY_DIR})
if (Z3_BUILD_OCAML_EXTERNAL_LIBZ3) if (Z3_BUILD_OCAML_EXTERNAL_LIBZ3)
add_custom_target(libz3_z3ml add_custom_target(libz3_z3ml
ALL 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}) set(libz3_path ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3})
else() else()
@ -24,13 +21,11 @@ else()
set(libz3_path ${PROJECT_BINARY_DIR}) set(libz3_path ${PROJECT_BINARY_DIR})
endif() endif()
set(Z3ml_native_stubs_c "${z3ml_bin}/z3native_stubs.c")
add_custom_command( add_custom_command(
OUTPUT OUTPUT
"${z3ml_bin}/z3native.ml" ${z3ml_bin}/z3native.ml
${Z3ml_native_stubs_c} ${z3ml_bin}/z3native_stubs.c
COMMAND "${PYTHON_EXECUTABLE}" COMMAND "${Python3_EXECUTABLE}"
"${PROJECT_SOURCE_DIR}/scripts/update_api.py" "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--ml-src-dir" "--ml-src-dir"
@ -38,37 +33,36 @@ add_custom_command(
"--ml-output-dir" "--ml-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}" "${CMAKE_CURRENT_BINARY_DIR}"
DEPENDS DEPENDS
${PROJECT_SOURCE_DIR}/scripts/update_api.py
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${PROJECT_SOURCE_DIR}/scripts/update_api.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${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 VERBATIM
) )
set(gen_z3enum "${z3ml_bin}/z3enums.ml")
add_custom_command( add_custom_command(
OUTPUT OUTPUT
${gen_z3enum} ${z3ml_bin}/z3enums.ml
COMMAND "${PYTHON_EXECUTABLE}" COMMAND "${Python3_EXECUTABLE}"
"${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"--ml-output-dir" "--ml-output-dir"
"${CMAKE_CURRENT_BINARY_DIR}" "${CMAKE_CURRENT_BINARY_DIR}"
DEPENDS DEPENDS
${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py
${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
"${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
COMMENT "Generating ${gen_z3enum}" COMMENT "Generating ${z3ml_bin}/z3enums.ml"
VERBATIM VERBATIM
) )
add_custom_command( add_custom_command(
OUTPUT "${z3ml_bin}/z3.ml" OUTPUT ${z3ml_bin}/z3.ml
"${z3ml_bin}/z3.mli" ${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.ml" "${z3ml_bin}/z3.ml"
COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.mli" "${z3ml_bin}/z3.mli" COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.mli" "${z3ml_bin}/z3.mli"
DEPENDS "${z3ml_src}/z3.ml" DEPENDS ${z3ml_src}/z3.ml
"${z3ml_src}/z3.mli" ${z3ml_src}/z3.mli
COMMENT "Copying z3.ml and z3.mli to build area") COMMENT "Copying z3.ml and z3.mli to build area")
set(z3ml_common_flags "-package" "zarith" set(z3ml_common_flags "-package" "zarith"
@ -88,17 +82,16 @@ add_custom_command(
"-I" "${PROJECT_SOURCE_DIR}/src/api" "-I" "${PROJECT_SOURCE_DIR}/src/api"
"-I" "${ocaml_stub_lib_path}" "-I" "${ocaml_stub_lib_path}"
"-c" "${z3ml_bin}/z3native_stubs.c" "-c" "${z3ml_bin}/z3native_stubs.c"
DEPENDS ${Z3ml_native_stubs_c} DEPENDS ${z3ml_bin}/z3native_stubs.c
COMMENT "Building z3native_stubs.o" COMMENT "Building z3native_stubs.o"
VERBATIM) VERBATIM)
# z3enum.ml depends on nothing # z3enum.ml depends on nothing
add_custom_command( add_custom_command(
OUTPUT "${z3ml_bin}/z3enums.mli" OUTPUT ${z3ml_bin}/z3enums.mli
"${z3ml_bin}/z3enums.cmi" ${z3ml_bin}/z3enums.cmi
"${z3ml_bin}/z3enums.cmo" ${z3ml_bin}/z3enums.cmo
"${z3ml_bin}/z3enums.cmx" ${z3ml_bin}/z3enums.cmx
COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags}
"-i" "-i"
"-c" "${z3ml_bin}/z3enums.ml" "-c" "${z3ml_bin}/z3enums.ml"
@ -109,17 +102,16 @@ add_custom_command(
"-c" "${z3ml_bin}/z3enums.ml" "-c" "${z3ml_bin}/z3enums.ml"
COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags}
"-c" "${z3ml_bin}/z3enums.ml" "-c" "${z3ml_bin}/z3enums.ml"
DEPENDS ${gen_z3enum} DEPENDS ${z3ml_bin}/z3enums.ml
COMMENT "Building z3enums.{mli,cmi,cmo,cmx}" COMMENT "Building z3enums.{mli,cmi,cmo,cmx}"
VERBATIM) VERBATIM)
# z3native.ml depends on z3enums # z3native.ml depends on z3enums
add_custom_command( add_custom_command(
OUTPUT "${z3ml_bin}/z3native.mli" OUTPUT ${z3ml_bin}/z3native.mli
"${z3ml_bin}/z3native.cmi" ${z3ml_bin}/z3native.cmi
"${z3ml_bin}/z3native.cmo" ${z3ml_bin}/z3native.cmo
"${z3ml_bin}/z3native.cmx" ${z3ml_bin}/z3native.cmx
COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags}
"-i" "-i"
"-c" "${z3ml_bin}/z3native.ml" "-c" "${z3ml_bin}/z3native.ml"
@ -130,30 +122,30 @@ add_custom_command(
"-c" "${z3ml_bin}/z3native.ml" "-c" "${z3ml_bin}/z3native.ml"
COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags}
"-c" "${z3ml_bin}/z3native.ml" "-c" "${z3ml_bin}/z3native.ml"
DEPENDS "${z3ml_bin}/z3enums.cmo" DEPENDS ${z3ml_bin}/z3enums.cmo
"${z3ml_bin}/z3native.ml" ${z3ml_bin}/z3native.ml
COMMENT "Building z3native.{mli,cmi,cmo,cmx}" COMMENT "Building z3native.{mli,cmi,cmo,cmx}"
VERBATIM) VERBATIM)
# z3.ml depends on z3enums and z3native # z3.ml depends on z3enums and z3native
add_custom_command( add_custom_command(
OUTPUT "${z3ml_bin}/z3.cmi" OUTPUT ${z3ml_bin}/z3.cmi
"${z3ml_bin}/z3.cmo" ${z3ml_bin}/z3.cmo
"${z3ml_bin}/z3.cmx" ${z3ml_bin}/z3.cmx
COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags}
"-c" "${z3ml_bin}/z3.mli" "-c" "${z3ml_bin}/z3.mli"
COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags}
"-c" "${z3ml_bin}/z3.ml" "-c" "${z3ml_bin}/z3.ml"
COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags}
"-c" "${z3ml_bin}/z3.ml" "-c" "${z3ml_bin}/z3.ml"
DEPENDS "${z3ml_bin}/z3enums.cmo" DEPENDS ${z3ml_bin}/z3enums.cmo
"${z3ml_bin}/z3native.cmo" ${z3ml_bin}/z3native.cmo
"${z3ml_bin}/z3.ml" ${z3ml_bin}/z3.ml
"${z3ml_bin}/z3.mli" ${z3ml_bin}/z3.mli
COMMENT "Building z3.cmo" COMMENT "Building z3.cmo"
VERBATIM) VERBATIM)
# making ocaml stublibs
execute_process( execute_process(
COMMAND ${OCAMLFIND} printconf destdir COMMAND ${OCAMLFIND} printconf destdir
OUTPUT_VARIABLE ocaml_destdir_path OUTPUT_VARIABLE ocaml_destdir_path
@ -173,37 +165,119 @@ set(ocamlmklib_flags "-o" "z3ml"
"-I" "${z3ml_bin}") "-I" "${z3ml_bin}")
add_custom_command( add_custom_command(
OUTPUT "${z3ml_bin}/dllz3ml${so_ext}" OUTPUT ${z3ml_bin}/dllz3ml${so_ext}
"${z3ml_bin}/libz3ml.a" ${z3ml_bin}/libz3ml.a
"${z3ml_bin}/z3ml.cma" ${z3ml_bin}/z3ml.cma
"${z3ml_bin}/z3ml.cmxa" ${z3ml_bin}/z3ml.cmxa
"${z3ml_bin}/z3ml.cmxs" ${z3ml_bin}/z3ml.cmxs
COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags} COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags}
"${z3ml_bin}/z3enums.cmo" "${z3ml_bin}/z3enums.cmo"
"${z3ml_bin}/z3native.cmo" "${z3ml_bin}/z3native.cmo"
"${z3ml_bin}/z3native_stubs.o" "${z3ml_bin}/z3native_stubs.o"
"${z3ml_bin}/z3.cmo" "${z3ml_bin}/z3.cmo"
COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags} COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags}
"${z3ml_bin}/z3enums.cmx" "${z3ml_bin}/z3enums.cmx"
"${z3ml_bin}/z3native.cmx" "${z3ml_bin}/z3native.cmx"
"${z3ml_bin}/z3native_stubs.o" "${z3ml_bin}/z3native_stubs.o"
"${z3ml_bin}/z3.cmx" "${z3ml_bin}/z3.cmx"
COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared" COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared"
"-o" "${z3ml_bin}/z3ml.cmxs" "-o" "${z3ml_bin}/z3ml.cmxs"
"-I" "${z3ml_bin}" "-I" "${z3ml_bin}"
"${z3ml_bin}/z3ml.cmxa" "${z3ml_bin}/z3ml.cmxa"
DEPENDS DEPENDS
libz3_z3ml libz3_z3ml
${z3ml_bin}/z3native_stubs.o ${z3ml_bin}/z3native_stubs.o
"${z3ml_bin}/z3enums.cmo" ${z3ml_bin}/z3enums.cmo
"${z3ml_bin}/z3native.cmo" ${z3ml_bin}/z3native.cmo
"${z3ml_bin}/z3.cmo" ${z3ml_bin}/z3.cmo
"${z3ml_bin}/z3enums.cmx" ${z3ml_bin}/z3enums.cmx
"${z3ml_bin}/z3native.cmx" ${z3ml_bin}/z3native.cmx
"${z3ml_bin}/z3.cmx" ${z3ml_bin}/z3.cmx
COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml${so_ext}, and libz3ml.a" COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml${so_ext}, and libz3ml.a"
VERBATIM) 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. # 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 # I don't know how to use conditional `COMMAND` nor specify a file dependency for itself
# Renaming it and back seems a simple solution. # Renaming it and back seems a simple solution.
@ -224,92 +298,4 @@ add_custom_command(
# COMMAND mv "${z3ml_bin}/dllz3ml.pre${so_ext}" "${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}" # DEPENDS "${z3ml_bin}/dllz3ml.pre${so_ext}"
# ) # )
# endif() # 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
###############################################################################