fixes for newer emscripten thread handling behavior

src/api/js/examples/high-level/miracle-sudoku.ts

@@ -1,4 +1,4 @@
-import { init } from '../../build/node';
+import { init } from '../../build/node.js';
 
 import type { Solver, Arith } from '../../build/node';
 
@@ -198,8 +198,6 @@ function parseSudoku(str: string) {
 .........
 .........
 `);
-
-  em.PThread.terminateAllThreads();
 })().catch(e => {
   console.error('error', e);
   process.exit(1);

src/api/js/examples/low-level/example-raw.ts

@@ -1,6 +1,6 @@
 // @ts-ignore we're not going to bother with types for this
 import process from 'process';
-import { init, Z3_error_code } from '../../build/node';
+import { init, Z3_error_code } from '../../build/node.js';
 
 // demonstrates use of the raw API
 
@@ -58,10 +58,21 @@ import { init, Z3_error_code } from '../../build/node';
   }
   console.log('confirming error messages work:', Z3.get_error_msg(ctx, Z3.get_error_code(ctx)));
 
+  Z3.global_param_set('verbose', '0');
+  let result = await Z3.eval_smtlib2_string(ctx, `
+    (declare-const p Bool)
+    (declare-const q Bool)
+    (declare-const r Bool)
+    (declare-const s Bool)
+    (declare-const t Bool)
+    (assert ((_ pbeq 5 2 1 3 3 2) p q r s t))
+    (check-sat)
+    (get-model)
+  `);
+  console.log('checking string evaluation', result);
+
   Z3.dec_ref(ctx, strAst);
   Z3.del_context(ctx);
-
-  em.PThread.terminateAllThreads();
 })().catch(e => {
   console.error('error', e);
   process.exit(1);

src/api/js/examples/low-level/test-ts-api.ts

@@ -20,7 +20,7 @@ import type {
   Z3_sort,
   Z3_symbol,
 } from '../../build/node';
-import { init, Z3_ast_kind, Z3_lbool, Z3_sort_kind, Z3_symbol_kind } from '../../build/node';
+import { init, Z3_ast_kind, Z3_lbool, Z3_sort_kind, Z3_symbol_kind } from '../../build/node.js';
 
 let printf = (str: string, ...args: unknown[]) => console.log(sprintf(str.replace(/\n$/, ''), ...args));
 
@@ -383,9 +383,6 @@ let printf = (str: string, ...args: unknown[]) => console.log(sprintf(str.replac
 
   await bitvector_example2();
   await unsat_core_and_proof_example();
-
-  // shut down
-  em.PThread.terminateAllThreads();
 })().catch(e => {
   console.error('error', e);
   process.exit(1);

src/api/js/scripts/build-wasm.ts

@@ -40,7 +40,7 @@ function spawnSync(command: string, opts: SpawnOptions = {}) {
 }
 
 function exportedFuncs(): string[] {
-  const extras = ['_malloc', '_set_throwy_error_handler', '_set_noop_error_handler', ...asyncFuncs.map(f => '_async_' + f)];
+  const extras = ['_malloc', '_free', '_set_throwy_error_handler', '_set_noop_error_handler', ...asyncFuncs.map(f => '_async_' + f)];
 
   // TODO(ritave): This variable is unused in original script, find out if it's important
   const fns: any[] = (functions as any[]).filter(f => !asyncFuncs.includes(f.name));
@@ -66,10 +66,10 @@ fs.mkdirSync(path.dirname(ccWrapperPath), { recursive: true });
 fs.writeFileSync(ccWrapperPath, makeCCWrapper());
 
 const fns = JSON.stringify(exportedFuncs());
-const methods = '["ccall","FS","allocate","UTF8ToString","intArrayFromString","ALLOC_NORMAL"]';
+const methods = '["PThread","ccall","FS","UTF8ToString","intArrayFromString"]';
 const libz3a = path.normalize('../../../build/libz3.a');
 spawnSync(
-  `emcc build/async-fns.cc ${libz3a} --std=c++20 --pre-js src/low-level/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=2GB -s TOTAL_STACK=20MB -I z3/src/api/ -o build/z3-built.js`,
+  `emcc build/async-fns.cc ${libz3a} --std=c++20 --pre-js src/low-level/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 TOTAL_MEMORY=2GB -s TOTAL_STACK=20MB -I z3/src/api/ -o build/z3-built.js`,
 );
 
 fs.rmSync(ccWrapperPath);

src/api/js/scripts/make-cc-wrapper.ts

@@ -58,8 +58,24 @@ void wrapper(Args&&... args) {
         reject_async('failed with unknown exception');
       });
     }
+    MAIN_THREAD_ASYNC_EM_ASM({
+      // this clears the earliest timeout
+      // not necessarily the one corresponding to this thread
+      // but that's ok
+      clearTimeout(threadTimeouts.shift());
+    });
   });
   t.detach();
+  EM_ASM({
+    // https://github.com/emscripten-core/emscripten/issues/23092
+    // in Node.js, the process will die if there is no active work
+    // which can happen while the thread is spawning
+    // or while it is running
+    // so we set a timeout here so it stays alive
+    // this needs to be longer than it could conceivably take to call the one function
+    // it gets cleared as soon as the thread actually finishes
+    threadTimeouts.push(setTimeout(() => {}, 600000));
+  });
 }
 
 template<typename Fn, Fn fn, typename... Args>
@@ -79,8 +95,24 @@ void wrapper_str(Args&&... args) {
         reject_async(new Error('failed with unknown exception'));
       });
     }
+    MAIN_THREAD_ASYNC_EM_ASM({
+      // this clears the earliest timeout
+      // not necessarily the one corresponding to this thread
+      // but that's ok
+      clearTimeout(threadTimeouts.shift());
+    });
   });
   t.detach();
+  EM_ASM({
+    // https://github.com/emscripten-core/emscripten/issues/23092
+    // in Node.js, the process will die if there is no active work
+    // which can happen while the thread is spawning
+    // or while it is running
+    // so we set a timeout here so it stays alive
+    // this needs to be longer than it could conceivably take to call the one function
+    // it gets cleared as soon as the thread actually finishes
+    threadTimeouts.push(setTimeout(() => {}, 600000));
+  });
 }
 
 

src/api/js/src/low-level/async-wrapper.js

@@ -1,6 +1,8 @@
 // this wrapper works with async-fns to provide promise-based off-thread versions of some functions
 // It's prepended directly by emscripten to the resulting z3-built.js
 
+let threadTimeouts = [];
+
 let capability = null;
 function resolve_async(val) {
   // setTimeout is a workaround for https://github.com/emscripten-core/emscripten/issues/15900