mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

Fix reference counting in the C layer of the OCaml bindings

Browse source 
The Z3 context and its reference counters are stored in a structure which is allocated
by the C layer outside the OCaml heap, whenever a Z3 context is created. The structure
and its Z3 context are disposed, once the last reference counter reaches zero. Reference
counters are decremented by C-level finalizers.

The OCaml representations for a Z3 context wrap only a pointer to the corresponding structure.
This commit is contained in:
martin-neuhaeusser 2016-04-03 09:41:06 +02:00
parent b178420797
commit b85516c271
2 changed files with 76 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

2
scripts/update_api.py
View file

@ -1333,7 +1333,7 @@ def mk_z3native_stubs_c(ml_dir): # C interface
i = 0 i = 0
for param in params: for param in params:
if param_type(param) == CONTEXT and i == 0: 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') ml_wrapper.write(' Z3_context _a0 = ctx_p->ctx;\n')
have_context = True have_context = True
else: else:

67
src/api/ml/z3native_stubs.c.pre
View file

@ -68,50 +68,67 @@ static struct custom_operations default_custom_ops = {
CAMLprim DLL_PUBLIC value n_context_of_ ## X(value v) { \ CAMLprim DLL_PUBLIC value n_context_of_ ## X(value v) { \
CAMLparam1(v); \ CAMLparam1(v); \
CAMLlocal1(result); \ CAMLlocal1(result); \
Z3_context_plus cp; \
Z3_ ## X ## _plus * p = (Z3_ ## X ## _plus *) Data_custom_val(v); \ 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); \ 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); \ CAMLreturn(result); \
} }
/* Context objects */ /* 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 { typedef struct {
Z3_context ctx; Z3_context ctx;
unsigned long obj_count:sizeof(unsigned long)-1; unsigned long obj_count;
unsigned ok_to_delete:1; } Z3_context_plus_data;
} Z3_context_plus;
/* 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 Z3_context_plus_mk(Z3_context c) {
Z3_context_plus r; Z3_context_plus r = (Z3_context_plus)malloc(sizeof(Z3_context_plus_data));
r.ctx = c; r->ctx = c;
r.obj_count = 0; /* The context created here will be wrapped into a custom block.
r.ok_to_delete = 0; Hence, we assign it a counter of one. */
/* printf("ctx++ %p\n", c); */ r->obj_count = 1;
return r; return r;
} }
Z3_context Z3_context_plus_raw(Z3_context_plus * cp) { 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) { inline void try_to_delete_context(Z3_context_plus cp) {
if (!cp->ok_to_delete || cp->obj_count != 0) if (cp->obj_count > 0)
/* printf("Trying to delete context %p.\n", cp->ctx) */ ; /* 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 { 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); Z3_del_context(cp->ctx);
cp->ctx = 0; cp->ctx = NULL;
cp->obj_count = 0; cp->obj_count = 0;
cp->ok_to_delete = 0; free(cp);
} }
} }
void Z3_context_finalize(value v) { void Z3_context_finalize(value v) {
Z3_context_plus * cp = (Z3_context_plus*)Data_custom_val(v); Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v);
/* printf("ctx--; cnt=%lu\n", cp->obj_count); */ cp->obj_count--;
cp->ok_to_delete = 1;
try_to_delete_context(cp); try_to_delete_context(cp);
} }
@ -129,11 +146,11 @@ static struct custom_operations Z3_context_plus_custom_ops = {
/* AST objects */ /* AST objects */
typedef struct { typedef struct {
Z3_context_plus * cp; Z3_context_plus cp;
Z3_ast a; Z3_ast a;
} Z3_ast_plus; } 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; Z3_ast_plus r;
r.cp = cp; r.cp = cp;
r.a = a; r.a = a;
@ -203,11 +220,11 @@ MK_CTX_OF(ast)
#define MK_PLUS_OBJ_NO_REF(X) \ #define MK_PLUS_OBJ_NO_REF(X) \
typedef struct { \ typedef struct { \
Z3_context_plus * cp; \ Z3_context_plus cp; \
Z3_ ## X p; \ Z3_ ## X p; \
} Z3_ ## X ## _plus; \ } 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; \ Z3_ ## X ## _plus r; \
r.cp = cp; \ r.cp = cp; \
r.p = p; \ r.p = p; \
@ -239,11 +256,11 @@ MK_CTX_OF(ast)
#define MK_PLUS_OBJ(X) \ #define MK_PLUS_OBJ(X) \
typedef struct { \ typedef struct { \
Z3_context_plus * cp; \ Z3_context_plus cp; \
Z3_ ## X p; \ Z3_ ## X p; \
} Z3_ ## X ## _plus; \ } 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; \ Z3_ ## X ## _plus r; \
r.cp = cp; \ r.cp = cp; \
r.p = p; \ r.p = p; \