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.
- 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
You can call the executable with
wasp [option | file ...]
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
.
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
The option -e
allows to provide arbitrary script commands
directly on the command line. For example:
wasp module.wasm -e '(invoke "foo")'
WASP extends the WebAssembly Reference Interpreter. Hence, all other additional functionalities of the reference interpreter are available in WASP.