Skip to content

Commit

Permalink
Document WAST test contributing
Browse files Browse the repository at this point in the history
  • Loading branch information
chfast committed Sep 18, 2020
1 parent d576e44 commit f12735e
Showing 1 changed file with 145 additions and 0 deletions.
145 changes: 145 additions & 0 deletions cmake/spectests_contributing.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,145 @@


## Run fuzzer

Run Fizzy vs WABT verification fuzzer, currently in `fuzzing` branch.
Start with small inputs.

```shell script
bin/fizzy-fuzz-parser corpus -max_len=13
```

In case it finds a failure you will see output like
```text
INFO: Seed: 770491456
INFO: Loaded 1 modules (64068 inline 8-bit counters): 64068 [0xb8dc90, 0xb9d6d4),
INFO: Loaded 1 PC tables (64068 PCs): 64068 [0xb9d6d8,0xc97b18),
INFO: 10986 files found in corpus
INFO: seed corpus: files: 10986 min: 1b max: 27419b total: 740862b rss: 40Mb
#11160 INITED cov: 7782 ft: 9644 corp: 227/2677b exec/s: 0 rss: 186Mb
#65536 pulse cov: 7782 ft: 9644 corp: 227/2677b lim: 13 exec/s: 32768 rss: 215Mb
#131072 pulse cov: 7782 ft: 9644 corp: 227/2677b lim: 13 exec/s: 32768 rss: 248Mb
#262144 pulse cov: 7782 ft: 9644 corp: 227/2677b lim: 13 exec/s: 32768 rss: 314Mb
MALFORMED: invalid limits 4
/home/chfast/Projects/wasmx/fizzy/test/fuzzer/parser_fuzzer.cpp:47:9: runtime error: execution reached an unreachable program point
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior /home/chfast/Projects/wasmx/fizzy/test/fuzzer/parser_fuzzer.cpp:47:9 in
MS: 1 ChangeBit-; base unit: 846f4928f92649789961543e93544b4c2ed6fc44
0x0,0x61,0x73,0x6d,0x1,0x0,0x0,0x0,0x5,0x3,0x1,0x4,0x2b,
\x00asm\x01\x00\x00\x00\x05\x03\x01\x04+
artifact_prefix='./'; Test unit written to ./crash-016934f781c41276bfacda9a90385cef85a88d5f
Base64: AGFzbQEAAAAFAwEEKw==
```

In this example Fizzy reported the error `MALFORMED: invalid limits 4`
while WABT considers the Wasm binary valid.
The test unit (Wasm binary) is also printed in various forms and saved as
`crash-016934f781c41276bfacda9a90385cef85a88d5f`.


## Check WebAssembly spec interpreter

In case of false negative validation result in WABT it is likely that
such case is missing in the WAST spec test.

Build the `wasm reference interpreter` following official instructions.

Rename `crash-016934f781c41276bfacda9a90385cef85a88d5f` to `crash.wasm`
as the interpreter need proper files extension to recognize file type.

```shell script
./wasm crash.wasm
```

Output:
```text
crash.wasm:0xb: decoding error: integer too large
```

Good news. This is effectively the same error reported as in Fizzy. In Wasm 1.0 `limits` kind
can be 0 or 1. The the value 4 in the `crash.wasm` is larger than the max 1.


## Inspect with WABT tools

You can use `wasm2wat` or `wasm-validate` tools to confirm the bug in WABT.
Make sure you use the same version as used for fuzzing.
Disable all extensions except "mutable globals".

In our example, `wasm2wat crash.wasm`:
```webassembly
(module
(memory (;0;) 43 i64))
```
This indicates that the issue is in the memory section.

Unfortunately, we get different error as the data section also has invalid length.
Let's fix that.


## Prepare WAST test

Dump the test unit (`xxd -p -c1000 crash.wasm`):

```hexdump
0061736d01000000050301042b
```

Here are created WAST tests, placed in `new.wast` file. In the original `crash.wasm` the invalid 4
is followed by `2b` byte. We added 2 more variants of the test with byte `00` and without any
following byte (remember to change the section length if you actually modify the length).

```wast
(assert_malformed
(module binary
"\00asm" "\01\00\00\00"
"\05\03\01" ;; memory section
"\04\2b" ;; malformed memory limit 4
)
"integer too large"
)
(assert_malformed
(module binary
"\00asm" "\01\00\00\00"
"\05\03\01" ;; memory section
"\04\00" ;; malformed memory limit 4
)
"integer too large"
)
(assert_malformed
(module binary
"\00asm" "\01\00\00\00"
"\05\02\01" ;; memory section
"\04" ;; malformed memory limit 4
)
"integer too large"
)
```

These tests can be rechecked with WABT.

```shell script
wast2json new.wast
wasm-validate new.0.wasm
wasm-validate new.1.wasm
wasm-validate new.2.wasm
```

The last test case is actually failing in WABT for some other reason, but it can stay as a valid
spectests addition.

```text
000000c: error: unable to read u32 leb128: memory initial page count
```


## Debug & fix WABT

Debug `wasm-validate new.0.wasm` to find out why it passes validation.
Binary loading code is in `binary-reader.cc`.

The example bug is fixed by https://github.com/WebAssembly/wabt/pull/1547.


## Send WAST tests upstream

0 comments on commit f12735e

Please sign in to comment.