Remove runner's core_unix dependency

bench/runner/dune

@@ -4,8 +4,8 @@
   bos
   cohttp
   cohttp-lwt-unix
-  core_unix
   cmdliner
+  extunix
   dune-glob
   owl
   lwt

bench/runner/multi_query.ml

@@ -1,8 +1,3 @@
-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 ->
@@ -66,8 +61,8 @@ let write_data_frame started_at results_dir (prover, df) =
 
 let main _hook provers from_file 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
+  let now = Unix.(localtime @@ gettimeofday ()) in
+  let started_at = ExtUnix.Specific.strftime "%Y%m%dT%H%M%S" now in
   assert (List.for_all Tool.is_available provers);
   List.iter
     (fun (p : Tool.prover) -> match p with Z3 -> () | Smtml p -> p.st <- true)
@@ -80,7 +75,7 @@ let main _hook provers from_file dirs =
           Tool.fork_and_run ?from_file p dirs
         in
         Fmt.pr "@[<v 2>Run %a@;Exited: %a@;Stdout:@; %a@;Stderr:@; %a@]@."
-          Tool.pp_prover p pp_exit_status status Fmt.string
+          Tool.pp_prover p Util.pp_exit_status status Fmt.string
           (String.escaped stdout) Fmt.string (String.escaped stderr);
         (p, result) )
       provers

bench/runner/single_query.ml

@@ -7,11 +7,6 @@ let files_to_run d =
   | 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 ->
@@ -92,9 +87,9 @@ let make_data_frames results =
             , 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 ) )
+            , rusage.ExtUnix.Specific.ru_utime :: utime_acc
+            , rusage.ExtUnix.Specific.ru_stime :: stime_acc
+            , rusage.ExtUnix.Specific.ru_maxrss :: maxrss_acc ) )
           ([], [], [], [], [], [], [], [], [])
           prover_results
       in
@@ -133,23 +128,23 @@ let write_data_frame started_at results_dir (prover, df) =
 
 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
+  let now = Unix.(localtime @@ gettimeofday ()) 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 run_provers ?timeout provers benchmark =
     List.map
       (fun prover ->
-        let start = Core_unix.gettimeofday () in
+        let start = 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 rtime = Unix.gettimeofday () -. start in
         let prover = Fmt.str "%a" Tool.pp_prover prover in
         Fmt.pr "@[<v 2>%-*s: %a@;Exited: %a@;Result: %s@;Time  : %0.03f@]@."
-          w_prover prover Fpath.pp benchmark pp_exit_status status
+          w_prover prover Fpath.pp benchmark Util.pp_exit_status status
           (String.trim stdout) rtime;
         (status, benchmark, stdout, stderr, rtime, rusage) )
       provers

bench/runner/tool.ml

@@ -1,5 +1,3 @@
-module Unix = Core_unix
-
 type prover_name =
   | Z3
   | Bitwuzla
@@ -45,7 +43,7 @@ let is_available =
 
 let cmd ?from_file prover files =
   match prover with
-  | Z3 -> ("z3", "z3" :: files)
+  | Z3 -> ("z3", Array.of_list @@ ("z3" :: files))
   | Smtml { name; st } ->
     ( "smtml"
     , let args =
@@ -56,37 +54,41 @@ let cmd ?from_file prover files =
         | None -> files
         | Some file -> "--from-file" :: [ file ] )
       in
-      "smtml" :: "run" :: (if st then "--print-statistics" :: args else args) )
+      Array.of_list
+      @@ "smtml" :: "run"
+         :: (if st then "--print-statistics" :: args else args) )
 
 let dup2 ~src ~dst =
-  Unix.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 time_limit = Some (Int64.of_int time_limit) in
+  ExtUnix.Specific.setrlimit RLIMIT_CPU ~soft:time_limit ~hard: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 ?from_file 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 stdout_read, stdout_write = Unix.pipe () in
+  let stderr_read, stderr_write = Unix.pipe () in
   let prog, argv = cmd ?from_file 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)
+  let pid = Unix.fork () in
+  if pid = 0 then begin
+    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;
+    Unix.execv prog argv
+  end
+  else begin
+    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 waited_pid, status, usage = ExtUnix.Specific.wait4 [] pid in
+    assert (pid = waited_pid);
+    (status, stdout, stderr, usage)
+  end

bench/runner/util.ml

@@ -0,0 +1,4 @@
+let pp_exit_status fmt = function
+  | Unix.WEXITED n -> Fmt.pf fmt "Exited %d" n
+  | WSIGNALED n -> Fmt.pf fmt "Signaled %d" n
+  | WSTOPPED n -> Fmt.pf fmt "Stopped %d" n

dune-project

@@ -103,7 +103,7 @@
    :with-dev-setup)
   (cohttp-lwt-unix
    :with-dev-setup)
-  (core_unix
+  (extunix
    :with-dev-setup)
   (dune-glob
    :with-dev-setup)

smtml.opam

@@ -42,7 +42,7 @@ depends: [
   "benchpress" {with-dev-setup & = "dev"}
   "cohttp" {with-dev-setup}
   "cohttp-lwt-unix" {with-dev-setup}
-  "core_unix" {with-dev-setup}
+  "extunix" {with-dev-setup}
   "dune-glob" {with-dev-setup}
   "lwt" {with-dev-setup}
   "mdx" {with-test}
@@ -76,4 +76,5 @@ pin-depends: [
   ["alt-ergo-lib.2.6.0" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"]
   ["cvc5.dev" "git+https://github.com/formalsec/ocaml-cvc5.git#b7aade52d49a19d646036d7e6aac09039c3e95cf"]
   ["benchpress.dev" "git+https://github.com/sneeuwballen/benchpress.git#7f44cdd9f0511afcce2c9ad3c04cc9b72919bcff"]
+  ["extunix.0.4.3" "git+https://github.com/filipeom/extunix.git#ff54e8cc7ec9cdc7171861d74d85f326dbcec62e"]
 ]

smtml.opam.template

@@ -5,4 +5,5 @@ pin-depends: [
   ["alt-ergo-lib.2.6.0" "git+https://github.com/OCamlPro/alt-ergo.git#7ee96296a5de9588a4d585b3b8abec35f4755425"]
   ["cvc5.dev" "git+https://github.com/formalsec/ocaml-cvc5.git#b7aade52d49a19d646036d7e6aac09039c3e95cf"]
   ["benchpress.dev" "git+https://github.com/sneeuwballen/benchpress.git#7f44cdd9f0511afcce2c9ad3c04cc9b72919bcff"]
+  ["extunix.0.4.3" "git+https://github.com/filipeom/extunix.git#ff54e8cc7ec9cdc7171861d74d85f326dbcec62e"]
 ]