call_provers.mli 6.86 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   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 15 16
(** {1 Call provers and parse their outputs} *)

(** {2 data types for prover answers} *)
Francois Bobot's avatar
Francois Bobot committed
17

18 19 20 21 22 23 24
(** The reason why unknown was reported *)
type reason_unknown =
  | Resourceout
  (** Out of resources  *)
  | Other
  (** Other reason *)

25
type prover_answer =
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
26
  | Valid
Francois Bobot's avatar
Francois Bobot committed
27
      (** The task is valid according to the prover *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
28
  | Invalid
Francois Bobot's avatar
Francois Bobot committed
29
      (** The task is invalid *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
30
  | Timeout
31
      (** the task timeouts, ie it takes more time than specified *)
32
  | OutOfMemory
33
      (** the task runs out of memory *)
34
  | StepLimitExceeded
35
      (** the task required more steps than the limit provided *)
36
  | Unknown of (string * reason_unknown option)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
37
      (** The prover can't determine if the task is valid *)
38
  | Failure of string
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
39 40 41 42
      (** 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 *)
43

44 45
type prover_result = {
  pr_answer : prover_answer;
46 47 48
  (** The answer of the prover on the given task *)
  pr_status : Unix.process_status;
  (** The process exit status *)
49
  pr_output : string;
50
  (** The output of the prover currently stderr and stdout *)
51
  pr_time   : float;
52
  (** The time taken by the prover *)
53 54
  pr_steps  : int;
  (** The number of steps taken by the prover (-1 if not available) *)
55
  pr_model  : model;
56
  (** The model produced by a the solver *)
57
}
58

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

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

67
val debug : Debug.flag
68
(** debug flag for the calling procedure (option "--debug call_prover")
69
    If set [call_on_buffer] prints on stderr the commandline called
70 71
    and the output of the prover. *)

72 73 74
type timeregexp
(** The type of precompiled regular expressions for time parsing *)

75
type stepregexp
76 77
(** The type of precompiled regular expressions for parsing of steps *)

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

82 83 84
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. *)
85

86 87 88
type prover_result_parser = {
  prp_regexps     : (Str.regexp * prover_answer) list;
  prp_timeregexps : timeregexp list;
89
  prp_stepregexps : stepregexp list;
90
  prp_exitcodes   : (int * prover_answer) list;
91 92
  (* The parser for a model returned by the solver. *)
  prp_model_parser : Model_parser.model_parser;
93
}
94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
(*
    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.

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

    @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.
*)
110

111
(** {2 Functions for calling external provers} *)
Andrei Paskevich's avatar
Andrei Paskevich committed
112 113 114 115 116
type prover_call
(** Type that represents a single prover run *)

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

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

121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141
type resource_limit =
  {
    limit_time  : int option;
    limit_mem   : int option;
    limit_steps : int option;
  }
(* represents the three ways a prover run can be limited: in time, memory
   and/or steps *)

val empty_limit : resource_limit
(* the limit object which imposes no limits *)

val limit_max : resource_limit -> resource_limit -> resource_limit
(* return the limit object whose components represent the maximum of the
   corresponding components of the arguments *)

val get_time : resource_limit -> int
(* return time, return default value 0 if not set *)
val get_mem : resource_limit -> int
(* return time, return default value 0 if not set *)
val get_steps : resource_limit -> int
142
(* return time, return default value 0 if not set *)
143 144 145 146 147

val mk_limit : int -> int -> int -> resource_limit
(* build a limit object, transforming the default values into None on the fly
   *)

148
val call_on_file :
149 150 151
  command         : string ->
  limit           : resource_limit ->
  res_parser      : prover_result_parser ->
152
  printer_mapping : Printer.printer_mapping ->
153 154 155 156
  ?cleanup        : bool ->
  ?inplace        : bool ->
  ?interactive    : bool ->
  ?redirect       : bool ->
157 158
  string -> pre_prover_call

159
val call_on_buffer :
160 161
  command         : string ->
  limit           : resource_limit ->
Johannes Kanig's avatar
Johannes Kanig committed
162
  res_parser      : prover_result_parser ->
163
  filename        : string ->
164
  printer_mapping : Printer.printer_mapping ->
165 166
  ?inplace        : bool ->
  ?interactive    : bool ->
Andrei Paskevich's avatar
Andrei Paskevich committed
167
  Buffer.t -> pre_prover_call
Francois Bobot's avatar
Francois Bobot committed
168
(** Call a prover on the task printed in the {!type: Buffer.t} given.
169

170 171
    @param limit : set the available time limit (def. 0 : unlimited), memory
    limit (def. 0 : unlimited) and step limit (def. -1 : unlimited)
172

173
    @param res_parser : prover result parser
174

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

178
val query_call : prover_call -> post_prover_call option
Andrei Paskevich's avatar
Andrei Paskevich committed
179
(** Thread-safe non-blocking function that checks if the prover
Andrei Paskevich's avatar
Andrei Paskevich committed
180 181
    has finished. *)

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

185 186 187
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 *)
188 189

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