Fuzzing multicore monad and smt solver

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)
       )

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
@@ -89,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
@@ -102,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) )

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
@@ -123,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

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