π Owi 
Owi is a toolchain to work with WebAssembly. It is written in OCaml. It provides a binary with many subcommands:
owi c: a bug finding tool for C code that performs symbolic execution by compiling to Wasm and using our symbolic Wasm interpreter;owi conc: a concolic Wasm interpreter;owi fmt: a formatter for Wasm;owi opt: an optimizer for Wasm;owi replay: run a module containing symbols with concrete values from a model produced by a previous symbolic executionowi run: a concrete Wasm interpreter;owi script: an interpreter for Wasm scripts;owi sym: a symbolic Wasm interpreter;owi validate: a validator for Wasm modules;owi wasm2wat: a Wasm binary to text format translater;owi wat2wasm: a Wasm text to binary format translater.
It also provides an OCaml library which allows for instance to import OCaml functions in a Wasm module in a type-safe way!
We also have a fuzzer that is able to generate random valid Wasm programs. For now it has not been made available as a subcommand so you'll have to hack the code a little bit to play with it.
π§βπ We are looking for interns, have a look at the internship labeled issues.
owi can be installed with opam:
$ opam install owi
# if you intend to use symbolic execution you must install one solver
# you can choose any solver supported by smtml
# z3, colibri2, bitwuzla-cxx or cvc5 for instance
$ opam install z3
If you don't have opam, you can install it following the how to install opam guide.
If you can't or don't want to use opam, you can build the package with dune build -p owi @install but you'll first have to install the dependencies by yourself. You can find the list of dependencies in the dune-project file.
To get the development version:
$ git clone git@github.com:OCamlPro/owi.git
$ cd owi
$ opam install . --deps-only
$ dune build -p owi @install
$ dune install
To get a proper development setup:
$ git clone git@github.com:OCamlPro/owi.git
$ cd owi
$ opam install . --deps-only --with-test --with-doc --with-dev-setup
$ dune build @all
The π status means the proposal is not applicable to Owi.
| Proposal | Status |
|---|---|
| Import/Export of Mutable Globals | βοΈ |
| Non-trapping float-to-int conversions | βοΈ |
| Sign-extension operators | βοΈ |
| Multi-value | βοΈ |
| Reference Types | βοΈ |
| Bulk memory operations | βοΈ |
| Fixed-width SIMD | β |
| JavaScript BigInt to WebAssembly i64 integration | π |
We only list proposals that reached phase 3 at least.
| Proposal | Status |
|---|---|
| Tail call | βοΈ |
| Typed Function References | βοΈ |
| Extended Constant Expressions | βοΈ |
| Garbage collection | Ongoing |
| Custom Annotation Syntax in the Text Format | Ongoing |
| Multiple memories | β |
| Memory64 | β |
| Exception handling | β |
| Branch Hinting | β |
| Relaxed SIMD | β |
| Threads | β |
| Web Content Security Policy | π |
| JS Promise Integration | π |
| Type Reflection for WebAssembly JavaScript API | π |
- september 2023: ICFP OCaml track
- october 2023: Wasm Research Day organized by the WebAssembly Research Center and hosted in Google Munich
- april 2024: OUPS (OCaml UserS in Paris)
- november 2024: LVP working group day of the GdR GPL
Although the name Owi comes from an acronym (OCaml WebAssembly Interpreter), it must be written as a proper noun and only the first letter must be capitalized. It is possible to write the name in full lowercase when referring to the opam package or to the name of the binary.
The reason we chose this spelling rather than the fully capitalized version is that in French, Owi is pronounced [oβwi(Κ)] which sounds like "Oh oui !" which means "Oh yes!". Thus it should be pronounced this way and not by spelling the three letters it is made of.
See CHANGELOG.
Owi
Copyright (C) 2021-2024 OCamlPro
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU Affero General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU Affero General Public License for more details.
You should have received a copy of the GNU Affero General Public License
along with this program. If not, see <http://www.gnu.org/licenses/>.
See LICENSE.
A few files have been taken from the WebAssembly reference interpreter. They are licensed under the Apache License 2.0 and have a different copyright which is stated in the header of the files.
Some code has been taken from the base library from Jane Street. It is licensed under the MIT License and have a different copyright which is stated in the header of the files.
Some code has been taken from the E-ACSL plugin of Frama-C. It is licensed under the GNU Lesser General Public License 2.1 and have a different copyright which is stated in the header of the files.
This project was partly funded through the NGI0 Core Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme. See Owi project on NLnet.