Remove mention of why3-cpulimit from provers-detection-data.conf

Instead, the call to why3-cpulimit is added in Call_provers, when
requested. The arguments for why3-cpulimit are now computed depending on
the command line and if the prover is interactive or not.

src/driver/call_provers.ml

@@ -249,10 +249,14 @@ let parse_prover_run res_parser time out ret on_timelimit limit ~printer_mapping
     pr_model  = model;
   }
 
-let actualcommand command limit file =
+let actualcommand command ~use_why3cpulimit limit interactive file =
   let timelimit = get_time limit in
   let memlimit  = get_mem limit in
   let steplimit = get_steps limit in
+  let utime = string_of_int (2 * timelimit + 1) in
+  let ttime = string_of_int (succ timelimit) in
+  let stime = string_of_int timelimit in
+  let smem = string_of_int memlimit in
   let arglist = Cmdline.cmdline_split command in
   let use_stdin = ref true in
   let on_timelimit = ref false in
@@ -261,9 +265,9 @@ let actualcommand command limit file =
     | "%" -> "%"
     | "f" -> use_stdin := false; file
     | "t" -> on_timelimit := true; string_of_int timelimit
-    | "T" -> string_of_int (succ timelimit)
-    | "U" -> string_of_int (2 * timelimit + 1)
-    | "m" -> string_of_int memlimit
+    | "T" -> ttime
+    | "U" -> utime
+    | "m" -> smem
     (* FIXME: libdir and datadir can be changed in the configuration file
        Should we pass them as additional arguments? Or would it be better
        to prepare the command line in a separate function? *)
@@ -275,16 +279,30 @@ let actualcommand command limit file =
   let args =
     List.map (Str.global_substitute cmd_regexp replace) arglist
   in
+  let args =
+    if use_why3cpulimit && not interactive then
+      let cpulimit_bin = Filename.concat Config.libdir "why3-cpulimit" in
+      let cpulimit_time =
+        (* for steps limit use 2 * t + 1 time *)
+        if limit.limit_steps <> None then utime
+        (* if prover implements time limit, use t + 1 *)
+        else if !on_timelimit then ttime
+        (* otherwise use t *)
+        else stime in
+       cpulimit_bin :: cpulimit_time :: smem :: "-s" :: args
+    else
+      args in
   args, !use_stdin, !on_timelimit
 
 let call_on_file ~command
                  ~limit
                  ~res_parser
 		 ~printer_mapping
-                 ?(cleanup=false) ?(inplace=false) ?(redirect=true) fin =
+                 ?(cleanup=false) ?(inplace=false) ?(interactive=false)
+                 ?(redirect=true) fin =
 
   let command, use_stdin, on_timelimit =
-    try actualcommand command limit fin
+    try actualcommand command ~use_why3cpulimit:true limit interactive fin
     with e ->
       if cleanup then Sys.remove fin;
       if inplace then Sys.rename (save fin) fin;
@@ -335,7 +353,7 @@ let call_on_file ~command
 
 let call_on_buffer ~command ~limit ~res_parser ~filename
 		   ~printer_mapping
-                   ?(inplace=false) buffer =
+                   ?(inplace=false) ?interactive buffer =
 
   let fin,cin =
     if inplace then begin
@@ -345,7 +363,8 @@ let call_on_buffer ~command ~limit ~res_parser ~filename
       Filename.open_temp_file "why_" ("_" ^ filename) in
   Buffer.output_buffer cin buffer; close_out cin;
   call_on_file ~command ~limit
-               ~res_parser ~printer_mapping ~cleanup:true ~inplace fin
+               ~res_parser ~printer_mapping ~cleanup:true
+               ~inplace ?interactive fin
 
 let query_call pc =
   let pid, ret = Unix.waitpid [Unix.WNOHANG] pc.pid in

src/driver/call_provers.mli

@@ -91,6 +91,22 @@ type prover_result_parser = {
   (* The parser for a model returned by the solver. *)
   prp_model_parser : Model_parser.model_parser;
 }
+(*
+    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.
+*)
 
 (** {2 Functions for calling external provers} *)
 type prover_call
@@ -130,43 +146,30 @@ val mk_limit : int -> int -> int -> resource_limit
    *)
 
 val call_on_file :
-  command     : string ->
-  limit       : resource_limit ->
-  res_parser  : prover_result_parser ->
+  command         : string ->
+  limit           : resource_limit ->
+  res_parser      : prover_result_parser ->
   printer_mapping : Printer.printer_mapping ->
-  ?cleanup    : bool ->
-  ?inplace    : bool ->
-  ?redirect   : bool ->
+  ?cleanup        : bool ->
+  ?inplace        : bool ->
+  ?interactive    : bool ->
+  ?redirect       : bool ->
   string -> pre_prover_call
 
 val call_on_buffer :
