call_provers.mli 4.89 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

12
(** Call provers and parse their outputs *)
Francois Bobot's avatar
Francois Bobot committed
13

14
type prover_answer =
Andrei Paskevich's avatar
Andrei Paskevich committed
15
  | Valid
Francois Bobot's avatar
Francois Bobot committed
16
      (** The task is valid according to the prover *)
Andrei Paskevich's avatar
Andrei Paskevich committed
17
  | Invalid
Francois Bobot's avatar
Francois Bobot committed
18
      (** The task is invalid *)
Andrei Paskevich's avatar
Andrei Paskevich committed
19 20
  | Timeout
      (** the task timeout, ie it takes more time than specified *)
21 22
  | OutOfMemory
      (** the task timeout, ie it takes more time than specified *)
Andrei Paskevich's avatar
Andrei Paskevich committed
23 24
  | Unknown of string
      (** The prover can't determine if the task is valid *)
25
  | Failure of string
Andrei Paskevich's avatar
Andrei Paskevich committed
26 27 28 29
      (** The prover reports a failure *)
  | HighFailure
      (** An error occured during the call to the prover or none
          of the given regexps match the output of the prover *)
30

31 32
type prover_result = {
  pr_answer : prover_answer;
33 34 35
  (** The answer of the prover on the given task *)
  pr_status : Unix.process_status;
  (** The process exit status *)
36
  pr_output : string;
37
  (** The output of the prover currently stderr and stdout *)
38
  pr_time   : float;
39
  (** The time taken by the prover *)
40
}
41

42
val print_prover_answer : Format.formatter -> prover_answer -> unit
Francois Bobot's avatar
Francois Bobot committed
43 44
(** Pretty-print a {! prover_answer} *)

45
val print_prover_result : Format.formatter -> prover_result -> unit
Francois Bobot's avatar
Francois Bobot committed
46
(** Pretty-print a prover_result. The answer and the time are output.
Andrei Paskevich's avatar
Andrei Paskevich committed
47 48
    The output of the prover is printed if and only if the answer is
    a [HighFailure] *)
49

50
val debug : Debug.flag
51
(** debug flag for the calling procedure (option "--debug call_prover")
52
    If set [call_on_buffer] prints on stderr the commandline called
53 54
    and the output of the prover. *)

55 56 57 58 59 60
type timeregexp
(** The type of precompiled regular expressions for time parsing *)

val timeregexp : string -> timeregexp
(** Converts a regular expression with special markers '%h','%m',
    '%s','%i' (for milliseconds) into a value of type [timeregexp] *)
61

62 63 64 65 66
type prover_call
(** Type that represents a single prover run *)

type pre_prover_call = unit -> prover_call
(** Thread-safe closure that launches the prover *)
67

68 69
type post_prover_call = unit -> prover_result
(** Thread-unsafe closure that interprets the prover's results *)
70

71 72 73 74 75 76 77 78
val call_on_file :
  command     : string ->
  ?timelimit  : int ->
  ?memlimit   : int ->
  regexps     : (Str.regexp * prover_answer) list ->
  timeregexps : timeregexp list ->
  exitcodes   : (int * prover_answer) list ->
  ?cleanup    : bool ->
79
  ?inplace    : bool ->
80
  ?redirect   : bool ->
81 82
  string -> pre_prover_call

83
val call_on_buffer :
84 85 86 87
  command     : string ->
  ?timelimit  : int ->
  ?memlimit   : int ->
  regexps     : (Str.regexp * prover_answer) list ->
88
  timeregexps : timeregexp list ->
89 90
  exitcodes   : (int * prover_answer) list ->
  filename    : string ->
91
  ?inplace    : bool ->
92
  Buffer.t -> pre_prover_call
Francois Bobot's avatar
Francois Bobot committed
93
(** Call a prover on the task printed in the {!type: Buffer.t} given.
94

95 96 97 98 99 100 101
    @param timelimit : set the available time limit (def. 0 : unlimited)
    @param memlimit : set the available time limit (def. 0 : unlimited)

    @param regexps : if the first field matches the prover output,
    the second field is the answer. Regexp groups present in
    the first field are substituted in the second field (\0,\1,...).
    The regexps are tested in the order of the list.
102

103 104 105 106 107
    @param timeregexps : a list of regular expressions with special
    markers '%h','%m','%s','%i' (for milliseconds), constructed with
    [timeregexp] function, and used to extract the time usage from
    the prover's output. If the list is empty, wallclock is used.
    The regexps are tested in the order of the list.
108

109 110 111
    @param exitcodes : if the first field is the exit code, then
    the second field is the answer. Exit codes are tested in the order
    of the list and before the regexps.
112

113 114 115
    @param filename : the suffix of the proof task's file, if the prover
    doesn't accept stdin. *)

116
val query_call : prover_call -> post_prover_call option
Andrei Paskevich's avatar
Andrei Paskevich committed
117
(** Thread-safe non-blocking function that checks if the prover
118 119
    has finished. *)

120
val wait_on_call : prover_call -> post_prover_call
Andrei Paskevich's avatar
Andrei Paskevich committed
121
(** Thread-safe blocking function that waits until the prover finishes. *)
Andrei Paskevich's avatar
Andrei Paskevich committed
122

123 124 125
val post_wait_call : prover_call -> Unix.process_status -> post_prover_call
(** Thread-safe non-blocking function that should be called when the
    prover's exit status was obtained from a prior call of Unix.waitpid *)
126 127

val prover_call_pid : prover_call -> int
128
(** Return the pid of the prover *)