z3.wasm

This repo contains a build script to compile Z3 to WebAssembly using emscripten. To make things more reproducible, the build script may be run in a Vagrant VM.

Loading Z3 is fairly slow (~15 seconds on Chrome, though less than 1 second on Firefox), but verification typically is within a factor 2 to 5 of native performance.

Pre-build archives are available at https://github.com/cpitclaudel/z3.wasm/releases. Demo at https://people.csail.mit.edu/cpitcla/z3.wasm/z3.html.

Building

In a VM

Install Vagrant, then run this:

vagrant up
vagrant ssh
VAGRANT=true /vagrant/z3.sh

The first build can take up to two hours (emscripten may require a custom build of LLVM, Z3 is large, and all of this is running in a VM). The output (z3w.js, z3w.wasm, z3smt2w.js, and z3smt2w.wasm) is written to build/z3/.

Some Vagrant configurations can cause clang to crash or Vagrant to hang. Building on a physical machine is the most reliable workaround.

Natively

On Debian/Ubuntu systems, you may prefer to build natively, which will be much faster. In that case, just run ./z3.sh, which will place all outputs in build/.

Using the generated code

The build script produces two artefacts: a copy of the full Z3 command line application (z3w.js, z3w.wasm), and a Javascript version of a small SMT2 REPL-style API, built by linking z3smt2.c with libz3.

z3w.js

There is a small example script using nodejs for demonstration purposes in the repo:

$ nodejs z3test.js /nodefs/test.smt2
sat
(model
  (define-fun y () Int
    3)
  (define-fun x () Int
    2)
  (define-fun z () Int
    1)
  (define-fun g ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 2) (= x!1 2)) 0
      0))
  (define-fun f ((x!0 Int)) Int
    (ite (= x!0 2) (- 1)
    (ite (= x!0 3) 1
      (- 1))))
)
unsat
(error "line 14 column 10: model is not available")
unsat

From a webpage the process is roughly the same: write Z3's input to a file using emscripten's virtual file system, and use callMain(args) to run Z3. To capture Z3's output, you can pass a custom print function to the emscripten module upon initialization.

This is all demoed in html/z3.html (that example also uses a WebWorker to run Z3, keeping the page responsive while it runs). Try it like this:

cp build/z3/z3w.js build/z3/z3w.wasm ./html
python3 -m http.server
# Open your browser to http://localhost:8000/html/z3.html

z3smt2w.js

This script exposes a small API useful for verifiers (like F* or Dafny) that interact with Z3 on through pipes. It exposes the following functions:

// Create a fresh SMT2 context
Z3_context smt2Init()

// Globally set `option` to `value`.
void smt2SetParam(const char* option, const char* value)

// Send `query` to `ctx` and fetch the response as a string.
const char* smt2Ask(Z3_context ctx, const char* query)

// Release the resources used by `ctx`.
void smt2Destroy(Z3_context ctx)

There is a small example script using nodejs for demonstration purposes in the repo:

$ nodejs ./z3smt2test.js
sat
(model
  (define-fun y () Int
    4)
  (define-fun x () Int
    2)
  (define-fun z () Int
    0)
  (define-fun g ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 2) (= x!1 2)) 0
      0))
  (define-fun f ((x!0 Int)) Int
    (ite (= x!0 2) (- 1)
    (ite (= x!0 4) 1
      (- 1))))
)
unsat
(error "line 1 column 11: model is not available")
unsat

Check the source code of F*.js for an example of how to use this in a larger application.

Known issues, tips

Chrome precompiles WebAssembly programs before running them — this makes startup slow, though verification after that is fast. The recommendation is to cache compiled modules, but Chrome doesn't (2018-03) allow that yet.

Firefox is much better at this, though the code eventually does run a slower.

Compression

The limited z3smt2.wasm is a bit smaller than the full Z3: use that if you can.

On Apache servers, use the following to compress WASM files (gzipping saves about 75%):

AddType application/wasm .wasm
AddOutputFilterByType DEFLATE application/wasm