wasm: attempt to GC in tests (#7400)

Author: bakkot

.github/workflows/wasm.yml

@@ -48,7 +48,7 @@ jobs:
           source $(dirname $(which emsdk))/emsdk_env.sh
           which node
           which clang++
-          npm run build:wasm -- -sINITIAL_MEMORY=128MB -sALLOW_MEMORY_GROWTH
+          npm run build:wasm
 
       - name: Test
         run: npm test

src/api/js/package.json

@@ -29,7 +29,7 @@
     "clean": "rimraf build 'src/**/*.__GENERATED__.*'",
     "lint": "prettier -c '{./,src/,scripts/,examples/}**/*.{js,ts}'",
     "format": "prettier --write '{./,src/,scripts/}**/*.{js,ts}'",
-    "test": "jest",
+    "test": "node --expose-gc ./node_modules/.bin/jest",
     "docs": "typedoc",
     "check-engine": "check-engine"
   },

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

@@ -69,7 +69,7 @@ const fns = JSON.stringify(exportedFuncs());
 const methods = '["ccall","FS","allocate","UTF8ToString","intArrayFromString","ALLOC_NORMAL"]';
 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=1GB -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 DEMANGLE_SUPPORT=1 -s TOTAL_MEMORY=2GB -s TOTAL_STACK=20MB -I z3/src/api/ -o build/z3-built.js`,
 );
 
 fs.rmSync(ccWrapperPath);

src/api/js/src/high-level/high-level.test.ts

@@ -4,6 +4,12 @@ import { init, killThreads } from '../jest';
 import { Arith, Bool, Model, Quantifier, Z3AssertionError, Z3HighLevel, AstVector } from './types';
 import { expectType } from 'ts-expect';
 
+// this should not be necessary but there may be a Jest bug
+// https://github.com/jestjs/jest/issues/7874
+afterEach(() => {
+  global.gc && global.gc();
+});
+
 /**
  * Generate all possible solutions from given assumptions.
  *
@@ -356,8 +362,7 @@ describe('high-level', () => {
   });
 
 
-    describe('bitvectors', () => {
-      /** 
+  describe('bitvectors', () => {
     it('can do simple proofs', async () => {
       const { BitVec, Concat, Implies, isBitVecVal } = api.Context('main');
 
@@ -376,7 +381,6 @@ describe('high-level', () => {
 
       await prove(Implies(Concat(x, y).eq(Concat(y, x)), x.eq(y)));
     });
-      **/
 
     it('finds x and y such that: x ^ y - 103 == x * y', async () => {
       const { BitVec, isBitVecVal } = api.Context('main');