fiv various issues with why3server

* separate editor and prover call
* fix problems with cleanup, inplace, interactive, redirect

src/driver/call_provers.ml

@@ -197,14 +197,14 @@ let rec grep out l = match l with
         | HighFailure -> assert false
       with Not_found -> grep out l end
 
-let save f = f ^ ".save"
+let backup_file f = f ^ ".save"
 
 let debug_print_model model =
   let model_str = Model_parser.model_to_string model in
   Debug.dprintf debug "Call_provers: %s@." model_str
 
 
-let parse_prover_run res_parser time out ret on_timelimit limit ~printer_mapping =
+let parse_prover_run res_parser time out ret limit ~printer_mapping =
   let ans = match ret with
     | Unix.WSTOPPED n ->
         Debug.dprintf debug "Call_provers: stopped by signal %d@." n;
@@ -226,7 +226,7 @@ let parse_prover_run res_parser time out ret on_timelimit limit ~printer_mapping
     | _ -> ans in
   let ans = match ans, limit with
     | (Unknown _ | HighFailure), { limit_time = Some tlimit }
-      when on_timelimit && time >= (0.9 *. float tlimit) -> Timeout
+      when time >= (0.9 *. float tlimit) -> Timeout
     | _ -> ans in
   let model = res_parser.prp_model_parser out printer_mapping in
   Debug.dprintf debug "Call_provers: model:@.";
@@ -239,7 +239,7 @@ let parse_prover_run res_parser time out ret on_timelimit limit ~printer_mapping
     pr_model  = model;
   }
 
-let actualcommand command ~use_why3cpulimit limit interactive file =
+let actualcommand command limit file =
   let timelimit = get_time limit in
   let memlimit  = get_mem limit in
   let steplimit = get_steps limit in
@@ -265,27 +265,30 @@ let actualcommand command ~use_why3cpulimit limit interactive 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 "why3cpulimit" in
-      let cpulimit_time =
-        (* for steps limit use 2 * t + 1 time *)
-        if limit.limit_steps <> None then string_of_int (2 * timelimit + 1)
-        (* if prover implements time limit, use t + 1 *)
-        else if !on_timelimit then string_of_int (succ timelimit)
-        (* otherwise use t *)
-        else stime in
-        on_timelimit := true;
-      cpulimit_bin :: cpulimit_time :: smem :: "-s" :: args
-    else
-      args in
   args, !use_stdin, !on_timelimit
 
+let actualcommand ~cleanup ~inplace command limit file =
+  try actualcommand command limit file
+  with e ->
+    if cleanup then Sys.remove file;
+    if inplace then Sys.rename (backup_file file) file;
+    raise e
+
+let adapt_limits limit on_timelimit =
+  let new_time_limit =
+    let timelimit = get_time limit in
+    (* for steps limit use 2 * t + 1 time *)
+    if limit.limit_steps <> None then (2 * timelimit + 1)
+    (* if prover implements time limit, use t + 1 *)
+    else if on_timelimit then succ timelimit
+    (* otherwise use t *)
+    else timelimit in
+  { limit with limit_time = Some new_time_limit }
+
 let set_socket_name =
   Prove_client.set_socket_name
 
 type server_id = int
-
 let gen_id =
   let x = ref 0 in
   fun () ->
@@ -294,30 +297,28 @@ let gen_id =
 
 type save_data =
   { vc_file      : string;
-    is_temporary : bool;
-    redirect     : bool;
+    inplace      : bool;
     limit        : resource_limit;
     res_parser   : prover_result_parser;
     printer_mapping : Printer.printer_mapping;
   }
 
-let regexs : (int, save_data) Hashtbl.t = Hashtbl.create 17
+let saved_data : (int, save_data) Hashtbl.t = Hashtbl.create 17
 
 let prove_file_server ~res_parser ~command ~limit
-                      ~printer_mapping ?(redirect=true)
-                      ?(inplace=false) ?(interactive=false)
+                      ~printer_mapping ?(inplace=false)
                       file =
   let id = gen_id () in
-  let cmd, _, _ =
-    actualcommand command ~use_why3cpulimit:false limit interactive file in
-  let saved_data =
+  let cmd, _, on_timelimit =
+    actualcommand ~cleanup:true ~inplace command limit file in
+  let limit = adapt_limits limit on_timelimit in
+  let save =
     { vc_file      = file;
-      is_temporary = not inplace;
+      inplace      = inplace;
       limit        = limit;
-      redirect     = redirect;
       res_parser   = res_parser;
       printer_mapping = printer_mapping } in
-  Hashtbl.add regexs id saved_data;
+  Hashtbl.add saved_data id save;
   let timelimit = get_time limit in
   let memlimit = get_mem limit in
   Prove_client.send_request ~id ~timelimit ~memlimit ~cmd;
@@ -325,34 +326,26 @@ let prove_file_server ~res_parser ~command ~limit
 
 let read_and_delete_file fn =
   let cin = open_in fn in
