Fuzzing against verified fork of spec interpreter (#3843)

* Revert "Remove spec interpreter fuzz target temporarily (#3399)"

This reverts commit 25d3fa4d7b.

* add support for differential fuzzing against verified OCaml interpreter

* formatting

* comments

* fix missing dep case

* fix build error

* fix unit tests?

* restore previous differential_v8 max_table config

* attempt: add OCaml deps

* fix interpeter github repo

* fix spec repo url

* fix zarith package

* fix unit test

crates/fuzzing/wasm-spec-interpreter/ocaml/Makefile

@@ -11,14 +11,19 @@ SPEC_DIR := spec/interpreter
 SPEC_BUILD_DIR := $(SPEC_DIR)/_build
 SPEC_LIB := $(SPEC_BUILD_DIR)/wasm.cmxa
 
+# A space-separated list of paths that the linker will use to search for libgmp.
+# Override with `make LIBGMP_PATHS=...`.
+LIBGMP_PATHS := /usr/lib /usr/lib/x86_64-linux-gnu
+
+PKGS = zarith
 
 # Build and package the static library, `libinterpret.a`.
 $(BUILD_DIR)/libinterpret.a: $(BUILD_DIR)/interpret.lib.o
 	ar qs $@ $^
 $(BUILD_DIR)/interpret.lib.o: $(SPEC_LIB) $(BUILD_DIR)/interpret.cmx
-	ocamlopt $(OCAML_FLAGS) -I $(SPEC_BUILD_DIR) -o $@ -output-complete-obj $^
+	ocamlfind ocamlopt $(OCAML_FLAGS) -I $(SPEC_BUILD_DIR) -o $@ -output-complete-obj $^ -linkpkg $(PKGS:%=-package %) -cclib "$(LIBGMP_PATHS:%=-L%)"
 $(BUILD_DIR)/interpret.cmx: interpret.ml $(SPEC_BUILD_DIR) $(BUILD_DIR)
-	ocamlopt $(OCAML_FLAGS) -I $(SPEC_BUILD_DIR) -o $@ -c -impl $<
+	ocamlfind ocamlopt $(OCAML_FLAGS) -I $(SPEC_BUILD_DIR) -o $@ -c -impl $< -linkpkg $(PKGS:%=-package %)
 $(BUILD_DIR):
 	mkdir -p $@
 

crates/fuzzing/wasm-spec-interpreter/ocaml/README.md

@@ -1,7 +1,10 @@
 This directory contains the necessary parts for building a library with FFI
 access to the Wasm spec interpreter. Its major parts:
  - `spec`: the Wasm spec code as a Git submodule (you may need to retrieve it:
-   `git clone https://github.com/bytecodealliance/wasm-spec-mirror).
+   `git clone https://github.com/conrad-watt/spec/tree/wasmtime_fuzzing).
  - `interpret.ml`: a shim layer for calling the Wasm spec code and exposing it
    for FFI access
  - `Makefile`: the steps for gluing these pieces together into a static library
+
+Note: the makefile must be configured with the path to libgmp. See LIBGMP_PATHS
+in the makefile.

crates/fuzzing/wasm-spec-interpreter/ocaml/interpret.ml

@@ -7,6 +7,7 @@ understand this better, see:
 
 (* Here we access the WebAssembly specification interpreter; this must be linked in. *)
 open Wasm
+open Wasm.WasmRef_Isa_m.WasmRef_Isa
 
 (** Enumerate the types of values we pass across the FFI boundary. This must match `Value` in
 `src/lib.rs` *)
@@ -17,18 +18,18 @@ type ffi_value =
   | F64 of int64
 
 (** Helper for converting the FFI values to their spec interpreter type. *)
-let convert_to_wasm (v: ffi_value) : Values.value = match v with
-| I32 n -> Values.Num (I32 n)
-| I64 n -> Values.Num (I64 n)
-| F32 n -> Values.Num (F32 (F32.of_bits n))
-| F64 n -> Values.Num (F64 (F64.of_bits n))
+let convert_to_wasm (v: ffi_value) : v = match v with
+| I32 n -> ConstInt32 (I32_impl_abs n)
+| I64 n -> ConstInt64 (I64_impl_abs n)
+| F32 n -> ConstFloat32 (F32.of_bits n)
+| F64 n -> ConstFloat64 (F64.of_bits n)
 
 (** Helper for converting the spec interpreter values to their FFI type. *)
-let convert_from_wasm (v: Values.value) : ffi_value = match v with
-| Values.Num (I32 n) -> I32 n
-| Values.Num (I64 n) -> I64 n
-| Values.Num (F32 n) -> F32 (F32.to_bits n)
-| Values.Num (F64 n) -> F64 (F64.to_bits n)
+let convert_from_wasm (v: v) : ffi_value = match v with
+| (ConstInt32 (I32_impl_abs n)) -> I32 n
+| (ConstInt64 (I64_impl_abs n)) -> I64 n
+| (ConstFloat32 n) -> F32 (F32.to_bits n)
+| (ConstFloat64 n) -> F64 (F64.to_bits n)
 | _ -> failwith "Unknown type"
 
 (** Parse the given WebAssembly module binary into an Ast.module_. At some point in the future this
@@ -36,30 +37,37 @@ should also be able to parse the textual form (TODO). *)
 let parse bytes =
   (* Optionally, use Bytes.unsafe_to_string here to avoid the copy *)
   let bytes_as_str = Bytes.to_string bytes in
-  Decode.decode "default" bytes_as_str
+  (Decode.decode "default" bytes_as_str)
 
 (** Return true if an export is a function. *)
 let match_exported_func export = match export with
-| (_, Instance.ExternFunc(func)) -> true
+| Module_export_ext(_,Ext_func n,_) -> true
 | _ -> false
 
 (** Extract a function from its export or fail. *)
 let extract_exported_func export = match export with
-| (_, Instance.ExternFunc(func)) -> func
+| Module_export_ext(_,Ext_func n,_) -> n
 | _ -> failwith ""
 
-(** Interpret the first exported function with the given parameters and return the result. *)
-let interpret_exn module_bytes params =
-  let params' = List.map convert_to_wasm params in
+(** Interpret the first exported function and return the result. Use provided
+parameters if they exist, otherwise use default (zeroed) values. *)
+let interpret_exn module_bytes opt_params =
+  let opt_params_ = Option.map (List.map convert_to_wasm) opt_params in
   let module_ = parse module_bytes in
-  let instance = Eval.init module_ [] in
-  let func = extract_exported_func (List.find match_exported_func instance.exports) in
-  let returns = Eval.invoke func params' in
-  let returns' = List.map convert_from_wasm returns in
-  returns' (* TODO eventually we should hash the memory state and return the hash *)
+  let m_isa = Ast_convert.convert_module (module_.it) in
+  let fuel = Z.of_string "4611686018427387904" in
+  let max_call_depth = Z.of_string "300" in
+  (match run_fuzz (nat_of_integer fuel) (nat_of_integer max_call_depth) (make_empty_store_m ()) m_isa [] opt_params_ () with
+  | (s', RValue vs_isa') -> List.map convert_from_wasm (List.rev vs_isa')
+  | (s', RTrap str) -> raise (Eval.Trap (Source.no_region, "(Isabelle) trap: " ^ str))
+  | (s', (RCrash (Error_exhaustion str))) -> raise (Eval.Exhaustion (Source.no_region, "(Isabelle) call stack exhausted"))
+  | (s', (RCrash (Error_invalid str))) -> raise (Eval.Crash (Source.no_region, "(Isabelle) error: " ^ str))
+  | (s', (RCrash (Error_invariant str))) -> raise (Eval.Crash (Source.no_region, "(Isabelle) error: " ^ str))
+  (* TODO eventually we should hash the memory state and return the hash *)
+  )
 
-let interpret module_bytes params =
-  try Ok(interpret_exn module_bytes params) with
+let interpret module_bytes opt_params =
+  try Ok(interpret_exn module_bytes opt_params) with
   | _ as e -> Error(Printexc.to_string e)
 
 let () =