bench.ml 4.75 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

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
open Thread
open Why
open Env
open Theory
open Task
open Trans
open Driver
open Call_provers
open Scheduler

type 'a tool = {
  tval     : 'a;
  ttrans   : task trans;
  tdriver  : driver;
  tcommand : string;
  tenv     : env;
  tuse     : task;
  ttime    : int;
  tmem     : int;
}

type 'a prob = {
  ptask  : env -> task -> ('a * task) list; (** needed for tenv *)
  ptrans : task list trans;
}

type ('a,'b) result = {tool   : 'a;
                       prob   : 'b;
                       task   : task;
                       idtask : int;
                       result : prover_result}

type ('a,'b) callback = 'a -> 'b -> task -> int -> proof_attempt_status -> unit

let debug = Debug.register_flag "call"

module MTask :
sig
  type shared
  val create : unit -> shared
  val start : shared -> unit
  val stop : shared -> unit
  val lock : shared -> unit
  val unlock : shared -> unit
  val wait : shared -> unit
end
=
struct
  type shared =
      { m : Mutex.t; c : Condition.t;
        mutable nb_task : int;
      }

  let create () =
    { m = Mutex.create ();
      c = Condition.create ();
      nb_task = 0}

  let start s = Mutex.lock s.m; s.nb_task <- s.nb_task + 1; Mutex.unlock s.m
  let stop s = Mutex.lock s.m; s.nb_task <- s.nb_task - 1;
80
    if s.nb_task = 0 then Condition.signal s.c; Mutex.unlock s.m
81
82
83
84
85
86
87
  let wait s = Mutex.lock s.m; Condition.wait s.c s.m
  let lock s = Mutex.lock s.m
  let unlock s = Mutex.unlock s.m
end

let call s callback tool prob =
  (** Prove goal *)
88
89
  let call q cb task =
    Queue.add (create_proof_attempt ~debug:(Debug.test_flag debug)
90
91
      ~timelimit:(tool.ttime) ~memlimit:(tool.tmem)
      ~command:(tool.tcommand) ~driver:(tool.tdriver)
92
93
      ~callback:cb task) q in
  let iter q pval i task =
94
95
96
    MTask.start s;
    let cb res = callback pval i task res;
      match res with Done _ | InternalFailure _ -> MTask.stop s | _ -> () in
97
    call q cb task; succ i in
98
  let trans_cb pval tl =
99
100
101
102
    let q = Queue.create () in
    ignore (List.fold_left (iter q pval) 0 (List.rev tl));
    transfer_proof_attempts q;
    MTask.stop s in
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
  (** Apply trans *)
  let iter_task (pval,task) =
    MTask.start s;
    let trans = Trans.compose_l prob.ptrans (Trans.singleton tool.ttrans) in
    apply_transformation_l ~callback:(trans_cb pval) trans task in
  (** Split *)
  let ths = prob.ptask tool.tenv tool.tuse in
  MTask.start s;
  List.iter iter_task ths;
  MTask.stop s

let general ?(callback=fun _ _ _ _ _ -> ()) iter add =
  let s = MTask.create () in
  iter (fun v tool prob ->
    let cb pval i task res =
      callback tool.tval pval task i res;
      match res with
        | Done r -> MTask.lock s;
          add v {tool = tool.tval; prob = pval; task = task;
                 idtask = i; result = r};
          MTask.unlock s
        | _ -> () in
    call s cb tool prob);
  MTask.wait s

let any ?callback toolprob =
  let l = ref [] in
  general ?callback (fun f -> List.iter (fun (t,p) -> f () t p) toolprob)
    (fun () r -> l:=r::!l);
  !l


let all_list ?callback tools probs =
  let l = ref [] in
  general ?callback (fun f ->
    List.iter (fun t -> List.iter (fun p -> f () t p) probs) tools)
    (fun () r -> l:=r::!l);
  !l

let all_array ?callback tools probs =
  let m = Array.make_matrix (Array.length tools) (Array.length probs)
    [] in
  general ?callback (fun f ->
    Array.iteri (fun i t -> Array.iteri (fun j p -> f (i,j) t p) probs) tools)
    (fun (i,j) r -> m.(i).(j) <- r::m.(i).(j));
  m