-  let buf = Buffer.create 1024 in
-  try
-    while true do
-      Buffer.add_string buf (input_line cin);
-      Buffer.add_char buf '\n'
-    done;
-    assert false
-  with End_of_file ->
-  begin
-    close_in cin;
-    Sys.remove fn;
-    Buffer.contents buf
-  end
+  let out = Sysutil.channel_contents cin in
+  close_in cin;
+  if Debug.test_noflag debug then Sys.remove fn;
+  out
 
 let handle_answer answer =
   let id = answer.Prove_client.id in
-  let save = Hashtbl.find regexs id in
-  Hashtbl.remove regexs id;
-  if save.is_temporary then
+  let save = Hashtbl.find saved_data id in
+  Hashtbl.remove saved_data id;
+  if Debug.test_noflag debug then begin
     Sys.remove save.vc_file;
+    if save.inplace then Sys.rename (backup_file save.vc_file) save.vc_file
+  end;
   let out = read_and_delete_file answer.Prove_client.out_file in
-  let out = if save.redirect then out else "" in
   let ret = Unix.WEXITED answer.Prove_client.exit_code in
   let printer_mapping = save.printer_mapping in
   let ans =
     parse_prover_run save.res_parser
                      answer.Prove_client.time
-                     out ret answer.Prove_client.timeout save.limit
+                     out ret save.limit
                      ~printer_mapping
   in
   id, ans
@@ -362,44 +355,78 @@ let wait_for_server_result ~blocking =
 
 type post_prover_call = unit -> prover_result
 
-type prover_call = server_id
+type prover_call =
+  | ServerCall of server_id
+  | EditorCall of (Unix.process_status -> post_prover_call) * int
 
 type pre_prover_call = unit -> prover_call
 
 let result_buffer : (server_id, prover_result) Hashtbl.t = Hashtbl.create 17
 
 let call_on_file ~command ~limit ~res_parser ~printer_mapping
-                 ?(cleanup=false) ?(inplace=false) ?(interactive=false)
-                 ?(redirect=true) fin =
-  fun () ->
-      prove_file_server ~res_parser ~command ~limit ~printer_mapping
-                        ~redirect ~inplace ~interactive fin
+                 ?(inplace=false) fin () =
+  let id = prove_file_server ~res_parser ~command ~limit ~printer_mapping
+                             ~inplace fin in
+  ServerCall id
 
 let get_new_results ~blocking =
   List.iter (fun (id, r) -> Hashtbl.add result_buffer id r)
     (wait_for_server_result ~blocking)
 
-let query_call id =
-  try
-    get_new_results ~blocking:false;
-    Some (let r = Hashtbl.find result_buffer id in (fun () -> r))
-  with Not_found -> None
+let query_call = function
+  | ServerCall id ->
+      begin try
+        get_new_results ~blocking:false;
+        Some (let r = Hashtbl.find result_buffer id in (fun () -> r))
+      with Not_found -> None end
+  | EditorCall (call, pid) ->
+      let pid, ret = Unix.waitpid [Unix.WNOHANG] pid in
+      if pid = 0 then None else Some (call ret)
 
-let rec wait_on_call id =
-  try let r = Hashtbl.find result_buffer id in (fun () -> r)
-  with Not_found ->
-    get_new_results ~blocking:true;
-    wait_on_call id
+
+let rec wait_on_call = function
+  | ServerCall id as pc ->
+      begin try
+        let r = Hashtbl.find result_buffer id in (fun () -> r)
+      with Not_found ->
+        get_new_results ~blocking:true;
+        wait_on_call pc
+      end
+  | EditorCall (call, pid) ->
+      let _, ret = Unix.waitpid [] pid in call ret
 
 let call_on_buffer ~command ~limit ~res_parser ~filename ~printer_mapping
-                   ?(inplace=false) ?(interactive=false) buffer =
+                   ?(inplace=false) buffer =
   let fin,cin =
     if inplace then begin
-      Sys.rename filename (save filename);
+      Sys.rename filename (backup_file filename);
       filename, open_out filename
     end else
       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 ~interactive fin
-
+  call_on_file ~command ~limit ~res_parser ~printer_mapping ~inplace fin
+
+let call_editor ~command fin =
+  let command, use_stdin, _ =
+    actualcommand ~cleanup:false ~inplace:false command empty_limit fin in
+  let exec = List.hd command in
+  Debug.dprintf debug "@[<hov 2>Call_provers: editor command is: %a@]@."
+    (Pp.print_list Pp.space pp_print_string) command;
+  let argarray = Array.of_list command in
+  fun () ->
+    let fd_in =
+      if use_stdin then Unix.openfile fin [Unix.O_RDONLY] 0 else Unix.stdin in
+    let pid = Unix.create_process exec argarray fd_in Unix.stdout Unix.stderr in
+    if use_stdin then Unix.close fd_in;
+    let call = fun ret ->
+      let r =
+        { pr_answer = Unknown ("", None);
+          pr_status = ret;
+          pr_output = "";
+          pr_time   = 0.0;
+          pr_steps  = 0;
+          pr_model  = Model_parser.default_model;
+        } in
+      (fun () -> r)
+    in
+    EditorCall (call, pid)

