Start making benchmark runner declarative

Start making benchmark more declarative by having a configuration
file which we can specify what datasets to download and what
experiments to run with which solvers.

This commit removes multi query mode, adds a `setup` command to download
datasets from smtcomp zenodo page, and renames `singl-query` to `exec`
and makes this command just parse smt2 benchmarks so it's easier to
redirect efforts into checking parsing errors.

Author: filipeom

bench/datasets.sexp

@@ -0,0 +1,10 @@
+(dataset
+ (name QF_FP)
+ (url "https://zenodo.org/records/15493090/files/QF_FP.tar.zst")
+ (md5sum "b7f9786b5317d7be8a185c861088f504"))
+
+(dataset
+ (name QF_S)
+ (url "https://zenodo.org/records/15493090/files/QF_S.tar.zst")
+ (md5sum "22c3c79ddd6bbcb2be5a9cae8b3ffdcf"))
+

bench/runner/cmd_exec.ml

@@ -0,0 +1,204 @@
+let files_to_run d =
+  match
+    Bos.OS.Dir.fold_contents ~traverse:`Any
+      (fun path acc -> if Fpath.has_ext ".smt2" path then path :: acc else acc)
+      [] d
+  with
+  | Ok results -> results
+  | Error (`Msg err) -> Fmt.failwith "%s" err
+
+let parse_status =
+  let re = Dune_re.(compile @@ Perl.re {|^(sat|unsat|unknown)|}) in
+  fun stdout ->
+    match Dune_re.exec_opt re stdout with
+    | None -> `Unknown
+    | Some group -> (
+      match Dune_re.Group.get group 1 with
+      | "sat" -> `Sat
+      | "unsat" -> `Unsat
+      | "unknown" -> `Unknown
+      | _ -> assert false )
+
+let pp_status fmt = function
+  | `Sat -> Fmt.string fmt "sat"
+  | `Unsat -> Fmt.string fmt "unsat"
+  | `Unknown -> Fmt.string fmt "unknown"
+
+let summarize results =
+  let results_list =
+    List.map
+      (fun (prover, prover_results) ->
+        ( prover
+        , List.fold_left
+            (fun (total, sat, unsat, unknown, time)
+                 (_, _, stdout, _, rtime, _rusage) ->
+              let sat, unsat, unknown =
+                match parse_status stdout with
+                | `Sat -> (succ sat, unsat, unknown)
+                | `Unsat -> (sat, succ unsat, unknown)
+                | `Unknown -> (sat, unsat, succ unknown)
+              in
+              (succ total, sat, unsat, unknown, time +. rtime) )
+            (0, 0, 0, 0, 0.) prover_results ) )
+      results
+  in
+  (* let solver, total, sat, unsat, unknwon, rtime = *)
+  let _ =
+    List.fold_left
+      (fun (solver, total, sat, unsat, unknown, rtime)
+           (prover, (p_total, p_sat, p_unsat, p_unknown, p_rtime)) ->
+        ( Tool.prover_to_string prover :: solver
+        , p_total :: total
+        , p_sat :: sat
+        , p_unsat :: unsat
+        , p_unknown :: unknown
+        , p_rtime :: rtime ) )
+      ([], [], [], [], [], []) results_list
+  in
+  (* Owl_dataframe.make *)
+  (*   [| "solver"; "total"; "sat"; "unsat"; "unknown"; "rtime" |] *)
+  (*   ~data: *)
+  (*     [| Owl_dataframe.pack_string_series @@ Array.of_list solver *)
+  (*      ; Owl_dataframe.pack_int_series @@ Array.of_list total *)
+  (*      ; Owl_dataframe.pack_int_series @@ Array.of_list sat *)
+  (*      ; Owl_dataframe.pack_int_series @@ Array.of_list unsat *)
+  (*      ; Owl_dataframe.pack_int_series @@ Array.of_list unknwon *)
+  (*      ; Owl_dataframe.pack_float_series @@ Array.of_list rtime *)
+  (*     |] *)
+  assert false
+
+(* Maybe we can clean this up later *)
+(* let make_data_frames results = *)
+(*   List.map *)
+(*     (fun (prover, prover_results) -> *)
+(*       let provers, benchmark, res, stdout, stderr, rtime, utime, stime, maxrss = *)
+(*         List.fold_left *)
+(*           (fun ( prover_acc *)
+(*                , bench_acc *)
+(*                , res_acc *)
+(*                , stdout_acc *)
+(*                , stderr_acc *)
+(*                , rtime_acc *)
+(*                , utime_acc *)
+(*                , stime_acc *)
+(*                , maxrss_acc ) *)
+(*                (_status, benchmark, stdout, stderr, rtime, rusage) -> *)
+(*             ( Tool.prover_to_string prover :: prover_acc *)
+(*             , Fmt.str "%a" Fpath.pp benchmark :: bench_acc *)
+(*             , Fmt.str "%a" pp_status (parse_status stdout) :: res_acc *)
+(*             , String.escaped stdout :: stdout_acc *)
+(*             , String.escaped stderr :: stderr_acc *)
+(*             , rtime :: rtime_acc *)
+(*             , rusage.ExtUnix.Specific.ru_utime :: utime_acc *)
+(*             , rusage.ExtUnix.Specific.ru_stime :: stime_acc *)
+(*             , rusage.ExtUnix.Specific.ru_maxrss :: maxrss_acc ) ) *)
+(*           ([], [], [], [], [], [], [], [], []) *)
+(*           prover_results *)
+(*       in *)
+(*       let df = *)
+(*         Owl_dataframe.make *)
+(*           [| "prover" *)
+(*            ; "benchmark" *)
+(*            ; "res" *)
+(*            ; "stdout" *)
+(*            ; "stderr" *)
+(*            ; "rtime" *)
+(*            ; "utime" *)
+(*            ; "stime" *)
+(*            ; "maxrss" *)
+(*           |] *)
+(*           ~data: *)
+(*             [| Owl_dataframe.pack_string_series @@ Array.of_list provers *)
+(*              ; Owl_dataframe.pack_string_series @@ Array.of_list benchmark *)
+(*              ; Owl_dataframe.pack_string_series @@ Array.of_list res *)
+(*              ; Owl_dataframe.pack_string_series @@ Array.of_list stdout *)
+(*              ; Owl_dataframe.pack_string_series @@ Array.of_list stderr *)
+(*              ; Owl_dataframe.pack_float_series @@ Array.of_list rtime *)
+(*              ; Owl_dataframe.pack_float_series @@ Array.of_list utime *)
+(*              ; Owl_dataframe.pack_float_series @@ Array.of_list stime *)
+(*              ; Owl_dataframe.pack_int_series *)
+(*                @@ Array.of_list (List.map Int64.to_int maxrss) *)
+(*             |] *)
+(*       in *)
+(*       (prover, df) ) *)
+(*     results *)
+
+let write_data_frame started_at results_dir (prover, _df) =
+  let csv_file = Fmt.str "%a-%s.csv" Tool.pp_prover prover started_at in
+  let _csv_path = Fpath.(results_dir / csv_file) in
+  (* Owl_dataframe.to_csv ~sep:',' df (Fpath.to_string csv_path) *)
+  assert false
+
+let main ~hook:_ ~timeout ~provers ~dirs =
+  let open Result in
+  let start_time = Unix.gettimeofday () in
+  let now = Unix.(localtime start_time) in
+  let _started_at = ExtUnix.Specific.strftime "%Y%m%dT%H%M%S" now in
+  assert (List.for_all Tool.is_available provers);
+  let files = List.concat_map files_to_run dirs in
+  let provers_str = List.map Tool.prover_to_string provers in
+  let w_prover = List.fold_left max 0 (List.map String.length provers_str) in
+  let num_files = List.length files in
+  let num_provers = List.length provers in
+  let run_provers ?timeout provers run_id benchmark =
+    List.map
+      (fun prover ->
+        let start = Unix.gettimeofday () in
+        let status, stdout, stderr, rusage =
+          Tool.fork_and_run ?timeout prover [ Fpath.to_string benchmark ]
+        in
+        let rtime = Unix.gettimeofday () -. start in
+        let prover = Fmt.str "%a" Tool.pp_prover prover in
+        Fmt.pr
+          "@[<v 2>%-*s: [%05d/%05d]@;\
+           File: %a@;\
+           Exited: %a@;\
+           Result: %s@;\
+           Time  : %0.03f@]@."
+          w_prover prover run_id num_files Fpath.pp benchmark
+          Util.pp_exit_status status (String.trim stdout) rtime;
+        (status, benchmark, stdout, stderr, rtime, rusage) )
+      provers
+  in
+  (* For every benchmark we run the selected provers *)
+  let results =
+    let run_id = ref 0 in
+    let init = List.init num_provers (fun _i -> []) in
+    List.fold_left
+      (fun acc file ->
+        incr run_id;
+        let res = run_provers ?timeout provers !run_id file in
+        List.map2 (fun res acc -> res :: acc) res acc )
+      init files
+  in
+  let results = List.map2 (fun p results -> (p, results)) provers results in
+  let summary =
+    List.map
+      (fun (prover, results) ->
+        ( prover
+        , List.fold_left
+            (fun acc (status, _, _, _, _, _) ->
+              match status with Unix.WEXITED 0 -> succ acc | _ -> acc )
+            0 results ) )
+      results
+  in
+  let time_elapsed = Unix.gettimeofday () -. start_time in
+  List.iter
+    (fun (prover, passed) ->
+      let percent = (float passed /. float num_files) *. 100. in
+      Fmt.pr "@[<v 2>%-*s:@;Passed: %05d/%05d (%03.2f%%)@." w_prover
+        (Tool.prover_to_string prover)
+        passed num_files percent )
+    summary;
+  Fmt.pr "Time elasped: %.2f@." time_elapsed;
+  (* let data_frames = make_data_frames results in *)
+  (* let summary = summarize results in *)
+  (* let msg = *)
+  (*   Fmt.str "@[Single-Query Results:@;%a@]@." Owl_pretty.pp_dataframe summary *)
+  (* in *)
+  (* let results_dir = Fmt.kstr Fpath.v "res-single-query-%s" started_at in *)
+  (* let* _ = Bos.OS.Dir.create ~path:true results_dir in *)
+  (* List.iter (write_data_frame started_at results_dir) data_frames; *)
+  (* Option.iter (Notify.notify_done msg) hook; *)
+  (* Ok (Fmt.pr "%s" msg) *)
+  Ok ()

