Awesome

KWasm: Semantics of WebAssembly in K

Want to Support KWasm Development?

This repository presents a prototype formal semantics of WebAssembly. It is currently under construction. For examples of current capabilities, see the unit tests under the tests/simple directory.

Repository Structure

Semantics Layout

The following files constitute the KWasm semantics:

data.md provides the (functional) data of WebAssembly (basic types, type constructors, and values).
numeric.md provides the functional rules for numeric operators.
wasm.md is the main KWasm semantics, containing the configuration and transition rules of WebAssembly.

These additional files extend the semantics to make the repository more useful:

test.md is an execution harness for KWasm, providing a simple language for describing tests/programs.

Example usage: `./kwasm` runner script

After building the definition, you can run the definition using ./kwasm. The most up-to-date documentation will always be in ./kwasm help.

Run the file tests/simple/arithmetic.wast:

./kwasm run tests/simple/arithmetic.wast

To run proofs, you can similarly use ./kwasm, but must specify the module to use for proving. For example, to prove the specification tests/proofs/simple-arithmetic-spec.k:

./kwasm prove tests/proofs/simple-arithmetic-spec.k kwasm-lemmas

To prove WRC-20 specifications:

./kwasm prove tests/proofs/wrc20-spec.k wrc20

You can optionally override the default backend using the --backend BACKEND flag:

./kwasm run   --backend llvm    tests/simple/arithmetic.wast
./kwasm prove --backend haskell tests/proofs/simple-arithmetic-spec.k kwasm-lemmas

Installing/Building

K Backends

There are two backends of K available, the LLVM backend for concrete execution, and the Haskell backend for symbolic reasoning and proofs. This repository generates the build-products for the backends in .build/defn/llvm and .build/defn/haskell.

Dependencies

The following are needed for building/running KWasm:

git
Pandoc >= 1.17 is used to generate the *.k files from the *.md files.
GNU Bison, Flex, and Autoconf.
GNU libmpfr and libtool.
Java 8 JDK (eg. OpenJDK)
Haskell Stack. Note that the version of the stack tool provided by your package manager might not be recent enough. Please follow installation instructions from the Haskell Stack website linked above.
LLVM For building the LLVM backend.
Z3 version 4.8.15

On Ubuntu >= 15.04 (for example):

sudo apt-get install --yes                                                            \
    autoconf bison clang++-8 clang-8 cmake curl flex gcc libboost-test-dev libffi-dev \
    libgmp-dev libjemalloc-dev libmpfr-dev libprocps-dev libprotobuf-dev libtool      \
    libyaml-dev lld-8 llvm llvm-8 llvm-8-tools maven openjdk-8-jdk pandoc pkg-config  \
    protobuf-compiler python3 python-pygments python-recommonmark python-sphinx time  \
    zlib1g-dev

To upgrade stack (if needed):

stack upgrade
export PATH=$HOME/.local/bin:$PATH

After installing the above dependencies, make sure the submodules are setup:

git submodule update --init --recursive

Install repository specific dependencies:

make deps

Installing Z3

Note that KWASM requires Z3 version 4.8.15, which you may need to install from a source build if your package manager supplies a different version. To do so, follow the instructions here after checking out the correct tag in the Z3 repository:

git clone https://github.com/Z3Prover/z3.git
cd z3
git checkout z3-4.8.15
python scripts/mk_make.py
cd build
make
sudo make install

Building

And then build the semantics:

make build

To only build a specific backend, you can do make build-llvm or make build-haskell.

Media and documents

The media/ directory contains presentations and reports about about KWasm. The documents are named with an approximate date of presentation/submission, what type of document it is, and a brief contextual name, e.g., name of conference where it was held.

GhostScript is a dependency for building documents of type report.

sudo apt install ghostscript

To build all documents in the media file:

make media

Testing

The target test contains all the currently passing tests.

make test