wasm build: disable error handler (#5996)

* wasm: set error handler to no-op

* wasm: better wrapper for use in html

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