use Owi to check for equivalence of the fuzzer-generated programs

[zapashcanon]

Hi,

This PR adds the possibility to use Owi to check for the equivalence of programs generated by the fuzzer before and after optimization.

Owi performs symbolic execution, which allows to compare the output of two given functions "for any input value", rather than with concrete inputs (like 0, or 1, as it is currently done IIUC what @tlively told me). Owi can perform symbolic execution in parallel and has been shown to be the best symbolic execution tool for Wasm (disclaimer: I am one of the author of the tool, you can have a look at the paper if you want more details, but I am also happy to answer any question you might have).

This is implemented by using the new owi iso file1.wasm file2.wasm subcommand that I wrote for making this PR easier. This command will get the list of all common imports between the two modules (same name and signature). Then, for each of them, it'll build a harness to invoke the two functions with symbols and check if the two (symbolic) outputs can be shown to be equivalent.

For now, this does not handle Wasm traps (as shown by the use of the --fail-on-assertion-only flag), but I plan to extend it in the short term. It needs the development version of Owi and the following PR: https://github.com/OCamlPro/owi/pull/582/files

There are a few things left to do.

First, I don't understand why sometimes log-i64 is imported with the following signature:

  (import "fuzzing-support" "log-i64" (func  (param i32) (param i32)))

And sometimes with the following one:

  (import "fuzzing-support" "log-i64" (func  (param i64)))

I also noticed some error happening during Owi's parsing of binary files. Is binaryen still generating non-standard opcodes in the binary format (for compatibily with previous proposal draft for instance)? If not, it may simply be a bug in Owi, or an unhandled Wasm proposal that I forgot in all_disallowed (is there a full list of the proposals somewhere?).

Finally, a few imports are missing in Owi (table-get and table-set).

(I commented out the other handlers, but this is of course only temporary to make testing easier).

Moreover, I only tested this locally. Is the fuzzer tested in CI or is there something special I should do about installing Owi?

[kripken]

Very cool!

I don't understand why sometimes log-i64 is imported with [different signatures]

That is due to JS legalization. i64s are not legal in JS, at least before BigInt integration, so i64s are passed as pairs of i32s in many cases.

You can either handle both signatures, or you can run only when !LEGALIZE (in which case you'll always get an i64).

I also noticed some error happening during Owi's parsing of binary files. Is binaryen still generating non-standard opcodes in the binary format (for compatibily with previous proposal draft for instance)?

You may be seeing string opcodes, or exact types. It may be best to run only when those features are disabled. For the list of "unstable" features you can probably copy from our ClusterFuzz integration:

https://github.com/WebAssembly/binaryen/blob/main/scripts/clusterfuzz/run.py#L83-L91

Finally, a few imports are missing in Owi (table-get and table-set).

Note btw that you can use a recent option to avoid the fuzzer adding any imports or exports,

#7300

Is the fuzzer tested in CI

We run it continuously offline (and manually as needed), but it doesn't run in github actions here.