call_provers.mli 5.74 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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.                           *)
(*                                                                  *)
(********************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11

12 13
open Model_parser

14
(** Call provers and parse their outputs *)
Francois Bobot's avatar
Francois Bobot committed
15

16
type prover_answer =
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
17
  | Valid
Francois Bobot's avatar
Francois Bobot committed
18
      (** The task is valid according to the prover *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
19
  | Invalid
Francois Bobot's avatar
Francois Bobot committed
20
      (** The task is invalid *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
21
  | Timeout
22
      (** the task timeouts, ie it takes more time than specified *)
23
  | OutOfMemory
24
      (** the task runs out of memory *)
25
  | StepLimitExceeded
26
      (** the task required more steps than the limit provided *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
27 28
  | Unknown of string
      (** The prover can't determine if the task is valid *)
29
  | Failure of string
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
30 31 32 33
      (** 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 *)
34

35 36
type prover_result = {
  pr_answer : prover_answer;
37 38 39
  (** The answer of the prover on the given task *)
  pr_status : Unix.process_status;
  (** The process exit status *)
40
  pr_output : string;
41
  (** The output of the prover currently stderr and stdout *)
42
  pr_time   : float;
43
  (** The time taken by the prover *)
44 45
  pr_steps  : int;
  (** The number of steps taken by the prover (-1 if not available) *)
46
  (** The model produced by a the solver *)
47
  pr_model  : model;
48
}
49

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

53
val print_prover_result : Format.formatter -> prover_result -> unit
Francois Bobot's avatar
Francois Bobot committed
54
(** Pretty-print a prover_result. The answer and the time are output.
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
55 56
    The output of the prover is printed if and only if the answer is
    a [HighFailure] *)
57

58
val debug : Debug.flag
59
(** debug flag for the calling procedure (option "--debug call_prover")
60
    If set [call_on_buffer] prints on stderr the commandline called
61 62
    and the output of the prover. *)

63 64 65
type timeregexp
(** The type of precompiled regular expressions for time parsing *)

66
type stepregexp
67 68
(** The type of precompiled regular expressions for parsing of steps *)

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

73 74 75
val stepregexp : string -> int -> stepregexp
(** [stepregexp s n] creates a regular expression to match the number of steps.
    [s] is a regular expression, [n] is the group number with steps number. *)
76

77 78 79
type prover_result_parser = {
  prp_regexps     : (Str.regexp * prover_answer) list;
  prp_timeregexps : timeregexp list;
80
  prp_stepregexps : stepregexp list;
81
  prp_exitcodes   : (int * prover_answer) list;
82 83
  (* The parser for a model returned by the solver. *)
  prp_model_parser : Model_parser.model_parser;
84 85
}

Andrei Paskevich's avatar
Andrei Paskevich committed
86 87 88 89 90
type prover_call
(** Type that represents a single prover run *)

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

Andrei Paskevich's avatar
Andrei Paskevich committed
92 93
type post_prover_call = unit -> prover_result
(** Thread-unsafe closure that interprets the prover's results *)
94

95 96 97 98
val call_on_file :
  command     : string ->
  ?timelimit  : int ->
  ?memlimit   : int ->
99
  ?steplimit  : int ->
100
  res_parser  : prover_result_parser ->
101
  printer_mapping : Printer.printer_mapping ->
102
  ?cleanup    : bool ->
103
  ?inplace    : bool ->
104
  ?redirect   : bool ->
105 106
  string -> pre_prover_call

107
val call_on_buffer :
108 109 110
  command     : string ->
  ?timelimit  : int ->
  ?memlimit   : int ->
111
  ?steplimit  : int ->
112
  res_parser  : prover_result_parser ->
113
  filename    : string ->
114
  printer_mapping : Printer.printer_mapping ->
115
  ?inplace    : bool ->
Andrei Paskevich's avatar
Andrei Paskevich committed
116
  Buffer.t -> pre_prover_call
Francois Bobot's avatar
Francois Bobot committed
117
(** Call a prover on the task printed in the {!type: Buffer.t} given.
118

119
    @param timelimit : set the available time limit (def. 0 : unlimited)
120 121
    @param memlimit : set the available memory limit (def. 0 : unlimited)
    @param steplimit : set the available step limit (def. -1 : unlimited)
122 123 124 125 126

    @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.
127

128 129 130 131 132
    @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.
133

134 135 136
    @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.
137

Andrei Paskevich's avatar
Andrei Paskevich committed
138 139 140
    @param filename : the suffix of the proof task's file, if the prover
    doesn't accept stdin. *)

141
val query_call : prover_call -> post_prover_call option
Andrei Paskevich's avatar
Andrei Paskevich committed
142
(** Thread-safe non-blocking function that checks if the prover
Andrei Paskevich's avatar
Andrei Paskevich committed
143 144
    has finished. *)

145
val wait_on_call : prover_call -> post_prover_call
Andrei Paskevich's avatar
Andrei Paskevich committed
146
(** Thread-safe blocking function that waits until the prover finishes. *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
147

148 149 150
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 *)
151 152

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