src/driver/call_provers.mli

@@ -145,15 +145,14 @@ val mk_limit : int -> int -> int -> resource_limit
 (* build a limit object, transforming the default values into None on the fly
    *)
 
+val call_editor : command : string -> string -> pre_prover_call
+
 val call_on_file :
   command         : string ->
   limit           : resource_limit ->
   res_parser      : prover_result_parser ->
   printer_mapping : Printer.printer_mapping ->
-  ?cleanup        : bool ->
   ?inplace        : bool ->
-  ?interactive    : bool ->
-  ?redirect       : bool ->
   string -> pre_prover_call
 
 val call_on_buffer :
@@ -163,7 +162,6 @@ val call_on_buffer :
   filename        : string ->
   printer_mapping : Printer.printer_mapping ->
   ?inplace        : bool ->
-  ?interactive    : bool ->
   Buffer.t -> pre_prover_call
 (** Call a prover on the task printed in the {!type: Buffer.t} given.
 
@@ -191,9 +189,7 @@ val prove_file_server :
           command : string ->
           limit : resource_limit ->
           printer_mapping : Printer.printer_mapping ->
-          ?redirect : bool ->
           ?inplace : bool ->
-          ?interactive : bool ->
           string -> server_id
 
 val wait_for_server_result : blocking:bool -> (server_id * prover_result) list

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 ?interactive ~filename ~printer_mapping drv buffer =
+                   ?inplace ~filename ~printer_mapping drv buffer =
   Call_provers.call_on_buffer
     ~command ~limit ~res_parser:drv.drv_res_parser
-    ~filename ~printer_mapping ?inplace ?interactive buffer
+    ~filename ~printer_mapping ?inplace buffer
 
 (** print'n'prove *)
 
@@ -333,7 +333,7 @@ let file_name_of_task ?old ?inplace drv task =
         let fn = try Filename.chop_extension fn with Invalid_argument _ -> fn in
         get_filename drv fn "T" pr.pr_name.id_string
 
-let prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task =
+let prove_task_prepared ~command ~limit ?old ?inplace 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,14 +343,14 @@ let prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task =
   Opt.iter close_in old_channel;
   let res =
     call_on_buffer ~command ~limit
-                   ?inplace ?interactive ~filename ~printer_mapping drv buf in
+                   ?inplace ~filename ~printer_mapping drv buf in
   Buffer.reset buf;
   res
 
 let prove_task ~command ~limit ?(cntexample=false) ?old
-               ?inplace ?interactive drv task =
+               ?inplace drv task =
   let task = prepare_task ~cntexample drv task in
-  prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task
+  prove_task_prepared ~command ~limit ?old ?inplace drv task
 
 let prove_task_server command ~limit ~cntexample ?old ?inplace drv task =
   let task = prepare_task ~cntexample drv task in

src/driver/driver.mli

@@ -38,7 +38,6 @@ val call_on_buffer :
   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
@@ -60,7 +59,6 @@ val prove_task :
   ?cntexample  : bool ->
   ?old         : string ->
   ?inplace     : bool ->
-  ?interactive : bool ->
   driver -> Task.task -> Call_provers.pre_prover_call
 
 (** Split the previous function in two simpler functions *)
@@ -81,7 +79,6 @@ val prove_task_prepared :
   limit        : Call_provers.resource_limit ->
   ?old         : string ->
   ?inplace     : bool ->
-  ?interactive : bool ->
   driver -> Task.task -> Call_provers.pre_prover_call
 
 

src/session/session_scheduler.ml

@@ -292,19 +292,7 @@ let schedule_proof_attempt ~cntexample ~limit ?old ~inplace
 
 let schedule_edition t command filename callback =
   Debug.dprintf debug "[Sched] Scheduling an edition@.";
-  let res_parser =
-    { Call_provers.prp_exitcodes = [(0,Call_provers.Unknown ("", None))];
-      Call_provers.prp_regexps = [];
-      Call_provers.prp_timeregexps = [];
-      Call_provers.prp_stepregexps = [];
-      Call_provers.prp_model_parser = fun _ _ -> Model_parser.default_model
-    } in
-  let nolimit =
-    { Call_provers.limit_time = None; limit_mem = None; limit_steps = None } in
-  let precall =
-    Call_provers.call_on_file ~command ~limit:nolimit ~res_parser
-      ~redirect:false filename
-      ~printer_mapping:Printer.get_default_printer_mapping in
+  let precall = Call_provers.call_editor ~command filename in
   callback Running;
   t.running_proofs <- (Check_prover(callback, precall ())) :: t.running_proofs;
   run_timeout_handler t