js: Adding manual release methods

[HalfdanJ]

Adding methods allowing manual reference cleanup of object created by high level api.

I was considering if it instead should be called decRef like the native api, and java api is called. https://github.com/Z3Prover/z3/blob/master/src/api/java/Solver.java#L418, or if it should be called something more intuitive to a javascript developer, for whom the concept of references is abstracted away. My suggestion in this pr is the latter.

Also considering if we want to add runtime checks that asserts no methods can be called on objects that are released.

Fixes #7427

@bakkot

[bakkot]

You'll need to pass this as the third argument to register for the unregister call to work.

[HalfdanJ]

Good catch.

[bakkot]

Looks good. It would kind of be nice to be defensive against the user calling release multiple times, or using the other methods after calling it, but that requires runtime checks and so may not be worthwhile.

[HalfdanJ]

Yeah was considering that, could be done storing a Boolean on the objects. I think what would make sense design wise is make a super class that provides the registration and release of the reference, that super class can then be providing that Boolean flag, and assertion function without it having to be implemented on all class implementations.

The child classes just have to provide the increase and decrease functions to the super constructor.

[bakkot]

could be done storing a Boolean on the objects

That would work, but the standard practice here is to set ptr to null once it's been released. That also means you don't need a second field.

I think what would make sense design wise is make a super class that provides the registration and release of the reference

Eh... you still need to call the assertion function in every method on every class, so having the actual implementation be in a superclass doesn't buy you much (vs just having a top-level function checkNonNull(ptr: number | null) { if (ptr == null) throw new TypeError } which you call at the top of every method). And adding a superclass adds complexity to some already quite complex types. I would prefer avoid the superclass.

[HalfdanJ]

I'm going to limit the scope to just adding release to Solver Optimize and Model in this case i think. Making ptr possibly null on all objects means assertions need to be added a lot of places.

One big downside of doing this is that its a breaking change type wise to the library. Any usage of the library that references .ptr will have a new type.

[bakkot]

Sound fine.

I wouldn't worry too much about making ptr nullable changing the types: that change reflects a change in the underlying reality, i.e., that now the ptr might no longer point to valid memory, where it always did before (unless you were reaching into the low-level API). Also I doubt many people are relying on it anyway. But that can be changed later, if we are inclined to.

[HalfdanJ]

Ok, assertion added, i think this solution with an internal _ptr field is best since it avoids any issues with typescript not allowing setting ptr to null, and it adds assertion to any place that requests the ptr field from any of the objects.