conrad-watt opened PR #3843 from verified-fuzzing
to main
:
Following discussions with @fitzgen, @alexcrichton, @cfallin, and @abrown, and at the Feb 17th meeting, this is a patch to update the previously disabled spec-interpreter differential fuzzing to instead use my verified Wasm interpreter (https://github.com/conrad-watt/spec/tree/wasmtime_fuzzing/interpreter). Currently all post-MVP features are disabled, although I'm working towards enabling SIMD.
Unfortunately I couldn't find a way to make the OCaml build system automatically find the
gmp
library (a new dependency, along with thezarith
OCaml library), so thewasm-spec-interpreter/ocaml
makefile now uses aLIBGMP_PATHS
var to manually feed in this information.
conrad-watt updated PR #3843 from verified-fuzzing
to main
.
alexcrichton created PR review comment:
Ah yeah our current wasm-smith generator has independent settings for
max_tables
andreference_types_enabled
. I think it's fine to move this intoset_differential_config
since this is likely silently affecting other differential targets without us being aware of it!
alexcrichton created PR review comment:
Since your spec interpreter has a notion of fuel, would it be possible to avoid this? We could similarly enable fuel for differential-spec modules in Wasmtime and then if either wasmtime or the spec interpreter returns "out of fuel" we'd just discard the fuzz test case and move on
alexcrichton created PR review comment:
These should be safe to omit setting to
false
here since we can rely onset_differential_config
above setting them all to false, although settingmulti_value_enabled
to false below would need to stay sinceset_differential_config
doesn't specifically set that one tofalse
alexcrichton submitted PR review.
alexcrichton submitted PR review.
conrad-watt submitted PR review.
conrad-watt created PR review comment:
Would it be possible to tackle this as a follow-up? If I'm interpreting correctly, currently the fuzzing config allows me to set
consume_fuel
to true, but automatically addsu64:max_value()
fuel in this case. If we add the capability to configure the precise amount of fuel to be added via a parameter, it might be desirable to align other parts of the fuzzing infrastructure to use this parameter too (I'm looking atgenerate_timeout
ingenerators.rs
).
conrad-watt edited PR review comment.
conrad-watt updated PR #3843 from verified-fuzzing
to main
.
conrad-watt updated PR #3843 from verified-fuzzing
to main
.
conrad-watt updated PR #3843 from verified-fuzzing
to main
.
conrad-watt updated PR #3843 from verified-fuzzing
to main
.
conrad-watt updated PR #3843 from verified-fuzzing
to main
.
alexcrichton submitted PR review.
alexcrichton created PR review comment:
Certainly! This can definitely be handled later.
conrad-watt updated PR #3843 from verified-fuzzing
to main
.
conrad-watt updated PR #3843 from verified-fuzzing
to main
.
conrad-watt updated PR #3843 from verified-fuzzing
to main
.
conrad-watt updated PR #3843 from verified-fuzzing
to main
.
conrad-watt updated PR #3843 from verified-fuzzing
to main
.
conrad-watt updated PR #3843 from verified-fuzzing
to main
.
alexcrichton submitted PR review.
alexcrichton merged PR #3843.
Last updated: Dec 23 2024 at 12:05 UTC