fix usestdin mode for why3server

src/driver/call_provers.ml

@@ -347,7 +347,7 @@ let result_buffer : (server_id, prover_result) Hashtbl.t = Hashtbl.create 17
 let call_on_file ~command ~limit ~res_parser ~printer_mapping
                  ?(inplace=false) fin () =
   let id = gen_id () in
-  let cmd, _, on_timelimit =
+  let cmd, use_stdin, on_timelimit =
     actualcommand ~cleanup:true ~inplace command limit fin in
   let limit = adapt_limits limit on_timelimit in
   let save =
@@ -359,7 +359,7 @@ let call_on_file ~command ~limit ~res_parser ~printer_mapping
   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;
+  Prove_client.send_request ~use_stdin ~id ~timelimit ~memlimit ~cmd;
   ServerCall id
 
 let get_new_results ~blocking =

src/driver/prove_client.ml

@@ -92,10 +92,11 @@ let set_max_running_provers x =
   if !socket <> None then
     send_request_string ("parallel;" ^ string_of_int x)
 
-let send_request ~id ~timelimit ~memlimit ~cmd =
+let send_request ~use_stdin ~id ~timelimit ~memlimit ~cmd =
   force_connect ();
   let buf = Buffer.create 128 in
-  Buffer.add_string buf "run;";
+  let servercommand = if use_stdin then "runstdin;" else "run;" in
+  Buffer.add_string buf servercommand;
   Buffer.add_string buf (string_of_int id);
   Buffer.add_char buf ';';
   Buffer.add_string buf (string_of_int timelimit);

src/driver/prove_client.mli

@@ -6,6 +6,7 @@ val set_max_running_provers : int -> unit
 val connect : unit -> unit
 
 val send_request :
+ use_stdin:bool ->
  id:int ->
  timelimit:int ->
  memlimit:int ->

src/server/README.server

@@ -20,7 +20,7 @@ A client request is a single line which looks like this:
   commandkind;payload
 
 Where commandkind is a simple string and payload is a semicolon-separated
-list. There are currently only two possible commands. The first command looks
+list. There are currently three possible commands. The first command looks
 like this:
 
   run;id;timeout;memlimit;cmd;arg1;arg2;...;argn
@@ -52,7 +52,16 @@ Their meaning is the following:
   file     - the path to a file which contains the stdout and stderr of the
              executed program
 
-The second commmand is like this:
+The second command is very similar:
+
+  runstdin;id;timeout;memlimit;cmd;arg1;arg2;...;argn;filename
+
+The meaning of this command is identical to the "run" command, with the
+difference that an extra filename is given as the last argument to the
+command. This filename is not passed to the command as a commandline argument,
+instead it is "piped" into the stdin of the command.
+
+The third commmand is like this:
 
   parallel;num
 

src/server/request.c

@@ -49,6 +49,7 @@ prequest parse_request(char* str_req, int len, int key) {
   int pos = 0;
   prequest req;
   char* tmp;
+  bool runstdin = false;
 
   semic = count_semicolons(str_req, len);
   if (semic == 0) {
@@ -73,11 +74,16 @@ prequest parse_request(char* str_req, int len, int key) {
   }
   pos = copy_up_to_semicolon(str_req, pos, len, &tmp);
   if (strncmp(tmp, "run", pos) != 0) {
-    return NULL;
+    if (strncmp(tmp, "runstdin", pos) == 0) {
+      runstdin = true;
+    } else {
+      return NULL;
+    }
   }
   req = (prequest) malloc(sizeof(request));
   req->key = key;
   req->numargs = numargs;
+  req->usestdin = runstdin;
   pos = copy_up_to_semicolon(str_req, pos, len, &(req->id));
   pos = copy_up_to_semicolon(str_req, pos, len, &tmp);
   req->timeout = atoi(tmp);

src/server/request.h

 #ifndef REQUEST_H
 #define REQUEST_H
 
+#include <stdbool.h>
+
 typedef struct {
   int key;
   char* id;
   int timeout;
   int memlimit;
+  bool usestdin;
   char* cmd;   // the command to execute
   int numargs; // the length of the following array
   char** args; // the arguments of the process to run (not including the command)

src/server/server-unix.c

@@ -241,12 +241,19 @@ void queue_write(pclient client, char* msgbuf) {
 pid_t create_process(char* cmd,
                      int argc,
                      char** argv,
+                     bool usestdin,
                      int outfile,
                      int timelimit,
                      int memlimit) {
   struct rlimit res;
   int i;
   char** unix_argv;
+  int count = argc;
+  // in the case of usestdin, the last argument is in fact not passed to
+  // execvp, it contains the filename instead
+  if (usestdin) {
+    count--;
+  }
   unix_argv = (char**)malloc(sizeof(char*) * (argc + 2));
   unix_argv[0] = cmd;
   unix_argv[argc + 1] = NULL;
@@ -292,6 +299,9 @@ pid_t create_process(char* cmd,
   //adapt stdout/stderr
   dup2(outfile, 1);
   dup2(outfile, 2);
+  if (usestdin) {
+    freopen(argv[argc-1], "r", stdin);
+  }
 
   /* execute the command */
   execvp(cmd,unix_argv);
@@ -405,6 +415,7 @@ void run_request (prequest r) {
   id = create_process(r->cmd,
                       r->numargs,
                       r->args,
+                      r->usestdin,
                       out_descr,
                       r->timeout,
                       r->memlimit);

src/server/server-win.c

@@ -224,13 +224,20 @@ void run_request (prequest r) {
    char* outfile;
    pproc proc;
    int key;
+   int argcount = r->numargs;
    JOBOBJECT_EXTENDED_LIMIT_INFORMATION limits;
    JOBOBJECT_ASSOCIATE_COMPLETION_PORT portassoc;
    STARTUPINFO si;
-   HANDLE ghJob, outfilehandle;
+   HANDLE ghJob, outfilehandle, infilehandle;
    PROCESS_INFORMATION pi;
    pclient client;
 
+  // in the case of usestdin, the last argument is in fact not passed to
+  // CreateProcess, it contains the filename instead
+   if (r->usestdin) {
+     argcount--;
+   }
+
    client = (pclient) list_lookup(clients, r->key);
    if (client==NULL) {
       return;
@@ -246,6 +253,17 @@ void run_request (prequest r) {
    // set the stdout for the childprocess
    si.hStdOutput = outfilehandle;
    si.hStdError = outfilehandle;
+   if (r->usestdin) {
+     infilehandle =
+       CreateFile(r->args[argcount],
+                 GENERIC_READ,
+                 FILE_SHARE_READ,
+                 NULL,
+                 OPEN_ALWAYS,
+                 FILE_ATTRIBUTE_NORMAL,
+                 NULL);
+     si->hSdtInput = infilehandle;
+   }
    // if we don't set that flag, the stdout we just set won't even be looked at
    si.dwFlags = STARTF_USESTDHANDLES;
    /* Compute command line string. When a parameter contains a " or a space we
@@ -260,7 +278,7 @@ void run_request (prequest r) {
    /* Now take care of the arguments */
    {
      int k;
-     for (k = 0; k < r->numargs; k++)
+     for (k = 0; k < argcount; k++)
        {
          char *ca = r->args[k]; /* current arg */
          int ca_index; /* index of the current character in ca */