============= z3.wasm

This repo contains a build script to compile Z3 <https://github.com/Z3Prover/z3/>_ to WebAssembly using emscripten <https://github.com/kripken/emscripten/>. To make things more reproducible, the build script may be run in a Vagrant <https://www.vagrantup.com/> 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 <https://www.vagrantup.com/>_, 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