diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-09-29 14:04:59 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-09-29 14:04:59 +0200 |
commit | e5b59af8a21c42b504b1beeb89208dd0cb0c8b3b (patch) | |
tree | c257060ca943eade1562bf9071a54a6f82fa5467 /driver/Timing.ml | |
parent | 6087efa0b68ae3a1b003dac86970719728976395 (diff) | |
download | compcert-e5b59af8a21c42b504b1beeb89208dd0cb0c8b3b.tar.gz compcert-e5b59af8a21c42b504b1beeb89208dd0cb0c8b3b.zip |
Moved the timing facility to a seperate file.
Diffstat (limited to 'driver/Timing.ml')
-rw-r--r-- | driver/Timing.ml | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/driver/Timing.ml b/driver/Timing.ml new file mode 100644 index 00000000..b45dad40 --- /dev/null +++ b/driver/Timing.ml @@ -0,0 +1,63 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +open Clflags + +(** Timing facility *) + +let timers : (string * float) list ref = ref [] + +let add_to_timer name time = + let rec add = function + | [] -> [name, time] + | (name1, time1 as nt1) :: rem -> + if name1 = name then (name1, time1 +. time) :: rem else nt1 :: add rem + in timers := add !timers + +let time name fn arg = + if not !option_timings then + fn arg + else begin + let start = Sys.time() in + try + let res = fn arg in + add_to_timer name (Sys.time() -. start); + res + with x -> + add_to_timer name (Sys.time() -. start); + raise x + end + +let time2 name fn arg1 arg2 = time name (fun () -> fn arg1 arg2) () +let time3 name fn arg1 arg2 arg3 = time name (fun () -> fn arg1 arg2 arg3) () + +let time_coq name fn arg = + if not !option_timings then + fn arg + else begin + let start = Sys.time() in + try + let res = fn arg in + add_to_timer (Camlcoq.camlstring_of_coqstring name) (Sys.time() -. start); + res + with x -> + add_to_timer (Camlcoq.camlstring_of_coqstring name) (Sys.time() -. start); + raise x + end + +let print_timers () = + if !option_timings then + List.iter + (fun (name, time) -> Printf.printf "%7.2fs %s\n" time name) + !timers + +let _ = at_exit print_timers |