WebAssembly Symbolic Processor (WASP)

The WebAssembly Symbolic Processor (WASP), is a symbolic execution engine for testing Wasm modules, which works directly on Wasm code and was built on top of a standard-compliant Wasm reference implementation.

Build from source

• Install opam.
• Bootstrap the OCaml compiler:

opam init -y
opam switch create wasp 4.14.0 4.14.0
eval $(opam env)

• Then, install the library dependencies:

git clone --recurse-submodules https://github.com/wasp-platform/wasp.git
cd wasp
opam install . ./encoding/encoding.opam --deps-only

• Build and test:

dune build
dune runtest
make -C share/libc
dune install

Running WASP

You can call the executable with

wasp [option | file ...]

wasp: undefined symbol Z3_fixedpoint_pop

If you encounter this or other Z3 symbol related errors add the following line to your shell configuration file:

# change /default/ if you installed z3 on another version of OCaml
export LD_LIBRARY_PATH="${HOME}/.opam/default/lib/z3/:${LD_LIBRARY_PATH}"

On macOS the environment variable should be DYLD_LIBRARY_PATH.

Converting Modules or Scripts

The option -o allows to output module definitions to files. Depending on its extension, it'll write out the module definition in either S-expression or binary format. This option allows to convert between the two in both directions. For example:

wasp -d module.wast -o module.wasm
wasp -d module.wasm -o module.wast

Command Line Expressions

The option -e allows to provide arbitrary script commands directly on the command line. For example:

wasp module.wasm -e '(invoke "foo")'

Additional Details

WASP extends the WebAssembly Reference Interpreter. Hence, all other additional functionalities of the reference interpreter are available in WASP.