mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-12 17:06:14 +00:00
Code Activity

Beginnings of a new ML API

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-12-11 13:37:02 +00:00
parent decb09bb9e
commit 90cb046684
3 changed files with 166 additions and 426 deletions
Download patch file Download diff file Expand all files Collapse all files

11
scripts/mk_util.py
View file

@ -1428,6 +1428,13 @@ class MLComponent(Component):
if IS_WINDOWS: if IS_WINDOWS:
out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(LIB_EXT)') out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(LIB_EXT)')
out.write('\n\n') 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): def main_component(self):
return is_ml_enabled() return is_ml_enabled()
@ -1841,7 +1848,11 @@ def mk_config():
if GPROF: if GPROF:
print('gprof: enabled') print('gprof: enabled')
print('Python version: %s' % distutils.sysconfig.get_python_version()) print('Python version: %s' % distutils.sysconfig.get_python_version())
<<<<<<< HEAD
print('ML API: %s' % is_ml_enabled()) print('ML API: %s' % is_ml_enabled())
=======
print 'ML API: %s' % is_ml_enabled()
>>>>>>> Beginnings of a new ML API
if is_java_enabled(): if is_java_enabled():
print('JNI Bindings: %s' % JNI_HOME) print('JNI Bindings: %s' % JNI_HOME)
print('Java Compiler: %s' % JAVAC) print('Java Compiler: %s' % JAVAC)

576
scripts/update_api.py
View file

