mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

tweak GC in OCaml bindings (#5600)

Browse source 
* 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
This commit is contained in:
Simon Cruanes 2021-10-14 15:46:14 -04:00 • committed by GitHub
parent f60ed2ce92
commit 6302b864c8
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 31 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

8
azure-pipelines.yml
View file

@ -43,15 +43,15 @@ jobs:
- ${{if eq(variables['runRegressions'], 'True')}}: - ${{if eq(variables['runRegressions'], 'True')}}:
- template: scripts/test-regressions.yml - template: scripts/test-regressions.yml
- job: "Ubuntu18Python" - job: "Ubuntu20OCaml"
displayName: "Ubuntu 18 with ocaml" displayName: "Ubuntu 20 with ocaml"
pool: pool:
vmImage: "Ubuntu-18.04" vmImage: "Ubuntu-20.04"
steps: steps:
- script: sudo apt-get install ocaml opam libgmp-dev - script: sudo apt-get install ocaml opam libgmp-dev
- script: opam init -y - script: opam init -y
- script: eval `opam config env`; opam install zarith ocamlfind -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: | - script: |
set -e set -e
cd build cd build

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

@ -76,14 +76,14 @@ int compare_pointers(void* pt1, void* pt2) {
return +1; return +1;
} }
#define MK_CTX_OF(X) \ #define MK_CTX_OF(X, USED) \
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_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; \ 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; \ *(Z3_context_plus *)Data_custom_val(result) = cp; \
/* We increment the usage counter of the context, as we just \ /* We increment the usage counter of the context, as we just \
created a second custom block holding that context */ \ created a second custom block holding that context */ \
@ -102,7 +102,7 @@ int compare_pointers(void* pt1, void* pt2) {
CAMLlocal1(result); \ CAMLlocal1(result); \
Z3_context_plus cp = *(Z3_context_plus*)(Data_custom_val(v)); \ Z3_context_plus cp = *(Z3_context_plus*)(Data_custom_val(v)); \
Z3_ ## X ## _plus a = Z3_ ## X ## _plus_mk(cp, NULL); \ 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; \ *(Z3_ ## X ## _plus*)(Data_custom_val(result)) = a; \
CAMLreturn(result); \ CAMLreturn(result); \
} }
@ -294,9 +294,9 @@ static struct custom_operations Z3_ast_plus_custom_ops = {
Z3_ast_compare_ext 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 { \ typedef struct { \
Z3_context_plus cp; \ Z3_context_plus cp; \
Z3_ ## X p; \ Z3_ ## X p; \
@ -349,9 +349,9 @@ MK_CTX_OF(ast)
Z3_ ## X ## _compare_ext \ 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 { \ typedef struct { \
Z3_context_plus cp; \ Z3_context_plus cp; \
Z3_ ## X p; \ Z3_ ## X p; \
@ -408,27 +408,27 @@ MK_CTX_OF(ast)
Z3_ ## X ## _compare_ext \ Z3_ ## X ## _compare_ext \
}; \ }; \
\ \
MK_CTX_OF(X) MK_CTX_OF(X, USED)
MK_PLUS_OBJ_NO_REF(symbol) MK_PLUS_OBJ_NO_REF(symbol, 32)
MK_PLUS_OBJ_NO_REF(constructor) MK_PLUS_OBJ_NO_REF(constructor, 32)
MK_PLUS_OBJ_NO_REF(constructor_list) MK_PLUS_OBJ_NO_REF(constructor_list, 32)
MK_PLUS_OBJ_NO_REF(rcf_num) MK_PLUS_OBJ_NO_REF(rcf_num, 32)
MK_PLUS_OBJ(params) MK_PLUS_OBJ(params, 128)
MK_PLUS_OBJ(param_descrs) MK_PLUS_OBJ(param_descrs, 128)
MK_PLUS_OBJ(model) MK_PLUS_OBJ(model, 512)
MK_PLUS_OBJ(func_interp) MK_PLUS_OBJ(func_interp, 128)
MK_PLUS_OBJ(func_entry) MK_PLUS_OBJ(func_entry, 128)
MK_PLUS_OBJ(goal) MK_PLUS_OBJ(goal, 128)
MK_PLUS_OBJ(tactic) MK_PLUS_OBJ(tactic, 128)
MK_PLUS_OBJ(probe) MK_PLUS_OBJ(probe, 128)
MK_PLUS_OBJ(apply_result) MK_PLUS_OBJ(apply_result, 128)
MK_PLUS_OBJ(solver) MK_PLUS_OBJ(solver, 20 * 1000 * 1000) // pretend a solver is 20MB
MK_PLUS_OBJ(stats) MK_PLUS_OBJ(stats, 128)
MK_PLUS_OBJ(ast_map) MK_PLUS_OBJ(ast_map, 1024 * 2)
MK_PLUS_OBJ(ast_vector) MK_PLUS_OBJ(ast_vector, 128)
MK_PLUS_OBJ(fixedpoint) MK_PLUS_OBJ(fixedpoint, 20 * 1000 * 1000)
MK_PLUS_OBJ(optimize) MK_PLUS_OBJ(optimize, 20 * 1000 * 1000)
#ifdef __cplusplus #ifdef __cplusplus
extern "C" { extern "C" {