Skip to content

Latest commit

 

History

History
84 lines (59 loc) · 2.21 KB

README.md

File metadata and controls

84 lines (59 loc) · 2.21 KB
Raw

WebAssembly Symbolic Processor (WASP)

Apache 2.0 Platform GitHub last commit

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.