From df793f9f3079ec2f6db0194d465d4c2d5237ec7d Mon Sep 17 00:00:00 2001 From: Kevin Gibbons Date: Fri, 6 Dec 2024 12:14:57 -0800 Subject: [PATCH] fixes for newer emscripten thread handling behavior --- .../js/examples/high-level/miracle-sudoku.ts | 4 +-- src/api/js/examples/low-level/example-raw.ts | 17 ++++++++-- src/api/js/examples/low-level/test-ts-api.ts | 5 +-- src/api/js/scripts/build-wasm.ts | 6 ++-- src/api/js/scripts/make-cc-wrapper.ts | 32 +++++++++++++++++++ src/api/js/src/low-level/async-wrapper.js | 2 ++ 6 files changed, 53 insertions(+), 13 deletions(-) diff --git a/src/api/js/examples/high-level/miracle-sudoku.ts b/src/api/js/examples/high-level/miracle-sudoku.ts index 093d599f3..763581ae7 100644 --- a/src/api/js/examples/high-level/miracle-sudoku.ts +++ b/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); diff --git a/src/api/js/examples/low-level/example-raw.ts b/src/api/js/examples/low-level/example-raw.ts index 2790f9594..68e7997e6 100644 --- a/src/api/js/examples/low-level/example-raw.ts +++ b/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); diff --git a/src/api/js/examples/low-level/test-ts-api.ts b/src/api/js/examples/low-level/test-ts-api.ts index 3eaef5bfe..7e69f1e06 100644 --- a/src/api/js/examples/low-level/test-ts-api.ts +++ b/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); diff --git a/src/api/js/scripts/build-wasm.ts b/src/api/js/scripts/build-wasm.ts index 497b67c10..a5b57ee3f 100644 --- a/src/api/js/scripts/build-wasm.ts +++ b/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); diff --git a/src/api/js/scripts/make-cc-wrapper.ts b/src/api/js/scripts/make-cc-wrapper.ts index 2b7ca2536..bf98219e2 100644 --- a/src/api/js/scripts/make-cc-wrapper.ts +++ b/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 @@ -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)); + }); } diff --git a/src/api/js/src/low-level/async-wrapper.js b/src/api/js/src/low-level/async-wrapper.js index 78b3fee53..f4e62e51a 100644 --- a/src/api/js/src/low-level/async-wrapper.js +++ b/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