diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 5cfcbb4d3..7a054256d 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1428,6 +1428,13 @@ class MLComponent(Component): if IS_WINDOWS: out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(LIB_EXT)') 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('ml: %s\n' % libfile) + out.write('\n') def main_component(self): return is_ml_enabled() @@ -1841,7 +1848,11 @@ def mk_config(): if GPROF: print('gprof: enabled') print('Python version: %s' % distutils.sysconfig.get_python_version()) +<<<<<<< HEAD print('ML API: %s' % is_ml_enabled()) +======= + print 'ML API: %s' % is_ml_enabled() +>>>>>>> Beginnings of a new ML API if is_java_enabled(): print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) diff --git a/scripts/update_api.py b/scripts/update_api.py index 4669b78fc..945496781 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -213,7 +213,10 @@ def type2javaw(ty): def type2ml(ty): global Type2ML - return Type2ML[ty] + if (ty >= FIRST_OBJ_ID): + return 'long' + else: + return Type2ML[ty] def _in(ty): return (IN, ty); @@ -1066,216 +1069,76 @@ def mk_bindings(): exe_c.write("}\n") def ml_method_name(name): - return name[3:] # Remove Z3_ - -def is_out_param(p): - if param_kind(p) == OUT or param_kind(p) == INOUT or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT_MANAGED_ARRAY: - return True - else: - return False - -def outparams(params): - op = [] - for param in params: - if is_out_param(param): - op.append(param) - return op - -def is_in_param(p): - if param_kind(p) == IN or param_kind(p) == INOUT or param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY: - return True - else: - return False - -def inparams(params): - ip = [] - for param in params: - if is_in_param(param): - ip.append(param) - return ip - -def is_array_param(p): - if param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT_ARRAY: - return True - else: - return False - -def arrayparams(params): - op = [] - for param in params: - if is_array_param(param): - op.append(param) - return op - - -def ml_unwrap(t, ts, s): - if t == STRING: - return '(' + ts + ') String_val(' + s + ')' - elif t == BOOL: - return '(' + ts + ') Bool_val(' + s + ')' - elif t == INT or t == PRINT_MODE or t == ERROR_CODE: - return '(' + ts + ') Int_val(' + s + ')' - elif t == UINT: - return '(' + ts + ') Unsigned_int_val(' + s + ')' - elif t == INT64: - return '(' + ts + ') Long_val(' + s + ')' - elif t == UINT64: - return '(' + ts + ') Unsigned_long_val(' + s + ')' - elif t == DOUBLE: - return '(' + ts + ') Double_val(' + s + ')' - else: - return '* (' + ts + '*) Data_custom_val(' + s + ')' - -def ml_set_wrap(t, d, n): - if t == VOID: - return d + ' = Val_unit;' - elif t == BOOL: - return d + ' = Val_bool(' + n + ');' - elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE: - return d + ' = Val_int(' + n + ');' - elif t == INT64 or t == UINT64: - return d + ' = Val_long(' + n + ');' - elif t == DOUBLE: - return 'Store_double_val(' + d + ', ' + n + ');' - elif t == STRING: - return d + ' = caml_copy_string((const char*) ' + n + ');' - else: - ts = type2str(t) - return d + ' = caml_alloc_custom(&default_custom_ops, sizeof(' + ts + '), 0, 1); memcpy( Data_custom_val(' + d + '), &' + n + ', sizeof(' + ts + '));' + result = '' + name = name[3:] # Remove Z3_ + return result def mk_ml(): - global Type2Str if not is_ml_enabled(): return ml_dir = get_component('ml').src_dir - ml_nativef = os.path.join(ml_dir, 'z3native.ml') - ml_nativefi = os.path.join(ml_dir, 'z3native.mli') - ml_wrapperf = os.path.join(ml_dir, 'z3native_stubs.c') + ml_nativef = os.path.join(ml_dir, 'z3_native.ml') + ml_wrapperf = os.path.join(ml_dir, 'z3_native.c') ml_native = open(ml_nativef, 'w') - ml_i = open(ml_nativefi, 'w') - ml_native.write('(* Automatically generated file *)\n\n') - ml_native.write('(** The native (raw) interface to the dynamic Z3 library. *)\n\n') - ml_i.write('(* Automatically generated file *)\n\n') - ml_i.write('(** The native (raw) interface to the dynamic Z3 library. *)\n\n') - ml_i.write('(**/**)\n\n'); - ml_native.write('open Z3enums\n\n') - ml_native.write('(**/**)\n') - ml_native.write('type ptr\n') - ml_i.write('type ptr\n') - ml_native.write('and z3_symbol = ptr\n') - ml_i.write('and z3_symbol = ptr\n') - for k, v in Type2Str.iteritems(): - if is_obj(k): - ml_native.write('and %s = ptr\n' % v.lower()) - ml_i.write('and %s = ptr\n' % v.lower()) + ml_native.write('// Automatically generated file\n') ml_native.write('\n') - ml_i.write('\n') - ml_native.write('external is_null : ptr -> bool\n = "n_is_null"\n\n') - ml_native.write('external mk_null : unit -> ptr\n = "n_mk_null"\n\n') - ml_native.write('external set_internal_error_handler : ptr -> unit\n = "n_set_internal_error_handler"\n\n') - ml_native.write('exception Exception of string\n\n') - ml_i.write('val is_null : ptr -> bool\n') - ml_i.write('val mk_null : unit -> ptr\n') - ml_i.write('val set_internal_error_handler : ptr -> unit\n\n') - ml_i.write('exception Exception of string\n\n') - - # ML declarations - ml_native.write('module ML2C = struct\n\n') for name, result, params in _dotnet_decls: - ml_native.write(' external n_%s : ' % ml_method_name(name)) - ml_i.write('val %s : ' % ml_method_name(name)) - ip = inparams(params) - op = outparams(params) - if len(ip) == 0: - ml_native.write(' unit -> ') - ml_i.write(' unit -> ') - for p in ip: - ml_native.write('%s -> ' % param2ml(p)) - ml_i.write('%s -> ' % param2ml(p)) - if len(op) > 0: - ml_native.write('(') - ml_i.write('(') + ml_native.write(' external %s : (' % ml_method_name(name)) first = True - if result != VOID or len(op) == 0: - ml_native.write('%s' % type2ml(result)) - ml_i.write('%s' % type2ml(result)) - first = False - for p in op: + i = 0; + for param in params: if first: first = False else: - ml_native.write(' * ') - ml_i.write(' * ') - ml_native.write('%s' % param2ml(p)) - ml_i.write('%s' % param2ml(p)) - if len(op) > 0: - ml_native.write(')') - ml_i.write(')') - ml_native.write('\n') - ml_i.write('\n') - if len(ip) > 5: - ml_native.write(' = "n_%s_bytecode"\n' % ml_method_name(name)) - ml_native.write(' "n_%s"\n' % ml_method_name(name)) - else: - ml_native.write(' = "n_%s"\n' % ml_method_name(name)) - ml_native.write('\n') - ml_native.write(' end\n\n') - ml_i.write('\n(**/**)\n'); - - # Exception wrappers - for name, result, params in _dotnet_decls: - ip = inparams(params) - op = outparams(params) - ml_native.write(' let %s ' % ml_method_name(name)) - - first = True - i = 0; - for p in params: - if is_in_param(p): - if first: - first = False; - else: - ml_native.write(' ') - ml_native.write('a%d' % i) + ml_native.write(', ') + ml_native.write('%s a%d' % (param2ml(param), i)) i = i + 1 - if len(ip) == 0: - ml_native.write('()') - ml_native.write(' = \n') - ml_native.write(' ') - if result == VOID and len(op) == 0: - ml_native.write('let _ = ') - else: - ml_native.write('let res = ') - ml_native.write('(ML2C.n_%s' % (ml_method_name(name))) - if len(ip) == 0: - ml_native.write(' ()') - first = True - i = 0; - for p in params: - if is_in_param(p): - ml_native.write(' a%d' % i) - i = i + 1 - ml_native.write(') in\n') - if name not in Unwrapped and len(params) > 0 and param_type(params[0]) == CONTEXT: - ml_native.write(' let err = (error_code_of_int (ML2C.n_get_error_code a0)) in \n') - ml_native.write(' if err <> OK then\n') - ml_native.write(' raise (Exception (ML2C.n_get_error_msg_ex a0 (int_of_error_code err)))\n') - ml_native.write(' else\n') - if result == VOID and len(op) == 0: - ml_native.write(' ()\n') - else: - ml_native.write(' res\n') - ml_native.write('\n') - ml_native.write('(**/**)\n') - - # C interface + ml_native.write('%s)\n' % (type2ml(result))) + # ml_native.write(' = "NATIVE_%s"' % ml_method_name(name)) + # ml_native.write('\n\n') + # # Exception wrappers + # for name, result, params in _dotnet_decls: + # java_native.write(' public static %s %s(' % (type2java(result), java_method_name(name))) + # first = True + # i = 0; + # for param in params: + # if first: + # first = False + # else: + # java_native.write(', ') + # java_native.write('%s a%d' % (param2java(param), i)) + # i = i + 1 + # java_native.write(')') + # if len(params) > 0 and param_type(params[0]) == CONTEXT: + # java_native.write(' throws Z3Exception') + # java_native.write('\n') + # java_native.write(' {\n') + # java_native.write(' ') + # if result != VOID: + # java_native.write('%s res = ' % type2java(result)) + # java_native.write('INTERNAL%s(' % (java_method_name(name))) + # first = True + # i = 0; + # for param in params: + # if first: + # first = False + # else: + # java_native.write(', ') + # java_native.write('a%d' % i) + # i = i + 1 + # java_native.write(');\n') + # if len(params) > 0 and param_type(params[0]) == CONTEXT: + # java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n') + # java_native.write(' if (err != Z3_error_code.Z3_OK)\n') + # java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n') + # if result != VOID: + # java_native.write(' return res;\n') + # java_native.write(' }\n\n') + # java_native.write('}\n') ml_wrapper = open(ml_wrapperf, 'w') ml_wrapper.write('// Automatically generated file\n\n') ml_wrapper.write('#include \n') - ml_wrapper.write('#include \n\n') - ml_wrapper.write('#ifdef __cplusplus\n') - ml_wrapper.write('extern "C" {\n') - ml_wrapper.write('#endif\n') + ml_wrapper.write('#include \n') ml_wrapper.write('#include \n') ml_wrapper.write('#include \n') ml_wrapper.write('#include \n') @@ -1285,237 +1148,100 @@ def mk_ml(): ml_wrapper.write('#include \n') ml_wrapper.write('#include \n') ml_wrapper.write('#endif\n') - ml_wrapper.write('#ifdef __cplusplus\n') - ml_wrapper.write('}\n') - ml_wrapper.write('#endif\n\n') - ml_wrapper.write('#include \n\n') - ml_wrapper.write('#define CAMLlocal6(X1,X2,X3,X4,X5,X6) \\\n') - ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n') - ml_wrapper.write(' CAMLlocal1(X6) \n') - ml_wrapper.write('#define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \\\n') - ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n') - ml_wrapper.write(' CAMLlocal2(X6,X7) \n') - ml_wrapper.write('#define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \\\n') - ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n') - ml_wrapper.write(' CAMLlocal3(X6,X7,X8) \n') - ml_wrapper.write('\n') - ml_wrapper.write('#define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \\\n') - ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') - ml_wrapper.write(' CAMLxparam2(X6,X7) \n') - ml_wrapper.write('#define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \\\n') - ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') - ml_wrapper.write(' CAMLxparam3(X6,X7,X8) \n') - ml_wrapper.write('#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \\\n') - ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') - ml_wrapper.write(' CAMLxparam4(X6,X7,X8,X9) \n') - ml_wrapper.write('#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \\\n') - ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') - ml_wrapper.write(' CAMLxparam5(X6,X7,X8,X9,X10); \\\n') - ml_wrapper.write(' CAMLxparam2(X11,X12) \n') - ml_wrapper.write('#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \\\n') - ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') - ml_wrapper.write(' CAMLxparam5(X6,X7,X8,X9,X10); \\\n') - ml_wrapper.write(' CAMLxparam3(X11,X12,X13) \n') - ml_wrapper.write('\n\n') - ml_wrapper.write('static struct custom_operations default_custom_ops = {\n') - ml_wrapper.write(' (char*) "default handling",\n') - ml_wrapper.write(' custom_finalize_default,\n') - ml_wrapper.write(' custom_compare_default,\n') - ml_wrapper.write(' custom_hash_default,\n') - ml_wrapper.write(' custom_serialize_default,\n') - ml_wrapper.write(' custom_deserialize_default\n') - ml_wrapper.write('};\n\n') - ml_wrapper.write('#ifdef __cplusplus\n') - ml_wrapper.write('extern "C" {\n') - ml_wrapper.write('#endif\n\n') - ml_wrapper.write('CAMLprim value n_is_null(value p) {\n') - ml_wrapper.write(' void * t = * (void**) Data_custom_val(p);\n') - ml_wrapper.write(' return Val_bool(t == 0);\n') - ml_wrapper.write('}\n\n') - ml_wrapper.write('CAMLprim value n_mk_null( void ) {\n') - ml_wrapper.write(' CAMLparam0();\n') - ml_wrapper.write(' CAMLlocal1(result);\n') - ml_wrapper.write(' void * z3_result = 0;\n') - ml_wrapper.write(' result = caml_alloc_custom(&default_custom_ops, sizeof(void*), 0, 1);\n') - ml_wrapper.write(' memcpy( Data_custom_val(result), &z3_result, sizeof(void*));\n') - ml_wrapper.write(' CAMLreturn (result);\n') - ml_wrapper.write('}\n\n') - ml_wrapper.write('void MLErrorHandler(Z3_context c, Z3_error_code e)\n') - ml_wrapper.write('{\n') - ml_wrapper.write(' // Internal do-nothing error handler. This is required to avoid that Z3 calls exit()\n') - ml_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n') - ml_wrapper.write(' // wrappers below.\n') - ml_wrapper.write('}\n\n') - ml_wrapper.write('void n_set_internal_error_handler(value a0)\n') - ml_wrapper.write('{\n') - ml_wrapper.write(' Z3_context _a0 = * (Z3_context*) Data_custom_val(a0);\n') - ml_wrapper.write(' Z3_set_error_handler(_a0, MLErrorHandler);\n') - ml_wrapper.write('}\n\n') - for name, result, params in _dotnet_decls: - ip = inparams(params) - op = outparams(params) - ap = arrayparams(params) - ret_size = len(op) - if result != VOID: - ret_size = ret_size + 1 - - # Setup frame - ml_wrapper.write('CAMLprim value n_%s(' % ml_method_name(name)) - first = True - i = 0 - for p in params: - if is_in_param(p): - if first: - first = False - else: - ml_wrapper.write(', ') - ml_wrapper.write('value a%d' % i) - i = i + 1 - ml_wrapper.write(') {\n') - ml_wrapper.write(' CAMLparam%d(' % len(ip)) - i = 0 - first = True - for p in params: - if is_in_param(p): - if first: - first = False - else: - ml_wrapper.write(', ') - ml_wrapper.write('a%d' % i) - i = i + 1 - ml_wrapper.write(');\n') - i = 0 - if len(op) + len(ap) == 0: - ml_wrapper.write(' CAMLlocal1(result);\n') - else: - c = 0 - for p in params: - if is_out_param(p) or is_array_param(p): - c = c + 1 - ml_wrapper.write(' CAMLlocal%s(result, res_val' % (c+2)) - for p in params: - if is_out_param(p) or is_array_param(p): - ml_wrapper.write(', _a%s_val' % i) - i = i + 1 - ml_wrapper.write(');\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)) - if len(ap) != 0: - ml_wrapper.write(' unsigned _i;\n') - - # declare locals, preprocess arrays, strings, in/out arguments - i = 0 - for param in params: - k = param_kind(param) - if k == OUT_ARRAY: - ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % ( - type2str(param_type(param)), - i, - type2str(param_type(param)), - type2str(param_type(param)), - param_array_capacity_pos(param))) - elif k == OUT_MANAGED_ARRAY: - ml_wrapper.write(' %s * _a%s = 0;\n' % (type2str(param_type(param)), i)) - elif k == IN_ARRAY or k == INOUT_ARRAY: - t = param_type(param) - ts = type2str(t) - ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * _a%s);\n' % (ts, i, ts, ts, param_array_capacity_pos(param))) - elif k == IN: - t = param_type(param) - ml_wrapper.write(' %s _a%s = %s;\n' % (type2str(t), i, ml_unwrap(t, type2str(t), 'a' + str(i)))) - elif k == OUT: - ml_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i)) - elif k == INOUT: - ml_wrapper.write(' %s _a%s = a%s;\n' % (type2str(param_type(param)), i, i)) - i = i + 1 - - if result != VOID: - ml_wrapper.write(' %s z3_result;\n' % type2str(result)) - - i = 0 - for param in params: - k = param_kind(param) - if k == IN_ARRAY or k == INOUT_ARRAY: - t = param_type(param) - ts = type2str(t) - ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) { _a%s[_i] = %s; }\n' % (param_array_capacity_pos(param), i, ml_unwrap(t, ts, 'Field(a' + str(i) + ', _i)'))) - i = i + 1 - - # invoke procedure - ml_wrapper.write(' ') - if result != VOID: - ml_wrapper.write('z3_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 or k == OUT_MANAGED_ARRAY: - ml_wrapper.write('&_a%s' % i) - else: - ml_wrapper.write('_a%i' % i) - i = i + 1 - ml_wrapper.write(');\n') - - # convert output params - if len(op) > 0: - if result != VOID: - ml_wrapper.write(' %s\n' % ml_set_wrap(result, "res_val", "z3_result")) - i = 0; - for p in params: - if param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY: - ml_wrapper.write(' _a%s_val = caml_alloc(_a%s, 0);\n' % (i, param_array_capacity_pos(p))) - ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) { value t; %s Store_field(_a%s_val, _i, t); }\n' % (param_array_capacity_pos(p), ml_set_wrap(param_type(p), 't', '_a' + str(i) + '[_i]'), i)) - elif param_kind(p) == OUT_MANAGED_ARRAY: - ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a" + str(i) )) - elif is_out_param(p): - ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a" + str(i) )) - i = i + 1 - - # return tuples - if len(op) == 0: - ml_wrapper.write(' %s\n' % ml_set_wrap(result, "result", "z3_result")) - else: - ml_wrapper.write(' result = caml_alloc(%s, 0);\n' % ret_size) - i = j = 0 - if result != VOID: - ml_wrapper.write(' Store_field(result, 0, res_val);\n') - j = j + 1 - for p in params: - if is_out_param(p): - ml_wrapper.write(' Store_field(result, %s, _a%s_val);\n' % (j, i)) - j = j + 1; - i = i + 1 - - # local array cleanup - i = 0 - for p in params: - k = param_kind(p) - if k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY: - ml_wrapper.write(' free(_a%s);\n' % i) - i = i + 1 - - # return - ml_wrapper.write(' CAMLreturn(result);\n') - ml_wrapper.write('}\n\n') - if len(ip) > 5: - ml_wrapper.write('CAMLprim value n_%s_bytecode(value * argv, int argn) {\n' % ml_method_name(name)) - ml_wrapper.write(' return n_%s(' % ml_method_name(name)) - i = 0 - while i < len(ip): - if i == 0: - ml_wrapper.write('argv[0]') - else: - ml_wrapper.write(', argv[%s]' % i) - i = i + 1 - ml_wrapper.write(');\n}\n') - ml_wrapper.write('\n\n') - ml_wrapper.write('#ifdef __cplusplus\n') - ml_wrapper.write('}\n') - ml_wrapper.write('#endif\n') + # 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') if is_verbose(): print "Generated '%s'" % ml_nativef diff --git a/src/api/ml/README b/src/api/ml/README index beee7d864..f8984c79e 100644 --- a/src/api/ml/README +++ b/src/api/ml/README @@ -1,8 +1,11 @@ This directory is work in progress. We are currently working on a brand new ML API. +<<<<<<< HEAD On Windows, there are no less than four different ports of OCaml. The Z3 build system assumes that either the win32 or the win64 port is installed. This means that OCaml will use `cl' as the underlying C compiler and not the cygwin or -mingw compilers. \ No newline at end of file +mingw compilers. +======= +>>>>>>> Beginnings of a new ML API