From 45ef6d0109e721396f547885b586a0fd38cf43e4 Mon Sep 17 00:00:00 2001 From: Jonas Jongejan <227529+HalfdanJ@users.noreply.github.com> Date: Tue, 22 Oct 2024 12:15:49 -0400 Subject: [PATCH] js: Adding manual release methods (#7428) * js: Adding manual release methods * Add unregister token * Add pointer assertion * Add missing line --- src/api/js/src/high-level/high-level.ts | 74 ++++++++++++++++++------- src/api/js/src/high-level/types.ts | 22 +++++++- 2 files changed, 75 insertions(+), 21 deletions(-) diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 0869dbd7b46..2c69848c3e2 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -178,6 +178,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel { ctxs.forEach(other => assert('ctx' in other ? ctx === other.ctx : ctx === other, 'Context mismatch')); } + function _assertPtr(ptr: T | null): asserts ptr is T { + if (ptr == null) throw new TypeError('Expected non-null pointer'); + } + // call this after every nontrivial call to the underlying API function throwIfError() { if (Z3.get_error_code(contextPtr) !== Z3_error_code.Z3_OK) { @@ -1203,7 +1207,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { const myAst = this.ast; Z3.inc_ref(contextPtr, myAst); - cleanup.register(this, () => Z3.dec_ref(contextPtr, myAst)); + cleanup.register(this, () => Z3.dec_ref(contextPtr, myAst), this); } get ast(): Z3_ast { @@ -1240,8 +1244,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel { class SolverImpl implements Solver { declare readonly __typename: Solver['__typename']; - readonly ptr: Z3_solver; readonly ctx: Context; + private _ptr: Z3_solver | null; + get ptr(): Z3_solver { + _assertPtr(this._ptr); + return this._ptr; + } constructor(ptr: Z3_solver | string = Z3.mk_solver(contextPtr)) { this.ctx = ctx; @@ -1251,9 +1259,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } else { myPtr = ptr; } - this.ptr = myPtr; + this._ptr = myPtr; Z3.solver_inc_ref(contextPtr, myPtr); - cleanup.register(this, () => Z3.solver_dec_ref(contextPtr, myPtr)); + cleanup.register(this, () => Z3.solver_dec_ref(contextPtr, myPtr), this); } set(key: string, value: any): void { @@ -1327,21 +1335,32 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Z3.solver_from_string(contextPtr, this.ptr, s); throwIfError(); } + + release() { + Z3.solver_dec_ref(contextPtr, this.ptr); + // Mark the ptr as null to prevent double free + this._ptr = null; + cleanup.unregister(this); + } } class OptimizeImpl implements Optimize { declare readonly __typename: Optimize['__typename']; - readonly ptr: Z3_optimize; readonly ctx: Context; + private _ptr: Z3_optimize | null; + get ptr(): Z3_optimize { + _assertPtr(this._ptr); + return this._ptr; + } constructor(ptr: Z3_optimize = Z3.mk_optimize(contextPtr)) { this.ctx = ctx; let myPtr: Z3_optimize; myPtr = ptr; - this.ptr = myPtr; + this._ptr = myPtr; Z3.optimize_inc_ref(contextPtr, myPtr); - cleanup.register(this, () => Z3.optimize_dec_ref(contextPtr, myPtr)); + cleanup.register(this, () => Z3.optimize_dec_ref(contextPtr, myPtr), this); } set(key: string, value: any): void { @@ -1363,11 +1382,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { }); } - addSoft(expr: Bool, weight: number | bigint | string | CoercibleRational, id: number | string = "") { + addSoft(expr: Bool, weight: number | bigint | string | CoercibleRational, id: number | string = '') { if (isCoercibleRational(weight)) { weight = `${weight.numerator}/${weight.denominator}`; } - check(Z3.optimize_assert_soft(contextPtr, this.ptr, expr.ast, weight.toString(), _toSymbol(id))) + check(Z3.optimize_assert_soft(contextPtr, this.ptr, expr.ast, weight.toString(), _toSymbol(id))); } addAndTrack(expr: Bool, constant: Bool | string) { @@ -1395,9 +1414,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { _assertContext(expr); return expr.ast; }); - const result = await asyncMutex.runExclusive(() => - check(Z3.optimize_check(contextPtr, this.ptr, assumptions)), - ); + const result = await asyncMutex.runExclusive(() => check(Z3.optimize_check(contextPtr, this.ptr, assumptions))); switch (result) { case Z3_lbool.Z3_L_FALSE: return 'unsat'; @@ -1422,17 +1439,28 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Z3.optimize_from_string(contextPtr, this.ptr, s); throwIfError(); } - } + release() { + Z3.optimize_dec_ref(contextPtr, this.ptr); + this._ptr = null; + cleanup.unregister(this); + } + } class ModelImpl implements Model { declare readonly __typename: Model['__typename']; readonly ctx: Context; + private _ptr: Z3_model | null; + get ptr(): Z3_model { + _assertPtr(this._ptr); + return this._ptr; + } - constructor(readonly ptr: Z3_model = Z3.mk_model(contextPtr)) { + constructor(ptr: Z3_model = Z3.mk_model(contextPtr)) { this.ctx = ctx; + this._ptr = ptr; Z3.model_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.model_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.model_dec_ref(contextPtr, ptr), this); } length() { @@ -1594,6 +1622,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel { _assertContext(sort); return new AstVectorImpl(check(Z3.model_get_sort_universe(contextPtr, this.ptr, sort.ptr))); } + + release() { + Z3.model_dec_ref(contextPtr, this.ptr); + this._ptr = null; + cleanup.unregister(this); + } } class FuncEntryImpl implements FuncEntry { @@ -1604,7 +1638,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(readonly ptr: Z3_func_entry) { this.ctx = ctx; Z3.func_entry_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.func_entry_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.func_entry_dec_ref(contextPtr, ptr), this); } numArgs() { @@ -1627,7 +1661,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(readonly ptr: Z3_func_interp) { this.ctx = ctx; Z3.func_interp_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.func_interp_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.func_interp_dec_ref(contextPtr, ptr), this); } elseValue(): Expr { @@ -1922,7 +1956,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { this.ptr = myPtr; Z3.tactic_inc_ref(contextPtr, myPtr); - cleanup.register(this, () => Z3.tactic_dec_ref(contextPtr, myPtr)); + cleanup.register(this, () => Z3.tactic_dec_ref(contextPtr, myPtr), this); } } @@ -2586,7 +2620,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(readonly ptr: Z3_ast_vector = Z3.mk_ast_vector(contextPtr)) { this.ctx = ctx; Z3.ast_vector_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.ast_vector_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.ast_vector_dec_ref(contextPtr, ptr), this); } length(): number { @@ -2684,7 +2718,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(readonly ptr: Z3_ast_map = Z3.mk_ast_map(contextPtr)) { this.ctx = ctx; Z3.ast_map_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.ast_map_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.ast_map_dec_ref(contextPtr, ptr), this); } [Symbol.iterator](): Iterator<[Key, Value]> { diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index 6f3630a6db5..45a06bda609 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -663,6 +663,13 @@ export interface Solver { check(...exprs: (Bool | AstVector>)[]): Promise; model(): Model; + + /** + * Manually decrease the reference count of the solver + * This is automatically done when the solver is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; } export interface Optimize { @@ -695,8 +702,14 @@ export interface Optimize { check(...exprs: (Bool | AstVector>)[]): Promise; model(): Model; -} + /** + * Manually decrease the reference count of the optimize + * This is automatically done when the optimize is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; +} /** @hidden */ export interface ModelCtor { @@ -746,6 +759,13 @@ export interface Model extends Iterable, defaultValue: CoercibleToMap, Name>, ): FuncInterp; + + /** + * Manually decrease the reference count of the model + * This is automatically done when the model is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; } /**