diff --git a/src/api/js/PUBLISHED_README.md b/src/api/js/PUBLISHED_README.md index 42d58a916..c096bbe41 100644 --- a/src/api/js/PUBLISHED_README.md +++ b/src/api/js/PUBLISHED_README.md @@ -16,6 +16,16 @@ const { This package has different initialization for browser and node. Your bundler and node should choose good version automatically, but you can import the one you need manually - `const { init } = require('z3-solver/node');` or `const { init } = require('z3-solver/browser');`. +The `init` function also accepts an optional Emscripten module overrides object. This is useful in runtimes such as Deno where you may want to provide a wasm load path explicitly instead of relying on filesystem reads. For example: + +```typescript +import { init } from 'npm:z3-solver'; + +const api = await init({ + locateFile: (file) => import.meta.resolve(`npm:z3-solver/build/${file}`), +}); +``` + ### Limitations The package requires threads, which means you'll need to be running in an environment which supports `SharedArrayBuffer`. In browsers, in addition to ensuring the browser has implemented `SharedArrayBuffer`, you'll need to serve your page with [special headers](https://web.dev/coop-coep/). There's a [neat trick](https://github.com/gzuidhof/coi-serviceworker) for doing that client-side on e.g. Github Pages, though you shouldn't use that trick in more complex applications. diff --git a/src/api/js/scripts/make-ts-wrapper.ts b/src/api/js/scripts/make-ts-wrapper.ts index d19307243..15652aa8e 100644 --- a/src/api/js/scripts/make-ts-wrapper.ts +++ b/src/api/js/scripts/make-ts-wrapper.ts @@ -444,8 +444,8 @@ ${Object.entries(primitiveTypes) .map(e => `type ${e[0]} = ${e[1]};`) .join('\n')} -export async function init(initModule: any) { - let Mod = await initModule(); +export async function init(initModule: any, moduleOverrides: Record = {}) { + let Mod = await initModule(moduleOverrides); // this works for both signed and unsigned, because JS will wrap for you when constructing the Uint32Array function intArrayToByteArr(ints: number[]) { diff --git a/src/api/js/src/browser.test.ts b/src/api/js/src/browser.test.ts new file mode 100644 index 000000000..827f7281d --- /dev/null +++ b/src/api/js/src/browser.test.ts @@ -0,0 +1,43 @@ +const mockInitWrapper = jest.fn(); +const mockCreateApi = jest.fn(); + +jest.mock('./low-level', () => ({ + init: mockInitWrapper, + Z3Core: undefined, + Z3LowLevel: undefined, +})); +jest.mock('./high-level', () => ({ + createApi: mockCreateApi, +})); + +import { init } from './browser'; + +describe('browser init', () => { + beforeEach(() => { + delete (global as any).initZ3; + mockInitWrapper.mockReset(); + mockCreateApi.mockReset(); + }); + + it('passes module overrides to the browser initializer', async () => { + const initZ3 = jest.fn(); + const locateFile = jest.fn((file: string) => `https://example.test/${file}`); + const lowLevel = { Z3: { low: true }, em: { module: true } }; + const highLevel = { Context: jest.fn() }; + (global as any).initZ3 = initZ3; + mockInitWrapper.mockResolvedValue(lowLevel); + mockCreateApi.mockReturnValue(highLevel); + + const api = await init({ locateFile }); + + expect(mockInitWrapper).toHaveBeenCalledWith(initZ3, { locateFile }); + expect(mockCreateApi).toHaveBeenCalledWith(lowLevel.Z3, lowLevel.em); + expect(api).toEqual({ ...lowLevel, ...highLevel }); + }); + + it('throws when initZ3 is unavailable', async () => { + await expect(init()).rejects.toThrow( + 'initZ3 was not imported correctly. Please consult documentation on how to load Z3 in browser', + ); + }); +}); diff --git a/src/api/js/src/browser.ts b/src/api/js/src/browser.ts index 1a6e41f39..83acec7f6 100644 --- a/src/api/js/src/browser.ts +++ b/src/api/js/src/browser.ts @@ -1,16 +1,16 @@ import { createApi, Z3HighLevel } from './high-level'; -import { init as initWrapper, Z3LowLevel } from './low-level'; +import { init as initWrapper, Z3LowLevel, Z3ModuleOverrides } from './low-level'; export * from './high-level/types'; export { Z3Core, Z3LowLevel } from './low-level'; export * from './low-level/types.__GENERATED__'; -export async function init(): Promise { +export async function init(moduleOverrides: Z3ModuleOverrides = {}): Promise { const initZ3 = (global as any).initZ3; if (initZ3 === undefined) { throw new Error('initZ3 was not imported correctly. Please consult documentation on how to load Z3 in browser'); } - const lowLevel = await initWrapper(initZ3); + const lowLevel = await initWrapper(initZ3, moduleOverrides); const highLevel = createApi(lowLevel.Z3, lowLevel.em); return { ...lowLevel, ...highLevel }; } diff --git a/src/api/js/src/low-level/index.ts b/src/api/js/src/low-level/index.ts index 1791eae27..25330c494 100644 --- a/src/api/js/src/low-level/index.ts +++ b/src/api/js/src/low-level/index.ts @@ -1,4 +1,5 @@ export * from './types.__GENERATED__'; export * from './wrapper.__GENERATED__'; +export type Z3ModuleOverrides = Record; export type Z3Core = Awaited>['Z3']; export type Z3LowLevel = Awaited>; diff --git a/src/api/js/src/node.test.ts b/src/api/js/src/node.test.ts new file mode 100644 index 000000000..7ea67cb21 --- /dev/null +++ b/src/api/js/src/node.test.ts @@ -0,0 +1,37 @@ +const mockInitModule = jest.fn(); +const mockInitWrapper = jest.fn(); +const mockCreateApi = jest.fn(); + +jest.mock('./z3-built', () => mockInitModule, { virtual: true }); +jest.mock('./low-level', () => ({ + init: mockInitWrapper, + Z3Core: undefined, + Z3LowLevel: undefined, +})); +jest.mock('./high-level', () => ({ + createApi: mockCreateApi, +})); + +import { init } from './node'; + +describe('node init', () => { + beforeEach(() => { + mockInitModule.mockReset(); + mockInitWrapper.mockReset(); + mockCreateApi.mockReset(); + }); + + it('passes module overrides to the low-level initializer', async () => { + const locateFile = jest.fn((file: string) => `npm:z3-solver/build/${file}`); + const lowLevel = { Z3: { low: true }, em: { module: true } }; + const highLevel = { Context: jest.fn() }; + mockInitWrapper.mockResolvedValue(lowLevel); + mockCreateApi.mockReturnValue(highLevel); + + const api = await init({ locateFile }); + + expect(mockInitWrapper).toHaveBeenCalledWith(mockInitModule, { locateFile }); + expect(mockCreateApi).toHaveBeenCalledWith(lowLevel.Z3, lowLevel.em); + expect(api).toEqual({ ...lowLevel, ...highLevel }); + }); +}); diff --git a/src/api/js/src/node.ts b/src/api/js/src/node.ts index 87be038e5..c25387ccb 100644 --- a/src/api/js/src/node.ts +++ b/src/api/js/src/node.ts @@ -2,7 +2,7 @@ import initModule = require('./z3-built'); import { createApi, Z3HighLevel } from './high-level'; -import { init as initWrapper, Z3LowLevel } from './low-level'; +import { init as initWrapper, Z3LowLevel, Z3ModuleOverrides } from './low-level'; export * from './high-level/types'; export { Z3Core, Z3LowLevel } from './low-level'; export * from './low-level/types.__GENERATED__'; @@ -29,10 +29,16 @@ export * from './low-level/types.__GENERATED__'; * * console.log(`x=${model.get(x)}, y=${model.get(y)}`); * // x=0, y=12 + * + * // Deno users can provide an Emscripten locateFile hook to load the wasm + * // through npm's asset resolution instead of filesystem reads. + * // const api = await init({ + * // locateFile: (file) => import.meta.resolve(`npm:z3-solver/build/${file}`), + * // }); * ``` * @category Global */ -export async function init(): Promise { - const lowLevel = await initWrapper(initModule); +export async function init(moduleOverrides: Z3ModuleOverrides = {}): Promise { + const lowLevel = await initWrapper(initModule, moduleOverrides); const highLevel = createApi(lowLevel.Z3, lowLevel.em); return { ...lowLevel, ...highLevel }; }