bench/runner/cmd_setup.ml

@@ -0,0 +1,65 @@
+let debug = true
+
+let debug k = if debug then k Fmt.epr
+
+let init ~datasets_dir =
+  let open Result in
+  let* dir_exists = Bos.OS.Dir.create ~path:true datasets_dir in
+  if not dir_exists then debug (fun epr -> epr "Datasets dir already exists@.");
+  Ok ()
+
+type conf = { datasets : Dataset.t list }
+
+let parse_conf fpath =
+  In_channel.with_open_text (Fpath.to_string fpath) @@ fun ic ->
+  let datasets = Sexplib.Sexp.input_sexps ic |> List.map Dataset.of_sexp in
+  { datasets }
+
+let file_exists ?hash fpath =
+  let open Result in
+  let* file_exists = Bos.OS.File.exists fpath in
+  if not file_exists then Ok false
+  else begin
+    match hash with
+    | None -> Ok true
+    | Some hash ->
+      let md5sum = Digest.MD5.(to_hex (file (Fpath.to_string fpath))) in
+      if Digest.MD5.equal hash md5sum then Ok true
+      else
+        Error
+          (`Msg
+             (Fmt.str "%a: expected hash %s but got %s" Fpath.pp fpath hash
+                md5sum ) )
+  end
+
+let curl url out_file = Bos.Cmd.(v "curl" % url % "--output" % p out_file)
+
+let tar_extract archive output_dir =
+  Bos.Cmd.(v "tar" % "-xf" % p archive % "-C" % p output_dir)
+
+let setup ~datasets_dir { datasets } =
+  let open Result in
+  list_iter
+    (fun { Dataset.name; url; md5sum } ->
+      let this_dataset_dir = Fpath.(datasets_dir / name) in
+      let* _ = Bos.OS.Dir.create this_dataset_dir in
+      debug (fun epr -> epr "Downloading %s from %s@." name url);
+      let out_file = Fpath.(this_dataset_dir // base (v url)) in
+      let* file_exists = file_exists ~hash:md5sum out_file in
+      if file_exists then begin
+        debug (fun epr -> epr "Skipping: correct file exists@.");
+        Ok ()
+      end
+      else begin
+        debug (fun epr -> epr "Saving to %a@." Fpath.pp out_file);
+        let* () = Bos.OS.Cmd.run (curl url out_file) in
+        Bos.OS.Cmd.run (tar_extract out_file this_dataset_dir)
+      end )
+    datasets
+
+let main ~datasets_dir ~file =
+  let open Result in
+  debug (fun epr -> epr "Using config: '%a'@." Fpath.pp file);
+  let* () = init ~datasets_dir in
+  let conf = parse_conf file in
+  setup ~datasets_dir conf

bench/runner/dataset.ml

@@ -0,0 +1,29 @@
+type t =
+  { name : string
+  ; url : string
+  ; md5sum : string
+  }
+
+let pp fmt { name; url; md5sum } =
+  Fmt.pf fmt "@[<hov 1>{@ name@ =@ %a;@ url@ =@ %a;@ md5sum@ =@ %a@ }@]"
+    Fmt.string name Fmt.string url Fmt.string md5sum
+
+let of_sexp sexp =
+  match sexp with
+  | Sexplib.Sexp.List
+      [ Atom "dataset"
+      ; List [ Atom "name"; Atom name ]
+      ; List [ Atom "url"; Atom url ]
+      ; List [ Atom "md5sum"; Atom md5sum ]
+      ] ->
+    { name; url; md5sum }
+  | _ -> Fmt.failwith "Unable to parse sexp: %a" Sexplib.Sexp.pp_hum sexp
+
+let to_sexp { name; url; md5sum } =
+  Sexplib.Sexp.(
+    List
+      [ Atom "dataset"
+      ; List [ Atom "name"; Atom name ]
+      ; List [ Atom "url"; Atom url ]
+      ; List [ Atom "md5sum"; Atom md5sum ]
+      ] )

bench/runner/dune

@@ -1,17 +1,16 @@
 (executable
- (enabled_if false)
- (name runner)
+ (name main)
  (libraries
   bos
   cohttp
   cohttp-lwt-unix
   cmdliner
   extunix
   dune-glob
-  owl
   lwt
   yojson
   str
+  sexplib
   smtml
   smtml.prelude)
  (flags

bench/runner/main.ml

@@ -0,0 +1,62 @@
+open Cmdliner
+
+let file =
+  let fpath = Arg.conv (Fpath.of_string, Fpath.pp) in
+  Arg.(required & pos 0 (some fpath) None & info [] ~docv:"FILE")
+
+let fpath_dir =
+  let dir_parser = Arg.(conv_parser dir) in
+  Arg.conv
+    ( (fun str ->
+        match dir_parser str with
+        | Ok dir -> Ok (Fpath.v dir)
+        | Error _ as err -> err )
+    , Fpath.pp )
+
+let dir_arg ~default arg_name =
+  Arg.(value & opt fpath_dir default & info [ arg_name ])
+
+let dirs = Arg.(value & pos_all fpath_dir [] & info [] ~docv:"PATH")
+
+let provers =
+  let prover_conv = Arg.conv (Tool.prover_of_string, Tool.pp_prover) in
+  let default = Tool.(Smtml { name = Z3; st = false }) in
+  Arg.(value & opt_all prover_conv [ default ] & info [ "prover" ])
+
+let timeout = Arg.(value & opt (some int) None & info [ "timeout" ])
+
+let hook = Arg.(value & opt (some string) None & info [ "webhook" ])
+
+let _from_file = Arg.(value & opt (some file) None & info [ "from-file" ])
+
+let exec =
+  let open Term.Syntax in
+  let info = Cmd.info "exec" in
+  let cmd =
+    let+ hook
+    and+ timeout
+    and+ provers
+    and+ dirs in
+    Cmd_exec.main ~hook ~timeout ~provers ~dirs
+  in
+  Cmd.v info cmd
+
+let setup =
+  let open Term.Syntax in
+  let info = Cmd.info "setup" in
+  let cmd =
+    let+ file
+    and+ datasets_dir = dir_arg ~default:Fpath.(v "_datasets") "datasets-dir" in
+    Cmd_setup.main ~datasets_dir ~file
+  in
+  Cmd.v info cmd
+
+let cli =
+  let info = Cmd.info "benchme" in
+  Cmd.group info [ exec; setup ]
+
+let () =
+  match Cmdliner.Cmd.eval_value' cli with
+  | `Exit code -> exit code
+  | `Ok (Error (`Msg err)) -> Fmt.failwith "%s" err
+  | `Ok (Ok ()) -> exit 0