Revise the "bench" entries of the test suite

Initially, the "bench" entries of the test suite used a "xtime" utility
developed in-house and not publically available.

This commit adds a version of "xtime" written in OCaml (tools/xtime.ml)
and updates the "bench" entries of the test/*/Makefile to use it.

5 files changed, 110 insertions, 12 deletions

diff --git a/test/c/Makefile b/test/c/Makefile
index 51a8f105..4b521bb5 100644
--- a/test/c/Makefile
+++ b/test/c/Makefile
@@ -7,8 +7,7 @@ CFLAGS=-O1 -Wall
 
 LIBS=$(LIBMATH)
 
-TIME=xtime -o /dev/null -mintime 2.0     # Xavier's hack
-#TIME=time >/dev/null                    # Otherwise
+TIME=ocaml unix.cma ../../tools/xtime.ml -o /dev/null -mintime 2.0 -minruns 4
 
 PROGS=fib integr qsort fft fftsp fftw sha1 sha3 aes almabench \
   lists binarytrees fannkuch knucleotide mandelbrot nbody \
@@ -48,12 +47,12 @@ test_gcc:
 
 bench_gcc:
 	@for i in $(PROGS); do \
-	   echo -n "$$i: "; $(TIME) ./$$i.gcc; \
+	   $(TIME) -name $$i -- ./$$i.gcc; \
          done
 
 bench:
 	@for i in $(PROGS); do \
-	   echo -n "$$i: "; $(TIME) ./$$i.compcert; \
+	   $(TIME) -name $$i -- ./$$i.compcert; \
          done
 
 clean:
diff --git a/test/compression/Makefile b/test/compression/Makefile
index 2e14e646..e8f3cf4d 100644
--- a/test/compression/Makefile
+++ b/test/compression/Makefile
@@ -3,7 +3,7 @@ include ../../Makefile.config
 CC=../../ccomp 
 CFLAGS=$(CCOMPOPTS) -U__GNUC__ -stdlib ../../runtime -dclight -dasm
 LIBS=
-TIME=xtime -o /dev/null -mintime 1.0
+TIME=ocaml unix.cma ../../tools/xtime.ml -mintime 2.0 -minruns 2
 
 EXE=arcode lzw lzss
 
@@ -48,8 +48,7 @@ test:
 bench:
 	@rm -f $(TESTCOMPR)
 	@for i in $(EXE); do \
-          echo -n "$$i: "; \
-          $(TIME) sh -c "./$$i -c -i $(TESTFILE) -o $(TESTCOMPR) && ./$$i -d -i $(TESTCOMPR) -o /dev/null"; \
+          $(TIME) -name $$i -- sh -c "./$$i -c -i $(TESTFILE) -o $(TESTCOMPR) && ./$$i -d -i $(TESTCOMPR) -o /dev/null"; \
          done
 	@rm -f $(TESTCOMPR)
 
diff --git a/test/raytracer/Makefile b/test/raytracer/Makefile
index 8f6541a1..24461bd1 100644
--- a/test/raytracer/Makefile
+++ b/test/raytracer/Makefile
@@ -3,7 +3,7 @@ include ../../Makefile.config
 CC=../../ccomp 
 CFLAGS=$(CCOMPOPTS) -stdlib ../../runtime -dparse -dclight -dasm -fstruct-return
 LIBS=$(LIBMATH)
-TIME=xtime
+TIME=ocaml unix.cma ../../tools/xtime.ml -mintime 2.0 -minruns 4
 
 OBJS=memory.o gmllexer.o gmlparser.o eval.o \
   arrays.o vector.o matrix.o object.o intersect.o surface.o light.o \
@@ -30,4 +30,4 @@ test:
         fi
 
 bench:
-	@echo -n "raytracer: "; $(TIME) sh -c './render < kal.gml'
+	@$(TIME) -name raytracer -- sh -c './render < kal.gml'
diff --git a/test/spass/Makefile b/test/spass/Makefile
index 0e89d6d1..d512ea95 100644
--- a/test/spass/Makefile
+++ b/test/spass/Makefile
@@ -24,11 +24,10 @@ clean:
 test:
 	$(SIMU) ./spass small_problem.dfg | grep 'Proof found'
 
-TIME=xtime -o /dev/null     # Xavier's hack
-#TIME=time >/dev/null       # Otherwise
+TIME=ocaml unix.cma ../../tools/xtime.ml -o /dev/null -mintime 5.0
 
 bench:
-	@echo -n "spass: "; $(TIME) ./spass problem.dfg
+	@$(TIME) -name spass -- ./spass problem.dfg
 
 depend:
 	gcc -MM $(SRCS) > .depend
diff --git a/tools/xtime.ml b/tools/xtime.ml
new file mode 100644
index 00000000..fbb25a49
--- /dev/null
+++ b/tools/xtime.ml
@@ -0,0 +1,101 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Timing the execution of a command, with more options than the
+   standard Unix "time" utility. *)
+
+open Printf
+
+let outfile = ref ""
+let errfile = ref ""
+let command_name = ref ""
+let num_runs = ref 1
+let min_runs = ref 0
+let min_time = ref 0.0
+let print_sys = ref false
+
+let error fmt =
+  eprintf "Error: "; kfprintf (fun _ -> exit 2) stderr fmt
+
+let open_file out dfl =
+  if out = ""
+  then dfl
+  else Unix.(openfile out [O_WRONLY; O_CREAT; O_TRUNC] 0o666)
+
+let close_file out fd =
+  if out <> "" then Unix.close fd
+  
+let run1 (cmd, args) =
+  let fd_out = open_file !outfile Unix.stdout in
+  let fd_err = open_file !errfile Unix.stderr in
+  let pid =
+    Unix.create_process cmd (Array.of_list (cmd :: args))
+                        Unix.stdin fd_out fd_err in
+  close_file !outfile fd_out;
+  close_file !errfile fd_err;
+  let (_, st) = Unix.waitpid [] pid in
+  match st with
+  | Unix.WEXITED 127 -> error "cannot execute '%s'\n" cmd
+  | Unix.WSIGNALED signo -> error "terminated by signal %d\n" signo
+  | _ -> ()
+
+let run (cmd, arg) =
+  let rec repeat n =
+    run1 (cmd, arg);
+    if (!min_time > 0.0 && Unix.((times()).tms_cutime) < !min_time)
+    || (!min_runs > 0 && n < !min_runs)
+    || n < !num_runs
+    then repeat (n + 1)
+    else n in
+  let n = repeat 1 in
+  let ts = Unix.times() in
+  let cmdname = if !command_name <> "" then !command_name else cmd in
+  if !print_sys then
+    Printf.printf "%.3f usr + %.3f sys %s\n"
+                  (ts.Unix.tms_cutime /. float n)
+                  (ts.Unix.tms_cstime /. float n)
+                  cmdname
+  else
+    Printf.printf "%.3f %s\n"
+                  (ts.Unix.tms_cutime /. float n)
+                  cmdname
+
+let _ =
+  let cmd_and_args = ref [] in
+  Arg.parse [
+    "-o", Arg.Set_string outfile,
+      " <file>  Redirect standard output of command to <file>";
+    "-e", Arg.Set_string outfile,
+      " <file>  Redirect standard error of command to <file>";
+    "-name", Arg.Set_string command_name,
+      " <name>  Name of command to report along with the time";
+    "-repeat", Arg.Int (fun n -> num_runs := n),
+      " <N>  Run the command N times";
+    "-mintime", Arg.Float (fun f -> min_time := f),
+      " <T>  Repeatedly run the command for a total duration of at least T seconds";
+    "-minruns", Arg.Int (fun n -> num_runs := n),
+      " <N>  Run the command at least N times (to be used in conjunction with -mintime)";
+    "-sys", Arg.Set print_sys,
+      "  Print system time (spent in the OS) in addition to user time (spent in the command)";
+    "--", Arg.Rest (fun s -> cmd_and_args := s :: !cmd_and_args),
+      " <executable> <arguments>   Specify the executable to time, with its arguments"
+  ]
+  (fun s -> raise (Arg.Bad (sprintf "Don't know what to do with '%s'" s)))
+  "Usage: xtime [options] -- <executable> [arguments].\n\nOptions are:";
+  match List.rev !cmd_and_args with
+  | [] ->
+      error "No command to execute\n"
+  | cmd :: args ->
+      Unix.handle_unix_error run (cmd, args)