Add WebAssembly/TypeScript bindings #5762

bakkot · 2022-01-10T00:13:37Z

As discussed. See the files named src/js/api/README.md and src/js/api/PUBLISHED_README.md for more details.

This includes two new GitHub Actions:

one which builds and tests the new bindings (replacing the existing WASM Build workflow, which wasn't doing much) on every PR and every commit to master,
one which builds, tests, and publishes them on npm, which must be triggered manually. It's easy to change to run whenever a release is published on GitHub, though.

I confirmed these work on my fork.

The version number for the release is read (with a regex) from release.yml.

In order to use the publish action, I'll need to add your npm account as a maintainer of the package, and then you'll need to create an automation token and add it as a secret for the repository named NPM_TOKEN. Please let me know the account you'd like to use.

npm will not let you publish over an existing version, but I published the version from my fork as -pre. So you should be able to trigger the publish job once this lands.

also, cc @cpitclaudel @philzook58 @bramvdbogaerde as people who have previously expressed interest in having wasm bindings.

NikolajBjorner · 2022-01-10T01:05:24Z

Please let me know the account you'd like to use: [email protected]

NikolajBjorner · 2022-01-10T01:18:45Z

.github/workflows/wasm.yml

@@ -1,43 +1,51 @@
-name: WASM Build
+name: WebAssembly Build


I see this replaces the old action.

Yeah, as mentioned in the PR message. The old one didn't do much useful - you couldn't use the artifact without having the same version of the compiler used to build it.

NikolajBjorner · 2022-01-10T01:20:53Z

.gitignore

@@ -75,6 +75,13 @@ src/api/ml/z3enums.ml
 src/api/ml/z3native.mli
 src/api/ml/z3enums.mli
 src/api/ml/z3.mllib
+src/api/js/node_modules/


Not sure why they are in .gitignore.

This is the usual practice for JS projects. This folder holds the dependencies used to build the project.

NikolajBjorner · 2022-01-10T01:24:45Z

.github/workflows/wasm-release.yml

+      - name: Publish
+        run: npm publish
+        env:
+          NODE_AUTH_TOKEN: ${{ secrets.NPM_TOKEN }}


I have installed an NPM token with my account that has write access to z3-solver.
I deleted the z3-solver organization.

NikolajBjorner · 2022-01-10T01:33:54Z

.github/workflows/wasm-release.yml

+
+      - name: Prepare for publish
+        run: |
+          npm version $(node -e 'console.log(fs.readFileSync("../../../scripts/release.yml", "utf8").match(/ReleaseVersion:\s*\x27(\S+)\x27/)[1])')


I guess this is the version without "-pre" because I can't find a reference to "-pre" in the pull request.

Yup, I deleted it just before opening this PR. Sorry that wasn't clearer.

NikolajBjorner · 2022-01-10T01:38:21Z

src/api/js/scripts/parse-api.js

+let types = {
+  __proto__: null,
+
+  // these are function types I can't be bothered to parse


I will likely create other such callbacks so if this list is required the more sustainable way is to mark them in z3_api as callbacks using some no-op macro. Based on the code below it looks like you match for "typedef enum" and other typedefs are not considered.

I added macros so the closures can be discovered instead of hard-wired

I can add support for parsing these properly, but to be sure I've done it right I'd like to have at least a test of them. Right now I can't find any uses of any of these types to compare against. Can you write a brief example (in C/C++) demonstrating how any one of the consumers of the Z3_whatever_eh types is intended to work, such that I could tell if my implementation has the right behavior?

z3/src/api/python/z3/z3.py

Line 212 in 56d3718

self.eh = Z3_set_error_handler(self.ctx, z3_error_handler)

Other callbacks are not exercised yet in examples I have published for python. They are used from C++

z3/src/api/c++/z3++.h

Line 3966 in 56d3718

static void pop_eh(void* p, unsigned num_scopes) {

and then for a self-contained example:
https://github.com/Z3Prover/z3/tree/master/examples/userPropagator

https://github.com/Z3Prover/z3/tree/master/examples/userPropagator looks like something I can re-implement, thanks. That PDF is very helpful.

For Z3_set_error_handler, what's an example of a case where it should be called? For example, should I expect it to be called if I perform Z3_query_constructor on a Z3_constructor which has not previously been passed to Z3_mk_datatypes?

Yes, the error handler gets invoked whenever there is some mistake in the API call.
For example, if you add two arrays. The addition is not well typed and it fails to create the expression.
Without the error handler it should return null. With the error handler you can raise an exception from the handler assuming stack unwinding works (which I guess for WebAssembly it should).

Another question: this line:

z3/src/api/z3_api.h

Line 6700 in 56d3718

* The registered function appears at the top level and is created using \ref Z3_propagate_solver_declare.

refers to a Z3_propagate_solver_declare. I can't find any other mention of that. Is it just a typo?

NikolajBjorner · 2022-01-10T01:42:09Z

src/api/js/scripts/parse-api.js

+  // but that's super painful
+  // and the files are regular enough that we can get away without it
+
+  // we could also do this by modifying the `update_api.py` script


I don't see adding things to update_api as a goal. It doesn't serve a purpose in itself. At best one can reuse some feature from update_api, but this seems needless now.
The goals are to ensure the bindings can be built on every push and the bindings can be exported (to npm).

NikolajBjorner · 2022-01-10T01:43:20Z

src/api/js/scripts/parse-api.js

+
+  // we _could_ use an actual C++ parser, which accounted for macros and everything
+  // but that's super painful
+  // and the files are regular enough that we can get away without it


The files have to be regular.

bakkot · 2022-01-10T02:51:32Z

Thanks for merging! You should try the new wasm-publish action to confirm you can publish the package.

This is to ease integration with external API wrappers that rely on accessing information about type names that are used. #5762

bakkot added 2 commits January 9, 2022 16:07

Add TypeScript bindings

9192719

mark Z3_eval_smtlib2_string as async

3aeb850

NikolajBjorner merged commit 2b934b6 into Z3Prover:master Jan 10, 2022

NikolajBjorner reviewed Jan 10, 2022

View reviewed changes

NikolajBjorner mentioned this pull request Jan 12, 2022

Bundling Dynamic Libraries Inside JAR for Ease of Redistribution #182

Open

NikolajBjorner added a commit that referenced this pull request Jan 12, 2022

add macro to track closures declared in z3_api

2bcc814

This is to ease integration with external API wrappers that rely on accessing information about type names that are used. #5762

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add WebAssembly/TypeScript bindings #5762

Add WebAssembly/TypeScript bindings #5762

bakkot commented Jan 10, 2022 •

edited

Loading

NikolajBjorner commented Jan 10, 2022

NikolajBjorner Jan 10, 2022

bakkot Jan 10, 2022

NikolajBjorner Jan 10, 2022

bakkot Jan 10, 2022

NikolajBjorner Jan 10, 2022 •

edited

Loading

NikolajBjorner Jan 10, 2022

bakkot Jan 10, 2022

NikolajBjorner Jan 10, 2022

NikolajBjorner Jan 12, 2022

bakkot Jan 12, 2022

NikolajBjorner Jan 12, 2022

bakkot Jan 12, 2022

NikolajBjorner Jan 12, 2022

bakkot Jan 12, 2022

NikolajBjorner Jan 10, 2022

NikolajBjorner Jan 10, 2022

bakkot commented Jan 10, 2022

Add WebAssembly/TypeScript bindings #5762

Add WebAssembly/TypeScript bindings #5762

Conversation

bakkot commented Jan 10, 2022 • edited Loading

NikolajBjorner commented Jan 10, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NikolajBjorner Jan 10, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bakkot commented Jan 10, 2022

bakkot commented Jan 10, 2022 •

edited

Loading

NikolajBjorner Jan 10, 2022 •

edited

Loading