-
Notifications
You must be signed in to change notification settings - Fork 1.5k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add WebAssembly/TypeScript bindings #5762
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,61 @@ | ||
name: WebAssembly Publish | ||
|
||
on: | ||
workflow_dispatch: | ||
|
||
defaults: | ||
run: | ||
working-directory: src/api/js | ||
|
||
env: | ||
EM_VERSION: 3.1.0 | ||
|
||
jobs: | ||
publish: | ||
name: Publish | ||
runs-on: ubuntu-latest | ||
steps: | ||
- name: Checkout | ||
uses: actions/checkout@v2 | ||
|
||
- name: Setup node | ||
uses: actions/setup-node@v2 | ||
with: | ||
node-version: 'lts/*' | ||
registry-url: 'https://registry.npmjs.org' | ||
|
||
- name: Prepare for publish | ||
run: | | ||
npm version $(node -e 'console.log(fs.readFileSync("../../../scripts/release.yml", "utf8").match(/ReleaseVersion:\s*\x27(\S+)\x27/)[1])') | ||
mv PUBLISHED_README.md README.md | ||
cp ../../../LICENSE.txt . | ||
|
||
- name: Setup emscripten | ||
uses: mymindstorm/setup-emsdk@v11 | ||
with: | ||
no-install: true | ||
version: ${{env.EM_VERSION}} | ||
actions-cache-folder: 'emsdk-cache' | ||
|
||
- name: Install dependencies | ||
run: npm ci | ||
|
||
- name: Build TypeScript | ||
run: npm run build-ts | ||
|
||
- name: Build wasm | ||
run: | | ||
emsdk install ${EM_VERSION} | ||
emsdk activate ${EM_VERSION} | ||
source $(dirname $(which emsdk))/emsdk_env.sh | ||
which node | ||
which clang++ | ||
npm run build-wasm | ||
|
||
- name: Test | ||
run: npm test | ||
|
||
- name: Publish | ||
run: npm publish | ||
env: | ||
NODE_AUTH_TOKEN: ${{ secrets.NPM_TOKEN }} | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I have installed an NPM token with my account that has write access to z3-solver. |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,43 +1,51 @@ | ||
name: WASM Build | ||
name: WebAssembly Build | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I see this replaces the old action. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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. |
||
|
||
on: | ||
push: | ||
branches: [ master ] | ||
pull_request: | ||
|
||
defaults: | ||
run: | ||
working-directory: src/api/js | ||
|
||
env: | ||
BUILD_TYPE: Release | ||
EM_VERSION: 3.1.0 | ||
|
||
jobs: | ||
build: | ||
check: | ||
name: Check | ||
runs-on: ubuntu-latest | ||
|
||
steps: | ||
- name: Checkout code | ||
uses: actions/checkout@v2 | ||
|
||
- name: Import emscripten | ||
uses: mymindstorm/setup-emsdk@v9 | ||
|
||
- name: Configure CMake and build | ||
run: | | ||
mkdir build | ||
cd build | ||
|
||
emcmake cmake \ | ||
-DCMAKE_BUILD_TYPE=MinSizeRel \ | ||
-DZ3_BUILD_LIBZ3_SHARED=OFF \ | ||
-DZ3_ENABLE_EXAMPLE_TARGETS=OFF \ | ||
-DZ3_BUILD_TEST_EXECUTABLES=OFF \ | ||
-DZ3_BUILD_EXECUTABLE=OFF \ | ||
-DZ3_SINGLE_THREADED=ON \ | ||
-DCMAKE_CXX_FLAGS="-s DISABLE_EXCEPTION_CATCHING=0" \ | ||
..; | ||
make | ||
tar -cvf z3-build-wasm.tar *.a | ||
|
||
- name: Archive production artifacts | ||
uses: actions/upload-artifact@v2 | ||
with: | ||
name: z3-build-wasm | ||
path: build/z3-build-wasm.tar | ||
retention-days: 5 | ||
- name: Checkout | ||
uses: actions/checkout@v2 | ||
|
||
- name: Setup node | ||
uses: actions/setup-node@v2 | ||
with: | ||
node-version: 'lts/*' | ||
|
||
- name: Setup emscripten | ||
uses: mymindstorm/setup-emsdk@v11 | ||
with: | ||
no-install: true | ||
version: ${{env.EM_VERSION}} | ||
actions-cache-folder: 'emsdk-cache' | ||
|
||
- name: Install dependencies | ||
run: npm ci | ||
|
||
- name: Build TypeScript | ||
run: npm run build-ts | ||
|
||
- name: Build wasm | ||
run: | | ||
emsdk install ${EM_VERSION} | ||
emsdk activate ${EM_VERSION} | ||
source $(dirname $(which emsdk))/emsdk_env.sh | ||
which node | ||
which clang++ | ||
npm run build-wasm | ||
|
||
- name: Test | ||
run: npm test |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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/ | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Not sure why they are in .gitignore. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is the usual practice for JS projects. This folder holds the dependencies used to build the project. |
||
src/api/js/*.js | ||
src/api/js/build/ | ||
src/api/js/**/*.d.ts | ||
!src/api/js/scripts/*.js | ||
!src/api/js/src/*.js | ||
|
||
out/** | ||
*.bak | ||
doc/api | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,124 @@ | ||
# Z3 TypeScript Bindings | ||
|
||
This project provides low-level TypeScript bindings for the [Z3 theorem prover](https://github.com/Z3Prover/z3). It is available on npm as [z3-solver](https://www.npmjs.com/package/z3-solver). | ||
|
||
Z3 itself is distributed as a wasm artifact as part of this package. You can find the documentation for the Z3 API [here](https://z3prover.github.io/api/html/z3__api_8h.html), though note the differences below. | ||
|
||
|
||
## Using | ||
|
||
This requires threads, which means you'll need to be running in an environment which supports `SharedArrayBuffer`. In browsers, in addition to ensuring the browser has implemented `SharedArrayBuffer`, you'll need to serve your page with [special headers](https://web.dev/coop-coep/). There's a [neat trick](https://github.com/gzuidhof/coi-serviceworker) for doing that client-side on e.g. Github Pages, though you shouldn't use that trick in more complex applications. | ||
|
||
Other than the differences below, the bindings can be used exactly as you'd use the C library. Because this is a wrapper around a C library, most of the values you'll use are just numbers representing pointers. For this reason you are strongly encouraged to make use of the TypeScript types to differentiate among the different kinds of value. | ||
|
||
The module exports an `init` function, is an async function which initializes the library and returns `{ em, Z3 }` - `em` contains the underlying emscripten module, which you can use to e.g. kill stray threads, and `Z3` contains the actual bindings. The other module exports are the enums defined in the Z3 API. | ||
|
||
[`test-ts-api.ts`](./test-ts-api.ts) contains a couple real cases translated very mechanically from [this file](https://github.com/Z3Prover/z3/blob/90fd3d82fce20d45ed2eececdf65545bab769503/examples/c/test_capi.c). | ||
|
||
|
||
## Differences from the C API | ||
|
||
### Integers | ||
|
||
JavaScript numbers are IEEE double-precisions floats. These can be used wherever the C API expects an `int`, `unsigned int`, `float`, or `double`. | ||
|
||
`int64_t` and `uint64_t` cannot be precisely represented by JS numbers, so in the TS bindings they are represented by [BigInts](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Data_structures#bigint_type). | ||
|
||
### Out parameters | ||
|
||
In C, to return multiple values a function will take an address to write to, conventionally referred to as an "out parameter". Sometimes the function returns a boolean to indicate success; other times it may return nothing or some other value. | ||
|
||
In JS the convention when returning multiple values is to return records containing the values of interest. | ||
|
||
The wrapper translates between the two conventions. For example, the C declaration | ||
|
||
```c | ||
void Z3_rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Z3_rcf_num * n, Z3_rcf_num * d); | ||
``` | ||
|
||
is represented in the TS bindings as | ||
|
||
```ts | ||
function rcf_get_numerator_denominator(c: Z3_context, a: Z3_rcf_num): { n: Z3_rcf_num; d: Z3_rcf_num } { | ||
// ... | ||
} | ||
``` | ||
|
||
When there is only a single out parameter, and the return value is not otherwise of interest, the parameter is not wrapped. For example, the C declaration | ||
|
||
```c | ||
Z3_bool Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v); | ||
``` | ||
|
||
is represented in the TS bindings as | ||
|
||
```ts | ||
function model_eval(c: Z3_context, m: Z3_model, t: Z3_ast, model_completion: boolean): Z3_ast | null { | ||
// ... | ||
} | ||
``` | ||
|
||
Note that the boolean return type of the C function is translated into a nullable return type for the TS binding. | ||
|
||
When the return value is of interest it is included in the returned record under the key `rv`. | ||
|
||
|
||
### Arrays | ||
|
||
The when the C API takes an array as an argument it will also require a parameter which specifies the length of the array (since arrays do not carry their own lengths in C). In the TS bindings this is automatically inferred. | ||
|
||
For example, the C declaration | ||
```js | ||
unsigned Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]); | ||
``` | ||
|
||
is represented in the TS bindings as | ||
|
||
```ts | ||
function rcf_mk_roots(c: Z3_context, a: Z3_rcf_num[]): { rv: number; roots: Z3_rcf_num[] } { | ||
// ... | ||
} | ||
``` | ||
|
||
When there are multiple arrays which the C API expects to be of the same length, the TS bindings will enforce that this is the case. | ||
|
||
|
||
### Null pointers | ||
|
||
Some of the C APIs accept or return null pointers (represented by types whose name end in `_opt`). These are represented in the TS bindings as `| null`. For example, the C declaration | ||
|
||
```js | ||
Z3_ast_opt Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a); | ||
``` | ||
|
||
is represented in the TS bindings as | ||
|
||
```ts | ||
function model_get_const_interp(c: Z3_context, m: Z3_model, a: Z3_func_decl): Z3_ast | null { | ||
// ... | ||
} | ||
``` | ||
|
||
|
||
### Async functions | ||
|
||
Certain long-running APIs are not appropriate to call on the main thread. In the TS bindings those APIs are marked as `async` and are automatically called on a different thread. This includes the following APIs: | ||
|
||
- `Z3_simplify` | ||
- `Z3_simplify_ex` | ||
- `Z3_solver_check` | ||
- `Z3_solver_check_assumptions` | ||
- `Z3_solver_cube` | ||
- `Z3_solver_get_consequences` | ||
- `Z3_tactic_apply` | ||
- `Z3_tactic_apply_ex` | ||
- `Z3_optimize_check` | ||
- `Z3_algebraic_roots` | ||
- `Z3_algebraic_eval` | ||
- `Z3_fixedpoint_query` | ||
- `Z3_fixedpoint_query_relations` | ||
- `Z3_fixedpoint_query_from_lvl` | ||
- `Z3_polynomial_subresultants` | ||
|
||
Note that these are not thread-safe, and so only one call can be running at a time. Trying to call a second async API before the first completes will throw. | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
# TypeScript Bindings | ||
|
||
This directory contains JavaScript code to automatically derive TypeScript bindings for the C API, which are published on npm as [z3-solver](https://www.npmjs.com/package/z3-solver). | ||
|
||
The readme for the bindings themselves is located in [`PUBLISHED_README.md`](./PUBLISHED_README.md). | ||
|
||
|
||
## Building | ||
|
||
You'll need to have emscripten set up, along with all of its dependencies. The easiest way to do that is with [emsdk](https://github.com/emscripten-core/emsdk). | ||
|
||
Then run `npm i` to install dependencies, `npm run build-ts` to build the TypeScript wrapper, and `npm run build-wasm` to build the wasm artifact. | ||
|
||
|
||
## Tests | ||
|
||
Current tests are very minimal: [`test-ts-api.ts`](./test-ts-api.ts) contains a couple real cases translated very mechanically from [this file](https://github.com/Z3Prover/z3/blob/90fd3d82fce20d45ed2eececdf65545bab769503/examples/c/test_capi.c). |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
#!/bin/bash | ||
|
||
set -euxo pipefail | ||
|
||
|
||
export ROOT=$PWD | ||
|
||
cd ../../.. | ||
export CXXFLAGS="-pthread -s USE_PTHREADS=1 -s DISABLE_EXCEPTION_CATCHING=0" | ||
export LDFLAGS="-s WASM_BIGINT -s -pthread -s USE_PTHREADS=1" | ||
if [ ! -f "build/Makefile" ]; then | ||
emconfigure python scripts/mk_make.py --staticlib --single-threaded | ||
fi | ||
|
||
cd build | ||
emmake make -j$(nproc) libz3.a | ||
|
||
cd $ROOT | ||
|
||
export EM_CACHE=$HOME/.emscripten/ | ||
export FNS=$(node scripts/list-exports.js) | ||
export METHODS='["ccall","FS","allocate","UTF8ToString","intArrayFromString","ALLOC_NORMAL"]' | ||
emcc build/async-fns.cc ../../../build/libz3.a --std=c++20 --pre-js src/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=$METHODS -s EXPORTED_FUNCTIONS=$FNS -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s DEMANGLE_SUPPORT=1 -s TOTAL_MEMORY=1GB -I z3/src/api/ -o build/z3-built.js |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,57 @@ | ||
import { init } from './build/wrapper'; | ||
|
||
// demonstrates use of the raw API | ||
|
||
(async () => { | ||
let { em, Z3 } = await init(); | ||
|
||
Z3.global_param_set('verbose', '10'); | ||
console.log('verbosity:', Z3.global_param_get('verbose')); | ||
|
||
let config = Z3.mk_config(); | ||
let ctx = Z3.mk_context_rc(config); | ||
Z3.del_config(config); | ||
|
||
let unicodeStr = [...'hello™'].map(x => x.codePointAt(0)!); | ||
let strAst = Z3.mk_u32string(ctx, unicodeStr); | ||
Z3.inc_ref(ctx, strAst); | ||
|
||
console.log(Z3.is_string(ctx, strAst)); | ||
console.log(Z3.get_string(ctx, strAst)); | ||
console.log(Z3.get_string_contents(ctx, strAst, unicodeStr.length)); | ||
|
||
let bv = Z3.mk_bv_numeral(ctx, [true, true, false]); | ||
let bs = Z3.mk_ubv_to_str(ctx, bv); | ||
console.log(Z3.ast_to_string(ctx, bs)); | ||
|
||
let intSort = Z3.mk_int_sort(ctx); | ||
let big = Z3.mk_int64(ctx, 42n, intSort); | ||
console.log(Z3.get_numeral_string(ctx, big)); | ||
console.log(Z3.get_numeral_int64(ctx, big)); | ||
|
||
console.log(Z3.get_version()); | ||
|
||
let head_tail = [Z3.mk_string_symbol(ctx, 'car'), Z3.mk_string_symbol(ctx, 'cdr')]; | ||
|
||
let nil_con = Z3.mk_constructor(ctx, Z3.mk_string_symbol(ctx, 'nil'), Z3.mk_string_symbol(ctx, 'is_nil'), [], [], []); | ||
let cons_con = Z3.mk_constructor( | ||
ctx, | ||
Z3.mk_string_symbol(ctx, 'cons'), | ||
Z3.mk_string_symbol(ctx, 'is_cons'), | ||
head_tail, | ||
[null, null], | ||
[0, 0], | ||
); | ||
|
||
let cell = Z3.mk_datatype(ctx, Z3.mk_string_symbol(ctx, 'cell'), [nil_con, cons_con]); | ||
console.log(Z3.query_constructor(ctx, nil_con, 0)); | ||
console.log(Z3.query_constructor(ctx, cons_con, 2)); | ||
|
||
Z3.dec_ref(ctx, strAst); | ||
Z3.del_context(ctx); | ||
|
||
em.PThread.terminateAllThreads(); | ||
})().catch(e => { | ||
console.error('error', e); | ||
process.exit(1); | ||
}); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess this is the version without "-pre" because I can't find a reference to "-pre" in the pull request.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yup, I deleted it just before opening this PR. Sorry that wasn't clearer.