@ -213,7 +213,10 @@ def type2javaw(ty):
def type2ml(ty): def type2ml(ty):
global Type2ML global Type2ML
return Type2ML[ty] if (ty >= FIRST_OBJ_ID):
return 'long'
else:
return Type2ML[ty]
def _in(ty): def _in(ty):
return (IN, ty); return (IN, ty);
@ -1066,216 +1069,76 @@ def mk_bindings():
exe_c.write("}\n") exe_c.write("}\n")
def ml_method_name(name): def ml_method_name(name):
return name[3:] # Remove Z3_ result = ''
name = name[3:] # Remove Z3_
def is_out_param(p): return result
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 + '));'
def mk_ml(): def mk_ml():
global Type2Str
if not is_ml_enabled(): if not is_ml_enabled():
return return
ml_dir = get_component('ml').src_dir ml_dir = get_component('ml').src_dir
ml_nativef = os.path.join(ml_dir, 'z3native.ml') ml_nativef = os.path.join(ml_dir, 'z3_native.ml')
ml_nativefi = os.path.join(ml_dir, 'z3native.mli') ml_wrapperf = os.path.join(ml_dir, 'z3_native.c')
ml_wrapperf = os.path.join(ml_dir, 'z3native_stubs.c')
ml_native = open(ml_nativef, 'w') ml_native = open(ml_nativef, 'w')
ml_i = open(ml_nativefi, 'w') ml_native.write('// Automatically generated file\n')
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('\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: for name, result, params in _dotnet_decls:
ml_native.write(' external n_%s : ' % ml_method_name(name)) ml_native.write(' external %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('(')
first = True first = True
if result != VOID or len(op) == 0: i = 0;
ml_native.write('%s' % type2ml(result)) for param in params:
ml_i.write('%s' % type2ml(result))
first = False
for p in op:
if first: if first:
first = False first = False
else: else:
ml_native.write(' * ') ml_native.write(', ')
ml_i.write(' * ') ml_native.write('%s a%d' % (param2ml(param), i))
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)
i = i + 1 i = i + 1
if len(ip) == 0: ml_native.write('%s)\n' % (type2ml(result)))
ml_native.write('()') # ml_native.write(' = "NATIVE_%s"' % ml_method_name(name))
ml_native.write(' = \n') # ml_native.write('\n\n')
ml_native.write(' ') # # Exception wrappers
if result == VOID and len(op) == 0: # for name, result, params in _dotnet_decls:
ml_native.write('let _ = ') # java_native.write(' public static %s %s(' % (type2java(result), java_method_name(name)))
else: # first = True
ml_native.write('let res = ') # i = 0;
ml_native.write('(ML2C.n_%s' % (ml_method_name(name))) # for param in params:
if len(ip) == 0: # if first:
ml_native.write(' ()') # first = False
first = True # else:
i = 0; # java_native.write(', ')
for p in params: # java_native.write('%s a%d' % (param2java(param), i))
if is_in_param(p): # i = i + 1
ml_native.write(' a%d' % i) # java_native.write(')')
i = i + 1 # if len(params) > 0 and param_type(params[0]) == CONTEXT:
ml_native.write(') in\n') # java_native.write(' throws Z3Exception')
if name not in Unwrapped and len(params) > 0 and param_type(params[0]) == CONTEXT: # java_native.write('\n')
ml_native.write(' let err = (error_code_of_int (ML2C.n_get_error_code a0)) in \n') # java_native.write(' {\n')
ml_native.write(' if err <> OK then\n') # java_native.write(' ')
ml_native.write(' raise (Exception (ML2C.n_get_error_msg_ex a0 (int_of_error_code err)))\n') # if result != VOID:
ml_native.write(' else\n') # java_native.write('%s res = ' % type2java(result))
if result == VOID and len(op) == 0: # java_native.write('INTERNAL%s(' % (java_method_name(name)))
ml_native.write(' ()\n') # first = True
else: # i = 0;
ml_native.write(' res\n') # for param in params:
ml_native.write('\n') # if first:
ml_native.write('(**/**)\n') # first = False
# else:
# C interface # 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 = open(ml_wrapperf, 'w')
ml_wrapper.write('// Automatically generated file\n\n') ml_wrapper.write('// Automatically generated file\n\n')
ml_wrapper.write('#include <stddef.h>\n') ml_wrapper.write('#include <stddef.h>\n')
ml_wrapper.write('#include <string.h>\n\n') ml_wrapper.write('#include <string.h>\n')
ml_wrapper.write('#ifdef __cplusplus\n')
ml_wrapper.write('extern "C" {\n')
ml_wrapper.write('#endif\n')
ml_wrapper.write('#include <caml/mlvalues.h>\n') ml_wrapper.write('#include <caml/mlvalues.h>\n')
ml_wrapper.write('#include <caml/memory.h>\n') ml_wrapper.write('#include <caml/memory.h>\n')
ml_wrapper.write('#include <caml/alloc.h>\n') ml_wrapper.write('#include <caml/alloc.h>\n')
@ -1285,237 +1148,100 @@ def mk_ml():
ml_wrapper.write('#include <caml/custom.h>\n') ml_wrapper.write('#include <caml/custom.h>\n')
ml_wrapper.write('#include <caml/bigarray.h>\n') ml_wrapper.write('#include <caml/bigarray.h>\n')
ml_wrapper.write('#endif\n') ml_wrapper.write('#endif\n')
ml_wrapper.write('#ifdef __cplusplus\n') # for name, result, params in _dotnet_decls:
ml_wrapper.write('}\n') # java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name)))
ml_wrapper.write('#endif\n\n') # i = 0;
ml_wrapper.write('#include <z3.h>\n\n') # for param in params:
ml_wrapper.write('#define CAMLlocal6(X1,X2,X3,X4,X5,X6) \\\n') # java_wrapper.write(', ')
ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n') # java_wrapper.write('%s a%d' % (param2javaw(param), i))
ml_wrapper.write(' CAMLlocal1(X6) \n') # i = i + 1
ml_wrapper.write('#define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \\\n') # java_wrapper.write(') {\n')
ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n') # # preprocess arrays, strings, in/out arguments
ml_wrapper.write(' CAMLlocal2(X6,X7) \n') # i = 0
ml_wrapper.write('#define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \\\n') # for param in params:
ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n') # k = param_kind(param)
ml_wrapper.write(' CAMLlocal3(X6,X7,X8) \n') # if k == OUT or k == INOUT:
ml_wrapper.write('\n') # java_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i))
ml_wrapper.write('#define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \\\n') # elif k == IN_ARRAY or k == INOUT_ARRAY:
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') # if param_type(param) == INT or param_type(param) == UINT:
ml_wrapper.write(' CAMLxparam2(X6,X7) \n') # java_wrapper.write(' %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i))
ml_wrapper.write('#define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \\\n') # else:
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') # java_wrapper.write(' GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, i))
ml_wrapper.write(' CAMLxparam3(X6,X7,X8) \n') # elif k == OUT_ARRAY:
ml_wrapper.write('#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \\\n') # java_wrapper.write(' %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)),
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') # i,
ml_wrapper.write(' CAMLxparam4(X6,X7,X8,X9) \n') # type2str(param_type(param)),
ml_wrapper.write('#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \\\n') # param_array_capacity_pos(param),
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') # type2str(param_type(param))))
ml_wrapper.write(' CAMLxparam5(X6,X7,X8,X9,X10); \\\n') # if param_type(param) == INT or param_type(param) == UINT:
ml_wrapper.write(' CAMLxparam2(X11,X12) \n') # java_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
ml_wrapper.write('#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \\\n') # else:
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n') # java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i))
ml_wrapper.write(' CAMLxparam5(X6,X7,X8,X9,X10); \\\n') # elif k == IN and param_type(param) == STRING:
ml_wrapper.write(' CAMLxparam3(X11,X12,X13) \n') # java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i))
ml_wrapper.write('\n\n') # i = i + 1
ml_wrapper.write('static struct custom_operations default_custom_ops = {\n') # # invoke procedure
ml_wrapper.write(' (char*) "default handling",\n') # java_wrapper.write(' ')
ml_wrapper.write(' custom_finalize_default,\n') # if result != VOID:
ml_wrapper.write(' custom_compare_default,\n') # java_wrapper.write('%s result = ' % type2str(result))
ml_wrapper.write(' custom_hash_default,\n') # java_wrapper.write('%s(' % name)
ml_wrapper.write(' custom_serialize_default,\n') # i = 0
ml_wrapper.write(' custom_deserialize_default\n') # first = True
ml_wrapper.write('};\n\n') # for param in params:
ml_wrapper.write('#ifdef __cplusplus\n') # if first:
ml_wrapper.write('extern "C" {\n') # first = False
ml_wrapper.write('#endif\n\n') # else:
ml_wrapper.write('CAMLprim value n_is_null(value p) {\n') # java_wrapper.write(', ')
ml_wrapper.write(' void * t = * (void**) Data_custom_val(p);\n') # k = param_kind(param)
ml_wrapper.write(' return Val_bool(t == 0);\n') # if k == OUT or k == INOUT:
ml_wrapper.write('}\n\n') # java_wrapper.write('&_a%s' % i)
ml_wrapper.write('CAMLprim value n_mk_null( void ) {\n') # elif k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY:
ml_wrapper.write(' CAMLparam0();\n') # java_wrapper.write('_a%s' % i)
ml_wrapper.write(' CAMLlocal1(result);\n') # elif k == IN and param_type(param) == STRING:
ml_wrapper.write(' void * z3_result = 0;\n') # java_wrapper.write('_a%s' % i)
ml_wrapper.write(' result = caml_alloc_custom(&default_custom_ops, sizeof(void*), 0, 1);\n') # else:
ml_wrapper.write(' memcpy( Data_custom_val(result), &z3_result, sizeof(void*));\n') # java_wrapper.write('(%s)a%i' % (param2str(param), i))
ml_wrapper.write(' CAMLreturn (result);\n') # i = i + 1
ml_wrapper.write('}\n\n') # java_wrapper.write(');\n')
ml_wrapper.write('void MLErrorHandler(Z3_context c, Z3_error_code e)\n') # # cleanup
ml_wrapper.write('{\n') # i = 0
ml_wrapper.write(' // Internal do-nothing error handler. This is required to avoid that Z3 calls exit()\n') # for param in params:
ml_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n') # k = param_kind(param)
ml_wrapper.write(' // wrappers below.\n') # if k == OUT_ARRAY:
ml_wrapper.write('}\n\n') # if param_type(param) == INT or param_type(param) == UINT:
ml_wrapper.write('void n_set_internal_error_handler(value a0)\n') # java_wrapper.write(' jenv->SetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
ml_wrapper.write('{\n') # else:
ml_wrapper.write(' Z3_context _a0 = * (Z3_context*) Data_custom_val(a0);\n') # java_wrapper.write(' SETLONGAREGION(a%s, 0, a%s, _a%s);\n' % (i, param_array_capacity_pos(param), i))
ml_wrapper.write(' Z3_set_error_handler(_a0, MLErrorHandler);\n') # java_wrapper.write(' free(_a%s);\n' % i)
ml_wrapper.write('}\n\n') # elif k == IN_ARRAY or k == OUT_ARRAY:
for name, result, params in _dotnet_decls: # if param_type(param) == INT or param_type(param) == UINT:
ip = inparams(params) # java_wrapper.write(' jenv->ReleaseIntArrayElements(a%s, (jint*)_a%s, JNI_ABORT);\n' % (i, i))
op = outparams(params) # else:
ap = arrayparams(params) # java_wrapper.write(' RELEASELONGAELEMS(a%s, _a%s);\n' % (i, i))
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')
if len(ap) != 0: # elif k == OUT or k == INOUT:
ml_wrapper.write(' unsigned _i;\n') # if param_type(param) == INT or param_type(param) == UINT:
# java_wrapper.write(' {\n')
# declare locals, preprocess arrays, strings, in/out arguments # java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
i = 0 # java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n')
for param in params: # java_wrapper.write(' jenv->SetIntField(a%s, fid, (jint) _a%s);\n' % (i, i))
k = param_kind(param) # java_wrapper.write(' }\n')
if k == OUT_ARRAY: # else:
ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % ( # java_wrapper.write(' {\n')
type2str(param_type(param)), # java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
i, # java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "J");\n')
type2str(param_type(param)), # java_wrapper.write(' jenv->SetLongField(a%s, fid, (jlong) _a%s);\n' % (i, i))
type2str(param_type(param)), # java_wrapper.write(' }\n')
param_array_capacity_pos(param))) # i = i + 1
elif k == OUT_MANAGED_ARRAY: # # return
ml_wrapper.write(' %s * _a%s = 0;\n' % (type2str(param_type(param)), i)) # if result == STRING:
elif k == IN_ARRAY or k == INOUT_ARRAY: # java_wrapper.write(' return jenv->NewStringUTF(result);\n')
t = param_type(param) # elif result != VOID:
ts = type2str(t) # java_wrapper.write(' return (%s) result;\n' % type2javaw(result))
ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * _a%s);\n' % (ts, i, ts, ts, param_array_capacity_pos(param))) # java_wrapper.write('}\n')
elif k == IN: # java_wrapper.write('#ifdef __cplusplus\n')
t = param_type(param) # java_wrapper.write('}\n')
ml_wrapper.write(' %s _a%s = %s;\n' % (type2str(t), i, ml_unwrap(t, type2str(t), 'a' + str(i)))) # java_wrapper.write('#endif\n')
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')
if is_verbose(): if is_verbose():
print "Generated '%s'" % ml_nativef print "Generated '%s'" % ml_nativef

5
src/api/ml/README
View file

@ -1,8 +1,11 @@
This directory is work in progress. This directory is work in progress.
We are currently working on a brand new ML API. 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 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 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 that OCaml will use `cl' as the underlying C compiler and not the cygwin or
mingw compilers. mingw compilers.
=======
>>>>>>> Beginnings of a new ML API