wasm build: disable error handler (#5996)

* wasm: set error handler to no-op

* wasm: better wrapper for use in html

Author: bakkot

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.
 

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);
 

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"

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)]));

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')}`);

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<T extends string> 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')}
+
     }
   };
 }

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);
+}

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';