package why3find

  1. Overview
  2. Docs
A Why3 Package Manager

Install 

dune-project
 Dependency

git.frama-c.com Readme Changelog LGPL-2.1-only License Edit opam file Versions (3)

Authors

  1. L
    Loïc Correnson <loic.correnson@cea.fr>
  2. B
    Benjamin Jorge <benjamin.jorge@cea.fr>

Maintainers

  1. B
    benjamin.jorge@cea.fr
  2. L
    loic.correnson@cea.fr

Sources

why3find-1.3.0.tar.gz
md5=435da830a513fd91ec5411c91126b763
sha512=fd8b04eb16d569c0dc9e5595a40b174d7858121b080c81d459b2f28fb3af1ebc32ef408859d5c1c5f45c61790625c027c2ecfc3d45e597943543de7212bab8d6

doc/src/why3find.utils/timer.ml.html

Source file timer.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

type timer = {
  mutable start_date : float;
  stats_time : Stats.stats;
}

let create () =  {
  start_date = infinity;
  stats_time = Stats.create ();
}

let start ti =
  assert (ti.start_date = infinity);
  let t = Unix.gettimeofday () in
  ti.start_date <- t

let stop ti =
  assert (ti.start_date <> infinity);
  let t = Unix.gettimeofday () in
  Stats.add ti.stats_time (t -. ti.start_date);
  ti.start_date <- infinity

let stats ti =
  ti.stats_time

let count ti =
  assert (ti.start_date = infinity);
  Stats.count ti.stats_time

let min_time ti =
  assert (ti.start_date = infinity);
  Stats.min ti.stats_time

let max_time ti =
  assert (ti.start_date = infinity);
  Stats.max ti.stats_time

let average_time ti =
  assert (ti.start_date = infinity);
  Stats.average ti.stats_time

let total_time ti =
  assert (ti.start_date = infinity);
  Stats.sum ti.stats_time

let global_timers = ref []

let create_global name =
  let ti = create () in
  global_timers := (name, ti) :: !global_timers;
  ti

let timed ~name f =
  let ti = create_global name in
  fun x ->
    start ti;
    let r = f x in
    stop ti;
    r

let timed2 ~name f =
  let ti = create_global name in
  fun x y ->
    start ti;
    let r = f x y in
    stop ti;
    r

let timed3 ~name f =
  let ti = create_global name in
  fun x y z ->
    start ti;
    let r = f x y z in
    stop ti;
    r

let print_global fmt (name, ti) =
  Format.fprintf fmt "%-20s %10f (%4d) | %f - %f - %f |"
    name
    (total_time ti)
    (Stats.count (stats ti))
    (min_time ti)
    (average_time ti)
    (max_time ti)

let print_timings fmt =
  Format.fprintf fmt "@[<v>%a@]"
    (Format.pp_print_list print_global) (List.rev !global_timers)

let throttle ?(delay=0.1) fn =
  let next = ref (Unix.gettimeofday () +. delay) in
  fun ?(force=false) x ->
    let time = Unix.gettimeofday () in
    if force || time > !next then
      (next := time +. delay ; fn x)