-  command     : string ->
-  limit       : resource_limit ->
-  res_parser  : prover_result_parser ->
-  filename    : string ->
+  command         : string ->
+  limit           : resource_limit ->
+  filename        : string ->
   printer_mapping : Printer.printer_mapping ->
-  ?inplace    : bool ->
+  ?inplace        : bool ->
+  ?interactive    : bool ->
   Buffer.t -> pre_prover_call
 (** Call a prover on the task printed in the {!type: Buffer.t} given.
 
-    @param timelimit : set the available time limit (def. 0 : unlimited)
-    @param memlimit : set the available memory limit (def. 0 : unlimited)
-    @param steplimit : set the available step limit (def. -1 : unlimited)
+    @param limit : set the available time limit (def. 0 : unlimited), memory
+    limit (def. 0 : unlimited) and step limit (def. -1 : 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.
-
-    @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.
+    @param res_parser : prover result parser
 
     @param filename : the suffix of the proof task's file, if the prover
     doesn't accept stdin. *)

src/driver/driver.ml

@@ -252,10 +252,10 @@ let file_of_theory drv input_file th =
   get_filename drv input_file th.th_name.Ident.id_string "null"
 
 let call_on_buffer ~command ~limit
-                   ?inplace ~filename ~printer_mapping drv buffer =
+                   ?inplace ?interactive ~filename ~printer_mapping drv buffer =
   Call_provers.call_on_buffer
     ~command ~limit ~res_parser:drv.drv_res_parser
-    ~filename ~printer_mapping ?inplace buffer
+    ~filename ~printer_mapping ?inplace ?interactive buffer
 
 
 (** print'n'prove *)
@@ -323,8 +323,7 @@ let print_theory ?old drv fmt th =
   let task = Task.use_export None th in
   print_task ?old drv fmt task
 
-let prove_task_prepared
-    ~command ~limit ?old ?inplace drv task =
+let prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task =
   let buf = Buffer.create 1024 in
   let fmt = formatter_of_buffer buf in
   let old_channel = Opt.map open_in old in
@@ -343,13 +342,14 @@ let prove_task_prepared
   in
   let res =
     call_on_buffer ~command ~limit
-                   ?inplace ~filename ~printer_mapping drv buf in
+                   ?inplace ?interactive ~filename ~printer_mapping drv buf in
   Buffer.reset buf;
   res
 
-let prove_task ~command ~limit ?(cntexample=false) ?old ?inplace drv task =
+let prove_task ~command ~limit ?(cntexample=false) ?old
+               ?inplace ?interactive drv task =
   let task = prepare_task ~cntexample drv task in
-  prove_task_prepared ~command ~limit ?old ?inplace drv task
+  prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task
 
 (* exception report *)
 

src/driver/driver.mli

@@ -35,10 +35,11 @@ val file_of_theory : driver -> string -> Theory.theory -> string
     for the prover of driver [d], for a theory [th] from filename [f] *)
 
 val call_on_buffer :
-  command    : string ->
-  limit      : Call_provers.resource_limit ->
-  ?inplace   : bool ->
-  filename   : string ->
+  command      : string ->
+  limit        : Call_provers.resource_limit ->
+  ?inplace     : bool ->
+  ?interactive : bool ->
+  filename     : string ->
   printer_mapping : Printer.printer_mapping ->
   driver -> Buffer.t -> Call_provers.pre_prover_call
 
@@ -54,11 +55,12 @@ val print_theory :
   (** produce a realization of the given theory using the given driver *)
 
 val prove_task :
-  command    : string ->
-  limit      : Call_provers.resource_limit ->
-  ?cntexample : bool ->
-  ?old       : string ->
-  ?inplace   : bool ->
+  command      : string ->
+  limit        : Call_provers.resource_limit ->
+  ?cntexample  : bool ->
+  ?old         : string ->
+  ?inplace     : bool ->
+  ?interactive : bool ->
   driver -> Task.task -> Call_provers.pre_prover_call
 
 (** Split the previous function in two simpler functions *)
@@ -69,10 +71,11 @@ val print_task_prepared :
   driver -> Format.formatter -> Task.task -> Printer.printer_mapping
 
 val prove_task_prepared :
-  command    : string ->
-  limit      : Call_provers.resource_limit ->
-  ?old       : string ->
-  ?inplace   : bool ->
+  command      : string ->
+  limit        : Call_provers.resource_limit ->
+  ?old         : string ->
+  ?inplace     : bool ->
+  ?interactive : bool ->
   driver -> Task.task -> Call_provers.pre_prover_call