diff --git a/.gitignore b/.gitignore index 2ae719b85..a3fa5e919 100644 --- a/.gitignore +++ b/.gitignore @@ -61,6 +61,7 @@ src/util/version.h src/api/java/Native.cpp src/api/java/Native.java src/api/java/enumerations/*.java + *.bak doc/api doc/code @@ -76,4 +77,6 @@ src/api/ml/z3enums.ml src/api/ml/z3.mllib src/api/ml/z3_native.c src/api/ml/z3_native.ml +src/api/ml/native.c +src/api/ml/Z3.ml src/api/ml/z3_enums.ml diff --git a/scripts/mk_util.py b/scripts/mk_util.py index d019e24e9..d324e5206 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1430,9 +1430,9 @@ class MLComponent(Component): out.write('\n\n') mk_dir(os.path.join(BUILD_DIR, 'api', 'ml')) libfile = '%s$(LIB_EXT)' % self.lib_name - out.write('%s: libz3$(SO_EXT) %s\n' % (libfile, os.path.join(self.to_src_dir, 'z3_native.c'))) - out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/ml/z3_native$(OBJ_EXT) %s/z3_native.c\n' % self.to_src_dir) - out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3ml$(LIB_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' % os.path.join('api', 'ml', 'z3_native')) + out.write('%s: libz3$(SO_EXT) %s\n' % (libfile, os.path.join(self.to_src_dir, 'native.c'))) + out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/ml/z3_native$(OBJ_EXT) -I%s %s/native.c\n' % (get_component(API_COMPONENT).to_src_dir, self.to_src_dir)) + out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3ml$(LIB_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' % os.path.join('api', 'ml', 'native')) out.write('ml: %s\n' % libfile) out.write('\n') diff --git a/scripts/update_api.py b/scripts/update_api.py index c1bb22a44..72fd32702 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1075,12 +1075,12 @@ def mk_ml(): if not is_ml_enabled(): return ml_dir = get_component('ml').src_dir - ml_nativef = os.path.join(ml_dir, 'z3_native.ml') - ml_wrapperf = os.path.join(ml_dir, 'z3_native.c') + ml_nativef = os.path.join(ml_dir, 'Z3.ml') + ml_wrapperf = os.path.join(ml_dir, 'native.c') ml_native = open(ml_nativef, 'w') ml_native.write('(* Automatically generated file *)\n') ml_native.write('\n') - ml_native.write('module Z3 = struct\n\n') + ml_native.write('module Z3Native = struct\n\n') ml_native.write('type context\n') ml_native.write('and symbol\n') ml_native.write('and ast\n') @@ -1166,101 +1166,118 @@ def mk_ml(): ml_wrapper.write('#ifdef Custom_tag\n') ml_wrapper.write('#include \n') ml_wrapper.write('#include \n') - ml_wrapper.write('#endif\n') - # for name, result, params in _dotnet_decls: - # java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name))) - # i = 0; - # for param in params: - # java_wrapper.write(', ') - # java_wrapper.write('%s a%d' % (param2javaw(param), i)) - # i = i + 1 - # java_wrapper.write(') {\n') - # # preprocess arrays, strings, in/out arguments - # i = 0 - # for param in params: - # k = param_kind(param) - # if k == OUT or k == INOUT: - # java_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i)) - # elif k == IN_ARRAY or k == INOUT_ARRAY: - # if param_type(param) == INT or param_type(param) == UINT: - # java_wrapper.write(' %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i)) - # else: - # java_wrapper.write(' GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, i)) - # elif k == OUT_ARRAY: - # java_wrapper.write(' %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)), - # i, - # type2str(param_type(param)), - # param_array_capacity_pos(param), - # type2str(param_type(param)))) - # if param_type(param) == INT or param_type(param) == UINT: - # java_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i)) - # else: - # java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i)) - # elif k == IN and param_type(param) == STRING: - # java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i)) - # i = i + 1 - # # invoke procedure - # java_wrapper.write(' ') - # if result != VOID: - # java_wrapper.write('%s result = ' % type2str(result)) - # java_wrapper.write('%s(' % name) - # i = 0 - # first = True - # for param in params: - # if first: - # first = False - # else: - # java_wrapper.write(', ') - # k = param_kind(param) - # if k == OUT or k == INOUT: - # java_wrapper.write('&_a%s' % i) - # elif k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY: - # java_wrapper.write('_a%s' % i) - # elif k == IN and param_type(param) == STRING: - # java_wrapper.write('_a%s' % i) - # else: - # java_wrapper.write('(%s)a%i' % (param2str(param), i)) - # i = i + 1 - # java_wrapper.write(');\n') - # # cleanup - # i = 0 - # for param in params: - # k = param_kind(param) - # if k == OUT_ARRAY: - # if param_type(param) == INT or param_type(param) == UINT: - # java_wrapper.write(' jenv->SetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i)) - # else: - # java_wrapper.write(' SETLONGAREGION(a%s, 0, a%s, _a%s);\n' % (i, param_array_capacity_pos(param), i)) - # java_wrapper.write(' free(_a%s);\n' % i) - # elif k == IN_ARRAY or k == OUT_ARRAY: - # if param_type(param) == INT or param_type(param) == UINT: - # java_wrapper.write(' jenv->ReleaseIntArrayElements(a%s, (jint*)_a%s, JNI_ABORT);\n' % (i, i)) - # else: - # java_wrapper.write(' RELEASELONGAELEMS(a%s, _a%s);\n' % (i, i)) + ml_wrapper.write('#endif\n\n') + ml_wrapper.write('#include \n\n') + for name, result, params in _dotnet_decls: + #return type = type2ml(result) + ml_wrapper.write('CAMLprim value n_%s(' % ml_method_name(name)) + first = True + i = 0 + for param in params: + if first: + first = False + else: + ml_wrapper.write(', ') + ml_wrapper.write('value a%d' % i) + # param type = param2ml(param) + i = i + 1 + ml_wrapper.write(') {\n') + ml_wrapper.write(' CAMLparam%d(' % len(params)) + i = 0 + first = True + for param in params: + if first: + first = False + else: + ml_wrapper.write(', ') + ml_wrapper.write('a%d' % i) + i = i + 1 + ml_wrapper.write(');\n') + # preprocess arrays, strings, in/out arguments + i = 0 + for param in params: + k = param_kind(param) + if k == OUT or k == INOUT: + ml_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i)) + elif k == IN_ARRAY or k == INOUT_ARRAY: + if param_type(param) == INT or param_type(param) == UINT: + ml_wrapper.write(' %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i)) + else: + ml_wrapper.write(' GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, i)) + elif k == OUT_ARRAY: + ml_wrapper.write(' %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)), + i, + type2str(param_type(param)), + param_array_capacity_pos(param), + type2str(param_type(param)))) + if param_type(param) == INT or param_type(param) == UINT: + ml_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i)) + else: + ml_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i)) + elif k == IN and param_type(param) == STRING: + ml_wrapper.write(' Z3_string _a%s = (Z3_string) String_val(a%s);\n' % (i, i)) + i = i + 1 + # invoke procedure + ml_wrapper.write(' ') + if result != VOID: + ml_wrapper.write('%s result = ' % type2str(result)) + ml_wrapper.write('%s(' % name) + i = 0 + first = True + for param in params: + if first: + first = False + else: + ml_wrapper.write(', ') + k = param_kind(param) + if k == OUT or k == INOUT: + ml_wrapper.write('&_a%s' % i) + elif k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY: + ml_wrapper.write('_a%s' % i) + elif k == IN and param_type(param) == STRING: + ml_wrapper.write('_a%s' % i) + else: + ml_wrapper.write('(%s)a%i' % (param2str(param), i)) + i = i + 1 + ml_wrapper.write(');\n') + # cleanup + i = 0 + for param in params: + k = param_kind(param) + if k == OUT_ARRAY: + if param_type(param) == INT or param_type(param) == UINT: + ml_wrapper.write(' jenv->SetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i)) + else: + ml_wrapper.write(' SETLONGAREGION(a%s, 0, a%s, _a%s);\n' % (i, param_array_capacity_pos(param), i)) + ml_wrapper.write(' free(_a%s);\n' % i) + elif k == IN_ARRAY or k == OUT_ARRAY: + if param_type(param) == INT or param_type(param) == UINT: + ml_wrapper.write(' jenv->ReleaseIntArrayElements(a%s, (jint*)_a%s, JNI_ABORT);\n' % (i, i)) + else: + ml_wrapper.write(' RELEASELONGAELEMS(a%s, _a%s);\n' % (i, i)) - # elif k == OUT or k == INOUT: - # if param_type(param) == INT or param_type(param) == UINT: - # java_wrapper.write(' {\n') - # java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i) - # java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n') - # java_wrapper.write(' jenv->SetIntField(a%s, fid, (jint) _a%s);\n' % (i, i)) - # java_wrapper.write(' }\n') - # else: - # java_wrapper.write(' {\n') - # java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i) - # java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "J");\n') - # java_wrapper.write(' jenv->SetLongField(a%s, fid, (jlong) _a%s);\n' % (i, i)) - # java_wrapper.write(' }\n') - # i = i + 1 - # # return - # if result == STRING: - # java_wrapper.write(' return jenv->NewStringUTF(result);\n') - # elif result != VOID: - # java_wrapper.write(' return (%s) result;\n' % type2javaw(result)) - # java_wrapper.write('}\n') - # java_wrapper.write('#ifdef __cplusplus\n') - # java_wrapper.write('}\n') - # java_wrapper.write('#endif\n') + elif k == OUT or k == INOUT: + if param_type(param) == INT or param_type(param) == UINT: + ml_wrapper.write(' {\n') + ml_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i) + ml_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n') + ml_wrapper.write(' jenv->SetIntField(a%s, fid, (jint) _a%s);\n' % (i, i)) + ml_wrapper.write(' }\n') + else: + ml_wrapper.write(' {\n') + ml_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i) + ml_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "J");\n') + ml_wrapper.write(' jenv->SetLongField(a%s, fid, (jlong) _a%s);\n' % (i, i)) + ml_wrapper.write(' }\n') + i = i + 1 + # return + if result == STRING: + ml_wrapper.write(' return caml_copy_string(result);\n') + elif result == VOID: + ml_wrapper.write(' CAMLreturn(Val_unit);\n') + elif result != VOID: + ml_wrapper.write(' return (value) result;\n') + ml_wrapper.write('}\n\n') if is_verbose(): print "Generated '%s'" % ml_nativef diff --git a/src/api/ml/Makefile b/src/api/ml/Makefile deleted file mode 100644 index 96fd0a55d..000000000 --- a/src/api/ml/Makefile +++ /dev/null @@ -1,10 +0,0 @@ -# This is a temporary support file for emacs annotations. -# It does not compile the Z3 ML API; this will be built -# in the top-level build directory. - -all: - ocamlbuild -cflag -annot z3.cmxa - -doc: *.ml - mkdir -p doc - ocamldoc -html -d doc -I _build -sort *.mli -hide Z3