From f7fb21020266b38ee8065c86441e6eaa1aa0e3ec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 3 Apr 2024 15:37:42 +0200 Subject: [PATCH 1/2] Add support for comparing results with a specific status This patch gives the option to compare only sat/unsat results in the compare2 view (the one that allows to select provers from different runs). --- src/core/Test_compare.ml | 43 +++++++++++++------- src/core/Test_compare.mli | 6 ++- src/server/benchpress_server.ml | 70 +++++++++++++++++++++++++++++---- 3 files changed, 96 insertions(+), 23 deletions(-) diff --git a/src/core/Test_compare.ml b/src/core/Test_compare.ml index 8def0d1..a14babf 100644 --- a/src/core/Test_compare.ml +++ b/src/core/Test_compare.ml @@ -2,6 +2,7 @@ open Common type filename = string type prover = filename * Prover.name +type status = [ `Sat | `Unsat ] let pb_v_record = Test.pb_v_record let pb_int_color = Test.pb_int_color @@ -35,6 +36,16 @@ let cmp2sql = function let pp_cmp = Fmt.of_to_string cmp2sql +let status_to_string = function + | `Sat -> {| + (r1.res = 'sat' or r2.res = 'sat') + |} + | `Unsat -> {| + (r1.res = 'unsat' or r2.res = 'unsat') + |} + +let pp_status = Fmt.of_to_string status_to_string + let pp_opt ?(none = Fmt.const_string "") pp ppf = function | None -> none ppf () | Some v -> pp ppf v @@ -43,12 +54,13 @@ let pp_prefix prefix pp ppf v = Fmt.fprintf ppf "%s" prefix; pp ppf v -let unsafe_sql ?order ?limit ?offset ?filter select = +let unsafe_sql ?order ?limit ?offset ?filter ?status select = let pp_filter ppf filter = match filter with | None -> () | Some filter -> Format.fprintf ppf "and (%a)" pp_cmp filter in + let pp_status = pp_opt (pp_prefix " and " pp_status) in let pp_select = Fmt.list ~sep:(fun ppf () -> Fmt.fprintf ppf ",@,") @@ -58,9 +70,9 @@ let unsafe_sql ?order ?limit ?offset ?filter select = {| select %a from db1.prover_res r1 inner join db2.prover_res r2 on r2.file = r1.file - where r1.prover = ? and r2.prover = ? %a %a %a %a + where r1.prover = ? and r2.prover = ? %a %a %a %a %a |} - pp_select select pp_filter filter + pp_select select pp_filter filter pp_status status (pp_opt (pp_prefix " order by " Fmt.string)) order (pp_opt (pp_prefix " limit " Fmt.int)) @@ -90,7 +102,7 @@ module Short = struct "regressed", pb_int_color Style.(fg_color Cyan) self.regressed; ] - let make1 db p1 p2 : t = + let make1 ?status db p1 p2 : t = (* Note: first ? is p1, second ? is p2 *) let get_n q = Db.exec db q p1 p2 @@ -115,20 +127,22 @@ module Short = struct and not exists (select file from db2.prover_res where db2.prover_res.prover=? and file = r1.file); |} - and same = get_n (unsafe_sql ~filter:`Same [ "count(r1.file)" ]) - and mismatch = get_n (unsafe_sql ~filter:`Mismatch [ "count(r1.file)" ]) - and improved = get_n (unsafe_sql ~filter:`Improved [ "count(r1.file)" ]) + and same = get_n (unsafe_sql ?status ~filter:`Same [ "count(r1.file)" ]) + and mismatch = + get_n (unsafe_sql ?status ~filter:`Mismatch [ "count(r1.file)" ]) + and improved = + get_n (unsafe_sql ?status ~filter:`Improved [ "count(r1.file)" ]) and regressed = - get_n (unsafe_sql ~filter:`Regressed [ "count(r1.file)" ]) + get_n (unsafe_sql ?status ~filter:`Regressed [ "count(r1.file)" ]) in { appeared; disappeared; same; mismatch; improved; regressed } - let make_provers (f1, p1) (f2, p2) : t = + let make_provers ?status (f1, p1) (f2, p2) : t = Error.guard (Error.wrapf "short comparison of '%s/%s' and '%s/%s'" f1 p1 f2 p2) - @@ fun () -> make1 (make_db f1 f2) p1 p2 + @@ fun () -> make1 ?status (make_db f1 f2) p1 p2 - let make f1 f2 : (_ * t) list = + let make ?status f1 f2 : (_ * t) list = Error.guard (Error.wrapf "short comparison of '%s' and '%s'" f1 f2) @@ fun () -> let db = Sqlite3.db_open ":memory:" in @@ -145,19 +159,20 @@ module Short = struct |> Misc.unwrap_db (fun () -> "listing all provers") in Logs.debug (fun k -> k "provers: [%s]" (String.concat ";" provers)); - CCList.map (fun prover -> prover, make1 db prover prover) provers + CCList.map (fun prover -> prover, make1 ?status db prover prover) provers end module Full = struct type filter = [ `Improved | `Regressed | `Mismatch | `Same ] type entry = string * Res.t * float * Res.t * float - let make_filtered ?(page = 0) ?(page_size = 500) ?filter (f1, p1) (f2, p2) = + let make_filtered ?(page = 0) ?(page_size = 500) ?filter ?status (f1, p1) + (f2, p2) = let tags = [] (* TODO? *) in let offset = page * page_size in let limit = page_size + 1 in Db.exec (make_db f1 f2) - (unsafe_sql ~order:"r1.file desc" ~limit ~offset ?filter + (unsafe_sql ~order:"r1.file desc" ~limit ~offset ?filter ?status [ "r1.file"; "r1.res"; "r2.res"; "r1.rtime"; "r2.rtime" ]) p1 p2 ~ty: diff --git a/src/core/Test_compare.mli b/src/core/Test_compare.mli index 9d028b1..885d64e 100644 --- a/src/core/Test_compare.mli +++ b/src/core/Test_compare.mli @@ -2,6 +2,7 @@ type filename = string type prover = filename * Prover.name +type status = [ `Sat | `Unsat ] module Short : sig type t = { @@ -14,9 +15,9 @@ module Short : sig } val to_printbox : t -> PrintBox.t - val make : filename -> filename -> (Prover.name * t) list + val make : ?status:status -> filename -> filename -> (Prover.name * t) list - val make_provers : prover -> prover -> t + val make_provers : ?status:status -> prover -> prover -> t (** Make a single comparison between two provers in (possibly) different files *) end @@ -28,6 +29,7 @@ module Full : sig ?page:int -> ?page_size:int -> ?filter:filter -> + ?status:status -> prover -> prover -> entry list diff --git a/src/server/benchpress_server.ml b/src/server/benchpress_server.ml index 6e7a815..990ce54 100644 --- a/src/server/benchpress_server.ml +++ b/src/server/benchpress_server.ml @@ -1154,6 +1154,14 @@ let handle_compare2 self : unit = None) @@ H.Request.query req in + let status = + match + String.lowercase_ascii @@ List.assoc "status" (H.Request.query req) + with + | "sat" -> Some `Sat + | "unsat" -> Some `Unsat + | _ | (exception Not_found) -> None + in (* H.Request.query reverses the query order, so we have to reverse it again *) let provers = List.rev provers in let prover1, prover2 = @@ -1183,6 +1191,30 @@ let handle_compare2 self : unit = in let options1 = CCList.mapi (mk_entry ?selected:prover1) entries in let options2 = CCList.mapi (mk_entry ?selected:prover2) entries in + let status_opt_to_string = function + | Some `Sat -> "sat" + | Some `Unsat -> "unsat" + | None -> "" + in + let status_option ?current status = + let open Html in + let attrs = + A.value (status_opt_to_string status) + :: + (if current = Some status then + [ A.selected "selected" ] + else + []) + in + option attrs [ txt (status_opt_to_string status) ] + in + let ostatus = + [ + status_option None; + status_option ~current:status (Some `Unsat); + status_option ~current:status (Some `Sat); + ] + in let prover_info = let file_link fname text = PrintBox.link ~uri:(uri_get_file fname) (PrintBox.text text) @@ -1203,7 +1235,7 @@ let handle_compare2 self : unit = | `Mismatch -> "Mismatch" | `Same -> "Same" in - let short = Test_compare.Short.make_provers (ff1, p1) (ff2, p2) in + let short = Test_compare.Short.make_provers ?status (ff1, p1) (ff2, p2) in let make filter = let total = get short filter in let page_size = min total 500 in @@ -1220,8 +1252,8 @@ let handle_compare2 self : unit = [ summary [] [ txtf "%s (%s)" (filter_to_string filter) limit_info ]; - Test_compare.Full.make_filtered ~page_size ~filter (ff1, p1) - (ff2, p2) + Test_compare.Full.make_filtered ?status ~page_size ~filter + (ff1, p1) (ff2, p2) |> Test_compare.Full.to_printbox ~file_link |> Html.pb_html; ]); @@ -1242,17 +1274,41 @@ let handle_compare2 self : unit = |> String.concat "," |> gnuplot_img; ] in + let plot_html = + if Option.is_none status then + plot_html + else + Html.( + strong [] + [ txt "Warning: this plot includes BOTH sat and unsat results." ]) + :: plot_html + in let html = let open Html in mk_page ~title:"compare2" ([ mk_navigation [ "/compare2/", "compare", true ]; h3 [] [ txt "compare" ]; - form [] + form + [ A.class_ "container" ] [ - select [ A.name "prover[]" ] options1; - select [ A.name "prover[]" ] options2; - mk_button ~cls:"btn-primary btn-sm" [] [ txt "Compare" ]; + div + [ A.class_ "row" ] + [ + div + [ A.class_ "col-6" ] + [ + select [ A.name "prover[]" ] options1; + select [ A.name "prover[]" ] options2; + mk_button ~cls:"btn-primary btn-sm" [] [ txt "Compare" ]; + ]; + div + [ A.class_ "col-3" ] + [ + Html.label [] [ Html.txt "Limit to:" ]; + select [ A.name "status" ] ostatus; + ]; + ]; ]; ] @ prover_info From c8ff073890ededf95a936ca1e66fa530ebf9cca1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 3 Apr 2024 16:08:15 +0200 Subject: [PATCH 2/2] Review comments --- src/core/Test_compare.ml | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/src/core/Test_compare.ml b/src/core/Test_compare.ml index a14babf..4ecc420 100644 --- a/src/core/Test_compare.ml +++ b/src/core/Test_compare.ml @@ -36,15 +36,11 @@ let cmp2sql = function let pp_cmp = Fmt.of_to_string cmp2sql -let status_to_string = function - | `Sat -> {| - (r1.res = 'sat' or r2.res = 'sat') - |} - | `Unsat -> {| - (r1.res = 'unsat' or r2.res = 'unsat') - |} +let status_to_sql = function + | `Sat -> {| (r1.res = 'sat' or r2.res = 'sat') |} + | `Unsat -> {| (r1.res = 'unsat' or r2.res = 'unsat') |} -let pp_status = Fmt.of_to_string status_to_string +let pp_status_sql = Fmt.of_to_string status_to_sql let pp_opt ?(none = Fmt.const_string "") pp ppf = function | None -> none ppf () @@ -60,7 +56,7 @@ let unsafe_sql ?order ?limit ?offset ?filter ?status select = | None -> () | Some filter -> Format.fprintf ppf "and (%a)" pp_cmp filter in - let pp_status = pp_opt (pp_prefix " and " pp_status) in + let pp_status = pp_opt (pp_prefix " and " pp_status_sql) in let pp_select = Fmt.list ~sep:(fun ppf () -> Fmt.fprintf ppf ",@,")