Update emscripten (#7473)

* fixes for newer emscripten thread handling behavior

* fix return type for async wrapper functions

* update prettier

* update typescript and fix errors

* update emscripten version in CI

* update js readme about tests

Author: bakkot

.github/workflows/wasm-release.yml

@@ -10,7 +10,7 @@ defaults:
     working-directory: src/api/js
 
 env:
-  EM_VERSION: 3.1.15
+  EM_VERSION: 3.1.73
 
 permissions:
   contents: read # to fetch code (actions/checkout)

.github/workflows/wasm.yml

@@ -10,7 +10,7 @@ defaults:
     working-directory: src/api/js
 
 env:
-  EM_VERSION: 3.1.15
+  EM_VERSION: 3.1.73
 
 permissions:
   contents: read # to fetch code (actions/checkout)

src/api/js/README.md

@@ -7,7 +7,7 @@ The readme for the bindings themselves is located in [`PUBLISHED_README.md`](./P
 
 ## Building
 
-You'll need to have emscripten set up, along with all of its dependencies. The easiest way to do that is with [emsdk](https://github.com/emscripten-core/emsdk).
+You'll need to have emscripten set up, along with all of its dependencies. The easiest way to do that is with [emsdk](https://github.com/emscripten-core/emsdk). Newer versions of emscripten may break the build; you can find the version used in CI in [this file](https://github.com/Z3Prover/z3/blob/master/.github/workflows/wasm.yml#L13).
 
 Then run `npm i` to install dependencies, `npm run build:ts` to build the TypeScript wrapper, and `npm run build:wasm` to build the wasm artifact.
 
@@ -17,4 +17,4 @@ Consult the file [build-wasm.ts](https://github.com/Z3Prover/z3/blob/master/src/
 
 ## Tests
 
-Current tests are very minimal: [`test-ts-api.ts`](./test-ts-api.ts) contains a couple real cases translated very mechanically from [this file](https://github.com/Z3Prover/z3/blob/90fd3d82fce20d45ed2eececdf65545bab769503/examples/c/test_capi.c).
+Run `npm test` after building to run tests.

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';
 
@@ -157,7 +157,9 @@ function parseSudoku(str: string) {
 
   async function solve(str: string) {
     let solver = new Z3.Solver();
-    let cells = Array.from({ length: 9 }, (_, col) => Array.from({ length: 9 }, (_, row) => Z3.Int.const(`c_${row}_${col}`)));
+    let cells = Array.from({ length: 9 }, (_, col) =>
+      Array.from({ length: 9 }, (_, row) => Z3.Int.const(`c_${row}_${col}`)),
+    );
     for (let { row, col, value } of parseSudoku(str)) {
       solver.add(cells[row][col].eq(value));
     }
@@ -198,8 +200,6 @@ function parseSudoku(str: string) {
 .........
 .........
 `);
-
-  em.PThread.terminateAllThreads();
 })().catch(e => {
   console.error('error', e);
   process.exit(1);

src/api/js/examples/high-level/using_smtlib2.ts

@@ -25,12 +25,11 @@ import assert from 'assert';
   const model = solver.model();
   let modelStr = model.sexpr();
   modelStr = modelStr.replace(/\n/g, ' ');
-  console.log("Model: ", modelStr);
+  console.log('Model: ', modelStr);
 
   const exprs = z3.ast_from_string(modelStr);
   console.log(exprs);
-
 })().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,24 @@ 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);