diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 68bb9da14..13c01567d 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -3027,10 +3027,12 @@ def mk_bindings(api_files): if is_dotnet_core_enabled(): dotnet_output_dir = os.path.join(BUILD_DIR, 'dotnet') mk_dir(dotnet_output_dir) + java_input_dir = None java_output_dir = None java_package_name = None if is_java_enabled(): java_output_dir = get_component('java').src_dir + java_input_dir = get_component('java').src_dir java_package_name = get_component('java').package_name ml_output_dir = None if is_ml_enabled(): @@ -3041,7 +3043,8 @@ def mk_bindings(api_files): api_output_dir=get_component('api').src_dir, z3py_output_dir=get_z3py_dir(), dotnet_output_dir=dotnet_output_dir, - java_output_dir=java_output_dir, + java_input_dir=java_input_dir, + java_output_dir=java_output_dir, java_package_name=java_package_name, ml_output_dir=ml_output_dir, ml_src_dir=ml_output_dir diff --git a/scripts/update_api.py b/scripts/update_api.py index 45899ddef..03aa80638 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -604,7 +604,7 @@ def java_array_element_type(p): else: return 'jlong' -def mk_java(java_dir, package_name): +def mk_java(java_src, java_dir, package_name): java_nativef = os.path.join(java_dir, 'Native.java') java_wrapperf = os.path.join(java_dir, 'Native.cpp') java_native = open(java_nativef, 'w') @@ -689,65 +689,9 @@ def mk_java(java_dir, package_name): java_native.write('}\n') java_wrapper = open(java_wrapperf, 'w') pkg_str = package_name.replace('.', '_') - java_wrapper.write('// Automatically generated file\n') - java_wrapper.write('#include\n') - java_wrapper.write('#include\n') - java_wrapper.write('#include"z3.h"\n') - java_wrapper.write('#ifdef __cplusplus\n') - java_wrapper.write('extern "C" {\n') - java_wrapper.write('#endif\n\n') - java_wrapper.write('#ifdef __GNUC__\n#if __GNUC__ >= 4\n#define DLL_VIS __attribute__ ((visibility ("default")))\n#else\n#define DLL_VIS\n#endif\n#else\n#define DLL_VIS\n#endif\n\n') - java_wrapper.write('#if defined(__LP64__) || defined(_WIN64)\n\n') - java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') - java_wrapper.write(' T * NEW = (OLD == 0) ? 0 : (T*) jenv->GetLongArrayElements(OLD, NULL);\n') - java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') - java_wrapper.write(' if (OLD != 0) jenv->ReleaseLongArrayElements(OLD, (jlong *) NEW, JNI_ABORT); \n\n') - java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n') - java_wrapper.write(' jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW); \n') - java_wrapper.write('#define SETLONGAREGION(OLD,Z,SZ,NEW) \\\n') - java_wrapper.write(' jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW) \n\n') - java_wrapper.write('#else\n\n') - java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') - java_wrapper.write(' T * NEW = 0; { \\\n') - java_wrapper.write(' jlong * temp = (OLD == 0) ? 0 : jenv->GetLongArrayElements(OLD, NULL); \\\n') - java_wrapper.write(' unsigned int size = (OLD == 0) ? 0 :jenv->GetArrayLength(OLD); \\\n') - java_wrapper.write(' if (OLD != 0) { \\\n') - java_wrapper.write(' NEW = (T*) (new int[size]); \\\n') - java_wrapper.write(' for (unsigned i=0; i < size; i++) \\\n') - java_wrapper.write(' NEW[i] = reinterpret_cast(temp[i]); \\\n') - java_wrapper.write(' jenv->ReleaseLongArrayElements(OLD, temp, JNI_ABORT); \\\n') - java_wrapper.write(' } \\\n') - java_wrapper.write(' } \n\n') - java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') - java_wrapper.write(' delete [] NEW; \n\n') - java_wrapper.write('#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \\\n') - java_wrapper.write(' { \\\n') - java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n') - java_wrapper.write(' jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)temp); \\\n') - java_wrapper.write(' for (int i = 0; i < (SZ); i++) \\\n') - java_wrapper.write(' NEW[i] = reinterpret_cast(temp[i]); \\\n') - java_wrapper.write(' delete [] temp; \\\n') - java_wrapper.write(' }\n\n') - java_wrapper.write('#define SETLONGAREGION(OLD,Z,SZ,NEW) \\\n') - java_wrapper.write(' { \\\n') - java_wrapper.write(' jlong * temp = new jlong[SZ]; \\\n') - java_wrapper.write(' for (int i = 0; i < (SZ); i++) \\\n') - java_wrapper.write(' temp[i] = reinterpret_cast(NEW[i]); \\\n') - java_wrapper.write(' jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,temp); \\\n') - java_wrapper.write(' delete [] temp; \\\n') - java_wrapper.write(' }\n\n') - java_wrapper.write('#endif\n\n') - java_wrapper.write('void Z3JavaErrorHandler(Z3_context c, Z3_error_code e)\n') - java_wrapper.write('{\n') - java_wrapper.write(' // Internal do-nothing error handler. This is required to avoid that Z3 calls exit()\n') - java_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n') - java_wrapper.write(' // wrappers below.\n') - java_wrapper.write('}\n\n') - java_wrapper.write('DLL_VIS JNIEXPORT void JNICALL Java_%s_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, jlong a0)\n' % pkg_str) - java_wrapper.write('{\n') - java_wrapper.write(' Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler);\n') - java_wrapper.write('}\n\n') - java_wrapper.write('') + with open(f"{java_src}/NativeStatic.txt") as ins: + for line in ins: + java_wrapper.write(line) for name, result, params in _dotnet_decls: java_wrapper.write('DLL_VIS JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name))) i = 0 @@ -1926,6 +1870,7 @@ def generate_files(api_files, api_output_dir=None, z3py_output_dir=None, dotnet_output_dir=None, + java_input_dir=None, java_output_dir=None, java_package_name=None, ml_output_dir=None, @@ -2003,7 +1948,7 @@ def generate_files(api_files, print("Generated '{}'".format(dotnet_file.name)) if java_output_dir: - mk_java(java_output_dir, java_package_name) + mk_java(java_input_dir, java_output_dir, java_package_name) if ml_output_dir: assert not ml_src_dir is None @@ -2027,6 +1972,10 @@ def main(args): dest="dotnet_output_dir", default=None, help="Directory to emit dotnet files. If not specified no files are emitted.") + parser.add_argument("--java-input-dir", + dest="java_input_dir", + default=None, + help="Directory where Java sources reside.") parser.add_argument("--java-output-dir", dest="java_output_dir", default=None, @@ -2049,6 +1998,9 @@ def main(args): if pargs.java_package_name == None: logging.error('--java-package-name must be specified') return 1 + if pargs.java_input_dir is None: + logging.error('--java-input-dir must be specified') + return 1 if pargs.ml_output_dir: if pargs.ml_src_dir is None: @@ -2064,6 +2016,7 @@ def main(args): api_output_dir=pargs.api_output_dir, z3py_output_dir=pargs.z3py_output_dir, dotnet_output_dir=pargs.dotnet_output_dir, + java_input_dir=pargs.java_input_dir, java_output_dir=pargs.java_output_dir, java_package_name=pargs.java_package_name, ml_output_dir=pargs.ml_output_dir, diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index dd7115aaa..695c946a3 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -19,6 +19,8 @@ add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}" COMMAND "${PYTHON_EXECUTABLE}" "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--java-input-dir" + "${CMAKE_CURRENT_SOURCE_DIR}" "--java-output-dir" "${CMAKE_CURRENT_BINARY_DIR}" "--java-package-name" diff --git a/src/api/java/NativeStatic.txt b/src/api/java/NativeStatic.txt new file mode 100644 index 000000000..2cd718627 --- /dev/null +++ b/src/api/java/NativeStatic.txt @@ -0,0 +1,78 @@ +// Automatically generated file +#include +#include +#include"z3.h" +#ifdef __cplusplus +extern "C" { +#endif + +#ifdef __GNUC__ +#if __GNUC__ >= 4 +#define DLL_VIS __attribute__ ((visibility ("default"))) +#else +#define DLL_VIS +#endif +#else +#define DLL_VIS +#endif + +#if defined(__LP64__) || defined(_WIN64) + +#define GETLONGAELEMS(T,OLD,NEW) \ + T * NEW = (OLD == 0) ? 0 : (T*) jenv->GetLongArrayElements(OLD, NULL); +#define RELEASELONGAELEMS(OLD,NEW) \ + if (OLD != 0) jenv->ReleaseLongArrayElements(OLD, (jlong *) NEW, JNI_ABORT); + +#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \ + jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW); +#define SETLONGAREGION(OLD,Z,SZ,NEW) \ + jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)NEW) + +#else + +#define GETLONGAELEMS(T,OLD,NEW) \ + T * NEW = 0; { \ + jlong * temp = (OLD == 0) ? 0 : jenv->GetLongArrayElements(OLD, NULL); \ + unsigned int size = (OLD == 0) ? 0 :jenv->GetArrayLength(OLD); \ + if (OLD != 0) { \ + NEW = (T*) (new int[size]); \ + for (unsigned i=0; i < size; i++) \ + NEW[i] = reinterpret_cast(temp[i]); \ + jenv->ReleaseLongArrayElements(OLD, temp, JNI_ABORT); \ + } \ + } + +#define RELEASELONGAELEMS(OLD,NEW) \ + delete [] NEW; + +#define GETLONGAREGION(T,OLD,Z,SZ,NEW) \ + { \ + jlong * temp = new jlong[SZ]; \ + jenv->GetLongArrayRegion(OLD,Z,(jsize)SZ,(jlong*)temp); \ + for (int i = 0; i < (SZ); i++) \ + NEW[i] = reinterpret_cast(temp[i]); \ + delete [] temp; \ + } + +#define SETLONGAREGION(OLD,Z,SZ,NEW) \ + { \ + jlong * temp = new jlong[SZ]; \ + for (int i = 0; i < (SZ); i++) \ + temp[i] = reinterpret_cast(NEW[i]); \ + jenv->SetLongArrayRegion(OLD,Z,(jsize)SZ,temp); \ + delete [] temp; \ + } + +#endif + +void Z3JavaErrorHandler(Z3_context c, Z3_error_code e) +{ + // Internal do-nothing error handler. This is required to avoid that Z3 calls exit() + // upon errors, but the actual error handling is done by throwing exceptions in the + // wrappers below. +} + +DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, jlong a0) +{ + Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler); +}