Skip to content

Commit

Permalink
js: Adding manual release methods (#7428)
Browse files Browse the repository at this point in the history 
* js: Adding manual release methods

* Add unregister token

* Add pointer assertion

* Add missing line
  • Loading branch information
@HalfdanJ
HalfdanJ authored Oct 22, 2024
1 parent 5cee19f commit 45ef6d0
Show file tree
Hide file tree
Showing 2 changed files with 75 additions and 21 deletions.
74 changes: 54 additions & 20 deletions src/api/js/src/high-level/high-level.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<T extends Number>(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) {
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -1240,8 +1244,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
class SolverImpl implements Solver<Name> {
declare readonly __typename: Solver['__typename'];

readonly ptr: Z3_solver;
readonly ctx: Context<Name>;
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;
Expand All @@ -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 {
Expand Down Expand Up @@ -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<Name> {
declare readonly __typename: Optimize['__typename'];

readonly ptr: Z3_optimize;
readonly ctx: Context<Name>;
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 {
Expand All @@ -1363,11 +1382,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
});
}

addSoft(expr: Bool<Name>, weight: number | bigint | string | CoercibleRational, id: number | string = "") {
addSoft(expr: Bool<Name>, 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<Name>, constant: Bool<Name> | string) {
Expand Down Expand Up @@ -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';
Expand All @@ -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<Name> {
declare readonly __typename: Model['__typename'];
readonly ctx: Context<Name>;
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() {
Expand Down Expand Up @@ -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<Name> {
Expand All @@ -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() {
Expand All @@ -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<Name> {
Expand Down Expand Up @@ -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);
}
}

Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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]> {
Expand Down
22 changes: 21 additions & 1 deletion src/api/js/src/high-level/types.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -663,6 +663,13 @@ export interface Solver<Name extends string = 'main'> {
check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult>;

model(): Model<Name>;

/**
* 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<Name extends string = 'main'> {
Expand Down Expand Up @@ -695,8 +702,14 @@ export interface Optimize<Name extends string = 'main'> {
check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult>;

model(): Model<Name>;
}

/**
* 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<Name extends string> {
Expand Down Expand Up @@ -746,6 +759,13 @@ export interface Model<Name extends string = 'main'> extends Iterable<FuncDecl<N
decl: FuncDecl<Name, DomainSort, RangeSort>,
defaultValue: CoercibleToMap<SortToExprMap<RangeSort, Name>, Name>,
): FuncInterp<Name>;

/**
* 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;
}

/**
Expand Down

0 comments on commit 45ef6d0

Please sign in to comment.