Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add owi c command and examples for all subcommands #100

Merged
merged 18 commits into from
Jan 16, 2024
Merged
Show file tree
Hide file tree
Changes from 12 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
148 changes: 25 additions & 123 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,19 @@
# [🐌] Owi [![build-badge]][build status] [![coverage-badge]][coverage percentage]

[Owi] is an [OCaml] toolchain to work with WebAssembly. It provides an interpreter as an executable and a library.
[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 fmt`]: a formatter for Wasm;
- [`owi opt`]: an optimizer for Wasm;
- [`owi run`]: a concrete Wasm interpreter;
- [`owi script`]: an interpreter for [Wasm scripts];
- [`owi sym`]: a symbolic Wasm interpreter.

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.

⚠️ For now, the optimizer and the formatter are quite experimental. The optimizer is well tested but only performs basic optimizations in an inefficient way. The formatter is mainly used for debugging purpose and is probably incorrect on some cases.

## Installation

Expand All @@ -26,127 +39,6 @@ $ dune build -p owi @install
$ dune install
```

## Quickstart

### Concrete interpretation

Given a file `test/passing/quickstart.wast` with the following content:

<!-- $MDX file=test/passing/quickstart.wast -->
```wast
(module $quickstart
(func $f
i32.const 24
i32.const 24
i32.add
drop
)
(start $f)
)
```

Running the executable interpreter is as simple as:
```sh
$ dune exec owi -- run --debug test/passing/quickstart.wast
parsing ...
checking ...
grouping ...
assigning ...
rewriting ...
typechecking ...
linking ...
interpreting ...
stack : [ ]
running instr: call 0
calling func : func f
stack : [ ]
running instr: i32.const 24
stack : [ i32.const 24 ]
running instr: i32.const 24
stack : [ i32.const 24 ; i32.const 24 ]
running instr: i32.add
stack : [ i32.const 48 ]
running instr: drop
stack : [ ]
stack : [ ]
```

If you want to run the file as a [reference test suite script], you can use the `script` command instead of the `run` one. This will allow you to add constructs like assertions and will also link the [spectest module], which provides function for e.g. printing.

If you're interested in the library part of Owi, here's how to get started:

```ocaml
# open Owi;;
# let filename = "test/passing/quickstart.wast";;
val filename : string = "test/passing/quickstart.wast"
# let m =
match Parse.Module.from_file ~filename with
| Ok script -> script
| Error e -> failwith e;;
val m : Text.modul =
...
# let module_to_run, link_state =
match Compile.until_link Link.empty_state ~unsafe:false ~optimize:false ~name:None m with
| Ok v -> v
| Error e -> failwith e;;
val module_to_run : '_weak1 Link.module_to_run =
...
val link_state : '_weak1 Link.state =
...
# let () =
Log.debug_on := true;
match Interpret.Concrete.modul link_state.envs module_to_run with
| Ok () -> ()
| Error e -> failwith e;;
interpreting ...
stack : [ ]
running instr: call 0
calling func : func f
stack : [ ]
running instr: i32.const 24
stack : [ i32.const 24 ]
running instr: i32.const 24
stack : [ i32.const 24 ; i32.const 24 ]
running instr: i32.add
stack : [ i32.const 48 ]
running instr: drop
stack : [ ]
stack : [ ]
```

For more, have a look at the [example] folder, at the [documentation] or at the [test suite].

### Symbolic interpretation

The interpreter can also be used in symbolic mode. This allows to find which input values are leading to a trap.

Given a file `test/sym/mini_test.wast` with the following content:

<!-- $MDX file=test/sym/mini_test.wast -->
```wast
(module
(import "symbolic" "i32" (func $gen_i32 (param i32) (result i32)))

(func $start (local $x i32)
(local.set $x (call $gen_i32 (i32.const 42)))
(if (i32.lt_s (i32.const 5) (local.get $x)) (then
unreachable
)))

(start $start)
)
```

You can run the symbolic interpreter through the `sym` command:
```sh
$ dune exec owi -- sym test/sym/mini_test.wast
Trap: unreachable
Model:
(model
(x_0 i32 (i32 6)))
Reached problem!
```

## Supported proposals

The 🐌 status means the proposal is not applicable to Owi.
Expand Down Expand Up @@ -250,7 +142,7 @@ This project was funded through the [NGI0 Core] Fund, a fund established by [NLn
[Owi project on NLnet]: https://nlnet.nl/project/OWI
[reference test suite script]: https://github.com/WebAssembly/spec/blob/main/interpreter/README.md#scripts
[september 2023]: https://invidious.zapashcanon.fr/watch?v=IM76cMP3Eqo
[spectest module]: https://github.com/WebAssembly/spec/blob/main/interpreter/README.md#spectest-host-module
[Wasm scripts]: https://github.com/WebAssembly/spec/tree/main/interpreter#scripts
[video of our talk]: https://invidious.zapashcanon.fr/watch?v=os_pknmiqmU
[WebAssembly]: https://webassembly.org
[WebAssembly Research Center]: https://www.cs.cmu.edu/wrc
Expand Down Expand Up @@ -278,4 +170,14 @@ This project was funded through the [NGI0 Core] Fund, a fund established by [NLn
[Relaxed SIMD]: https://github.com/WebAssembly/relaxed-simd
[JS Promise Integration]: https://github.com/WebAssembly/js-promise-integration

[`owi c`]: ./example/c
[`owi fmt`]: ./example/fmt
[`owi opt`]: ./example/opt
[`owi run`]: ./example/run
[`owi script`]: ./example/script
[`owi sym`]: ./example/sym
[import OCaml functions in a Wasm module]: ./example/define_host_function
[OCaml library]: ./example/lib
[a fuzzer]: ./test/fuzz

[🐌]: https://invidious.zapashcanon.fr/watch?v=XgK9Fd8ikxk
19 changes: 13 additions & 6 deletions dune-project
Original file line number Diff line number Diff line change
@@ -1,26 +1,28 @@
(lang dune 3.0)

(using menhir 2.1)

(using dune_site 0.1)
(using mdx 0.2)
(using directory-targets 0.1)

(cram enable)

(generate_opam_files true)

(name owi)

(license AGPL-3.0-or-later)

(authors
"Léo Andrès <contact@ndrs.fr>"
"Pierre Chambart <pierre.chambart@ocamlpro.com>")
"Pierre Chambart <pierre.chambart@ocamlpro.com>"
"Filipe Marques")
zapashcanon marked this conversation as resolved.
Show resolved Hide resolved
zapashcanon marked this conversation as resolved.
Show resolved Hide resolved

(maintainers "Léo Andrès <contact@ndrs.fr>")

(source
(github ocamlpro/owi))

(generate_opam_files true)

(package
(name owi)
(synopsis
Expand Down Expand Up @@ -53,7 +55,7 @@
(>= "0.1")
:dev))
(odoc :with-doc)
(bos :with-test)
bos
(mdx
(and
:with-test
Expand All @@ -62,4 +64,9 @@
(graphics :dev)
(tiny_httpd :dev)
(encoding (>= 0.0.3))
xmlm))
sha
xmlm
pyml
re2
dune-site)
(sites (share pyc) (share binc) (share libc)))
Loading
Loading