From d4e802e42cf720fb6d0475f19db79ea66a94d9ea Mon Sep 17 00:00:00 2001 From: Arthur Carcano Date: Wed, 3 Jul 2024 15:49:20 +0200 Subject: [PATCH 1/2] Simplify interprets interface --- test/fuzz/fuzzer.ml | 10 ++-------- test/fuzz/interprets.ml | 31 ++++++------------------------- 2 files changed, 8 insertions(+), 33 deletions(-) diff --git a/test/fuzz/fuzzer.ml b/test/fuzz/fuzzer.ml index 29804116a..39b904723 100644 --- a/test/fuzz/fuzzer.ml +++ b/test/fuzz/fuzzer.ml @@ -13,17 +13,11 @@ let compare (module I1 : Interprets.INTERPRET) Format.pp_err "running %s@\n" I1.name; Format.pp_flush Stdlib.Format.err_formatter () end; - let r1 = - let m = I1.of_symbolic m in - I1.run m - in + let r1 = I1.parse_and_run m in if Param.debug then begin Format.pp_err "running %s@\n" I2.name end; - let r2 = - let m = I2.of_symbolic m in - I2.run m - in + let r2 = I2.parse_and_run m in Format.pp_err "@]"; match (r1, r2) with | Ok (), Ok () -> true diff --git a/test/fuzz/interprets.ml b/test/fuzz/interprets.ml index cfe4703ed..83b0ab6aa 100644 --- a/test/fuzz/interprets.ml +++ b/test/fuzz/interprets.ml @@ -4,11 +4,7 @@ open Syntax exception Timeout module type INTERPRET = sig - type t - - val of_symbolic : Text.modul -> t - - val run : t -> unit Result.t + val parse_and_run : Text.modul -> unit Result.t val name : string end @@ -32,11 +28,7 @@ let timeout_call_run (run : unit -> unit Result.t) : 'a Result.t = with Timeout -> Error `Timeout module Owi_unoptimized : INTERPRET = struct - type t = Text.modul - - let of_symbolic = Fun.id - - let run modul = + let parse_and_run modul = let* simplified = Compile.Text.until_binary ~unsafe:false modul in let* () = Typecheck.modul simplified in let* regular, link_state = @@ -49,11 +41,7 @@ module Owi_unoptimized : INTERPRET = struct end module Owi_optimized : INTERPRET = struct - type t = Text.modul - - let of_symbolic = Fun.id - - let run modul = + let parse_and_run modul = let* simplified = Compile.Text.until_binary ~unsafe:false modul in let* () = Typecheck.modul simplified in let simplified = Optimize.modul simplified in @@ -67,13 +55,9 @@ module Owi_optimized : INTERPRET = struct end module Owi_symbolic : INTERPRET = struct - type t = Text.modul - - let of_symbolic = Fun.id - let dummy_workers_count = 42 - let run modul : unit Result.t = + let parse_and_run modul : unit Result.t = let* simplified = Compile.Text.until_binary ~unsafe:false modul in let* () = Typecheck.modul simplified in let* regular, link_state = @@ -96,11 +80,8 @@ module Owi_symbolic : INTERPRET = struct end module Reference : INTERPRET = struct - type t = string - - let of_symbolic modul = Format.asprintf "%a" Text.pp_modul modul - - let run modul : unit Result.t = + let parse_and_run modul : unit Result.t = + let modul = Format.asprintf "%a" Text.pp_modul modul in let prefix = "owi_fuzzer_official" in let suffix = ".wast" in let tmp_file = Filename.temp_file prefix suffix in From 8b8005c3f0d64ba0c6c3a350b69bbee2d6a42107 Mon Sep 17 00:00:00 2001 From: Arthur Carcano Date: Mon, 1 Jul 2024 11:58:28 +0200 Subject: [PATCH 2/2] wip --- src/symbolic/symbolic_wasm_ffi.ml | 22 +++++++++++++---- test/fuzz/fuzzer.ml | 39 ++++++++++++++++++++++++++++++- test/fuzz/interprets.ml | 37 +++++++++++++++++++++++++++++ test/fuzz/param.ml | 6 +++-- 4 files changed, 97 insertions(+), 7 deletions(-) diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml index e8ffd012e..a6f40ce8d 100644 --- a/src/symbolic/symbolic_wasm_ffi.ml +++ b/src/symbolic/symbolic_wasm_ffi.ml @@ -6,10 +6,14 @@ module Expr = Smtml.Expr module Choice = Symbolic_choice (* The constraint is used here to make sure we don't forget to define one of the expected FFI functions, this whole file is further constrained such that if one function of M is unused in the FFI module below, an error will be displayed *) -module M : - Wasm_ffi_intf.S0 - with type 'a t = 'a Choice.t - and module Value = Symbolic_value = struct +module M : sig + include + Wasm_ffi_intf.S0 + with type 'a t = 'a Choice.t + and module Value = Symbolic_value + + val symbol_i32_constant : Value.int32 -> Value.int32 t +end = struct type 'a t = 'a Choice.t module Value = Symbolic_value @@ -29,6 +33,13 @@ module M : let symbol_i32 () = Choice.with_new_symbol (Ty_bitv 32) Expr.symbol + let symbol_i32_constant v = + let open Choice in + let* s = Choice.with_new_symbol (Ty_bitv 32) Expr.symbol in + let eq = Value.I32.eq v s in + let+ () = Choice.add_pc eq in + s + let symbol_i64 () = Choice.with_new_symbol (Ty_bitv 64) Expr.symbol let symbol_f32 () = Choice.with_new_symbol (Ty_fp 32) Expr.symbol @@ -94,6 +105,9 @@ let symbolic_extern_module = ; ( "i32_symbol" , Symbolic.P.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_i32) ) + ; ( "i32_symbol_constant" + , Symbolic.P.Extern_func.Extern_func + (Func (Arg (I32, Res), R1 I32), symbol_i32_constant) ) ; ( "i64_symbol" , Symbolic.P.Extern_func.Extern_func (Func (UArg Res, R1 I64), symbol_i64) ) diff --git a/test/fuzz/fuzzer.ml b/test/fuzz/fuzzer.ml index 39b904723..3cb3520ec 100644 --- a/test/fuzz/fuzzer.ml +++ b/test/fuzz/fuzzer.ml @@ -83,6 +83,37 @@ let add_test name gen (module I1 : Interprets.INTERPRET) let gen (conf : Env.conf) = Crowbar.with_printer Owi.Text.pp_modul (Gen.modul conf) +let prepare_for_sym (modul : Owi.Text.modul) = + let open Owi.Text in + let open Types in + let process_inst inst inst_list = + match inst with + | I32_const i -> I32_const i :: Call (Text "constant_symbol") :: inst_list + | _ -> inst :: inst_list + in + let process_func fnc = + let updated_body = List.fold_right process_inst fnc.body [] in + { fnc with body = updated_body } + in + let process_field = function + | MFunc fnc -> MFunc (process_func fnc) + | fld -> fld + in + let import_sym_cst_i32 = + MImport + { modul = "symbolic" + ; name = "symbol_i32_constant" + ; desc = + Import_func + ( Some "symbol_i32_constant" + , Bt_raw (None, ([ (None, Num_type I32) ], [ Num_type I32 ])) ) + } + in + let updated_fields = + import_sym_cst_i32 :: List.map process_field modul.fields + in + { modul with fields = updated_fields } + let () = let open Interprets in if Param.optimize_fuzzing then @@ -96,4 +127,10 @@ let () = if Param.symbolic_fuzzing then add_test "symbolic_fuzzing" (gen Env.Symbolic) (module Owi_unoptimized) - (module Owi_symbolic) + (module Owi_symbolic); + if Param.full_symbolic_fuzzing then + add_test "full symbolic_fuzzing" (gen Env.Symbolic) + (module Owi_unoptimized) + ( module Owi_symbolic_multicore (struct + let symbolize = prepare_for_sym + end) ) diff --git a/test/fuzz/interprets.ml b/test/fuzz/interprets.ml index 83b0ab6aa..dde8951fd 100644 --- a/test/fuzz/interprets.ml +++ b/test/fuzz/interprets.ml @@ -104,3 +104,40 @@ module Reference : INTERPRET = struct let name = "reference" end + +module Owi_symbolic_multicore (Symbolizer : sig + val symbolize : Text.modul -> Text.modul +end) : INTERPRET = struct + let name = "multicore" + + let parse_and_run modul : unit Result.t = + let modul = Symbolizer.symbolize modul in + let* simplified = Compile.Text.until_binary ~unsafe:false modul in + let* () = Typecheck.modul simplified in + let* regular, link_state = + Link.modul Link.empty_state ~name:None simplified + in + let regular = Symbolic.convert_module_to_run regular in + timeout_call_run (fun () -> + let c = Interpret.SymbolicP.modul link_state.envs regular in + let init_thread : Thread.t = Thread.create () in + let res_acc = ref [] in + let res_acc_mutex = Mutex.create () in + let jhs = + Symbolic_choice.run ~workers:1 Smtml.Solver_dispatcher.Z3_solver c + init_thread + ~callback:(fun (res, _) -> + Mutex.protect res_acc_mutex (fun () -> res_acc := res :: !res_acc) ) + ~callback_init:(fun () -> ()) + ~callback_end:(fun () -> ()) + in + Array.iter (fun jh -> Domain.join jh) jhs; + match !res_acc with + | [ v ] -> begin + match v with + | EVal r -> r + | ETrap (t, _mdl) -> Error (`Trap t) + | EAssert (_expr, _mdl) -> Error `Assert_failure + end + | _ -> failwith "Unexpected multiple results." ) +end diff --git a/test/fuzz/param.ml b/test/fuzz/param.ml index bca8295ed..f68cffb23 100644 --- a/test/fuzz/param.ml +++ b/test/fuzz/param.ml @@ -3,11 +3,13 @@ let debug = false -let optimize_fuzzing = true +let optimize_fuzzing = false let reference_fuzzing = false -let symbolic_fuzzing = true +let symbolic_fuzzing = false + +let full_symbolic_fuzzing = true let initial_fuel = 100