Skip to content
A Prototype Formal Semantics of WebAssembly in K
WebAssembly Makefile Shell Other
Branch: master
Clone or download
ehildenb Build updates - enable LLVM backend (#185)
* Makefile: switch to capital variables

* Makefile: enable llvm backend

* Jenkinsfile: remove uneeded -B for make calls

* Dockerfile: install additional dependencies from KEVM

* Makefile: fix llvm_kompiled file

* Dockerfile: setup rust correctly

* Dockerfile: correct copy-paste error

* kwasm: enable llvm backend

* tests/success-llvm.out: add expected output for llvm backend

* Makefile: make sure K_BIN on PATH

* Jenkinsfile: test LLVM backend too

* tests/success-llvm: update expected output

* README: add install-rust step

* kwasm: allow setting KWASM_DEFN_DIR

* deps/k: update submodule

* Jenkinsfile: manually split float/non-float tests
Latest commit f38def0 Aug 21, 2019

README.md

KWasm: Semantics of WebAssembly in K

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 -m KWASM-LEMMAS

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

./kwasm run   --backend java    tests/simple/arithmetic.wast
./kwasm prove --backend haskell tests/proofs/simple-arithmetic-spec.k -m KWASM-LEMMAS

Installing/Building

K Backends

There are three backends of K available, the OCAML backend for concrete execution, the Java backend for symbolic reasoning and proofs, and the experimental Haskell backend for developers. This repository generates the build-products for both backends in .build/defn/java/ and .build/defn/ocaml/.

System 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)
  • Opam, important: Ubuntu users prior to 15.04 must build from source, as the Ubuntu install for 14.10 and prior is broken. opam repository also requires rsync.
  • 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.

On Ubuntu >= 15.04 (for example):

sudo apt install                                                      \
         autoconf curl flex gcc libffi-dev libmpfr-dev libtool maven  \
         opam openjdk-8-jdk pandoc pkg-config python3 python-pygments \
         python-recommonmark python-sphinx time zlib1g-dev

To upgrade stack (if needed):

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

Building

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

git submodule update --init --recursive

If you haven't already setup K's OCaml dependencies more recently than February 1, 2019, then you also need to setup the K OCaml dependencies:

./deps/k/k-distribution/src/main/scripts/bin/k-configure-opam-dev

NOTE: It may prove useful to first do rm -rf ~/.opam if you've setup K projcets in the past and are experiencing trouble with the newest opam libraries. This is a fairly destructive operation, and will break any other projects that depend on specific locally installed ocaml packages.

Similarly, you'll need to setup K's Rust dependencies:

./deps/k/llvm-backend/src/main/native/llvm-backend/install-rust

Install repository specific dependencies:

make deps

And then build the semantics:

make build

To only build specific backends, you can do make build-java, make build-ocaml, 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

Resources

You can’t perform that action at this time.