Issues importing z3-solver using Vite

[stefnotch]

I npm installed the z3-solver package, and then imported it, hoping that it would work in the browser. Since I didn't want to deal with the differences between CommonJS and ES Modules, I decided to use one of the more common bundlers (Vite).

Upon attempting to do

import { init } from "z3-solver";
const { Z3, Context } = await init();

it throws the following exception

I suppose the browser build is a bit borked?

Here's a reproduction project s-crackme.zip

[stefnotch]

Using the prebuilt version doesn't work, because it makes a wrong assumption about where the wasm files are

import init from "z3-solver/build/z3-built";
console.log(init);

[stefnotch]

Copying z3-built to the public directory, and then adding

    <script src="z3-built.js"></script>
    <script>
      globalThis.global = { initZ3: globalThis.initZ3 };
    </script>

to the index.html seems to work.

That's a questionable workaround.

[volisoft]

This behavior is actually documented here: https://www.npmjs.com/package/z3-solver?activeTab=readme

The Emscripten worker model will spawn multiple instances of z3-built.js for long-running operations. When building for the web, you should include that file as its own script on the page - using a bundler like webpack will prevent it from loading correctly.

Nor sure though, why webpack should prevent z3-built.js from loading.

[ym-han]

@stefnotch I'm running into similar issues (but the workarounds you've posted don't seem to work for me). Is there any chance you could share a link to your repo?

(There's a good chance that my issues have to do with sveltekit though.)

[stefnotch]

@ym-han I sadly don't have a public project that uses z3-solver.

I would have contributed a patch to this repository, but there's no good universal solution for this yet. Ideally, the following would work

import { whatever } from `./z3-built.wasm

but currently no browser, and only a few bundlers implement this. I think it'll become widely supported in a few years though.

But, I can still do my best to help out. So I set up a new project using sveltekit, and tried to add this library. I had to

• import { init } from "z3-solver"; and only call that in a script that will get executed client-side. In my case, I put it inside an onMount(() => { }) hook
• import z3-built.js near the top of app.html. It's important that it gets loaded before all other scripts
• change the vite config to allow SharedArrayBuffers to be used
• put the z3-built.js, z3-built.wasm and z3-built.worker.js in the static directory

import { sveltekit } from "@sveltejs/kit/vite";
import { defineConfig } from "vite";

export default defineConfig({
  plugins: [
    /**
     * We're using `SharedArrayBuffer`s in our code,
     * which requires either HTTPS or localhost, and it requires cross origin isolation.
     * So we're enabling the CORS headers here for development mode.
     *
     * Do note that your production server will need HTTPS and CORS headers set up correctly.
     * If you cannot control the HTTP headers that your production server sends back (like on GitHub pages),
     * then there's a workaround using a service worker. See https://dev.to/stefnotch/enabling-coop-coep-without-touching-the-server-2d3n
     */
    {
      // Plugin code is from https://github.com/chaosprint/vite-plugin-cross-origin-isolation
      name: "configure-response-headers",
      configureServer: (server) => {
        server.middlewares.use((_req, res, next) => {
          res.setHeader("Cross-Origin-Embedder-Policy", "require-corp");
          res.setHeader("Cross-Origin-Opener-Policy", "same-origin");
          next();
        });
      },
    },
    sveltekit(),
  ],
});

Here you go my-app.zip

Feel free to ping me if you've got any further questions.

[ym-han]

Thank you very much @stefnotch !!!! Managed to get it working with your help!!!!!!

It turns out there was just one small step I had done differently: namely, where z3-built.js should be imported. I had imported it in <svelte:head> in the +page.svelte I was testing with instead of doing it in the project-wide app.html. I haven't done enough testing to be 100% sure, but from what I've seen so far, it looks like doing it instead in app.html made all the difference --- I'm guessing sveltekit must be loading other scripts before it loads page-specific <svelte:head>s.

Thank you once again!!!!!

Minor note for other people trying this in the future with sveltekit: the z3 files don't need to be in static specifically, and they can be copied with a vite plugin. Eg in the vite.config.ts:

import { viteStaticCopy } from 'vite-plugin-static-copy';
export default defineConfig({
	plugins: [
	        ...
		viteStaticCopy({
			targets: [
				{
					src: 'node_modules/z3-solver/build/z3-built.*',
					dest: ''
				}
			]

[stefnotch]

@ym-han Lovely to hear that you got it to work!

I'm glad that I could help :) Do pay it forward and help the next person who needs your help.