From c92ab91a5ef3c4a0afdd08b59f285a3ac08132a1 Mon Sep 17 00:00:00 2001 From: Jonas Jongejan Date: Mon, 21 Oct 2024 15:37:38 -0400 Subject: [PATCH] Add pointer assertion --- src/api/js/src/high-level/high-level.ts | 64 +++++++++++-------------- src/api/js/src/high-level/types.ts | 32 ++----------- 2 files changed, 34 insertions(+), 62 deletions(-) diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index fa55e0d0c..c62b86863 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) { @@ -1235,18 +1239,17 @@ export function createApi(Z3: Z3Core): Z3HighLevel { toString() { return this.sexpr(); } - - release() { - Z3.dec_ref(contextPtr, this.ast); - cleanup.unregister(this); - } } 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; @@ -1256,7 +1259,7 @@ 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), this); } @@ -1335,6 +1338,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel { release() { Z3.solver_dec_ref(contextPtr, this.ptr); + // Mark the ptr as null to prevent double free + this._ptr = null; cleanup.unregister(this); } } @@ -1342,14 +1347,18 @@ export function createApi(Z3: Z3Core): Z3HighLevel { 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), this); } @@ -1373,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) { @@ -1405,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'; @@ -1442,9 +1449,15 @@ export function createApi(Z3: Z3Core): Z3HighLevel { 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), this); } @@ -1611,6 +1624,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { release() { Z3.model_dec_ref(contextPtr, this.ptr); + this._ptr = null; cleanup.unregister(this); } } @@ -1675,11 +1689,6 @@ export function createApi(Z3: Z3Core): Z3HighLevel { assert(this.arity() === argsVec.length(), "Number of arguments in entry doesn't match function arity"); check(Z3.func_interp_add_entry(contextPtr, this.ptr, argsVec.ptr, value.ptr as Z3_ast)); } - - release() { - Z3.func_interp_dec_ref(contextPtr, this.ptr); - cleanup.unregister(this); - } } class SortImpl extends AstImpl implements Sort { @@ -1948,11 +1957,6 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Z3.tactic_inc_ref(contextPtr, myPtr); cleanup.register(this, () => Z3.tactic_dec_ref(contextPtr, myPtr), this); } - - release() { - Z3.tactic_dec_ref(contextPtr, this.ptr); - cleanup.unregister(this); - } } class ArithSortImpl extends SortImpl implements ArithSort { @@ -2704,11 +2708,6 @@ export function createApi(Z3: Z3Core): Z3HighLevel { sexpr(): string { return check(Z3.ast_vector_to_string(contextPtr, this.ptr)); } - - release() { - Z3.ast_vector_dec_ref(contextPtr, this.ptr); - cleanup.unregister(this); - } } class AstMapImpl, Value extends AnyAst> implements AstMap { @@ -2768,11 +2767,6 @@ export function createApi(Z3: Z3Core): Z3HighLevel { sexpr(): string { return check(Z3.ast_map_to_string(contextPtr, this.ptr)); } - - release() { - Z3.ast_map_dec_ref(contextPtr, this.ptr); - cleanup.unregister(this); - } } function substitute(t: Expr, ...substitutions: [Expr, Expr][]): Expr { diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index c884126ff..45a06bda6 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -703,6 +703,11 @@ export interface Optimize { 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; } @@ -839,13 +844,6 @@ export interface FuncInterp { entry(i: number): FuncEntry; addEntry(args: Expr[], value: Expr): void; - - /** - * Manually decrease the reference count of the func interp - * This is automatically done when the func interp is garbage collected, - * but calling this eagerly can help release memory sooner. - */ - release(): void; } /** @hidden */ @@ -1630,13 +1628,6 @@ export interface Tactic { readonly ctx: Context; readonly ptr: Z3_tactic; - - /** - * Manually decrease the reference count of the tactic - * This is automatically done when the tactic is garbage collected, - * but calling this eagerly can help release memory sooner. - */ - release(): void; } /** @hidden */ @@ -1688,12 +1679,6 @@ export interface AstVector has(v: Item): boolean; sexpr(): string; - /** - * Manually decrease the reference count of the ast vector - * This is automatically done when the ast vector is garbage collected, - * but calling this eagerly can help release memory sooner. - */ - release(): void; } /** @hidden */ @@ -1752,13 +1737,6 @@ export interface AstMap< has(key: Key): boolean; sexpr(): string; - - /** - * Manually decrease the reference count of the ast map - * This is automatically done when the ast map is garbage collected, - * but calling this eagerly can help release memory sooner. - */ - release(): void; } /**