From 6302b864c807741223b0bf8ade4beb1da9e4f09d Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 14 Oct 2021 15:46:14 -0400 Subject: [PATCH] tweak GC in OCaml bindings (#5600) * feat(api/ml): use custom block hints to guide the GC this forces the GC to collect garbage when a few _large_ objects (solver, etc.) are dead. The current code would let arbitrarily many such objects die and not trigger a GC (which would have to come from OCaml code instead) * tuning * try to use caml_alloc_custom_mem with fake sizes * try to fix leak by explicitly finalizing OCaml context * chore: use more recent ubuntu for azure CI * remove finalizer causing segfault in example --- azure-pipelines.yml | 8 ++--- src/api/ml/z3native_stubs.c.pre | 56 ++++++++++++++++----------------- 2 files changed, 32 insertions(+), 32 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index ed2a7d0c312..ee00013857d 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -43,15 +43,15 @@ jobs: - ${{if eq(variables['runRegressions'], 'True')}}: - template: scripts/test-regressions.yml -- job: "Ubuntu18Python" - displayName: "Ubuntu 18 with ocaml" +- job: "Ubuntu20OCaml" + displayName: "Ubuntu 20 with ocaml" pool: - vmImage: "Ubuntu-18.04" + vmImage: "Ubuntu-20.04" steps: - script: sudo apt-get install ocaml opam libgmp-dev - script: opam init -y - script: eval `opam config env`; opam install zarith ocamlfind -y - - script: python scripts/mk_make.py --ml --staticlib + - script: eval `opam config env`; python scripts/mk_make.py --ml --staticlib - script: | set -e cd build diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre index 5c1a3bd06ee..895e2023502 100644 --- a/src/api/ml/z3native_stubs.c.pre +++ b/src/api/ml/z3native_stubs.c.pre @@ -76,14 +76,14 @@ int compare_pointers(void* pt1, void* pt2) { return +1; } -#define MK_CTX_OF(X) \ +#define MK_CTX_OF(X, USED) \ 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); \ + result = caml_alloc_custom_mem(&Z3_context_plus_custom_ops, sizeof(Z3_context_plus), USED); \ *(Z3_context_plus *)Data_custom_val(result) = cp; \ /* We increment the usage counter of the context, as we just \ created a second custom block holding that context */ \ @@ -102,7 +102,7 @@ int compare_pointers(void* pt1, void* pt2) { CAMLlocal1(result); \ Z3_context_plus cp = *(Z3_context_plus*)(Data_custom_val(v)); \ Z3_ ## X ## _plus a = Z3_ ## X ## _plus_mk(cp, NULL); \ - result = caml_alloc_custom(&Z3_ ## X ## _plus_custom_ops, sizeof(Z3_ ## X ## _plus), 0, 1); \ + result = caml_alloc_custom_mem(&Z3_ ## X ## _plus_custom_ops, sizeof(Z3_ ## X ## _plus), USED); \ *(Z3_ ## X ## _plus*)(Data_custom_val(result)) = a; \ CAMLreturn(result); \ } @@ -294,9 +294,9 @@ static struct custom_operations Z3_ast_plus_custom_ops = { Z3_ast_compare_ext }; -MK_CTX_OF(ast) +MK_CTX_OF(ast, 16) // let's say 16 bytes per ast -#define MK_PLUS_OBJ_NO_REF(X) \ +#define MK_PLUS_OBJ_NO_REF(X, USED) \ typedef struct { \ Z3_context_plus cp; \ Z3_ ## X p; \ @@ -349,9 +349,9 @@ MK_CTX_OF(ast) Z3_ ## X ## _compare_ext \ }; \ \ - MK_CTX_OF(X) + MK_CTX_OF(X, USED) -#define MK_PLUS_OBJ(X) \ +#define MK_PLUS_OBJ(X, USED) \ typedef struct { \ Z3_context_plus cp; \ Z3_ ## X p; \ @@ -408,27 +408,27 @@ MK_CTX_OF(ast) Z3_ ## X ## _compare_ext \ }; \ \ - MK_CTX_OF(X) - -MK_PLUS_OBJ_NO_REF(symbol) -MK_PLUS_OBJ_NO_REF(constructor) -MK_PLUS_OBJ_NO_REF(constructor_list) -MK_PLUS_OBJ_NO_REF(rcf_num) -MK_PLUS_OBJ(params) -MK_PLUS_OBJ(param_descrs) -MK_PLUS_OBJ(model) -MK_PLUS_OBJ(func_interp) -MK_PLUS_OBJ(func_entry) -MK_PLUS_OBJ(goal) -MK_PLUS_OBJ(tactic) -MK_PLUS_OBJ(probe) -MK_PLUS_OBJ(apply_result) -MK_PLUS_OBJ(solver) -MK_PLUS_OBJ(stats) -MK_PLUS_OBJ(ast_map) -MK_PLUS_OBJ(ast_vector) -MK_PLUS_OBJ(fixedpoint) -MK_PLUS_OBJ(optimize) + MK_CTX_OF(X, USED) + +MK_PLUS_OBJ_NO_REF(symbol, 32) +MK_PLUS_OBJ_NO_REF(constructor, 32) +MK_PLUS_OBJ_NO_REF(constructor_list, 32) +MK_PLUS_OBJ_NO_REF(rcf_num, 32) +MK_PLUS_OBJ(params, 128) +MK_PLUS_OBJ(param_descrs, 128) +MK_PLUS_OBJ(model, 512) +MK_PLUS_OBJ(func_interp, 128) +MK_PLUS_OBJ(func_entry, 128) +MK_PLUS_OBJ(goal, 128) +MK_PLUS_OBJ(tactic, 128) +MK_PLUS_OBJ(probe, 128) +MK_PLUS_OBJ(apply_result, 128) +MK_PLUS_OBJ(solver, 20 * 1000 * 1000) // pretend a solver is 20MB +MK_PLUS_OBJ(stats, 128) +MK_PLUS_OBJ(ast_map, 1024 * 2) +MK_PLUS_OBJ(ast_vector, 128) +MK_PLUS_OBJ(fixedpoint, 20 * 1000 * 1000) +MK_PLUS_OBJ(optimize, 20 * 1000 * 1000) #ifdef __cplusplus extern "C" {