Use with_ffi for wasm btree

src/bench.ml

@@ -130,7 +130,7 @@ let notify_finished runs timeout reference_name output_dir workers =
     let status = Response.status result in
     Fmt.epr "Server responded: %s@." (Code.string_of_status status)
 
-let run tool timeout max_tests files =
+let run tool timeout max_tests files bench_suite =
   let* () =
     match Bos.OS.Env.var Tool.tool_path_env_var_name with
     | None -> Tool.check_if_available tool
@@ -139,8 +139,9 @@ let run tool timeout max_tests files =
   let t = Unix.localtime @@ Unix.gettimeofday () in
   let reference_name = Tool.to_reference_name tool in
   let filename =
-    Fmt.str "results-testcomp-%s-%d-%02d-%02d_%02dh%02dm%02ds/" reference_name
-      (1900 + t.tm_year) (1 + t.tm_mon) t.tm_mday t.tm_hour t.tm_min t.tm_sec
+    Fmt.str "results-%s-%s-%d-%02d-%02d_%02dh%02dm%02ds/" bench_suite
+      reference_name (1900 + t.tm_year) (1 + t.tm_mon) t.tm_mday t.tm_hour
+      t.tm_min t.tm_sec
   in
   let output_dir = Fpath.v filename in
   let _ : bool =

src/bench.mli

@@ -3,4 +3,9 @@ val runs : Tool.t -> float -> Fpath.t -> int -> Fpath.t list -> Runs.t
 val notify_finished : Runs.t -> float -> string -> Fpath.t -> int -> unit
 
 val run :
-  Tool.t -> float -> int -> Fpath.t list -> (unit, [ `Msg of string ]) result
+     Tool.t
+  -> float
+  -> int
+  -> Fpath.t list
+  -> string
+  -> (unit, [ `Msg of string ]) result

src/cmd_testcomp.ml

@@ -87,4 +87,4 @@ let files () =
 
 let run tool timeout max_test =
   let files = Utils.ok_or_fail (files ()) in
-  Bench.run tool timeout max_test files
+  Bench.run tool timeout max_test files "testcomp"

src/cmd_wasm_btree.ml

@@ -1,6 +1,6 @@
 let root = Fpath.v "benchs/btree"
 
-let problems_root = Fpath.(root / "btree" / "native")
+let problems_root = Fpath.(root / "btree" / "with_ffi")
 
 let files () =
   Bos.OS.Dir.fold_contents ~dotfiles:false ~elements:`Files ~traverse:`Any
@@ -10,4 +10,4 @@ let files () =
 
 let run tool timeout max_test =
   let files = Utils.ok_or_fail (files ()) in
-  Bench.run tool timeout max_test files
+  Bench.run tool timeout max_test files "wasm_btree"

src/symbocalypse.ml

@@ -169,7 +169,8 @@ let testcomp_owi_cmd =
   and+ max_tests
   and+ owi in
   Cmd_testcomp.run
-    (owi ~fail_on_assertion_only:true ~entry_point:None ~mode:"c")
+    (owi ~fail_on_assertion_only:true ~entry_point:None ~mode:"c"
+       ~output_workspace:true ~no_stop_at_failure:false )
     timeout max_tests
 
 (* symbocalypse testcomp soteria *)
@@ -224,7 +225,8 @@ let wasm_btree_owi_cmd =
   and+ max_tests
   and+ owi in
   Cmd_wasm_btree.run
-    (owi ~fail_on_assertion_only:false ~entry_point:(Some "main") ~mode:"sym")
+    (owi ~fail_on_assertion_only:false ~entry_point:None ~mode:"sym"
+       ~output_workspace:false ~no_stop_at_failure:true )
     timeout max_tests
 
 (* symbocalypse wasm-btree *)

src/tool.ml

@@ -8,8 +8,10 @@ type t =
       ; solver : Smtml.Solver_type.t
       ; exploration_strategy : string
       ; fail_on_assertion_only : bool
+      ; no_stop_at_failure : bool
       ; entry_point : string option
       ; bench : bool
+      ; output_workspace : bool
       }
   | Klee
   | Symbiotic
@@ -35,15 +37,18 @@ let get_number_of_workers = function
   | Klee | Symbiotic | Soteria -> 1
 
 let mk_owi ~mode ~bench ~exploration_strategy ~optimisation_level ~solver
-  ~workers ~fail_on_assertion_only ~entry_point =
+  ~workers ~fail_on_assertion_only ~entry_point ~output_workspace
+  ~no_stop_at_failure =
   Owi
     { mode
     ; bench
     ; workers
     ; optimisation_level
+    ; output_workspace
     ; solver
     ; exploration_strategy
     ; fail_on_assertion_only
+    ; no_stop_at_failure
     ; entry_point
     }
 
@@ -209,14 +214,14 @@ let execvp ~output_dir tool file timeout =
         ; opts.mode
         ; "--unsafe"
         ; Fmt.str "-w%d" opts.workers
-        ; "--workspace"
-        ; output_dir
         ; "--exploration"
         ; opts.exploration_strategy
         ; "-q"
         ]
+        @ tool_option opts.no_stop_at_failure "--no-stop-at-failure"
         @ tool_option opts.bench "--bench"
         @ tool_option opts.fail_on_assertion_only "--fail-on-assertion-only"
+        @ (if opts.output_workspace then [ "--workpace"; output_dir ] else [])
         @ tool_option
             (opts.mode = "c" || opts.mode = "c++")
             (Fmt.str "-O%d" opts.optimisation_level)

src/tool.mli

@@ -17,6 +17,8 @@ val mk_owi :
   -> workers:int
   -> fail_on_assertion_only:bool
   -> entry_point:string option
+  -> output_workspace:bool
+  -> no_stop_at_failure:bool
   -> t
 
 val mk_klee : unit -> t