From 312e037458e18fbd203287e187752dcc751101dd Mon Sep 17 00:00:00 2001 From: Kevin Gibbons Date: Sun, 24 Apr 2022 03:04:08 -0700 Subject: [PATCH] wasm build: disable error handler (#5996) * wasm: set error handler to no-op * wasm: better wrapper for use in html --- src/api/js/PUBLISHED_README.md | 2 +- src/api/js/example-raw.ts | 12 ++++++++- src/api/js/package.json | 6 ++--- src/api/js/scripts/list-exports.js | 2 +- src/api/js/scripts/make-cc-wrapper.js | 39 ++++++++++++++++++++++++--- src/api/js/scripts/make-ts-wrapper.js | 26 +++++++++++++----- src/api/js/src/node-wrapper.ts | 10 +++++++ src/api/js/test-ts-api.ts | 4 +-- 8 files changed, 83 insertions(+), 18 deletions(-) create mode 100644 src/api/js/src/node-wrapper.ts diff --git a/src/api/js/PUBLISHED_README.md b/src/api/js/PUBLISHED_README.md index 4be8a7d5187..4ccd4bea7b6 100644 --- a/src/api/js/PUBLISHED_README.md +++ b/src/api/js/PUBLISHED_README.md @@ -9,7 +9,7 @@ Z3 itself is distributed as a wasm artifact as part of this package. You can fin 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. -The Emscripten worker model will spawn multiple instances of `z3-built.js` for long-running operations. If you are using a bundler like Webpack, Emscripten can no longer reference `z3-built.js` - that file will be merged with the rest of your codebase. To fix this, you need to host the unmodified file separately, and set `Module['mainScriptUrlOrBlob']` to the URL of this file. If you don't do this, your bundle `main.js` will be used in all workers, which will undoubtedly fail and cause weird issues. +The Emscripten worker model will spawn multiple instances of `z3-built.js` for long-running operations. When building for the web, you should include that file as its own script on the page - using a bundler like webpack will prevent it from loading correctly. That script defines a global variable named `initZ3`. Your main script, which can be bundled, should do `let { init } = require('z3-solver/build/wrapper.js'); let { Z3 } = await init(initZ3);`. 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. diff --git a/src/api/js/example-raw.ts b/src/api/js/example-raw.ts index 9b19e782c7d..0ade4273ac5 100644 --- a/src/api/js/example-raw.ts +++ b/src/api/js/example-raw.ts @@ -1,4 +1,4 @@ -import { init } from './build/wrapper'; +import { init, Z3_error_code } from './build/node-wrapper'; // demonstrates use of the raw API @@ -47,6 +47,16 @@ import { init } from './build/wrapper'; console.log(Z3.query_constructor(ctx, nil_con, 0)); console.log(Z3.query_constructor(ctx, cons_con, 2)); + if (Z3.get_error_code(ctx) !== Z3_error_code.Z3_OK) { + throw new Error('something failed: ' + Z3.get_error_msg(ctx, Z3.get_error_code(ctx))); + } + await Z3.eval_smtlib2_string(ctx, '(simplify)'); + if (Z3.get_error_code(ctx) === Z3_error_code.Z3_OK) { + throw new Error('expected call to eval_smtlib2_string with invalid argument to fail'); + } + console.log('confirming error messages work:', Z3.get_error_msg(ctx, Z3.get_error_code(ctx))); + + Z3.dec_ref(ctx, strAst); Z3.del_context(ctx); diff --git a/src/api/js/package.json b/src/api/js/package.json index 85fd2d24cc6..63a7e7568c4 100644 --- a/src/api/js/package.json +++ b/src/api/js/package.json @@ -6,13 +6,13 @@ "engines": { "node": ">=16" }, - "main": "build/wrapper.js", - "types": "build/wrapper.d.ts", + "main": "build/node-wrapper.js", + "types": "build/node-wrapper.d.ts", "files": [ "build/*.{js,d.ts,wasm}" ], "scripts": { - "build-ts": "mkdir -p build && node scripts/make-ts-wrapper.js > build/wrapper.ts && tsc", + "build-ts": "mkdir -p build && rm -rf build/*.ts && cp src/node-wrapper.ts build && node scripts/make-ts-wrapper.js > build/wrapper.ts && tsc", "build-wasm": "mkdir -p build && node scripts/make-cc-wrapper.js > build/async-fns.cc && ./build-wasm.sh", "format": "prettier --write --single-quote --arrow-parens avoid --print-width 120 --trailing-comma all '{,src/,scripts/}*.{js,ts}'", "test": "node test-ts-api.js" diff --git a/src/api/js/scripts/list-exports.js b/src/api/js/scripts/list-exports.js index 4513b7e5800..e86850e9108 100644 --- a/src/api/js/scripts/list-exports.js +++ b/src/api/js/scripts/list-exports.js @@ -5,7 +5,7 @@ let { functions } = require('./parse-api.js'); let asyncFns = require('./async-fns.js'); -let extras = asyncFns.map(f => '_async_' + f); +let extras = ['_set_throwy_error_handler', '_set_noop_error_handler', ...asyncFns.map(f => '_async_' + f)]; let fns = functions.filter(f => !asyncFns.includes(f.name)); console.log(JSON.stringify([...extras, ...functions.map(f => '_' + f.name)])); diff --git a/src/api/js/scripts/make-cc-wrapper.js b/src/api/js/scripts/make-cc-wrapper.js index b0860e3499a..b522e4ebc9a 100644 --- a/src/api/js/scripts/make-cc-wrapper.js +++ b/src/api/js/scripts/make-cc-wrapper.js @@ -51,11 +51,14 @@ void wrapper(Args&&... args) { MAIN_THREAD_ASYNC_EM_ASM({ resolve_async($0); }, result); + } catch (std::exception& e) { + MAIN_THREAD_ASYNC_EM_ASM({ + reject_async(new Error(UTF8ToString($0))); + }, e.what()); } catch (...) { MAIN_THREAD_ASYNC_EM_ASM({ reject_async('failed with unknown exception'); }); - throw; } }); t.detach(); @@ -69,14 +72,44 @@ void wrapper_str(Args&&... args) { MAIN_THREAD_ASYNC_EM_ASM({ resolve_async(UTF8ToString($0)); }, result); + } catch (std::exception& e) { + MAIN_THREAD_ASYNC_EM_ASM({ + reject_async(new Error(UTF8ToString($0))); + }, e.what()); } catch (...) { MAIN_THREAD_ASYNC_EM_ASM({ - reject_async('failed with unknown exception'); + reject_async(new Error('failed with unknown exception')); }); - throw; } }); t.detach(); } + + +class Z3Exception : public std::exception { +public: + const std::string m_msg; + Z3Exception(const std::string& msg) : m_msg(msg) {} + virtual const char* what() const throw () { + return m_msg.c_str(); + } +}; + +void throwy_error_handler(Z3_context ctx, Z3_error_code c) { + throw Z3Exception(Z3_get_error_msg(ctx, c)); +} + +void noop_error_handler(Z3_context ctx, Z3_error_code c) { + // pass +} + +extern "C" void set_throwy_error_handler(Z3_context ctx) { + Z3_set_error_handler(ctx, throwy_error_handler); +} + +extern "C" void set_noop_error_handler(Z3_context ctx) { + Z3_set_error_handler(ctx, noop_error_handler); +} + ${wrappers.join('\n\n')}`); diff --git a/src/api/js/scripts/make-ts-wrapper.js b/src/api/js/scripts/make-ts-wrapper.js index 4a51c5ec9c4..e80de68a8ed 100644 --- a/src/api/js/scripts/make-ts-wrapper.js +++ b/src/api/js/scripts/make-ts-wrapper.js @@ -19,6 +19,8 @@ let makePointerType = t => // or up to 3 out int64s const BYTES_TO_ALLOCATE_FOR_OUT_PARAMS = 24; +const CUSTOM_IMPLEMENTATIONS = ['Z3_mk_context', 'Z3_mk_context_rc']; + function toEmType(type) { if (type in primitiveTypes) { type = primitiveTypes[type]; @@ -70,6 +72,10 @@ function toEm(p) { let isInParam = p => ['in', 'in_array'].includes(p.kind); function wrapFunction(fn) { + if (CUSTOM_IMPLEMENTATIONS.includes(fn.name)) { + return null; + } + let inParams = fn.params.filter(isInParam); let outParams = fn.params.map((p, idx) => ({ ...p, idx })).filter(p => !isInParam(p)); @@ -318,9 +324,6 @@ function wrapFunction(fn) { `.trim(); } - if (isAsync) { - } - // prettier-ignore let invocation = `Mod.ccall('${isAsync ? 'async_' : ''}${fn.name}', '${cReturnType}', ${JSON.stringify(ctypes)}, [${args.map(toEm).join(', ')}])`; @@ -358,8 +361,6 @@ let out = ` // THIS FILE IS AUTOMATICALLY GENERATED BY ${path.basename(__filename)} // DO NOT EDIT IT BY HAND -// @ts-ignore no-implicit-any -import initModule = require('./z3-built.js'); interface Pointer extends Number { readonly __typeName: T; } @@ -381,7 +382,7 @@ ${Object.entries(enums) .map(e => wrapEnum(e[0], e[1])) .join('\n\n')} -export async function init() { +export async function init(initModule: any) { let Mod = await initModule(); // this works for both signed and unsigned, because JS will wrap for you when constructing the Uint32Array @@ -410,10 +411,21 @@ export async function init() { return { em: Mod, Z3: { - ${functions + mk_context: function(c: Z3_config): Z3_context { + let ctx = Mod._Z3_mk_context(c); + Mod._set_noop_error_handler(ctx); + return ctx; + }, + mk_context_rc: function(c: Z3_config): Z3_context { + let ctx = Mod._Z3_mk_context_rc(c); + Mod._set_noop_error_handler(ctx); + return ctx; + }, + ${functions .map(wrapFunction) .filter(f => f != null) .join(',\n')} + } }; } diff --git a/src/api/js/src/node-wrapper.ts b/src/api/js/src/node-wrapper.ts new file mode 100644 index 00000000000..cd315a02691 --- /dev/null +++ b/src/api/js/src/node-wrapper.ts @@ -0,0 +1,10 @@ +// @ts-ignore no-implicit-any +import initModule = require('./z3-built.js'); + +// @ts-ignore no-implicit-any +import { init as initWrapper } from './wrapper'; + +export * from './wrapper'; +export function init() { + return initWrapper(initModule); +} diff --git a/src/api/js/test-ts-api.ts b/src/api/js/test-ts-api.ts index 0e371fc6e4a..ace3c2b5c8c 100644 --- a/src/api/js/test-ts-api.ts +++ b/src/api/js/test-ts-api.ts @@ -16,8 +16,8 @@ import type { Z3_func_decl, Z3_func_interp, Z3_func_entry, -} from './build/wrapper'; -import { init, Z3_lbool, Z3_ast_kind, Z3_sort_kind, Z3_symbol_kind } from './build/wrapper'; +} from './build/node-wrapper'; +import { init, Z3_lbool, Z3_ast_kind, Z3_sort_kind, Z3_symbol_kind } from './build/node-wrapper'; // @ts-ignore we're not going to bother with types for this import { sprintf } from 'sprintf-js';