From f5a0520b838fa04ba5336daf35ffa268b670c6db Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 11 Dec 2012 16:35:39 +0000 Subject: [PATCH] More ML API Signed-off-by: Christoph M. Wintersteiger --- .gitignore | 3 + scripts/mk_util.py | 6 +- scripts/update_api.py | 211 +++++++++++++------------ src/api/ml/{ => old}/Makefile | 0 src/api/ml/{ => old}/Makefile.build | 0 src/api/ml/{ => old}/test_mlapi.ml | 0 src/api/ml/{ => old}/test_mlapiV3.ml | 0 src/api/ml/{ => old}/x3.ml | 0 src/api/ml/{ => old}/z3_stubs.c | 0 src/api/ml/{ => old}/z3_theory_stubs.c | 0 10 files changed, 120 insertions(+), 100 deletions(-) rename src/api/ml/{ => old}/Makefile (100%) rename src/api/ml/{ => old}/Makefile.build (100%) rename src/api/ml/{ => old}/test_mlapi.ml (100%) rename src/api/ml/{ => old}/test_mlapiV3.ml (100%) rename src/api/ml/{ => old}/x3.ml (100%) rename src/api/ml/{ => old}/z3_stubs.c (100%) rename src/api/ml/{ => old}/z3_theory_stubs.c (100%) diff --git a/.gitignore b/.gitignore index 3c4fb1218..f2a31c21e 100644 --- a/.gitignore +++ b/.gitignore @@ -64,9 +64,12 @@ src/util/version.h src/api/java/Native.cpp src/api/java/Native.java src/api/java/enumerations/*.java + *.bak doc/api doc/code 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 8543f1ffa..4249a04b0 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1286,9 +1286,9 @@ class MLComponent(Component): if is_ml_enabled(): 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 1e86dc0ef..9acdf1040 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/old/Makefile similarity index 100% rename from src/api/ml/Makefile rename to src/api/ml/old/Makefile diff --git a/src/api/ml/Makefile.build b/src/api/ml/old/Makefile.build similarity index 100% rename from src/api/ml/Makefile.build rename to src/api/ml/old/Makefile.build diff --git a/src/api/ml/test_mlapi.ml b/src/api/ml/old/test_mlapi.ml similarity index 100% rename from src/api/ml/test_mlapi.ml rename to src/api/ml/old/test_mlapi.ml diff --git a/src/api/ml/test_mlapiV3.ml b/src/api/ml/old/test_mlapiV3.ml similarity index 100% rename from src/api/ml/test_mlapiV3.ml rename to src/api/ml/old/test_mlapiV3.ml diff --git a/src/api/ml/x3.ml b/src/api/ml/old/x3.ml similarity index 100% rename from src/api/ml/x3.ml rename to src/api/ml/old/x3.ml diff --git a/src/api/ml/z3_stubs.c b/src/api/ml/old/z3_stubs.c similarity index 100% rename from src/api/ml/z3_stubs.c rename to src/api/ml/old/z3_stubs.c diff --git a/src/api/ml/z3_theory_stubs.c b/src/api/ml/old/z3_theory_stubs.c similarity index 100% rename from src/api/ml/z3_theory_stubs.c rename to src/api/ml/old/z3_theory_stubs.c