diff --git a/.gitignore b/.gitignore index f4e35a27..1f3c59bb 100644 --- a/.gitignore +++ b/.gitignore @@ -31,3 +31,5 @@ nix/profiles/ # dkml desktop CI /msys64 /.ci + +res-* diff --git a/bench/runner/benchpress.ml b/bench/runner/benchpress.ml deleted file mode 100644 index 689d7e7e..00000000 --- a/bench/runner/benchpress.ml +++ /dev/null @@ -1,60 +0,0 @@ -open Bos - -let ( let* ) v f = Result.bind v f - -let cfg = Fpath.v "./benchpress.sexp" - -let task task = Cmd.(v "benchpress" % "run" % "-c" % p cfg % "--task" % task) - -let list_files = Cmd.(v "benchpress" % "list-files") - -let show nc file = - Cmd.(v "benchpress" % "show" % "--detail" % file %% on nc (v "--no-color")) - -let string_of_run_out run_out = - let* output, (_, status) = OS.Cmd.out_string run_out in - match (status, output) with - | `Exited 0, output -> Ok output - | _ -> Error (`Msg "Cmd exited with non-zero code") - -let stdout_lines cmd = - let run_out = OS.Cmd.run_out cmd in - let* lines, (_, status) = OS.Cmd.out_lines run_out in - match (status, lines) with - | `Exited 0, lines -> Ok lines - | _ -> Error (`Msg "Cmd exited with non-zero code") - -let remove_ansi_escape_codes s = - let re = Str.regexp "\x1b\\[[0-9;]*m" in - Str.global_replace re "" s - -let notify_done url results = - let url = Webhook.url_of_string url in - let head = Git.get_head () in - let title = Fmt.str "Test results (commit hash=%s) :octopus:" head in - let body = Fmt.str "```%s```" (remove_ansi_escape_codes results) in - let body = Webhook.default_slack_mrkdwn title body in - Lwt_main.run @@ Webhook.post_and_forget url body - -let latest_results' nc = - let* lines = stdout_lines list_files in - match lines with - | [] -> Error (`Msg "Benchpress wasn't run yet") - | hd :: _ -> ( - match String.split_on_char ' ' hd with - | [ file; _ ] -> Ok (OS.Cmd.run_out @@ show nc file) - | _ -> assert false ) - -let latest_results nc = - let* run_out = latest_results' nc in - let _ = OS.Cmd.out_stdout run_out in - Ok () - -let run hook t = - let* () = OS.Cmd.run @@ task t in - match hook with - | None -> Ok () - | Some web_hook -> - let* run_out = latest_results' true in - let* output = string_of_run_out run_out in - Ok (notify_done web_hook output) diff --git a/bench/runner/dune b/bench/runner/dune index eca2c30f..24e17ee2 100644 --- a/bench/runner/dune +++ b/bench/runner/dune @@ -1,3 +1,17 @@ (executable (name runner) - (libraries bos cohttp cohttp-lwt-unix cmdliner lwt yojson str)) + (libraries + bos + cohttp + cohttp-lwt-unix + core_unix + cmdliner + dune-glob + owl + lwt + yojson + str + smtml + smtml.prelude) + (flags + (:standard -open Smtml_prelude))) diff --git a/bench/runner/git.ml b/bench/runner/git.ml index eab01a86..086da280 100644 --- a/bench/runner/git.ml +++ b/bench/runner/git.ml @@ -1,14 +1,14 @@ (** Best effort to try and get commit hash of HEAD *) let get_head ?(length = 6) () = let open Bos in - let short = Format.asprintf "--short=%d" length in + let short = Fmt.str "--short=%d" length in let cmd = Cmd.(v "git" % "rev-parse" % short % "HEAD") in let output = OS.Cmd.run_out ~err:OS.Cmd.err_run_out cmd in match OS.Cmd.out_string ~trim:true output with | Ok (stdout, (_, `Exited 0)) -> stdout | Error (`Msg err) -> - Format.eprintf "ERROR: %s@." err; + Fmt.epr "ERROR: %s@." err; "unknown" | Ok (stdout, (_, (`Exited _ | `Signaled _))) -> - Format.eprintf "%s@\nWARN: Unable to fetch git HEAD@." stdout; + Fmt.epr "%s@\nWARN: Unable to fetch git HEAD@." stdout; "unknown" diff --git a/bench/runner/multi_query.ml b/bench/runner/multi_query.ml new file mode 100644 index 00000000..accf5c8b --- /dev/null +++ b/bench/runner/multi_query.ml @@ -0,0 +1,93 @@ +let pp_exit_status fmt = function + | Ok () -> Fmt.pf fmt "Exited 0" + | Error (`Exit_non_zero n) -> Fmt.pf fmt "Exited %d" n + | Error (`Signal s) -> Fmt.pf fmt "Signal %s" (Core.Signal.to_string s) + +let parse_stdout = + let re = Dune_re.(compile @@ Perl.re {|Run\s(.*?)\sin\s([0-9.]+)|}) in + fun stdout -> + let matches = Dune_re.all re stdout in + List.map + (fun group -> + let benchmark = Dune_re.Group.get group 1 in + let rtime = Dune_re.Group.get group 2 in + (benchmark, Float.of_string rtime) ) + matches + +let parse_results (prover, (_status, stdout, _stderr, _rusage)) = + let results = parse_stdout stdout in + let results = + List.map + (fun (benchmark, rtime) -> + (Tool.prover_to_string prover, benchmark, rtime) ) + results + in + (prover, results) + +let summary results = + List.iter + (fun (prover, results) -> + let total, rtime = + List.fold_left + (fun (total, time) (_, _, rtime) -> (succ total, time +. rtime)) + (0, 0.) results + in + Fmt.pr "Ran %d benchmarks on %a in %0.03f" total Tool.pp_prover prover + rtime ) + results + +let make_data_frames results = + List.map + (fun (prover, prover_results) -> + let provers, benchmark, rtime = + List.fold_left + (fun (prover_acc, bench_acc, rtime_acc) (prover, benchmark, rtime) -> + (prover :: prover_acc, benchmark :: bench_acc, rtime :: rtime_acc) + ) + ([], [], []) prover_results + in + let df = + Owl_dataframe.make + [| "prover"; "benchmark"; "rtime" |] + ~data: + [| Owl_dataframe.pack_string_series @@ Array.of_list provers + ; Owl_dataframe.pack_string_series @@ Array.of_list benchmark + ; Owl_dataframe.pack_float_series @@ Array.of_list rtime + |] + 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) + +let main _hook provers dirs = + let open Result in + let now = Core_unix.(localtime @@ gettimeofday ()) in + let started_at = Core_unix.strftime now "%Y%m%dT%H%M%S" in + assert (List.for_all Tool.is_available provers); + List.iter + (fun (p : Tool.prover) -> match p with Z3 -> () | Smtml p -> p.st <- true) + provers; + let dirs = List.map Fpath.to_string dirs in + let results = + List.map + (fun p -> + let ((status, stdout, _stderr, _) as result) = + Tool.fork_and_run p dirs + in + Fmt.pr "@[Run %a@;Exited: %a@;Stdout:@; %a@]@." Tool.pp_prover p + pp_exit_status status Fmt.string (String.escaped stdout); + (p, result) ) + provers + in + let results = List.map parse_results results in + summary results; + let data_frames = make_data_frames results in + let results_dir = Fmt.kstr Fpath.v "res-multi-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 () diff --git a/bench/runner/notify.ml b/bench/runner/notify.ml new file mode 100644 index 00000000..c74d66aa --- /dev/null +++ b/bench/runner/notify.ml @@ -0,0 +1,7 @@ +let notify_done results url = + let url = Webhook.url_of_string url in + let head = Git.get_head () in + let title = Fmt.str "Test results (commit hash=%s) :octopus:" head in + let body = Fmt.str "```%s```" results in + let body = Webhook.default_slack_mrkdwn title body in + Lwt_main.run @@ Webhook.post_and_forget url body diff --git a/bench/runner/runner.ml b/bench/runner/runner.ml index 42595a62..66d380d8 100644 --- a/bench/runner/runner.ml +++ b/bench/runner/runner.ml @@ -1,21 +1,32 @@ +let prover_conv = Cmdliner.Arg.conv (Tool.prover_of_string, Tool.pp_prover) + +let fpath_dir = + let dir_parser, _ = Cmdliner.Arg.dir in + ( (fun str -> + match dir_parser str with + | `Ok dir -> `Ok (Fpath.v dir) + | `Error _ as err -> err ) + , Fpath.pp ) + let cli = let open Cmdliner in - let run = - let task = Arg.(required & opt (some string) None & info [ "task" ]) in - let hook = Arg.(value & opt (some string) None & info [ "web-hook" ]) in - let info = Cmd.info "run" in - Cmd.v info Term.(const Benchpress.run $ hook $ task) + let hook = Arg.(value & opt (some string) None & info [ "web-hook" ]) in + let dirs = Arg.(value & pos_all fpath_dir [] & info [] ~docv:"PATH") in + let provers = Arg.(value & opt_all prover_conv [] & info [ "p"; "prover" ]) in + let timeout = Arg.(value & opt (some int) None & info [ "timeout" ]) in + let single_query = + let info = Cmd.info "single-query" in + Cmd.v info Term.(const Single_query.main $ hook $ provers $ timeout $ dirs) in - let latest_results = - let nc = Arg.(value & flag & info [ "nc" ]) in - let info = Cmd.info "latest-results" in - Cmd.v info Term.(const Benchpress.latest_results $ nc) + let multi_query = + let info = Cmd.info "multi-query" in + Cmd.v info Term.(const Multi_query.main $ hook $ provers $ dirs) in let info = Cmd.info "runner" in - Cmd.group info [ run; latest_results ] + Cmd.group info [ single_query; multi_query ] let () = match Cmdliner.Cmd.eval_value' cli with | `Exit code -> exit code - | `Ok (Error (`Msg err)) -> failwith err + | `Ok (Error (`Msg err)) -> Fmt.failwith "%s" err | `Ok (Ok ()) -> exit 0 diff --git a/bench/runner/single_query.ml b/bench/runner/single_query.ml new file mode 100644 index 00000000..47dc7e6f --- /dev/null +++ b/bench/runner/single_query.ml @@ -0,0 +1,175 @@ +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 pp_exit_status fmt = function + | Ok () -> Fmt.pf fmt "Exited 0" + | Error (`Exit_non_zero n) -> Fmt.pf fmt "Exited %d" n + | Error (`Signal s) -> Fmt.pf fmt "Signal %s" (Core.Signal.to_string s) + +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 = + 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 + |] + +(* 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.Core_unix.Resource_usage.utime :: utime_acc + , rusage.Core_unix.Resource_usage.stime :: stime_acc + , rusage.Core_unix.Resource_usage.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) + +let main hook provers timeout dirs = + let open Result in + let now = Core_unix.(localtime @@ gettimeofday ()) in + let started_at = Core_unix.strftime now "%Y%m%dT%H%M%S" 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 run_provers ?timeout provers benchmark = + List.map + (fun prover -> + let start = Core_unix.gettimeofday () in + let status, stdout, stderr, rusage = + Tool.fork_and_run ?timeout prover [ Fpath.to_string benchmark ] + in + let rtime = Core_unix.gettimeofday () -. start in + let prover = Fmt.str "%a" Tool.pp_prover prover in + Fmt.pr "@[%-*s: %a@;Exited: %a@;Result: %s@;Time : %0.03f@]@." + w_prover prover Fpath.pp benchmark 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 = + List.fold_left + (fun acc file -> + let res = run_provers ?timeout provers file in + List.map2 (fun res acc -> res :: acc) res acc ) + (List.map (fun _ -> []) provers) + files + in + let results = List.map2 (fun p results -> (p, results)) provers results in + 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) diff --git a/bench/runner/tool.ml b/bench/runner/tool.ml new file mode 100644 index 00000000..00a5db64 --- /dev/null +++ b/bench/runner/tool.ml @@ -0,0 +1,89 @@ +module Unix = Core_unix + +type prover_name = + | Z3 + | Bitwuzla + | Cvc5 + | Colibri2 + +type prover = + | Z3 + | Smtml of + { name : prover_name + ; mutable st : bool + } + +let prover_of_string str = + match String.lowercase_ascii str with + | "z3" -> Ok Z3 + | "smtml-bitwuzla" -> Ok (Smtml { name = Bitwuzla; st = false }) + | "smtml-cvc5" -> Ok (Smtml { name = Cvc5; st = false }) + | "smtml-colibri2" -> Ok (Smtml { name = Colibri2; st = false }) + | "smtml-z3" -> Ok (Smtml { name = Z3; st = false }) + | _ -> Error (`Msg (Fmt.str "%s: unknown prover" str)) + +let pp_prover_name fmt : prover_name -> unit = function + | Z3 -> Fmt.string fmt "z3" + | Bitwuzla -> Fmt.string fmt "bitwuzla" + | Cvc5 -> Fmt.string fmt "cvc5" + | Colibri2 -> Fmt.string fmt "colibri2" + +let pp_prover fmt = function + | Z3 -> Fmt.string fmt "z3" + | Smtml { name; _ } -> Fmt.pf fmt "smtml-%a" pp_prover_name name + +let prover_to_string = Fmt.str "%a" pp_prover + +let is_available = function + | Z3 -> Smtml.Solver_dispatcher.is_available Z3_solver + | Smtml { name = Bitwuzla; _ } -> + Smtml.Solver_dispatcher.is_available Bitwuzla_solver + | Smtml { name = Cvc5; _ } -> Smtml.Solver_dispatcher.is_available Cvc5_solver + | Smtml { name = Colibri2; _ } -> + Smtml.Solver_dispatcher.is_available Colibri2_solver + | Smtml { name = Z3; _ } -> Smtml.Solver_dispatcher.is_available Z3_solver + +let cmd prover files = + match prover with + | Z3 -> ("z3", "z3" :: files) + | Smtml { name; st } -> + ( "smtml" + , let args = + "--mode" :: "incremental" :: "--solver" + :: Fmt.str "%a" pp_prover_name name + :: files + in + "smtml" :: "run" :: (if st then "--print-statistics" :: args else args) ) + +let dup2 ~src ~dst = + Unix.dup2 ~src ~dst (); + Unix.close src + +let limit_cpu time_limit = + let time_limit = Int64.of_int time_limit in + Unix.RLimit.( + set cpu_seconds { cur = Limit time_limit; max = Limit time_limit } ) + +let with_ic fd f = + let ic = Unix.in_channel_of_descr fd in + Fun.protect ~finally:(fun () -> In_channel.close ic) (fun () -> f ic) + +let fork_and_run ?timeout prover file = + let stdout_read, stdout_write = Unix.pipe ~close_on_exec:false () in + let stderr_read, stderr_write = Unix.pipe ~close_on_exec:false () in + let prog, argv = cmd prover file in + let pid = + Unix.fork_exec ~prog ~argv () ~preexec_fn:(fun () -> + Unix.close stdout_read; + Unix.close stderr_read; + dup2 ~src:stdout_write ~dst:Unix.stdout; + dup2 ~src:stderr_write ~dst:Unix.stderr; + Option.iter limit_cpu timeout ) + in + Unix.close stdout_write; + Unix.close stderr_write; + let stdout = with_ic stdout_read In_channel.input_all in + let stderr = with_ic stderr_read In_channel.input_all in + let (wpid, status), rusage = Unix.wait_with_resource_usage (`Pid pid) in + assert (Core.Pid.equal pid wpid); + (status, stdout, stderr, rusage) diff --git a/dune-project b/dune-project index 3916af81..5fed26c5 100644 --- a/dune-project +++ b/dune-project @@ -73,15 +73,19 @@ (>= "2.5.0"))) (benchpress (and - :with-test + :with-dev-setup (= "dev"))) (cohttp - :with-test) + :with-dev-setup) (cohttp-lwt-unix - :with-test) + :with-dev-setup) (lwt - :with-test) + :with-dev-setup) (tls-lwt - :with-test) + :with-dev-setup) (mdx - :with-test))) + :with-test) + (owl + :with-dev-setup) + (core_unix + :with-dev-setup))) diff --git a/smtml.opam b/smtml.opam index 233ba643..cb7e1c8a 100644 --- a/smtml.opam +++ b/smtml.opam @@ -25,12 +25,14 @@ depends: [ "odoc" {with-doc} "sherlodoc" {with-doc} "bisect_ppx" {with-test & >= "2.5.0"} - "benchpress" {with-test & = "dev"} - "cohttp" {with-test} - "cohttp-lwt-unix" {with-test} - "lwt" {with-test} - "tls-lwt" {with-test} + "benchpress" {with-dev-setup & = "dev"} + "cohttp" {with-dev-setup} + "cohttp-lwt-unix" {with-dev-setup} + "lwt" {with-dev-setup} + "tls-lwt" {with-dev-setup} "mdx" {with-test} + "owl" {with-dev-setup} + "core_unix" {with-dev-setup} ] depopts: ["z3" "colibri2" "bitwuzla-cxx" "cvc5"] conflicts: [