Symbolic fuzzing

test/fuzz/env.ml

@@ -1,5 +1,9 @@
 open Owi.Types
 
+type conf =
+  | Symbolic
+  | Concrete
+
 type block_kind =
   | Block
   | Loop
@@ -25,9 +29,10 @@ type t =
   ; mutable blocks : (block_kind * string * text block_type) list
   ; mutable funcs : (string * text block_type) list
   ; mutable fuel : int
+  ; conf : conf
   }
 
-let empty () =
+let empty conf =
   { next_data = 0
   ; next_memory = 0
   ; next_type = 0
@@ -47,6 +52,7 @@ let empty () =
   ; blocks = []
   ; funcs = []
   ; fuel = Param.initial_fuel
+  ; conf
   }
 
 let reset_locals env = env.locals <- []

test/fuzz/fuzzer.ml

@@ -71,28 +71,35 @@ let compare (module I1 : Interprets.INTERPRET)
     Format.pp_err "`%s` was OK but `%s` gave error `%s`" I2.name I1.name msg;
     false
 
-let check_optimized m =
-  let open Interprets in
-  let result1 =
-    if Param.optimize_fuzzing then
-      compare (module Owi_unoptimized) (module Owi_optimized) m
-    else true
-  in
-  let result2 =
-    if Param.reference_fuzzing then
-      compare (module Owi_unoptimized) (module Reference) m
-    else true
-  in
-  result1 && result2
+let check (module I1 : Interprets.INTERPRET) (module I2 : Interprets.INTERPRET)
+  m =
+  compare (module I1) (module I2) m
 
-let gen = Crowbar.with_printer Owi.Text.pp_modul Gen.modul
-
-let () =
-  Crowbar.add_test ~name:"fuzzing" [ gen ] (fun m ->
+let add_test name gen (module I1 : Interprets.INTERPRET)
+  (module I2 : Interprets.INTERPRET) =
+  Crowbar.add_test ~name [ gen ] (fun m ->
       incr global_count;
       if Param.debug then Format.pp_err "%a@\n" Owi.Text.pp_modul m;
       Format.pp_err "test module %d [got %d timeouts...]@\n@[<v>" !global_count
         !timeout_count;
       Format.pp_flush Stdlib.Format.err_formatter ();
-      Crowbar.check (check_optimized m);
+      Crowbar.check (check (module I1) (module I2) m);
       Format.pp_err "@]" )
+
+let gen (conf : Env.conf) =
+  Crowbar.with_printer Owi.Text.pp_modul (Gen.modul conf)
+
+let () =
+  let open Interprets in
+  if Param.optimize_fuzzing then
+    add_test "optimize_fuzzing" (gen Env.Concrete)
+      (module Owi_unoptimized)
+      (module Owi_optimized);
+  if Param.reference_fuzzing then
+    add_test "reference_fuzzing" (gen Env.Concrete)
+      (module Owi_unoptimized)
+      (module Reference);
+  if Param.symbolic_fuzzing then
+    add_test "symbolic_fuzzing" (gen Env.Symbolic)
+      (module Owi_unoptimized)
+      (module Owi_symbolic)

test/fuzz/gen.ml

@@ -18,7 +18,8 @@ let expr_always_available block loop expr ~locals ~stack env =
   @ B.global_i32 env @ B.global_i64 env @ B.global_f32 env @ B.global_f64 env
   @ B.local_i32 env @ B.local_i64 env @ B.local_f32 env @ B.local_f64 env
   @ B.data_drop env @ B.elem_drop env
-  @ if B.memory_exists env then [ B.memory_size ] else [] @ B.table_size env
+  @ (if B.memory_exists env then [ B.memory_size ] else [])
+  @ B.table_size env
 
 let expr_available_1_any = [ pair (const Drop) (const [ S.Pop ]) ]
 
@@ -140,9 +141,9 @@ let expr_available_2_f64 =
 
 let if_else expr ~locals ~stack env =
   match stack with
-  | Num_type I32 :: _stack -> begin
+  | Num_type I32 :: stack -> begin
     let* rt = list B.val_type in
-    let* pt = B.stack_prefix (List.tl stack) in
+    let* pt = B.stack_prefix stack in
     let typ =
       Bt_raw (None, (List.rev_map (fun t -> (None, t)) pt, List.rev rt))
     in
@@ -254,9 +255,9 @@ let rec expr ~block_type ~stack ~locals env =
     in
     let* i, ops = choose (expr_available env) in
     let stack = S.apply_stack_ops stack ops in
-    let next = expr ~block_type ~stack ~locals env in
-    let i = const i in
-    map [ i; next ] List.cons
+    let* next = expr ~block_type ~stack ~locals env in
+    let+ i = const i in
+    i :: next
 
 let data env =
   let* mode = B.data_mode env in
@@ -311,7 +312,14 @@ let func env =
   MFunc { type_f; locals; body; id }
 
 let fields env =
-  let* memory = option (memory env) in
+  let* memory =
+    (* No memory management in symbolic context.
+       TODO: When implementation will be more advanced,
+       reactivate and refine instruction by instruction (not_symbolic operator). *)
+    match env.Env.conf with
+    | Concrete -> option (memory env)
+    | Symbolic -> const None
+  in
   let* datas = list (data env) in
   let* types = list (typ env) in
   let* tables = list (table env) in
@@ -333,8 +341,8 @@ let fields env =
   | None -> datas @ types @ elems @ tables @ globals @ funcs
   | Some mem -> datas @ [ mem ] @ types @ elems @ tables @ globals @ funcs
 
-let modul =
+let modul conf =
   let id = Some "m" in
   let* env = const Env.empty in
-  let+ fields = fields (env ()) in
+  let+ fields = fields (env conf) in
   { id; fields }

test/fuzz/gen.mli

@@ -1 +1 @@
-val modul : Owi.Text.modul Crowbar.gen
+val modul : Env.conf -> Owi.Text.modul Crowbar.gen

test/fuzz/param.ml

@@ -7,8 +7,10 @@ let optimize_fuzzing = true
 
 let reference_fuzzing = false
 
+let symbolic_fuzzing = true
+
 let initial_fuel = 100
 
 let allow_partial_timeout = true
 
-let max_time_execution = 0.001 (* seconds *)
+let max_time_execution = 0.01 (* seconds *)