mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

wasm: attempt to GC in tests (#7400)

Browse source
This commit is contained in:
Kevin Gibbons 2024-09-25 07:53:36 -07:00 committed by GitHub
parent 82eb18674b
commit 103c5ad71c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/workflows/wasm.yml vendored
View file

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

2
src/api/js/package.json
View file

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

2
src/api/js/scripts/build-wasm.ts
View file

@ -69,7 +69,7 @@ const fns = JSON.stringify(exportedFuncs());
const methods = '["ccall","FS","allocate","UTF8ToString","intArrayFromString","ALLOC_NORMAL"]'; const methods = '["ccall","FS","allocate","UTF8ToString","intArrayFromString","ALLOC_NORMAL"]';
const libz3a = path.normalize('../../../build/libz3.a'); const libz3a = path.normalize('../../../build/libz3.a');
spawnSync( 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); fs.rmSync(ccWrapperPath);

10
src/api/js/src/high-level/high-level.test.ts
View file

@ -4,6 +4,12 @@ import { init, killThreads } from '../jest';
import { Arith, Bool, Model, Quantifier, Z3AssertionError, Z3HighLevel, AstVector } from './types'; import { Arith, Bool, Model, Quantifier, Z3AssertionError, Z3HighLevel, AstVector } from './types';
import { expectType } from 'ts-expect'; 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. * Generate all possible solutions from given assumptions.
* *
@ -356,8 +362,7 @@ describe('high-level', () => {
}); });
describe('bitvectors', () => { describe('bitvectors', () => {
/**
it('can do simple proofs', async () => { it('can do simple proofs', async () => {
const { BitVec, Concat, Implies, isBitVecVal } = api.Context('main'); 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))); 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 () => { it('finds x and y such that: x ^ y - 103 == x * y', async () => {
const { BitVec, isBitVecVal } = api.Context('main'); const { BitVec, isBitVecVal } = api.Context('main');