diff --git a/scripts/update_api.py b/scripts/update_api.py index a4bad305e..cd6895544 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -78,7 +78,7 @@ Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', # Mapping to Java types Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double', - FLOAT : 'float', STRING : 'String', STRING_PTR : 'StringPtr', + FLOAT : 'float', STRING : 'String', STRING_PTR : 'StringPtr', BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int'} Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble', @@ -87,7 +87,7 @@ Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', I # Mapping to ML types Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float', - FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**', + FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**', BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' } next_type_id = FIRST_OBJ_ID @@ -637,18 +637,18 @@ def mk_java(java_dir, package_name): 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: + 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), + 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)) + 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)) elif k == OUT_MANAGED_ARRAY: @@ -679,7 +679,7 @@ def mk_java(java_dir, package_name): java_wrapper.write('(%s)a%i' % (param2str(param), i)) i = i + 1 java_wrapper.write(');\n') - # cleanup + # cleanup i = 0 for param in params: k = param_kind(param) @@ -715,7 +715,7 @@ def mk_java(java_dir, package_name): 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(' return (%s) result;\n' % type2javaw(result)) java_wrapper.write('}\n') java_wrapper.write('#ifdef __cplusplus\n') java_wrapper.write('}\n') @@ -945,7 +945,7 @@ def def_API(name, result, params): error ("unsupported parameter for %s, %s" % (ty, name, p)) elif kind == OUT_ARRAY: sz = param_array_capacity_pos(p) - sz_p = params[sz] + sz_p = params[sz] sz_p_k = param_kind(sz_p) tstr = type2str(ty) if sz_p_k == OUT or sz_p_k == INOUT: @@ -1284,16 +1284,16 @@ def mk_z3native_stubs_c(ml_dir): # C interface ret_size = len(op) if result != VOID: ret_size = ret_size + 1 - + # Setup frame - ml_wrapper.write('CAMLprim DLL_PUBLIC value n_%s(' % ml_method_name(name)) + ml_wrapper.write('CAMLprim DLL_PUBLIC 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: + else: ml_wrapper.write(', ') ml_wrapper.write('value a%d' % i) i = i + 1 @@ -1333,7 +1333,7 @@ def mk_z3native_stubs_c(ml_dir): # C interface i = 0 for param in params: if param_type(param) == CONTEXT and i == 0: - ml_wrapper.write(' Z3_context_plus * ctx_p = (Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n') + ml_wrapper.write(' Z3_context_plus ctx_p = *(Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n') ml_wrapper.write(' Z3_context _a0 = ctx_p->ctx;\n') have_context = True else: @@ -1341,7 +1341,7 @@ def mk_z3native_stubs_c(ml_dir): # C interface if k == OUT_ARRAY: ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % ( type2str(param_type(param)), - i, + i, type2str(param_type(param)), type2str(param_type(param)), param_array_capacity_pos(param))) @@ -1350,14 +1350,14 @@ def mk_z3native_stubs_c(ml_dir): # C interface 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))) + 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)) + ml_wrapper.write(' %s _a%s = a%s;\n' % (type2str(param_type(param)), i, i)) i = i + 1 i = 0 @@ -1412,7 +1412,7 @@ def mk_z3native_stubs_c(ml_dir): # C interface if result != VOID: ts = type2str(result) if ml_has_plus_type(ts): - pts = ml_plus_type(ts) + pts = ml_plus_type(ts) ml_wrapper.write(' result = caml_alloc_custom(&%s, sizeof(%s), 0, 1);\n' % (ml_plus_ops_type(ts), pts)) if name in NULLWrapped: ml_wrapper.write(' %s z3rv = %s_mk(z3rv_m);\n' % (pts, pts)) @@ -1429,10 +1429,10 @@ def mk_z3native_stubs_c(ml_dir): # C interface 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++) {\n' % param_array_capacity_pos(p)) pts = ml_plus_type(ts) - pops = ml_plus_ops_type(ts) + pops = ml_plus_ops_type(ts) ml_wrapper.write(' value t;\n') ml_wrapper.write(' t = caml_alloc_custom(&%s, sizeof(%s), 0, 1);\n' % (pops, pts)) - if ml_has_plus_type(ts): + if ml_has_plus_type(ts): ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d[_i]);\n' % (pts, i, pts, ml_minus_type(ts), i)) ml_wrapper.write(' %s\n' % ml_set_wrap(pt, 't', '_a%dp' % i)) else: @@ -1453,7 +1453,7 @@ def mk_z3native_stubs_c(ml_dir): # C interface ml_wrapper.write(' %s\n' % ml_set_wrap(pt, '_a%d_val' % i, '_a%d' % i)) i = i + 1 - # return tuples + # return tuples if len(op) == 0: ml_wrapper.write(' %s\n' % ml_set_wrap(result, "result", "z3rv")) else: @@ -1480,7 +1480,7 @@ def mk_z3native_stubs_c(ml_dir): # C interface ml_wrapper.write(' CAMLreturn(result);\n') ml_wrapper.write('}\n\n') if len(ip) > 5: - ml_wrapper.write('CAMLprim DLL_PUBLIC value n_%s_bytecode(value * argv, int argn) {\n' % ml_method_name(name)) + ml_wrapper.write('CAMLprim DLL_PUBLIC 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): diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre index e4ed85373..de8ba62e6 100644 --- a/src/api/ml/z3native_stubs.c.pre +++ b/src/api/ml/z3native_stubs.c.pre @@ -26,31 +26,31 @@ extern "C" { #define CAMLlocal6(X1,X2,X3,X4,X5,X6) \ CAMLlocal5(X1,X2,X3,X4,X5); \ - CAMLlocal1(X6) + CAMLlocal1(X6) #define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \ CAMLlocal5(X1,X2,X3,X4,X5); \ - CAMLlocal2(X6,X7) + CAMLlocal2(X6,X7) #define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \ CAMLlocal5(X1,X2,X3,X4,X5); \ - CAMLlocal3(X6,X7,X8) + CAMLlocal3(X6,X7,X8) #define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \ CAMLparam5(X1,X2,X3,X4,X5); \ - CAMLxparam2(X6,X7) + CAMLxparam2(X6,X7) #define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \ CAMLparam5(X1,X2,X3,X4,X5); \ - CAMLxparam3(X6,X7,X8) + CAMLxparam3(X6,X7,X8) #define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \ CAMLparam5(X1,X2,X3,X4,X5); \ CAMLxparam4(X6,X7,X8,X9) #define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \ CAMLparam5(X1,X2,X3,X4,X5); \ CAMLxparam5(X6,X7,X8,X9,X10); \ - CAMLxparam2(X11,X12) + CAMLxparam2(X11,X12) #define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \ CAMLparam5(X1,X2,X3,X4,X5); \ CAMLxparam5(X6,X7,X8,X9,X10); \ - CAMLxparam3(X11,X12,X13) + CAMLxparam3(X11,X12,X13) static struct custom_operations default_custom_ops = { @@ -68,51 +68,68 @@ static struct custom_operations default_custom_ops = { CAMLprim DLL_PUBLIC value n_context_of_ ## X(value v) { \ CAMLparam1(v); \ CAMLlocal1(result); \ + Z3_context_plus cp; \ Z3_ ## X ## _plus * p = (Z3_ ## X ## _plus *) Data_custom_val(v); \ + cp = p->cp; \ result = caml_alloc_custom(&Z3_context_plus_custom_ops, sizeof(Z3_context_plus), 0, 1); \ - *(Z3_context_plus*)Data_custom_val(result) = *p->cp; \ + *(Z3_context_plus*)Data_custom_val(result) = cp; \ + /* We increment the usage counter of the context */ \ + cp->obj_count++; \ CAMLreturn(result); \ } /* Context objects */ +/* The Z3context_plus_data exists exactly once for each context, + no matter how many custom blocks for that context exist. + Each custom block only stores a pointer to the corresponding + Z3_context_plus_data. This ensures that the reference counting + is performed at exactly one place and not within the custom + blocks that get copied. */ typedef struct { Z3_context ctx; - unsigned long obj_count:sizeof(unsigned long)-1; - unsigned ok_to_delete:1; -} Z3_context_plus; + unsigned long obj_count; +} Z3_context_plus_data; + +/* A context is wrapped to an OCaml value by storing a pointer + to its associated Z3_context_plus_data instance. + This instance gets created in mk_context and is deleted + together with the Z3 context instance in try_to_delete_context + whenever the obj_count field is zero. */ +typedef Z3_context_plus_data* Z3_context_plus; Z3_context_plus Z3_context_plus_mk(Z3_context c) { - Z3_context_plus r; - r.ctx = c; - r.obj_count = 0; - r.ok_to_delete = 0; - /* printf("ctx++ %p\n", c); */ + Z3_context_plus r = (Z3_context_plus)malloc(sizeof(Z3_context_plus_data)); + r->ctx = c; + /* The context created here will be wrapped into a custom block. + Hence, we assign it a counter of one. */ + r->obj_count = 1; return r; } Z3_context Z3_context_plus_raw(Z3_context_plus * cp) { - return cp->ctx; + return (*cp)->ctx; } -void try_to_delete_context(Z3_context_plus * cp) { - if (!cp->ok_to_delete || cp->obj_count != 0) - /* printf("Trying to delete context %p.\n", cp->ctx) */ ; +inline void try_to_delete_context(Z3_context_plus cp) { + if (cp->obj_count > 0) + /* printf("try_to_delete_context: Not deleting context %p(%p) with cnt=%lu.\n", cp, cp->ctx, cp->obj_count) */ ; + else if (cp->obj_count < 0) + printf("try_to_delete_context: ERROR, found context %p(%p) with negative cnt=%lu.\n", cp, cp->ctx, cp->obj_count); else { - /* printf("Actually deleting context %p.\n", cp->ctx); */ + printf("try_to_delete_context: Deleting context %p(%p) with cnt=%lu.\n", cp, cp->ctx, cp->obj_count); Z3_del_context(cp->ctx); - cp->ctx = 0; + cp->ctx = NULL; cp->obj_count = 0; - cp->ok_to_delete = 0; + free(cp); } } void Z3_context_finalize(value v) { - Z3_context_plus * cp = (Z3_context_plus*)Data_custom_val(v); - /* printf("ctx--; cnt=%lu\n", cp->obj_count); */ - cp->ok_to_delete = 1; - try_to_delete_context(cp); + Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v); + cp->obj_count--; + try_to_delete_context(cp); } static struct custom_operations Z3_context_plus_custom_ops = { @@ -129,14 +146,14 @@ static struct custom_operations Z3_context_plus_custom_ops = { /* AST objects */ typedef struct { - Z3_context_plus * cp; + Z3_context_plus cp; Z3_ast a; } Z3_ast_plus; -Z3_ast_plus Z3_ast_plus_mk(Z3_context_plus * cp, Z3_ast a) { +Z3_ast_plus Z3_ast_plus_mk(Z3_context_plus cp, Z3_ast a) { Z3_ast_plus r; r.cp = cp; - r.a = a; + r.a = a; /* printf("++\n"); */ cp->obj_count++; Z3_inc_ref(cp->ctx, a); @@ -148,7 +165,7 @@ Z3_ast Z3_ast_plus_raw(Z3_ast_plus * ap) { } void Z3_ast_finalize(value v) { - /* printf("--\n"); */ + /* printf("--\n"); */ Z3_ast_plus * ap = (Z3_ast_plus*)(Data_custom_val(v)); Z3_dec_ref(ap->cp->ctx, ap->a); ap->cp->obj_count--; @@ -203,11 +220,11 @@ MK_CTX_OF(ast) #define MK_PLUS_OBJ_NO_REF(X) \ typedef struct { \ - Z3_context_plus * cp; \ + Z3_context_plus cp; \ Z3_ ## X p; \ } Z3_ ## X ## _plus; \ \ - Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus * cp, Z3_ ## X p) { \ + Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus cp, Z3_ ## X p) { \ Z3_ ## X ## _plus r; \ r.cp = cp; \ r.p = p; \ @@ -239,11 +256,11 @@ MK_CTX_OF(ast) #define MK_PLUS_OBJ(X) \ typedef struct { \ - Z3_context_plus * cp; \ + Z3_context_plus cp; \ Z3_ ## X p; \ } Z3_ ## X ## _plus; \ \ - Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus * cp, Z3_ ## X p) { \ + Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus cp, Z3_ ## X p) { \ Z3_ ## X ## _plus r; \ r.cp = cp; \ r.p = p; \ @@ -309,7 +326,7 @@ CAMLprim DLL_PUBLIC value n_is_null(value p) { CAMLprim DLL_PUBLIC value n_mk_null( void ) { CAMLparam0(); - CAMLlocal1(result); + CAMLlocal1(result); result = caml_alloc(1, 0); result = Val_int(0); CAMLreturn (result);