From 103c5ad71c4526bfc0b7580bce3383940f953c8f Mon Sep 17 00:00:00 2001
From: Kevin Gibbons <bakkot@gmail.com>
Date: Wed, 25 Sep 2024 07:53:36 -0700
Subject: [PATCH] wasm: attempt to GC in tests (#7400)

---
 .github/workflows/wasm.yml                   |  2 +-
 src/api/js/package.json                      |  2 +-
 src/api/js/scripts/build-wasm.ts             |  2 +-
 src/api/js/src/high-level/high-level.test.ts | 10 +++++++---
 4 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/wasm.yml b/.github/workflows/wasm.yml
index f0b8bd91b79..8e157f5a465 100644
--- a/.github/workflows/wasm.yml
+++ b/.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
diff --git a/src/api/js/package.json b/src/api/js/package.json
index 3e79ba8f4bc..bc6e006d4be 100644
--- a/src/api/js/package.json
+++ b/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"
   },
diff --git a/src/api/js/scripts/build-wasm.ts b/src/api/js/scripts/build-wasm.ts
index 5bdbdea3b47..497b67c10cb 100644
--- a/src/api/js/scripts/build-wasm.ts
+++ b/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);
diff --git a/src/api/js/src/high-level/high-level.test.ts b/src/api/js/src/high-level/high-level.test.ts
index a54f167c25c..53a0e724b13 100644
--- a/src/api/js/src/high-level/high-level.test.ts
+++ b/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');